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:

1. The set of atomic Δ₀ wff's is the set of wff's of the form σ = τ or σ ≤ τ, where σ and τ are terms of L_A.
2. The set of Δ₀ wff's is defined inductively by the following rules:
• Every atomic Δ₀ wff is a Δ₀ wff.
• If α and β are Δ₀ wff's, then so are ¬α, α ∧ β, α ∨ β, and α → β.
• If α is a Δ₀ 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 Δ₀ wff.
3. A wff is strictly Σ₁ iff it is of the form ∃α∃β...∃ω φ, where φ is Δ₀ and α, β, ... , ω are one or more distinct variables that appear free in φ.
4. A wff is Σ₁ iff it is logically equivalent to a strictly Σ₁ wff.
5. A wff is strictly Π₁ iff it is of the form ∀α∀β...∀ω φ, where φ is Δ₀ and α, β, ... , ω are one or more distinct variables that appear free in φ.
6. A wff is Π₁ iff it is logically equivalent to a strictly Π₁ 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 Δ₀ 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 Δ₀ 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 Δ₀ 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 Δ₀ wff, the entire wff is strictly Π₁. Recall that a strictly Π₁ wff is a Δ₀ wff preceded by a single group of one or more (unbounded) universal quantifiers. Similarly, a strictly Σ₁ wff is a Δ₀ 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 Δ₀ wff is also Δ₀.
• Lemma 2: The negation of a Σ₁ wff is Π₁ and vice versa.
• Lemma 3: A Δ₀ wff is also both Σ₁ and Π₁.
• Lemma 4: The function that assigns a truth value to each Δ₀ 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 Δ₀ 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 Σ₁.
• ∀z (φ ∧ z = z) is strictly Π₁.

Proof sketch of Lemma 4:

• Computing the truth value of any Δ₀ 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 Δ₀ 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 Σ₁-complete. 

Proof sketch:

• Q correctly decides every atomic Δ₀ 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 L_B; 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 Δ₀ sentence: we can again use structural induction here
• Q proves every true Σ₁ sentence: since each true bounded kernel (that is, every true Δ₀ 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 Π₁ sentence φ is true iff ¬φ cannot be derived in Q (i.e., φ is consistent with Q).

Proof sketch:

• If φ is false, then ¬φ is a true Σ₁ 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 Π₁ would be effectively computable.

Before the next and last corollary, a quick definition:

A theory T₂ extends a theory T₁ if:

• The language of T₁ is a subset of the language of T₂,
• The wff's common to T₁ and T₂ have the same truth values in both interpreted languages, and
• T₂ can prove (at least) all of the theorems of T₁.

Corollary 2:  If a theory T extends Q, then T is consistent iff T is Π₁-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 Π₁ sentences. Therefore, T is not Π₁-sound.
• If T is not Π₁-sound, then T proves some false Π₁ sentence φ. Thus, ¬φ is a true Σ₁ sentence (by Lemma 2) and T must derive ¬φ (since Q being Σ₁-complete implies that T is also Σ₁-complete). Therefore T is inconsistent (since it derives both φ and ¬φ). By contraposition, if T is consistent, it is Π₁-sound.