The Incompleteness Theorem

(the Completeness theorem is on another page)
Previous section : Non-standard models of Arithmetic
[see definitions of «meta» in 1.3., «predicate» and «invariant» in 1.4, and «closed» in 1.6, so here "invariant" will mean "definable"; and Tmeans that F is provable in the theory T]

Self-quotation theorem

The idea is that, in any theory able to describe formulas, any formula will also have the ability to take, as argument, a quotation of itself (this quotation included).

Theorem. Let T a theory able to describe itself, in the sense that it defines in (every one of) its model M an image of itself, thought of as «a theory» T ′ where :

Then, for every expression F of T with a distinguished variable x (ranging over the class of expressions of T' of the same type as F but without x), we can write a closed term X so that, denoting G the expression F(X) (that is F where x is replaced by X), we have T X = tG (in other words, the value of X is [G]). Thus T G = F(tG)

Proof.
Let H(A) be the expression F(A : J(A)) with variable A ranging over the class of expressions of T' with the same type (in T') as F (in T), and thus as H (without specifying the range of their distinguished variable).
Then let X be the term (tH : J(tH)). Thus G, that is F(tH : J(tH)), can also be abbreviated as H(tH). Thus T⊢ ( tH : J(tH) ) = tG  ∎

Note : T ' must contain a copy of T but might be bigger, as it must include formulas with size any number in M, thus with non-standard size if M has non-standard numbers. In this case T ' is not actually a theory, but it still behaves as such from the viewpoint of its description by T.

Truth Undefinability theorem

The Truth Undefinability theorem, by Tarski (see wikipedia article) expresses the impossibility to find, in a founding theory T (such as a set theory), any single formula v with one argument x ranging over the class of closed formulas of the image theory T' as above, that would correctly express the truth of every closed formula X of T, in the sense of satisfying v([X])⇔ X. Thus the values it might invariantly specify, even if they are logically consistent between themselves, would only fit with other models (such as non-standard models), not the one currently used.

Theorem. (With the same assumptions as above on theory T), for any unary predicate v applicable to the image [F] of each closed formula F of T, we can write a closed formula G of T on which v necessarily fails to give the correct value : T⊢ (Gv[G]).

Proof : by the self-quotation theorem, taking for G the formula made of ¬v applied to the quotation of itself ∎
Intuitively, if we read v as meaning "to be true", then G would claim its own falsity, which is absurd. 

Corollary. If M is explicitly built (meta-invariant) determining values of closed formulas F of T (or if M is any model agreeing with specific invariant determinations of these values), then the computation v[F] in M of these values by the same rules (if possible) is incorrect.

Proof. G and v[G] are computed by the same rules but respectively interpreted outside and inside M. As Gv[G], if the outside computation is correct, then the one in M is not. ∎

In particular, the construction in the proof of the Completeness theorem necessarily makes a «wrong choice» at some step. Namely, it is the provability predicate (whether each formula is refutable from previous axioms) used in each step of its construction, that is the weakly defined concept: it is a non-algorithmic operation, differently interpreted between models. Of course it will keep its unique true interpretation as long as the set of natural numbers remains standard. From this we deduce that any model of a founding theory (arithmetic or set theory) obtained by such a construction, necessarily contains non-standard numbers, that modify the first-order properties of the set of natural numbers (with addition and multiplications).
Finally, any construction of a model should be understood as implicitly depending on some (arbitrary) preexisting universe, with its set of natural numbers whose character of "being standard" cannot be defined in the absolute.

The Incompleteness Theorem

Continuing with the assumptions of the Truth Undefinability Theorem, let us present Gödel's 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 closed formula,
1) (T
F) ⇒ (T p[F])
2) (T
¬p[0]) ⇔ (T 0) (Gödel's second incompleteness theorem : no consistent theory can prove its own consistency)
3) (T
p[F] ⇒ F) ⇔ (T F) (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.



Next :  Comments on the powerset axiom
or directly :
Introduction to the foundations of geometry

Back to homepage : Set Theory and Foundations of Mathematics