1. ## First order logic (maybe linked to Peano axioms)

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 $\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))$

2. ## Re: First order logic (maybe linked to Peano axioms)

Can we assume that you are defining "3" to be "s(s(s(0)))"? How are you defining "less than" here?

3. ## Re: First order logic (maybe linked to Peano axioms)

Thank you for your answer. I have defined 3 as s(2) and 2 as s(1) and 1 as s(0), but I think I can only do so(assign numbers) for a finite number of terms with the software I am using. The less than or equal definition is at the bottom of the original post. If you are asking for a syrictly less than, I would have said like $x\neq y \land leq(x,y)$. Do you think the definition is wrong for this purpose? Maybe I should have used the successor somehow ? Thank you

4. ## Re: First order logic (maybe linked to Peano axioms)

Use induction.