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:

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

Since Q captures the ≤ relation, we can now add this predicate to

In fact, we will use a couple more abbreviations for

In conclusion, to unpack the two levels of abbreviation:

*L*(the interpreted, formal language of Q). In other words, we can use the abbreviation α ≤ β for ∃x (x + α = β)._{A}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))

## No comments:

## Post a Comment