3.10. The Incompleteness Theorem

In this section, "arithmetic" will mean the first-order theory of full arithmetic.
The famous incompleteness theorem by Kurt Gödel, comes from finding a way to write a formula saying "This formula is unprovable", then analyzing its status. The resulting paradox affects arithmetic (and thus any theory containing it), as he showed by a very hard work of developing proof theory from it.
Let us focus on the most interesting aspects of this result and its proof, by directly assuming the framework of proof theory in which they are naturally expressed.

Self-quotation theorem

The liar paradox, "This formula is false", uses two a priori dubious elements : Let us show that self-quotation is actually legitimate, as it can anyway be constructed, without assuming it, in any theory able to describe expressions (such as a set theory) : in any expression with a free variable ranging over the notion of expression (as objects), we can replace this variable by a quotation of this expression, this quotation included.
To avoid having multiple copies of "the same expression" among objects, let us assume a formalization generalizing the concept of term algebra, to the use of all needed symbols (with connectives and quantifiers). (Another method would be to work with equivalence classes of expressions, maybe implicitly by only using operations compatible with this equivalence)

Theorem. Let T a theory able to describe itself, in the sense that we can define there (thus find in every model M it may have) a system T ' representing an image of the first 2 levels of T (types, structure symbols, and the notion of expression made of them) in this sense:

Then, for every expression F of T with a distinguished variable x (ranging over expressions of T ' with "the same" list of free variables as F but without x), there is a ground term X so that TX = tF(X).

Proof.
Let H(y) be the expression F(y : J(y)) with variable y ranging over the class of expressions of T ' with the same type (in T ') as F (in T) except for the intended type of their distinguished variable (which will range over expressions with one more variable, but such a difference on the intended type of a variable does not affect the formal processes over expressions using it); and actually the same type as H.
Then let X be the term (tH : J(tH)). Thus F(X), that is F(tH : J(tH)), can also be abbreviated as H(tH).
Thus TX = (tH : ttH) = tF(X)
This is itself a theorem of finitistic mathematics, i.e. refers to a specific method (algorithm), which, given as input the data of some finite systems (expressions, proofs) provides related systems as output after finitely many operations (not unreasonably more than the size of input). Therefore it is valid in the framework of any theory able to describe expressions (such as arithmetic, through Godel's constructions), which may differ (be weaker than) the theory T it may describe (such as a set theory). Next theorems will also be of this kind.

T has non-standard models, that is where the quotation function is not surjective to T '. Non-standard expressions in T ' (those not reached by quotation) are those which either use a non-standard symbol (which may exist if T has an infinity of symbols), or have a non-standard size (which may be defined as the number of occurrences of symbols, with counting defined by T). In this case T ' is not actually a theory, but still looks like one as seen by T.

Truth Undefinability theorem

Now that self-quotation is known to be a legitimate mathematical tool, while logic naturally interprets any contradiction as refuting whatever assumption we started with, the actual lesson from the liar paradox is the Truth Undefinability theorem, by Tarski (see wikipedia article): the impossibility for any formula of T with only 1 free variable, to correctly express the predicate of "truth in the current model" over the class of all ground formulas.

Theorem. Under the above assumptions on theory T, for any invariant unary predicate v with domain the class of ground formulas of T', there is a ground formula G of T on which v necessarily gives the wrong value : TGv(tG).

Proof : by the self-quotation theorem, taking ¬v as F. ∎

Among unary predicates v over all ground formulas, the logically consistent ones, which we can call interpretations, represent classes of models for the relation of elementary equivalence (bijectively if we consider all unary relations disregarding their definability). The truth undefinability theorem implies that any invariant interpretation can only describe a class of models not containing the current one.

In particular, arithmetic cannot express the interpretation of all its own ground formulas in the standard model (the current interpretation, trivially interpreting the object symbols by those of the framework). Namely, while it can interpret by recursion all algebraic terms by a single formula, this cannot be extended to ground formulas with an unlimited number of quantifiers. Still, it can do things the other way round:
  1. define a formal interpretation of all ground formulas of a given consistent theory (assuming its consistency but not adding this assumption as an axiom in this object-theory so assumed to be consistent), and adding one by one to axioms each ground formula consistent with previous ones (like in the proof of the completeness theorem);
  2. then define a model which fits with this interpretation.
Whatever the method, if we can express the truth predicate of all ground formulas of a theory T in a model M, by a formula also expressible in T, then the interpretation of this formula by T in M is necessarily incorrect (defining a different elementary equivalence class of models when tested on a standard formula), as it differs from the supposedly correct first interpretation. Arithmetic can define interpretations of (an image of) its own ground formulas but always different from the standard interpretation, so that the corresponding models are necessarily non-standard.
Somehow, any "construction" of a model depends on the framework of a preexisting universe, with its model of arithmetic whose standardness cannot be defined in the absolute.

First Incompleteness Theorem

As particular cases of arithmetical definitions, algorithms (such as the logical deduction from a consistent list of axioms produced by an algorithm) cannot process the standard interpretation either. Now Gödel's First Incompleteness Theorem says that algorithms can do even less than arithmetic definability:

Theorem. No algorithm can produce any consistent interpretation of all ground formulas of arithmetic.

Here is a proof a bit different (simpler ?) than Gödel's:
An algorithm that stops to decide a formula as true or false (in standard time), will keep its result when interpreted in a non-standard model (the finiteness of its operations keeps it unaffected by non-standard numbers). The contradiction with the truth undefinability theorem refutes the existence of a deciding algorithm. ∎
Thus, the above described kind of arithmetic definition of an interpretation, cannot be reduced to an algorithm, for the following reason. Each step of its "construction" involves a search of a proof (a refutation of a formula from previous axioms); among these searches, will necessarily be endless ones, whose result is differently interpreted between models : an algorithm (here a search for proof) which does not stop in standard time, may be reinterpreted in a non-standard model as stopping (after a non-standard number of operations, finding a proof with non-standard size).

Second Incompleteness Theorem

Continuing with the assumptions of the Truth Undefinability Theorem, let us present Gödel's second incompleteness theorem, according to which whenever T is consistent (which we admitted in this study, since a model of T is used and thus exists) and T is supposed to have the same format (having the image of each axiom of T among its own axioms or at least theorems), then the consistency of T is not provable inside the formalism of T. To make things simple let us express it and sketch its proof in the context of proof theory (assuming the concept of "proof" to be already available):

Theorem. If T ′ is built like T which can express the provability p in T ′, and F is a ground formula,
1) (TF) ⇒ (Tp[F])
2) (T⊢ ¬p[0]) ⇔ (T⊢ 0) (Gödel's second incompleteness theorem : no consistent theory can prove its own consistency)
3) (Tp[F] ⇒ F) ⇔ (TF) (Löb's theorem, from which «This claim is provable» is deduced)

Proofs:
1) The proof of F in T can be copied into T ′, or converted to a proof of existence of a proof.
2) Let T⊢ (Gp[G]). The proof (TG) ⇔ (TGp[G]) ⇔ (T⊢ 0) formalized in T gives T⊢(p[G]⇔p[0]). Thus (T⊢ ¬p[0]) ⇔ (T⊢ ¬p[G]) ⇔ (TG) ⇔ (T⊢ 0).
3) from 2) applied to the theory (TF). Finally take FF is provable», ie T⊢ (F ⇔ p[F]). ∎

