**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:

Smith proves that Q satisfies a few of the 9 properties above, namely O1, O2, O3, and O8. Below, I attempt to prove a few of the other properties.

Robinson Arithmetic (or Q) is order-adequate.

Proof of O4: Assume that n is an arbitrary natural number.

- Assume that a is an arbitrary term of Q such that a ≤ n
- Using O3: ∀x (x ≤ n → (x = 0 ∨ x = 1 ∨ x = 2 ∨ ... ∨ x = n))
- a ≤ n → (a = 0 ∨ a = 1 ∨ a = 2 ∨ ... ∨ a = n) [by universal instantiation]
- a = 0 ∨ a = 1 ∨ a = 2 ∨ ... ∨ a = n [modus ponens 1&3]
- Sub-proof by cases:
- According to 4, a is equal to one of the terms in {0,1,2,..., n}
- In all cases, Q ⊢ φ(a) [hypothesis of O4]
- Therefore Q ⊢ φ(a)
- Q ⊢ a ≤ n → φ(a) [discharging assumption 1]
- Q ⊢ ∀x (x ≤ n → φ(x)) [by universal generalization]
- Q ⊢ (∀x ≤ n) φ(x) [by definition of the bounded universal quantifier]

Proof of O5: Assume that n is an arbitrary natural number.

- There is at least one numeral a such that Q ⊢ φ(a) [hypothesis of O5]
- Q ⊢ a ≤ n [since 'the number denoted by a' ≤ n and Q captures ≤]
- Q ⊢ a ≤ n ∧ φ(a) [conjunction of 1 and 2]
- Q ⊢ ∃x (x ≤ n ∧ φ(x)) [existential generalization]
- Q ⊢ (∃x ≤ n) φ(x) [by definition of the bounded existential quantifier]

Proof of O6: Assume that n is an arbitrary natural number.

- Assume (inside Q) that a is an arbitrary term such that a ≤ n
- Using O3: ∀x (x ≤ n → (x = 0 ∨ x = 1 ∨ x = 2 ∨ ... ∨ x = n))
- a ≤ n → (a = 0 ∨ a = 1 ∨ a = 2 ∨ ... ∨ a = n) [by universal instantiation]
- a = 0 ∨ a = 1 ∨ a = 2 ∨ ... ∨ a = n [modus ponens 1&3]
- a = 0 ∨ a = 1 ∨ a = 2 ∨ ... ∨ a = n ∨ a = Sn [added disjunct to 4]
- Using O2: ∀x ((x = 0 ∨ x = 1 ∨ x = 2 ∨ ... ∨ x = n ∨ x = Sn) → x ≤ Sn)
- (a = 0 ∨ a = 1 ∨ a = 2 ∨ ... ∨ a = n ∨ a = Sn) → a ≤ Sn [by universal instantiation]
- a ≤ Sn [modus ponens 5&7]
- a ≤ n → a ≤ Sn [discharging assumption 1]
- ∀x (x ≤ n → x ≤ Sn) [universal generalization]

## No comments:

## Post a Comment