The Incompleteness Theorem
Previous section : Non-standard
models of Arithmetic
We shall use previously defined concepts of meta (1.3), predicate (1.4), invariant (1.5, i.e. definable),
«ground» (1.8), and the notation T⊢F to mean that F
is provable in T.
The idea is that, in any theory able to describe expressions, any
expression can also take, as an argument designating an expression, 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 ground term X so that, denoting G
the expression F(X) (that is F where x is replaced
by X), we have T⊢ X = tG
(so that the value of X is [G]).
(This implies T⊢ G = F(tG)).
- Each expression F in the language of T, can
be quoted, i.e. we can write a ground term tF
also in the language of T, whose value is the copy [F] of F
- It can describe the quotation process in T ',
by a unary term J of T,
taking argument in some class of expressions of T ', and values in the class of ground terms of T '
: for any expression F we have T⊢
- It can operate formal substitutions (compositions) in T ' : given
a variable A in a class of expressions of T ' with a distinguished free variable,
and u in the class of ground terms of T ', the
operation (A : u) gives the expression in T ' obtained by replacing the variable of A by u. So, for any
unary formula F and
ground term K of T we have T⊢ (tF
: tK) = tF(K).
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).
Note : T ' must contain a copy of T but may
be bigger, as the sizes of its formulas, interpreted by T in M, range over the set playing the role of ℕ there, which may be a non-standard model of arithmetic. In this case T ' is not
actually a theory, but it still behaves as such from the viewpoint
of its description by T.
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)) = (tH : ttH)
Truth Undefinability theorem
The Truth Undefinability theorem, by Tarski (see wikipedia
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
ground formulas of the image theory T' as above, that would
correctly express the truth of every ground 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. Under the above assumptions on theory
T, for any unary predicate v applicable to the image [F]
of each ground formula F of T, we can
write a ground formula G of T on which v
necessarily fails to give the correct value : T⊢ (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 ground 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
G ⇎ v[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
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
Theorem. If T ′ is
built like T which can express the provability p
in T ′, and F is a
1) (T⊢ F) ⇒ (T⊢ p[F])
2) (T⊢ ¬p) ⇔ (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
Contrapositive viewpoint on 1) if T can describe models:
every model of some T ′ is a model
1) The proof of F in T can be copied into T ′, or converted to a proof of existence of a
2) Let T⊢ (G ⇎ p[G]). The proof (T⊢
G) ⇔ (T⊢ G∧p[G]) ⇔ (T⊢
0) formalized in T gives T⊢(p[G]⇔p).
Thus (T⊢ ¬p) ⇔ (T⊢ ¬p[G]) ⇔
(T⊢ G) ⇔ (T⊢ 0).
3) from 2) applied to the theory (T+¬F). Finally
take F=«F is provable», ie T⊢ (F ⇔ p[F]).
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.
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
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.
Back to homepage : Set Theory
and Foundations of Mathematics