Contrapositive viewpoint on 1) if T can describe models: every model of some T ′ is a model of T.
No converse for 1): a proof in T ′, model of proof theory that is «finite» according to T, may actually be infinite and thus no real proof. If a formula F only has infinite «proofs», its provability is undecidable and false: the unfound proofs of F seem to not have been seeked long enough, and models where F is false cannot be reliably built, so «do not always exist». Wherever models of T can be found, some of them cannot find any one of them anymore.

So, while the rules of provability are formally well-defined (as they have been effectively expressed by Gödel in the language of arithmetic), the interpretation of these rules and thus the very question of the provability of some formulas from some specified theory, will remain sometimes undecidable. Because they depend on ℕ (or equivalently, on the concept of finiteness) which admits non-standard models, while "proofs with non-standard length" are not real valid proofs, since an abstract "proof" needs to be of standard length for being valid, but while the notion of standardness seems philosophically clear, it is finally relative from a mathematical viewpoint.

Note on Skolem's paradox

One might object that the countable model made by the construction of the completeness theorem, only simulates a powerset, not of the true ℕ, but of a non-standard model of ℕ. Indeed, the models provided by the precise construction we described in the proof of the Completeness theorem, all contain non-standard natural numbers.

However, the argument of the Skolem's paradox still holds in 2 ways.

On the one hand, by the fact that it is still anyway a countable simulation of the powerset of a countable set : as (inside a fixed model of set theory) bijections between sets provide bijections between their powersets, the oddity of this being lost (thus getting a "powerset" that cannot be the "true" one) when comparing the interpretations of countability between different models, remains intact. We can also consider the correspondance by the embedding of the standard (external) ℕ into the internal (non-standard) one : being externally countable, the internal "P(ℕ)" is insufficient not only to exhaust the external powerset of the internal ℕ, but also (by restriction of the ∈ predicate) that of its (external) subset of standard numbers.

On the other hand, for example, in the framework of set theory with the axiom of choice, there is another construction of a countable model of (the first-order theory of) second-order arithmetic, with the "true" (standard) ℕ but a different (countable) P(ℕ), with an elementary embedding from this model (ℕ, P(ℕ)) to the "true" one.




Previous section : Non-standard models of Arithmetic
Back to homepage : Set Theory and Foundations of Mathematics