1.C. Introduction to incompleteness
The hierarchy of formulas
The facts of truth undefinability, undecidability or other indefiniteness of
formulas can be understood by analysing their syntax, as mainly coming from their use of binders:
the most definite formulas are those without binder ; then, intuitively, the definiteness
of a given binder is a matter of how set-like its range is. In set theories,
(ranging over the universe or a class) are less definite than bounded quantifiers
and other binders whose range is a set.
For FST, the essential condition for a class to be a set is finiteness. Similarly
in arithmetic, quantifiers can be bounded using the order : (∃x<k, )
and (∀x<k, ) respectively abbreviate (∃x,
x<k ∧ ) and (∀x, x<k ⇒ ) and the same for ≤.
The proofs of the truth undefinability theorems, explicitly giving some A on which
any C differs from truth, prove more than their mere conclusions: they somehow
specify the extent of this difference. Namely, A needs no more quantifier of any
kind than C, in this sense :
The values of bounded statements of FOTs, are independent of the model as their
interpretation only involves standard objects.
Any standard object of a FOT has all the same bounded properties (= expressed by
bounded formulas with no other free variable) in any model.
This equivalence is done by developing some FOT-bounded quantifiers, thus with finite
ranges ; its proof only uses axioms of TT, though C can use a broader language.
Therefore if C is definite on the whole class of statements of T, is constant along
TT-provably equivalent statements and faithfully interprets connectives over instances of C,
then ∃B∈S, C(⌜B⌝) ⇎ C(⌜C(⌜B⌝)⌝), i.e.
C differs from truth on C(⌜B⌝).
- the strong version just lets A be ¬C with
argument replaced by an explicit ground term (without binder but quite complex);
the Berry paradox shows
the existence of some A among formulas which are TT-provably equivalent to big
connectives over instances of C applied to diverse such terms (but simpler).
So any bounded C differs from truth on some bounded A. In FOTs this
is quite a bad difference, but not surprising by lack of bounded candidate truth-approaching
C to think of.
Existential classes and provabilityLet us qualify a formula as existential
if written ∃x, A(x), with an open ∃ as root (or several, which can
be re-expressed as one) followed by a bounded formula A. In this section this
will be meant in FOTs only. Existential statements amount to halting conditions of
algorithms processed by abstract "computers" with unlimited resources:
Similarly, an existential class of a FOT, i.e. defined by an existential formula ∃y,
A(y,x), can be equivalently qualified as algorithmically defined, i.e.
the range of all outputs given on the way by an endlessly
running algorithm; it defines truth over the existential
statements obtained from it by replacing x by any quote. This is linked to provability as follows.
- Any such ∃x, A(x) is equivalent to the halting of an algorithm that
enumerates all x, interprets A on each, and stops when it finds A true there;
- The halting condition of any algorithm is an existential statement
∃t, A(t) where A(t) says it halts at time t
(details are of course much more complex).
Usual existential classes of "theorems" among first-order statements with a given language, are formed in 2 steps:
- The truth of an existential statement (∃x, A(x)) implies
its FOT-provability (by existential
introduction over the quote of x), so both are equivalent;
- Any effective concept of theorem (class of provable statements s) of any
theory in any framework, must be an existential class (∃p,
V(p,s)) for some V(p,s) meaning that p is a valid
proof of s.
The provability formula (∃p, V(p,s)) from the second step
is independent of the chosen definition for a sound and complete concept of
proof in first-order logic, in the sense that any two of these leading to FOT-formulas
V, V' encoding proof verification for the same theory (defined by symbols τ, L, X),
they give the same theorems :
- Give a first-order theory with an existential class of axioms (usual ones, including all
theories from our list,
even have bounded definitions);
- Apply there the concept of proof of first-order logic.
FOT (+ symbols τ, L, X
⊢ ∀s, (∃p, V(p,s)) ⇔ (∃p,
As the first step defines τ, L, X in FOT, it simplifies the above as FOT ⊢ ...
Conversely, if C is an existential class of "theorems" among first-order
statements of a theory, and contains the first-order logical consequences of any
conjunction of its elements (intuitively, the proving framework contains the power of
first-order logic), then C is the class of T-provable statements
by first-order logic from some algorithmically defined first-order theory T :
at least trivially, the theory which takes C as its class of axioms.
First incompleteness theorem
Let C be a class of "T-provable" FOT-statements for an algorithmically
defined theory T able to express these (i.e. C is an existential class of FOT-statements
containing the first-order logical consequences of any conjunction of its elements). Further assume T stronger than
FOT (i.e. C contains all axioms of FOT, and thus its theorems).
Then for all existential A,
A ⇒ (A is FOT-provable) ⇒ C(⌜A⌝)
while the FOT-soundness of T means the converse (C(⌜A⌝) ⇒ A for all A).
By weak truth undefinability,
C being existential must differ from truth. If moreover T is FOT-sound,
then each case of difference is a case of T-undecidability, so that T is
incomplete (it leaves some statements undecidable).
Hence the incompleteness
of second-order logic (1.11). This approaches, yet does not give, the famous
First incompleteness theorem. Any algorithmically defined and consistent
theory stronger than FOT is incomplete.
Now by the proof by the Berry paradox, if T is FOT-sound then there exists a
connective over instances of C with diverse arguments, whose value is T-unprovable.
The value of a connective being deducible from the known values of its arguments, some A
must make C(A) undecidable. As C is existential, all its True values (1) are provable,
thus some False value (0) must be unprovable. So some FOT-statement A
must exist letting C(A) false but T-irrefutable; in other words,
A is T-unprovable but this unprovability is itself T-unprovable.
Second incompleteness theorem
The second incompleteness theorem (whose proof uses the strong
version of truth undefinability) says C(A) is T-irrefutable for all
statements A just if T is consistent :
¬C(⌜0⌝) ⇒ ∀A∈S, ¬C(⌜¬C⌝:A)
where the colon ( : ) means substitution between described expressions so that (⌜B⌝:⌜a⌝)
= ⌜B(a)⌝. This is
by the case A=0, namely C(⌜¬C(⌜0⌝)⌝) ⇒ C(⌜0⌝)
i.e. the consistency of T, if true, is T-unprovable.
by completeness, if T has no standard contradiction then it has a model containing
a non-standard contradiction (and thus no verifiable model).
Also equivalently, T cannot prove the existence of any truth predicate over a
notion it describes as the set of its own statements. This is somehow explained,
though not directly implied, by weak truth undefinability, which prevents using the
current model as an example, since the truth over all standard statements there
cannot be T-defined as any invariant predicate (not even speculatively i.e.
only working in some models).
So, any amount of resources spent seeking T-proofs of a statement A
in vain, remains unable to T-refute the T-provability of A, i.e.
T keeps "seeing a chance" for A to be T-provable by longer proofs.
A theory T' strictly stronger than T can refute the T-provability of some
A (namely by using a T-refutation of A) but remains indecisive on others (such
as A = the inconsistency of T').
Any FOT-sound foundational theory (as a knowledge criterion) will always leave some
existential statements practically undecidable, may they be
actually true or false, the search for proof or refutation appearing vain within any given
limits of available computing resources :
As another aspect of the same fact, provability predicates cannot be equivalent to
any bounded formula (due to truth undefinability, as they are equivalent to truth in the class of
No systematic prediction of a limit to the expectable size of the smallest proof(s) of any statement
can be expressed as directly measurable from its form (such as its size) :
such proofs may be too big to be stored in our galaxy, or even indescribably big.
(An example of statement expected to require a very big proof is given as object of Gödel's
- Undecidable (thus false) existential statements (∃x, A(x)) only have
non-standard examples of x such that A(x); but
these look very similar to the true case, as non-standard objects are precisely those appearing
"indescribably big" in the non-standard model containing them (just extending the
range of meant "describable sizes" to all standard ones).
Intuitively speaking, to interpret (see as definite) any provability predicate (equivalently,
the truth predicate over existential statements) requires a realistic view : a use
of the actual infinity of ℕ specifically
meant as its standard interpretation (which cannot be completely axiomatized).
In a kind of paradox, while the completeness theorem is proven by an abstract
construction taking the fact of absence of proof and using actual infinity to produce
a counter example (model), there is no "inverse construction" which from the fact about
infinities that no system exists with given properties, would produce any finite witness that is its
proof (which must nevertheless exist).
Instead, analyzing the proof of the completeness
theorem, it appears that the minimal size (complexity) of proofs of any theorem, roughly
reflects the number of well-chosen elements that need to be described in an attempted
construction of a counter-example, to discover the necessary failure of such a construction ;
the chosen formalization of proof theory can only affect the size of proofs in more
moderate (describable) proportions.
More concepts of strength
In the resulting perspective on the foundations of mathematics, 2 other concepts of
strength order between foundational theories may be considered (their properties remain
to be specified...) :
There can be no ultimate well-described foundational theory : for any FOT-sound one, adding
the statement of its consistency as axiom gives a "better" one, i.e. stronger and still FOT-sound
(and much more efficient ways to strengthen a theory with respect to complexity are possible).
- The deducibility (provable implication) between consistency statements:
T' is stronger than T if the consistency of T is deducible
from the consistency of T'; then T' is called strictly stronger than
T if the consistency of T is a theorem of T' ;
- The inclusion order between classes of theorems among statements of FOT (this
is related to the issue of proof of FOT-soundness, but to express the FOT-soundness of a theory
requires a stronger framework such as MT due to truth undefinability).
The justifications to accept any theory (version of set theory) as a valid (sound) foundation
of mathematics must remain somewhat philosophical as they cannot be completely
formalized as a proof.
FR : Introduction aux théorèmes d'incomplétude