The Incompleteness Theorem
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 T⊢
F means that F is provable in the
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 ′
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)
- Each expression F in the language of T, can
be quoted, i.e. we can write a closed term tF
of T in the same language, whose value is
the copy [F] of F
in T ′,
- 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 closed
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 closed 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
closed 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).
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
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⊢ (G ⇎ v[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
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 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
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.
Next : Comments on the powerset
or directly : Introduction
to the foundations of geometry
Back to homepage : Set Theory
and Foundations of Mathematics