1.C. Introduction to incompleteness
Existential classes and provabilityLet us qualify a formula as existential
if it is made of an open ∃ as root, followed by a bounded formula.
This section will implicitly only qualify as such those of FST or equivalent theories.
Existential statements are essentially the same as
halting conditions of
algorithms (processed by an abstract "computer" with unlimited available time and resources):
Similarly, an existential class of FST, defined by an existential formula
∃y, A(y,x) without parameter, is the range of all outputs x from a
given algorithm (which may run endlessly while giving outputs on the way, ignoring the order); it
can also be seen as a copy of the truth predicate over a specific range of existential statements.
This is linked to provability in both ways.
- Any existential statement ∃x, A(x) is the halting condition of an algorithm
that enumerates every x, interprets A over each, and stops when it finds A
- The halting condition of any algorithm is expressible as an existential statement
∃t, A(t) where, roughly speaking (details are of course more complex),
A claims that this algorithm will halt at time t.
Usual concepts of proof, leading to an existential class of theorems, are formed in 2 steps:
- The truth of an existential statement (∃x, A(x)), implies
its FST-provability, by existential
introduction over the quote of x, and thus also implies its truth in non-standard models;
while the converse holds (FST-provability ⇒ truth).
- Any effective concept of theorem, i.e. class of provable statements s by any specified theory
with its logical framework, must be an existential class (∃p, V(p,s))
where the bounded formula V expresses (in a possibly encoded way) that
p is a valid proof of s.
While the exact expression of this provability formula (∃p, V(p,s)) involves
a formal definition of proof in first-order logic, it is independent of the chosen sound and complete
way to define it, in the sense that all such formulas V, V' encoding (in FST or
equivalent) the verification of proofs for the same (other) theory (defined by symbols t,l,a),
are provably equivalent to each other:
- Give a first-order theory whose class of axioms is defined in TT without parameter
nor open quantifier, as is the case for all theories from
our list (but an
existential class of axioms would fit too ; each axiom may of course use open quantifiers);
- Apply the concept of proof of first-order logic to this theory.
FST (+ symbols t,l,a
⊢ ∀s, (∃p, V(p,s)) ⇔ (∃p,
First incompleteness theorem
Any existential class C of statements of FST including the axioms of FST and
stable by logical deduction, can be seen as a class of theorems of some theory T
containing FST and describable by it (a T-provability predicate) :
at least the theory T defined as FST but with C as its class of axioms, fits.
Let us call such a T FST-sound if all its theorems among statements of FST
are true in its standard model
(this is traditionally called arithmetical soundness).
In this case T-provability is equivalent to truth for all existential statements
(truth ⇒ FST-provability ⇒ T-provability ⇒ truth).
Gödel's first incompleteness theorem comes by applying the weak truth undefinability
theorem for FST (and thus the equivalent theory Z1), to these existential
classes C : while remarkably approaching truth, they still cannot coincide with it.
Hence the incompleteness of second-order logic announced in 1.11.
Now by the proof by the Berry paradox, if T is FST-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 X
must make C(X) undecidable. Since all its True (1) values are provable,
some False (0) value must be unprovable. So there must exist a statement X of FST
such that C(X) is false but T-irrefutable; in other words,
X is T-unprovable but this unprovability is itself T-unprovable.
Second incompleteness theorem
Using the strong truth undefinability theorem, the second incompleteness theorem
will extend the above result to all statements X of FST :
¬C(0) ⇒ ∀X∈S, ¬C("¬C":X)
where : interprets substitution ("A":"x" = "A(x)"), i.e. if
T is consistent then every C(X) is T-irrefutable, may
it be true or false. This is
summed up by the
case X=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 non-standard model containing a non-standard contradiction (and thus not containing
This can be compared to truth undefinability as follows. For any theory describing a
notion representing that of its own statements, truth undefinability says it cannot
(even speculatively i.e. only working in some models) define without parameter
the truth predicate of interpretation in the current model; second incompleteness means that it
cannot prove the existence of any (consistent) truth predicate
(while this existence is provably equivalent to the consistency of the theory).
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 FST-sound one, adding
the statement of its consistency as axiom gives a "better" one, i.e. stronger and still FST-sound
(and much more efficient ways to strengthen a theory with respect to complexity are possible).
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.
- 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 FST (this
is related to the issue of proof of FST-soundness, but to express the FST-soundness of a theory
requires a stronger framework such as MT due to truth undefinability).
The time of proving
So, any amount of resources spent seeking T-proofs of a statement X
in vain, remains unable to T-refute the T-provability of X, i.e.
T keeps "seeing a chance" for X to be T-provable by longer proofs.
A theory T' strictly stronger than T can refute the T-provability of some
X (namely by using a T-refutation of X) but remains indecisive on others (such
as X = the inconsistency of T').
Any FST-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.
FR : Temps en
théorie des modèles