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 $\displaystyle \forall x,y \ \rm{leq}(x,y) \Leftrightarrow \rm{natural}(x)\land \rm{natural}(y) \land (\exists a \ \rm{natural}(a) \land (y = x + a)) $