Robinson Arithmetic is Σ1-complete

Recall that Q (i.e., Robinson Arithmetic) is an axiomatized formal theory (AFT) of arithmetic couched in the interpreted formal language L_A. Let L be a subset of L_A and let T be some AFT of arithmetic.

We say that T is L-sound iff, for any sentence φ in L, if T ⊢ φ, then φ is true.

We say that T is L-complete iff, for any sentence φ in L, if φ is true, then T ⊢ φ.

In chapter 9, Peter Smith defines a subset of L_A, called Σ₁. Then, using the fact that Q is order-adequate, he proves that Q is Σ₁-complete. This is important because the well-formed formulas (wff's) of Σ₁ can express the decidable numerical properties and relations, and therefore Q will be sufficiently strong. Now to the details...

First, let's define a few interesting subsets of L_A:

Robinson Arithmetic is order-adequate

In chapter 9, Peter Smith defines the following concept: A theory T that captures the relation ≤ is order-adequate if it satisfies the following nine properties:

• O1: T ⊢ ∀x (0 ≤ x)
• O2: For any n, T ⊢ ∀x ((x = 0 ∨ x = 1 ∨ x = 2 ∨ ... ∨ x = n) → x ≤ n)
• O3: For any n, T ⊢ ∀x (x ≤ n → (x = 0 ∨ x = 1 ∨ x = 2 ∨ ... ∨ x = n))
• O4: For any n, if T ⊢ φ(0) and T ⊢ φ(1) and ... and T ⊢ φ(n) then T ⊢ (∀x ≤ n)φ(x)
• O5: For any n, if T ⊢ φ(0) or T ⊢ φ(1) or ... or T ⊢ φ(n) then T ⊢ (∃x ≤ n)φ(x)
• O6: For any n, T ⊢ ∀x (x ≤ n → x ≤ Sn)
• O7: For any n, T ⊢ ∀x (n ≤ x  → (n = x  ∨ Sn ≤ x))
• O8: For any n, T ⊢ ∀x (x ≤ n ∨ n ≤ x)
• O9: For any n>0, T ⊢ (∀x ≤ n-1)φ(x) → (∀x ≤ n)(x ≠ n → φ(x))

Then, we have the following theorem:

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: