Tuesday, July 9, 2013

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 LA. Let L be a subset of LA 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 LA, called Σ1. Then, using the fact that Q is order-adequate, he proves that Q is Σ1-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 LA:

Sunday, July 7, 2013

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:

Wednesday, July 3, 2013

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: