Robinson Arithmetic captures the "less-than-or-equal-to" relation

In this post, we'll start discussing the material in Chapter 9 of Peter Smith's book, namely up to section 9.3.

Before proceeding, review the definition of Robinson Arithmetic (denoted Q) as well as what it means for a theory to capture a numerical relation.

Now, we'll show that Robinson Arithmetic captures the ≤ numerical relation with the open well-formed formula: ∃x (x + m = n).

In other words, we are going to prove the following two-part theorem:

Theorem: If m and n are natural numbers, then:
1. If m ≤ n, then Q ⊢ ∃x (x + m = n)
2. If m > n, then Q ⊢ ¬ ∃x (x + m = n)

Recall that if m and n are natural numbers, then m and n are the numerical terms representing m and n, respectively, in the formal theory.

Proof sketch of part 1:

• Assume that m ≤ n
• There must exist a natural number k such that: k + m = n
• Since Q can prove everything that BA proves, and BA can prove all true equations, we have: Q ⊢ k + m = n
• By existential generalization (an inference rule also called 'existential quantifier introduction'), we have: Q ⊢ ∃x (x + m = n)

Now, here are axioms of Q that we will need in the second part of the proof:

• Axiom 1: ∀x (0 ≠ Sx)
• Axiom 2: ∀x∀y (Sx = Sy → x = y)
• Axiom 4: ∀x (x + 0 = x)
• Axiom 5: ∀x∀y (x + Sy = S(x + y))

Proof sketch of part 2:

• Assume that m > n. We need to prove Q ⊢ ¬ ∃x (x + m = n)
• Following Smith's lead, we will only write down a formal proof for the special case m = 2 and n = 1 here, hoping that the general proof pattern will be easily discernible. Note that Smith uses a Fitch-style, natural-deduction proof, while I came up with a Hilbert-style proof. Here is the formal proof of ¬ ∃x (x + SS0 = S0) in Q:

1. ∀x (0 ≠ Sx) [Axiom 1]
2. 0 ≠ Sa [Universal instantiation of 1 with arbitrary term a]
3. ∀x∀y (Sx = Sy → x = y) [Axiom 2]
4. ∀y (S0 = Sy → 0 = y) [Universal instantiation of 3 with specific term 0]
5. S0 = SSa → 0 = Sa [Universal instantiation of 4 with term Sa]
6. 0 ≠ Sa → S0 ≠ SSa [Contrapositive of 5]
7. S0 ≠ SSa [Modus ponens 2 & 6]
8. ∀x (x + 0 = x) [Axiom 4]
9. a + 0 = a [Universal instantiation of 8 with term a]
10. S0 ≠ SS(a+0) [Substitution of (a+0) for a in 7]
11. ∀x∀y (x + Sy = S(x + y)) [Axiom 5]
12. ∀y (a + Sy = S(a + y)) [Universal instantiation of 11 with term a]
13. a + S0 = S(a + 0) [Universal instantiation of 12 with term 0]
14. S0 ≠ S(a + S0) [Substitution of (a + S0) for S(a + 0) in 10]
15. a + SS0 = S(a + S0) [Universal instantiation of 12 with term S0]
16. S0 ≠ a + SS0 [Substitution of a + SS0 for S(a + S0) in 14]
17. ∀x (S0 ≠ a + SS0) [Universal generalization of 16]
18. ∀x ¬ (S0 = x + SS0) [Rewriting of 17]
19. ¬ ∃x (S0 = x + SS0) [Apply one of De Morgan's law for quantifiers to 18]
20. ¬ ∃x (x + SS0 = S0) [Switched order of terms in equation 19]

Since Q captures the ≤ relation, we can now add this predicate to L_A (the interpreted, formal language of Q). In other words, we can use the abbreviation α ≤ β for ∃x (x + α = β).

In fact, we will use a couple more abbreviations for bounded quantification, namely:

• (∀x ≤ k) φ(x) as syntactic sugar for ∀x (x ≤ k → φ(x)), and
• (∃x ≤ k) φ(x) as syntactic sugar for ∃x (x ≤ k ∧ φ(x))

In conclusion, to unpack the two levels of abbreviation:

• (∀x ≤ k) φ(x) is syntactic sugar for ∀x (∃y (y + x = k) → φ(x))
• (∃x ≤ k) φ(x) is syntactic sugar for ∃x (∃y (y + x = k) ∧ φ(x))