Hello,

I was trying to define natural numbers using first order logic in order to use them in an automated theorem prover. The problem is, I am apparently unable to solve the following problem:

Is it possible to specify, using FOL, that, for example, the only numbers lower or equal than 3 are: 0,s(0) (one), s(s(0)) (two), s(s(s(0))) (three) ?

Let's assume that the axiom system is made up of the axioms mentioned here (the very first system, the shorter one) (https://en.wikipedia.org/wiki/Peano_..._of_arithmetic), with multiplication removed (not needed at the moment), plus a "lower than or equal" predicate defined something like this