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:
  1. The set of atomic Δ0 wff's is the set of wff's of the form σ = τ or σ ≤ τ, where σ and τ are terms of LA.
  2. The set of Δ0 wff's is defined inductively by the following rules:
    • Every atomic Δ0 wff is a Δ0 wff.
    • If α and β are Δ0 wff's, then so are ¬α, α ∧ β, α ∨ β, and α → β.
    • If α is a Δ0 wff, then so are (∀χ ≤ κ) α and  (∃χ ≤ κ) α, where χ is any variable that appears free in α and κ is a numeral or a variable that is different from χ (see this post for the definition of these bounded quantifiers).
    • Nothing else is a Δ0 wff.
  3. A wff is strictly Σ1 iff it is of the form ∃α∃β...∃ω φ, where φ is Δ0 and α, β, ... , ω are one or more distinct variables that appear free in φ.
  4. A wff is Σ1 iff it is logically equivalent to a strictly Σ1 wff.
  5. A wff is strictly Π1 iff it is of the form ∀α∀β...∀ω φ, where φ is Δ0 and α, β, ... , ω are one or more distinct variables that appear free in φ.
  6. A wff is Π1 iff it is logically equivalent to a strictly Π1 wff.
Note that these sets contain not only sentences but also open wff's, that is, wff's with one or more free variables. Here are two examples of Δ0 wff's:

(∃v ≤ x) (2 × v = x) 

2 ≤ x  ∧  (∀t ≤ x) (∀u ≤ x) (t × u = x → (t = 1 ∨ u = 1))

Each one of these two wff's contains the free variable x. Let's refer to these open wff's as e(x) and p(x), since they express the facts that x is even and x is prime, respectively.

According to Smith, the set Δ0 is built in such a way that its elements do not contain any (unbounded) universal or existential quantifiers. I find this statement a bit surprising because the atomic Δ0 wff of the form σ ≤ τ  is really an abbreviation for:

 ∃v (v + σ = τ)

which does contain an unbounded existential quantifier. The only reasoning I could come up with to resolve this difficulty is that, to determine the truth value of σ ≤ τ, one only needs to check a finite number of addition facts, because the value of v that works, if it exists, must be less than or equal to the numerical value of τ (which must be a constant number for the truth value of the whole formula to be defined).

Now, let's consider the following wff:

∀x ( (e(x) ∧ 4 ≤ x) → (∃y ≤ x) (∃z ≤ x) (p(y) ∧ p(z) ∧ y + z = x) )

The interpretation of this open wff is "Every even number greater than 2 is the sum of two primes," which is the famous Goldbach conjecture. Since the sub-formula after the ∀x is a Δ0 wff, the entire wff is strictly Π1. Recall that a strictly Πwff is a Δ0 wff preceded by a single group of one or more (unbounded) universal quantifiers. Similarly, a strictly Σwff is a Δ0 wff preceded by a single group of one or more (unbounded) existential quantifiers.

Second, let's state some simple results:
  • Lemma 1: The negation of a Δ0 wff is also Δ0.
  • Lemma 2: The negation of a Σwff is Π1 and vice versa.
  • Lemma 3: A Δ0 wff is also both Σ1 and Π1.
  • Lemma 4: The function that assigns a truth value to each Δ0 wff is effectively computable.
Lemma 1 follows directly from the second bullet point in the second definition above.

Lemma 2 follows directly from De Morgan's laws for quantifiers, namely:
  • ¬∃x φ(x) is logically equivalent to ∀x ¬φ(x)
  • ¬∀x φ(x) is logically equivalent to ∃x ¬φ(x)

Proof sketch of Lemma 3:
  • Let φ be any Δ0 wff in which the variable z does not appear free.
  • φ is logically equivalent to both ∀z (φ ∧ z = z) and ∃z (φ ∧ z = z).
  • ∃z (φ ∧ z = z) is strictly Σ1.
  • ∀z (φ ∧ z = z) is strictly Π1.

Proof sketch of Lemma 4:
  • Computing the truth value of any Δ0 wff takes only a finite number of well-defined steps because:
    • Each universally or existentially bounded quantified wff can be converted to a finite conjunction or disjunction, respectively.
    • As mentioned above, any atomic Δ0 wff using ≤ can be converted to a finite disjunction.
    • One can use the truth tables of the connectives to compute truth values compositionally.
  • This proof can be made rigorous using structural induction, where each atomic wff has a structural complexity of 0 and each connective increments the structural complexity by 1. 

Third, we come to the main result of this post:

Theorem: Q is Σ1-complete. 

Proof sketch:
  • Q correctly decides every atomic Δ0 sentence: these sentences are either closed equalities or closed inequalities; the first case is already covered in our proof that BA correctly decides all sentences in LB; the second case also works out because each inequality between terms can be reduced to an inequality between numerals (since each closed term can be reduced to a numeral SSS...S0), which in turn is correctly decided, because Q captures the ≤ relation.
  • Q correctly decides every Δ0 sentence: we can again use structural induction here
  • Q proves every true Σsentence: since each true bounded kernel (that is, every true Δ0 sentence) is proved by Q, every true sentence obtained by adding one or more existential quantifiers in front of the kernel is derivable in Q, using the inference rule called existential generalization (or existential introduction).

Finally, let's wrap up this post with a couple of corollaries.

Corollary 1:  A Π1 sentence φ is true iff ¬φ cannot be derived in Q (i.e., φ is consistent with Q).

Proof sketch:
  • If φ is false, then ¬φ is a true Σ1 sentence (by Lemma 2) and thus derivable in Q.
  • If φ is true, then ¬φ is false and thus not derivable in Q (since Q is sound, because its axioms are true and its inference rules are truth-preserving).
So, if derivability in Q were effectively decidable (we'll see later that it's not), then the function that assigns a truth value to each sentence in Π1 would be effectively computable.

Before the next and last corollary, a quick definition:

A theory T2 extends a theory T1 if:
  • The language of T1 is a subset of the language of T2,
  • The wff's common to Tand T2 have the same truth values in both interpreted languages, and
  • T2 can prove (at least) all of the theorems of T1.

Corollary 2:  If a theory T extends Q, then T is consistent iff T is Π1-sound.

Proof sketch: Assume T extends Q.
  • If T is inconsistent, then it can derive everything in T's language, including all of the false Π1 sentences. Therefore, T is not Π1-sound.
  • If T is not Π1-sound, then T proves some false Π1 sentence φ. Thus, ¬φ is a true Σ1 sentence (by Lemma 2) and T must derive ¬φ (since Q being Σ1-complete implies that T is also Σ1-complete). Therefore T is inconsistent (since it derives both φ and ¬φ). By contraposition, if T is consistent, it is Π1-sound.

2 comments: