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:

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:

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:

Q - Robinson Arithmetic

Now that we are familiar with Baby Arithmetic (BA), we can make its language more expressive by allowing variables and quantifiers back into its logical vocabulary. When we do this, we simply obtain the interpreted language L_A, that was described earlier.

Since we now have variables and quantifiers, we can replace the schemata of BA with regular axioms (see below). The resulting formal system of arithmetic is called Robinson Arithmetic and is often denoted by the letter Q, as described in Chapter 8 of Peter Smith's book. Here is his definition of Q:

Baby arithmetic

Since chapter 7 in Peter Smith's book is so short, I'll summarize it quickly and then start discussing chapter 8.

Chapter 7 starts by comparing the two incompleteness theorems discussed in previous chapters (let's call these "Smith's theorems") to Gödel's first incompleteness theorem as follows:

Consistent, sufficiently strong formal systems of arithmetic are incomplete

In Chapter 6, Peter Smith proves another incompleteness theorem. To place this theorem in context, let's review some definitions about axiomatized formal theories (or AFTs) from earlier posts.

Let T be some AFT.

• T is consistent iff (if and only if) there is no sentence φ such that T proves both φ and ¬ φ.
• T is sound iff every theorem that T proves is true according to the interpretation that is built into T's language.
• T is (negation-)complete iff for every sentence φ in T's language, T proves either φ or ¬ φ.
• T is decidable iff there is an algorithm that, given any sentence φ in T's language, determines whether or not T proves φ.
• If needed, go here to review what it means for T's language to express a numerical property P or a numerical relation R.
• If needed, go here to review what it means for T to capture a numerical property P or a numerical relation R. 
• If needed, go here to review what it means for T's language to be sufficiently expressive.

We'll use the following abbreviations:

Sound formal systems with sufficiently expressive languages are incomplete

In chapter 5, Peter Smith uses a counting argument to prove that sound axiomatized formal theories (AFTs) that can express a good amount of arithmetic are incomplete. In short: since their set of theorems is effectively enumerable but their set of true sentences is not, the two sets must be different. In a sound theory, the theorems are all true. Therefore, some truths must remained unproved in such theories.

Let's start with a definition. The language of an AFT of arithmetic is sufficiently expressive if and only if:

1. It can express quantification over numbers, and
2. It can express every effectively decidable two-place numerical relation.

Now, to the pivotal theorem of this chapter:

An enumerable but not effectively enumerable set

Let's focus on the first half of chapter 5 in Peter Smith's book. First, Smith describes a new characterization of effectively enumerable sets. Second, Smith gives an example of a set of integers that is not effectively enumerable.

Let's define the numerical domain of an algorithm as the set of natural numbers with the following property: when the algorithm takes one of these numbers as input, it terminates and returns a result. Every algorithm has a numerical domain. If the input to some algorithm is not a single natural number, then the numerical domain of this algorithm is the empty set. Otherwise, the numerical domain is the set of those natural numbers on which the algorithm does not crash and does not go into an infinite loop.

It turns out that each numerical domain is effectively enumerable. In fact, the converse is also true, according to the following theorem:

Capturing numerical properties in a formal language of arithmetic

Peter Smith starts Chapter 4 by describing L_A, a formal language that is at the core of several AFTs (axiomatized formal theories) of arithmetic. Then Smith explains what it means for a formal language of arithmetic to "express" a numerical property and the stronger notion of "capturing" a numerical property.

Here is the definition of L_A:

Formal systems or axiomatized formal theories

In chapter 3, Peter Smith defines formal systems or, as he calls them, axiomatized formal theories (I will use AFT as an abbreviation for this phrase).

A theory T is an AFT if...

Effective computability, decidability and enumerability

In Chapter 2, Smith covers familiar ground. So this post will be short. Here is a quick summary, section by section.

Section 1 reviews terminology pertaining to functions, namely the notions of domain and range, as well as special cases of functions, namely injective (or one-to-one) functions, surjective (or onto) functions and bijective functions (or one-to-one correspondences).

Peter Smith's overview of Gödel's incompleteness theorems

Finally! As was my initial goal, I now turn my attention to Peter Smith's book on the proof of Gödel's incompleteness theorems (by the way, I own the first edition of his book; so that is the one I will be referring to). I did not expect to spend that much time on Nagel and Newman's book. But it was worthwhile in getting the big picture.

Chapter 1 is an introductory and user-friendly discussion of topics that were mentioned in earlier posts, such as basic arithmetic, formal systems, (in)completeness, consistency, the statement of Gödel's incompleteness theorems and some of their implications. Therefore, in this post, I will just highlight the points where Smith provides new information or has a different perspective.

Absolute proofs of consistency and meta-mathematics

In earlier posts, we explained why consistency is an important property of axiomatic systems and discussed relative proofs of consistency, in which the proof of consistency of a system is based on the assumption that another axiomatic system is consistent. In this post, we introduce absolute proofs of consistency that do not make any assumptions about any other axiomatic system. Apparently, David Hilbert was the first to study and propose such proofs, according to Nagel and Newman's book (Section III, page 26).

Recall that an axiomatic system is consistent if it cannot derive both a theorem and its negation. What do we mean by the negation of a theorem? Let's take, as a simple example, the theorem: "6 is divisible by 3." Its negation is simply the following statement: "6 is not divisible by 3" or equivalently "It is not the case that 6 is divisible by 3." This second formulation of the negation, although less elegant in English, is preferable because the negation is added to the front of the original theorem. In a formal system, negation is handled by simply adding a symbol for the phrase "it is not the case that." Several symbols have been used for negation, such as ~ and ¬ . We'll use the latter here. So, if T is any theorem in some formal system, then the formula  ¬T is the negation of T.

Remember that our formal system FS did not have a symbol for negation. So we will extend FS into a new formal system called FSN (for FS with Negation), whose alphabet is { E, 0, 1, ¬ }. FSN has exactly one axiom, namely the same as A1 in FS. FSN also has the same inference rules as FS, namely IR1 and IR2. But it has one additional inference rule that uses negation. Here is the full description of FSN:

I just want to understand the proof of Gödel's incompleteness theorems

So this is it! Summer 2013... This is when I get to master the proof of Gödel's incompleteness theorems (thereafter: GIT).

I discovered GIT as an undergraduate student in one of my Artificial Intelligence courses. My instructor was reading Gödel, Escher, Bach and was raving about the book. He even took some of our exam problems from it. But what I remember most is the outline of the proof of GIT, more precisely the first theorem. To be honest, the only part of it that stuck with me was the idea of numbering the formulas. Of course, at the time, I bought a copy of the book. I liked many parts of it but I never finished it.

Years later, while I was teaching computability theory and other computer science topics, I encountered GIT several times. At some point, I decided I wanted to understand the proof of GIT. 

First, I read the classic "Gödel's Proof" by Nagel and Newman. That is a concise and user-friendly overview of the proof. But it was only a proof sketch. So I looked at some textbooks on formal logic, which were neither concise nor user-friendly. I still did not understand the proof.

Finally, a couple of years ago, I came across a promising volume: "Introduction to Gödel’s Theorems" by Peter Smith. I read the first few chapters but then ran out of time (and motivation) to finish it. The following year, I made another attempt: I had to start from scratch and did not get any farther into it the second time around...