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:

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:

Proof sketch of Gödel's incompleteness theorems

In this post, I will follow the outline of the proof given in Section VII of Nagel and Newman's book. Recall that:

• a formal system F is consistent if there is no well-formed formula (wff) w such that F proves both w and ¬ w, and
• a formal system is (semantically) complete if it can prove all of the true wff's that it can express.

Now, Gödel's first incompleteness theorem can be paraphrased as:

Any consistent formal system that is expressive enough to model arithmetic is both incomplete and "incompletable."

and Gödel's second incompleteness theorem can be paraphrased as:

Any consistent formal system that is expressive enough to model arithmetic cannot prove its own consistency.

According to Nagel and Newman, a proof of the first theorem can be sketched in 4 steps: