1. Gödel’s first incompleteness theorem

We offer here a naïve presentation of Gödel’s first incompleteness theorem that relies on recursion theoretic techniques. It says that any “reasonable” axiomatic system that attempts to have as theorems precisely all the “true” (first order) formulas of arithmetic will fail: There will be infinitely many true formulas that are not theorems. The qualifier “reasonable” could well be replaced by “practical”: One must be able to tell, algorithmically, whether a formula is an axiom or not—for how else can one check a proof, let alone write one? “True” means true in the standard interpretation over the structure

𝔑 = (ℕ; 0, λx.x + 1, λxy.x + y, λxy.x × y, λxy.x < y)

where after the semicolon I have listed “important” constants, functions and predicates (see the table of interpretations below).

To set the stage more accurately, we will need some definitions and notation. In order to do arithmetic we need, first of all, a first order (logical) language which we use to write down formulas and proofs. Before we get to the language (that is, a set of strings) we need an “alphabet”.

This alphabet has two parts: One that is standard in all such languages (logical symbols), namely variables of natural number type (or “object variables”) denoted by x, y, z, u, v, w with or without accents and subscripts. The logical part also contains the symbols

¬, ∨, ∧, →, ↔, =, ∃, ∀, (,)

The other part of the alphabet is specific to doing arithmetic. It contains the “abstract” symbols

0, S, +, ×, <

These are the nonlogical symbols which we can interpret any way we please. However we decide to interpret them in the standard way:

Abstract (language) symbol Concrete interpretation
0  0 (zero)
S  λx.x + 1
+  λxy.x + y
×  λxy.x × y
<  λxy.x < y

One forms formulas now in the standard way (see for example [Tou98]). But what about symbols for “1”, “2” and “112056734555”? An arbitrary n ∈ ℕ has the formal counterpart

\underbrace{SS ⋯ S}_{n times} 0

which we denote by ñ.

Thus, an axiomatic system (or theory) that we use to formally (i.e., syntactically) prove theorems of arithmetic contains:

(1) The briefly described first order language above.^{∗}

(2) A recursive set of strings: The well-formed formulas (wff).^{†}

(3) A recursive subset of wff: The special (or nonlogical) axioms for arithmetic.^{‡}

(4) The logical axioms (cf. [Tou98])

(5) The rules of inference (cf. [Tou98])

1.1 Remark.

(i) Intuitively, (2) above says that there is an algorithm that for every string over our alphabet

¬, ∨, ∧, →, ↔, =, ∃, ∀, (,), v, 1, 0, S, +, ×, <  (A)

will decide the string’s membership in wff—i.e., whether or not the string parses correctly as a formula. But what do we mean when we say that a set of strings is recursive? After all, until now all our recursive sets were sets of numbers (or of tuples of numbers). Well, nothing has changed! Imagine that the symbols in our alphabet (A) above, in precisely the order given, are just (strange) symbols for the numbers 1 through 17. Then any string over the alphabet denotes a number base 18^{§} (if you buy hexadecimal numbers like BBC—i.e., 3004 in decimal—then you have to buy what I have just said). For example, (∃v1v)v1v = 0 denotes (in decimal notation) 33651680537461.

Thus, to speak of a set of strings over (A) is the same as talking about a subset of ℕ.

(ii) We have said right at the beginning that the set of axioms must be “reasonable”, i.e., “recognizable”. That is precisely what item (3) above asks for in stipulating “recursive”. But don’t we want to be able to recognize all the axioms, including the logical ones? Yes, but these do form a recursive (recognizable) set. You can easily check so after you refresh your memory on which are the logical axioms (cf. [Tou98]).

∗As we know from MATH 1090, first order means that we are only allowed to quantify object variables, i.e., write things such as ∃x and ∀x. We are not allowed to write “for some (all) predicates” for example.

†It is easy to do the following: (a) Generate all object variables—what we casually called by the meta names x, y, x′′, z′′′_{104}, etc—by the regular expression v1^{∗}v over {v, 1}. (b) Carefully define syntax of formulas so that the language is context-free. It then follows (cf. COSC 2001)

that the language—the set of all wff—is recursive.

‡A particularly famous choice of axioms is due to Peano—the so-called Peano Arithmetic, for short “PA”. It has axioms that give the behaviour of every nonlogical symbol, plus the induction “axiom schema”:

P (0) ∧ (∀x)(P (x) → P (Sx)) → (∀x)P (x)

The “schema” (or “form”, or “template” in English) gives one axiom for each choice of wff P.

§Why not number the symbols in (A) by 0 through 16 and work base 17? Because we will have trouble with things like ¬0 < 0. The “digit” in the most significant position is (of value)

0 and we lose information as we pass to numerical value. I.e., both ¬0 < 0 and 0 < 0 denote the same number.

Supplementary Lecture Notes, C4111. Fall 2002.\begin{matrix}c \\ ◯ \end{matrix} by George Tourlakis

It is also worth stating that the rules of inference are algorithmically applicable. For example, if we are to use the rules in [GS94], then they are all algorithmic—easily. Take “equanimity”

if A ↔ B and A then B

Whether it applies or not is determined by its form. □

1.2 Lemma. (Informal) The set of all theorems of an axiomatic arithmetic as this has been described in (1)–(5) above is r.e.

Proof. (Informal) Let us add one new symbol, # to the alphabet (A), to form the augmented alphabet

¬, ∨, ∧, →, ↔, =, ∃, ∀, (,), v, 1, 0, S, +, ×, <, #  (B)

We use # as “glue” to concatenate all the formulas in any given proof that we may write. I.e., we explicitly write # once between every pair of consecutive formulas

F_{1}, F_{2}, …, F_{n}

of a proof. We thus convert it to a single string (over (B))

F_{1}#F_{2}# … #F_{n}  (iii)

Giving “digit value” to # equal to 18, we can think of any expression (string) like (iii) above as a number notation base 19.

We now simultaneously and algorithmically generate two lists, L_{1} and L_{2}. L_{1} consists of all strings over (B), enumerated by increasing length and in

each length group lexicographically.

For every string S enumerated thus, we test (algorithmically—being able to tell an axiom from a non axiom helps here!) whether or not it has the form (iii) and is the glued form of a proof. If the test succeeds, then we add to list L_{2} the “tail” of S that follows the rightmost # in S (if S is exactly the sequence in (iii), then the tail is F_{n}).

This process lists algorithmically, under L_{2}, all the theorems of our theory. I.e., the theorem set is r.e. □

Let us call Complete Arithmetic, for short CA, the set

{S : S is a wff that is true when interpreted in 𝔑 as per table on p.1}

We now have:

1.3 Gödel’s First Incompleteness Theorem. \underline{Every} axiomatic system for arithmetic that satisfies (1)–(5) above is incomplete in the sense that its set of theorems cannot equal the set CA.

Proof. In view of the preceding lemma, it suffices to prove that CA is not r.e. To this end, consider the two sets of wffs below:

K̃ = {ϕã(ã) ↑: ϕã(ã) ↑ is true as interpreted in 𝔑}

and

Q = {ϕã(ã) ↑: a ∈ ℕ}  (1)

Before we proceed, let me note that “ϕã(ã) ↑” is an abbreviation of a formula of arithmetic—in other words, it can be written down, in principle, using no more than the symbols from the alphabet (A), and this wff will “formally say”, precisely, ϕ_{a}(a) ↑ (see Appendix).

Thus,

K̃ = \{ϕã(ã) ↑: a ∈ \overline{K}\}  (2)

Now, given any a ∈ ℕ, I can construct the formula ϕã(ã) ↑—or, using a different abbreviation, ¬(∃y)T (ã, ã, y). That is, viewing strings as numbers, the function f that on input a outputs (the number denoted by the string abbreviated by) ϕã(ã) ↑ is, intuitively at least, recursive.

Thus

\overline{K} ≤ K̃  (3)

by (2), since (2) says a ∈ \overline{K} iff f(a) ∈ K̃. On the other hand,

Q = ran(f)  (4)

by (1). Thus, K̃ is not r.e., while Q is r.e.

Note that

CA ∩ Q = K̃

thus CA cannot be r.e. by closure properties. □

Note the emphasized “every” in the theorem. It draws attention to the fact that we have not fixed any particular “reasonable” theory—whatever we said holds for all recursive theories. “Every” moreover implies that every theory that the theorem speaks of misses an infinite chunk of CA. Indeed, if it only misses a finite chunk, C, then adding the formulas of C as axioms we still get a recursive set of axioms (closure properties, and the fact that finite sets are recursive). But this new set covers all of CA (why?) contrary to Gödel’s theorem.

2. Appendix:

ϕã(ã) ↑ is a formula of arithmetic

To show that ϕã(ã) ↑ abbreviates a formula of arithmetic, it suffices to prove that there is a formula of arithmetic that expresses the Kleene predicate T (x, y, z).

2. Appendix: ϕã(ã) ↑ is a formula of arithmetic  5

It will so follow if we can prove that for every function f ∈ PR its graph is expressible arithmetically, for then if c_{T} is the characteristic function of T, c_{T} (x, y, z) = w—and therefore c_{T} (x, y, z) = 0—can be written down as a formula of our language of arithmetic.

To make life easy we add one more binary function symbol to the language— say, “@”—that we interpret as λxy.x^{y}. This will allow us—when the time comes in the present argument—to continue using prime power coding as we have been doing all along.^{¶}

2.1 Lemma. The following relations can be written in our formal language.

1. z = x −^{·} y

2. x | y

3. P r(x)

4. Seq(z)

5. Next(x, y) (meaning x < y are consecutive primes)

6. pow(z, x, y) (meaning x > 1 and y is the highest power of x dividing z)

7. W (z) (meaning z has the form p_{0}p_{1}^{2}p_{2}^{3} ⋯ p_{n}^{n+1} for some n)

8. y = p_{n}

9. z = exp(x, y)

If we keep a keen eye on the task at hand we realize that we do not worry about bounding our quantifications, for it is not our purpose to show these relations in PR_{∗}. Indeed we know from earlier work that they are in this set. This time we want to show that we can express them within our language, which allows us to write down, in the first instance, only the symbols for 0, successor, addition, multiplication, exponentiation (added in this section) and “less than”. We want to show that our language is rich enough to allow us write down a lot of other things, including all of the above.

Proof.

1. z = x −^{·} y: This is expressed by z = 0 ∧ x < y ∨ x = z + y

2. x | y: This is expressed by (∃z)y = xz (we are using “implied multiplication” throughout: “xy” rather than the formally correct “x × y”)

3. P r(x): This is expressed by x > 1 ∧ (∀y)(y | x → y = 1 ∨ y = x)^{∥} 4. Seq(z): This is expressed by

¶Using the so-called Chinese Remainder Theorem of number theory Gödel effected the coding with his “beta function” not needing to add exponentiation to the system.

∥If we wanted to be pedantic we would have written “S0” or ˜1” instead of “1”.

Supplementary Lecture Notes, C4111. Fall 2002.\begin{matrix}c \\ ◯ \end{matrix} by George Tourlakis

z > 1 ∧ (∀x)(∀y)(P r(x) ∧ P r(y) ∧ x < y ∧ y | z → x | z)

5. Next(x, y): This is expressed by

P r(x) ∧ P r(y) ∧ x < y ∧ ¬(∃z)(P r(z) ∧ x < z ∧ z < y)

6. pow(z, x, y): This is expressed by x > 1 ∧ x^{y} | z ∧ ¬x^{y+1} | z^{∗∗}

7. W (z): This is expressed by

Seq(z) ∧ ¬4 | z∧

(∀x)(∀y)(Next(x, y) ∧ y | z → (∃w)(pow(z, x, w) ∧ pow(z, y, w + 1)))

8. y = p_{n}: This is expressed by (∃z)(W (z) ∧ pow(z, y, n + 1))

9. z = exp(x, y): This is expressed by

(∃w)(pow(y, w, z) ∧ w = p_{x})
□

We can now prove the following theorem that concludes the business of this section.

2.2 Theorem. For every f ∈ PR, its graph y = f(x⃗_{n}) is expressible in our language of arithmetic (that now includes—as you recall—a symbol for exponentiation).

Proof. We do induction on PR:

(1) Basis. There are three graphs to worry about here: y = x + 1, y = 0 and y = x (or, fancily, y = x_{i}; or more fancily y = u_{i}^{n}(x⃗_{n})). Clearly, all are expressible in our language (e.g., the first looks somewhat different in the formal notation: y = Sx; the other two look the same whether formally or informally).

(2) Composition. Say, the property is true for the graphs of f, g_{1}, …, g_{n}. This is the induction hypothesis (I.H.)

How about y = f(g_{1}(x⃗_{m}), g_{2}(x⃗_{m}), …, g_{n}(x⃗_{m}))? Well, this graph is expressible as

(∃u_{1}) ⋯ (∃u_{n})(y = f(u⃗_{n}) ∧ u_{1} = g_{1}(x⃗_{m}) ∧ ⋯ ∧ u_{n} = g_{n}(x⃗_{m}))

and we are done by the I.H.

∗∗We wrote “y + 1” rather than the formal “Sy”. By the way, in defining pow we benefitted from the presence of exponentiation.

Supplementary Lecture Notes, C4111. Fall 2002.\begin{matrix}c \\ ◯ \end{matrix} by George Tourlakis

(3) Primitive recursion. This is the part that needs the previous lemma. Here’s why: Assume (I.H.) that the graphs of h and g are expressible, and let f be given for all x, y⃗ by

f(0, y⃗) = h(y⃗)
f(x + 1, y⃗) = g(x, y⃗, f(x, y⃗))

Now, to say z = f(x, y⃗) is equivalent to saying

\begin{aligned}(∃m_{0})(∃m_{1}) & ⋯ (∃m_{x})(m_{0} = h(y⃗) ∧ z = m_{x} \\ & ∧ (∀w)(w < x → m_{w+1} = g(w, y⃗, m_{w}))) \end{aligned}  (i)

The trouble with the “formula” (i) above is that it is not a formula at all, because it has a variable length prefix: (∃m_{0})(∃m_{1}) ⋯ (∃m_{x}). Coding to the rescue! Let us use a single number,^{††}

m = p_{0}^{m_{0}}p_{1}^{m_{1}} ⋯ p_{x}^{m_{x}}

to represent all the m_{i}, for i = 0, …, x. Clearly,

m_{i} = exp(i, m), for i = 0, …, x

We can now rewrite (i) as

(∃m)( exp(0, m) = h(y⃗) ∧ z = exp(x, m)
∧ (∀w)(w < x → exp(w + 1, m) = g(w, y⃗, exp(w, m))))

(ii)

The above is a formula of arithmetic because of the I.H. Some parts of it are a bit cryptic. For example, the part

exp(w + 1, m) = g(w, y⃗, exp(w, m))

can be expressed in more detail as

(∃u)(∃v)(u = exp(w + 1, m) ∧ v = exp(w, m) ∧ u = g(w, y⃗, v))

The above is expressible by the I.H. and the preceding Lemma. This completes the proof. □

††We do not need the more fancy ⟨m_{0}, …, m_{x}⟩ here.

Supplementary Lecture Notes, C4111. Fall 2002.\begin{matrix}c \\ ◯ \end{matrix} by George Tourlakis

8

Supplementary Lecture Notes, C4111. Fall 2002.\begin{matrix}c \\ ◯ \end{matrix} by George Tourlakis

Bibliography

[GS94] David Gries and Fred B. Schneider, A Logical Approach to Discrete Math, Springer-Verlag, New York, 1994.

[Tou98] G. Tourlakis, A basic formal equational predicate logic, Technical Report CS-1998-09, York University, Dept. of Comp. Sci., 1998.