Peano/Presburger axioms - "find" numbers lower or equal than another number

Question

[EDIT/CONCLUSION] It turns out it was actually working.. I was just like too stupid to let the prover run for more time and assumed it would take a lot / not be able to prove with what I've provided because it wasn't doing it fast and because it took it ~1 minute with a similar goal asking for numbers lower or equal than 1. However, the goal I gave as an example in this post (leq(x,2)) took ~1 minute as well and for leq(x,5), it was actually able to prove it faster I think (~40 seconds if I recall correctly). Thank you very much to everyone who helped!!

[EDIT:] I apologize for not describing my axioms properly.. I have now written them so as they pretty much resemble what I actually wrote.

Hello and Happy New Year,

I am trying to define natural numbers in order to use them in a First-Order Logic Theorem Prover. The problem is I'm unable to solve the following problem:

"Show that the only numbers lower or equal than (for example) 2 are 0,1 and 2".

My axioms go like this: $$nat(0)$$ $$\forall x( nat(x) \to nat(s(x)) )$$ $$\forall x,y( (nat(x)\land nat(y)) \to nat(add(x,y))$$ $$\forall x( nat(x) \to (s(x) \neq 0) )$$ $$\forall x,y ( (nat(x) \land nat(y)) \to ( (s(x)=s(y)) \to (s=y)))$$ $$\forall x( (nat(x)\land x\neq 0) \to (\exists z (nat(z) \land (x = s(z)))))$$ $$\forall x(nat(x) \to (add(x,0) = x))$$ $$\forall x,y((nat(x)\land nat(y)) \to (add(x,s(y)) = s(add(x,y))))$$ $$\forall x,y((nat(x)\land nat(y)) \to ((leq(x,y) \leftrightarrow (\exists z(nat(z)\land (y = x + z) )))))$$

I have also added addition axioms for commutativity and associativity of addition.

So, what I'd like to be able to prove is something like this (for any number, not just for $2$):

$ \forall x(nat(x) \to (x\leq 2 \to (x = 0) \lor(x=1)\lor(x=2))) $.

Are additional axioms needed in order to be able to prove this?

Answer 1

These axioms are sufficient. Here's an outline of the proof in natural language:

Since $x\leq s(s(0))$, there exists $z$ such that $x + z = s(s(0))$.

Case 1: $z = 0$. Then $x = x + z = s(s(0))$, and we're done ($x = 2$). [Note that you've stated as an axiom $\text{add}(x,0) = 0$, and I assume you meant $\text{add}(x,0) = x$!]

Case 2: $z\neq 0$. Then there exists $y$ such that $z = s(y)$. Then $x + s(y) = s(s(0))$, so $s(x+y) = s(s(0))$, so $x+y = s(0)$.

We've managed to decrease the number of applications of $s$ by one. Now we repeat.

Case 1: $y = 0$. Then $x = x+y = s(0)$, and we're done ($x = 1$).

Case 2: $y \neq 0$. Then there exists $w$ such that $y = s(w)$. Then $x + s(w) = s(0)$, so $s(x+w) = s(0)$, so $x+w = 0$.

If $w = 0$, we're done, just as above ($x = 0$). Otherwise, $w = s(t)$, so $0 = x+ s(t) = s(x+t)$, and $0$ is a successor, contradiction.

Answer 2

Here's a formal proof, copied and pasted from my Fitch software program (sorry for the lack of formatting!) which says it all checks out .. meaning that no: you don't need any further axioms (I did use all 9 axioms). It follows Alex's more informal proof:

1. Nat(0) Axiom
2. ∀x (Nat(x) → Nat(s(x))) Axiom
3. ∀x ∀y ((Nat(x) ∧ Nat(y)) → Nat(x + y)) Axiom
4. ∀x (Nat(x) → ¬s(x) = 0) Axiom
5. ∀x ∀y ((Nat(x) ∧ Nat(y)) → (s(x) = s(y) → x = y)) Axiom
6. ∀x ((Nat(x) ∧ ¬x = 0) → ∃z (Nat(z) ∧ x = s(z))) Axiom
7. ∀x (Nat(x) → x + 0 = x) Axiom
8. ∀x ∀y ((Nat(x) ∧ Nat(y)) → x + s(y) = s(x + y)) Axiom
9. ∀x ∀y ((Nat(x) ∧ Nat(y)) → (Leq(x,y) ↔ ∃z (Nat(z) ∧ y = x + z))) Axiom
10. Nat(0) → Nat(s(0)) ∀ Elim : 2
11. Nat(s(0)) → Elim : 1, 10
12. Nat(s(0)) → Nat(s(s(0))) ∀ Elim : 2
13. Nat(s(s(0))) → Elim : 11, 12
14. $\qquad$ a Nat(a) Assumption (introduces 'a' and assumes that 'a' is a Nat)
15. $\qquad$ Nat(a) → a + 0 = a ∀ Elim : 7
16. $\qquad$ a + 0 = a → Elim : 14, 15
17. $\qquad \qquad$ Leq(a,s(s(0))) Assumption
18. $\qquad \qquad$ (Nat(a) ∧ Nat(s(s(0)))) → (Leq(a,s(s(0))) ↔ ∃z (Nat(z) ∧ s(s(0)) = a + z)) ∀ Elim : 9
19. $\qquad \qquad$ Nat(a) ∧ Nat(s(s(0))) ∧ Intro : 14, 13
20. $\qquad \qquad$ Leq(a,s(s(0))) ↔ ∃z (Nat(z) ∧ s(s(0)) = a + z) → Elim : 18, 19
21. $\qquad \qquad$ ∃z (Nat(z) ∧ s(s(0)) = a + z) ↔ Elim : 20, 17
22. $\qquad \qquad \qquad$ b Nat(b) ∧ s(s(0)) = a + b Assumption (effectively: 'let 'b' be the 'z' from line 21')
23. $\qquad \qquad \qquad$ Nat(b) ∧ Elim : 22
24. $\qquad \qquad \qquad$ s(s(0)) = a + b ∧ Elim : 22
25. $\qquad \qquad \qquad$ s(s(0)) = s(s(0)) = Intro
26. $\qquad \qquad \qquad$ a + b = s(s(0)) = Elim : 24, 25
27. $\qquad \qquad \qquad \qquad$ ¬(a = 0 ∨ a = s(0) ∨ a = s(s(0))) Assumption (setting up a Proof by Contradiction)
28. $\qquad \qquad \qquad \qquad \qquad$ b = 0 Assumption
29. $\qquad \qquad \qquad \qquad \qquad$ a + 0 = s(s(0)) = Elim : 28, 26
30. $\qquad \qquad \qquad \qquad \qquad$ a = s(s(0)) = Elim : 16, 29
31. $\qquad \qquad \qquad \qquad \qquad$ a = 0 ∨ a = s(0) ∨ a = s(s(0)) ∨ Intro : 30
32. $\qquad \qquad \qquad \qquad \qquad$ ⊥ ⊥ Intro : 31, 27
33. $\qquad \qquad \qquad \qquad$ ¬b = 0 ¬ Intro : 28-32
34. $\qquad \qquad \qquad \qquad$ Nat(b) ∧ ¬b = 0 ∧ Intro : 23, 33
35. $\qquad \qquad \qquad \qquad$ (Nat(b) ∧ ¬b = 0) → ∃z (Nat(z) ∧ b = s(z)) ∀ Elim : 6
36. $\qquad \qquad \qquad \qquad$ ∃z (Nat(z) ∧ b = s(z)) → Elim : 34, 35
37. $\qquad \qquad \qquad \qquad \qquad$ c Nat(c) ∧ b = s(c) Assumption (effectively: 'let 'c' be the 'z' from line 36')
38. $\qquad \qquad \qquad \qquad \qquad$ Nat(c) ∧ Elim : 37
39. $\qquad \qquad \qquad \qquad \qquad$ b = s(c) ∧ Elim : 37
40. $\qquad \qquad \qquad \qquad \qquad$ a + s(c) = s(s(0)) = Elim : 39, 26
41. $\qquad \qquad \qquad \qquad \qquad$ Nat(a) ∧ Nat(c) ∧ Intro : 14, 38
42. $\qquad \qquad \qquad \qquad \qquad$ (Nat(a) ∧ Nat(c)) → a + s(c) = s(a + c) ∀ Elim : 8
43. $\qquad \qquad \qquad \qquad \qquad$ a + s(c) = s(a + c) → Elim : 41, 42
44. $\qquad \qquad \qquad \qquad \qquad$ s(a + c) = s(s(0)) = Elim : 43, 40
45. $\qquad \qquad \qquad \qquad \qquad$ (Nat(a) ∧ Nat(c)) → Nat(a + c) ∀ Elim : 3
46. $\qquad \qquad \qquad \qquad \qquad$ Nat(a + c) → Elim : 41, 45
47. $\qquad \qquad \qquad \qquad \qquad$ Nat(a + c) ∧ Nat(s(0)) ∧ Intro : 46, 11
48. $\qquad \qquad \qquad \qquad \qquad$ (Nat(a + c) ∧ Nat(s(0))) → (s(a + c) = s(s(0)) → a + c = s(0)) ∀ Elim : 5
49. $\qquad \qquad \qquad \qquad \qquad$ s(a + c) = s(s(0)) → a + c = s(0) → Elim : 47, 48
50. $\qquad \qquad \qquad \qquad \qquad$ a + c = s(0) → Elim : 44, 49
51. $\qquad \qquad \qquad \qquad \qquad\qquad$ c = 0 Assumption
52. $\qquad \qquad \qquad \qquad \qquad\qquad$ a + 0 = s(0) = Elim : 51, 50
53. $\qquad \qquad \qquad \qquad \qquad\qquad$ a = s(0) = Elim : 16, 52
54. $\qquad \qquad \qquad \qquad \qquad\qquad$ a = 0 ∨ a = s(0) ∨ a = s(s(0)) ∨ Intro : 53
55. $\qquad \qquad \qquad \qquad \qquad\qquad$ ⊥ ⊥ Intro : 54, 27
56. $\qquad \qquad \qquad \qquad \qquad$ ¬c = 0 ¬ Intro : 51-55
57. $\qquad \qquad \qquad \qquad \qquad$ Nat(c) ∧ ¬c = 0 ∧ Intro : 38, 56
58. $\qquad \qquad \qquad \qquad \qquad$ (Nat(c) ∧ ¬c = 0) → ∃z (Nat(z) ∧ c = s(z)) ∀ Elim : 6
59. $\qquad \qquad \qquad \qquad \qquad$ ∃z (Nat(z) ∧ c = s(z)) → Elim : 57, 58
60. $\qquad \qquad \qquad \qquad \qquad\qquad$ d Nat(d) ∧ c = s(d) Assumption (effectively: 'let 'd' be the 'z' from line 59')
61. $\qquad \qquad \qquad \qquad \qquad\qquad$ Nat(d) ∧ Elim : 60
62. $\qquad \qquad \qquad \qquad \qquad\qquad$ c = s(d) ∧ Elim : 60
63. $\qquad \qquad \qquad \qquad \qquad \qquad$ a + s(d) = s(0) = Elim : 62, 50
64. $\qquad \qquad \qquad \qquad \qquad \qquad$ Nat(a) ∧ Nat(d) ∧ Intro : 14, 61
65. $\qquad \qquad \qquad \qquad \qquad \qquad$ (Nat(a) ∧ Nat(d)) → a + s(d) = s(a + d) ∀ Elim : 8
66. $\qquad \qquad \qquad \qquad \qquad \qquad$ a + s(d) = s(a + d) → Elim : 64, 65
67. $\qquad \qquad \qquad \qquad \qquad \qquad$ s(a + d) = s(0) = Elim : 66, 63
68. $\qquad \qquad \qquad \qquad \qquad \qquad$ (Nat(a) ∧ Nat(d)) → Nat(a + d) ∀ Elim : 3
69. $\qquad \qquad \qquad \qquad \qquad \qquad$ Nat(a + d) → Elim : 64, 68
70. $\qquad \qquad \qquad \qquad \qquad \qquad$ Nat(a + d) ∧ Nat(0) ∧ Intro : 69, 1
71. $\qquad \qquad \qquad \qquad \qquad \qquad$ (Nat(a + d) ∧ Nat(0)) → (s(a + d) = s(0) → a + d = 0) ∀ Elim : 5
72. $\qquad \qquad \qquad \qquad \qquad \qquad$ s(a + d) = s(0) → a + d = 0 → Elim : 70, 71
73. $\qquad \qquad \qquad \qquad \qquad \qquad$ a + d = 0 → Elim : 67, 72
74. $\qquad \qquad \qquad \qquad \qquad \qquad \qquad$ d = 0 Assumption
75. $\qquad \qquad \qquad \qquad \qquad \qquad \qquad$ a + 0 = 0 = Elim : 74, 73
76. $\qquad \qquad \qquad \qquad \qquad \qquad \qquad$ a = 0 = Elim : 16, 75
77. $\qquad \qquad \qquad \qquad \qquad \qquad \qquad$ a = 0 ∨ a = s(0) ∨ a = s(s(0)) ∨ Intro : 76
78. $\qquad \qquad \qquad \qquad \qquad \qquad \qquad$ ⊥ ⊥ Intro : 77, 27
79. $\qquad \qquad \qquad \qquad \qquad \qquad $ ¬d = 0 ¬ Intro : 74-78
80. $\qquad \qquad \qquad \qquad \qquad \qquad $ Nat(d) ∧ ¬d = 0 ∧ Intro : 61, 79
81. $\qquad \qquad \qquad \qquad \qquad \qquad $ (Nat(d) ∧ ¬d = 0) → ∃z (Nat(z) ∧ d = s(z)) ∀ Elim : 6
82. $\qquad \qquad \qquad \qquad \qquad \qquad $ ∃z (Nat(z) ∧ d = s(z)) → Elim : 81, 80
83. $\qquad \qquad \qquad \qquad \qquad \qquad \qquad$ e Nat(e) ∧ d = s(e) Assumption (effectively: 'let 'e' be the 'z' from line 82')
84. $\qquad \qquad \qquad \qquad \qquad \qquad \qquad$ Nat(e) ∧ Elim : 83
85. $\qquad \qquad \qquad \qquad \qquad \qquad \qquad$ d = s(e) ∧ Elim : 83
86. $\qquad \qquad \qquad \qquad \qquad \qquad \qquad$ a + s(e) = 0 = Elim : 85, 73
87. $\qquad \qquad \qquad \qquad \qquad \qquad \qquad$ Nat(a) ∧ Nat(e) ∧ Intro : 14, 84
88. $\qquad \qquad \qquad \qquad \qquad \qquad \qquad$ (Nat(a) ∧ Nat(e)) → a + s(e) = s(a + e) ∀ Elim : 8
89. $\qquad \qquad \qquad \qquad \qquad \qquad \qquad$ a + s(e) = s(a + e) → Elim : 87, 88
90. $\qquad \qquad \qquad \qquad \qquad \qquad \qquad$ s(a + e) = 0 = Elim : 89, 86
91. $\qquad \qquad \qquad \qquad \qquad \qquad \qquad$ (Nat(a) ∧ Nat(e)) → Nat(a + e) ∀ Elim : 3
92. $\qquad \qquad \qquad \qquad \qquad \qquad \qquad$ Nat(a + e) → Elim : 87, 91
93. $\qquad \qquad \qquad \qquad \qquad \qquad \qquad$ Nat(a + e) → ¬s(a + e) = 0 ∀ Elim : 4
94. $\qquad \qquad \qquad \qquad \qquad \qquad \qquad$ ¬s(a + e) = 0 → Elim : 92, 93
95. $\qquad \qquad \qquad \qquad \qquad \qquad \qquad$ ⊥ ⊥ Intro : 90, 94
96. $\qquad \qquad \qquad \qquad \qquad \qquad$ ⊥ ∃ Elim : 83-95, 82
97. $\qquad \qquad \qquad \qquad \qquad$ ⊥ ∃ Elim : 60-96, 59
98. $\qquad \qquad \qquad \qquad$ ⊥ ∃ Elim : 37-97, 36
99. $\qquad \qquad \qquad$ ¬¬(a = 0 ∨ a = s(0) ∨ a = s(s(0))) ¬ Intro : 27-98
100. $\qquad \qquad \qquad$ a = 0 ∨ a = s(0) ∨ a = s(s(0)) ¬ Elim : 99
101. $\qquad \qquad$ a = 0 ∨ a = s(0) ∨ a = s(s(0)) ∃ Elim : 22-100, 21
102. $\qquad$ Leq(a,s(s(0))) → (a = 0 ∨ a = s(0) ∨ a = s(s(0))) → Intro : 17-101
103. ∀x (Nat(x) → (Leq(x,s(s(0))) → (x = 0 ∨ x = s(0) ∨ x = s(s(0))))) ∀ Intro : 14-102