1.C. Introduction to incompleteness
Existential classesLet 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.
- 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
- 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).
Provability predicatesProvability concepts are linked to existential classes
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 resulting class of theorems is independent of the chosen formal definition for
a sound and complete
concept of proof in first-order logic, i.e. any two of these leading to FOT-formulas
V, V' expressing proof verification for the same theory (defined by
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, for 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). By weak
truth undefinability, C being FOT-invariant must differ from truth :
C(⌜A⌝) ⇎ A for some A.
If T is FOT-sound (C(⌜A⌝) ⇒ A for all A) then for
each A on which C differs from truth, A is T-unprovable
but true, and thus T-undecidable. Thus T is incomplete
(there exist T-undecidable FOT-statements ).
Hence the incompleteness
of second-order logic (1.11). This gets close to, yet does not give, the famous
First incompleteness theorem. Any algorithmically defined and consistent
theory stronger than FOT is incomplete.The gap may be overlooked, as it is a
worse defect for a theory to be FOT-unsound than to be incomplete.
Yet it can be narrowed using our refined version of weak truth undefinability as follows.
Assume T stronger than FOT (i.e. C contains all axioms of FOT, and
thus its theorems). Then for all existential A, and thus for A of the
form C(B) for any B,
A ⇒ (A is FOT-provable) ⇒ C(⌜A⌝)
If T is consistent and decides all C(A) then
C faithfully processes connectives over instances of C (deducing results
from proven values of C, may these be incorrect). So:
literature reports possibilities to prove both incompleteness theorems from the Berry paradox,
but these seem very complicated, beyond the scope of this introduction.)
- If T is complete (C(B)∨C(¬B)) then it
proves its own inconsistency, i.e. C(⌜C(⌜0⌝)⌝).
- If T is FOT-sound, then C coincides with truth on all existential statements,
thus on all C(A). So there exist T-undecidable C(A).
Such C(A) is false but T-irrefutable, i.e.
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).
More concepts of strength
By the perspective given by incompleteness theorems, two other conceptions (definitions)
of the strength order between foundational theories may be considered, usually equivalent
to our definition of 1.A (possible exceptions are out of scope here) :
There can be no ultimate well-described foundational theory : for any FOT-sound one,
adding the statement of its consistency as an axiom gives a "better" one, i.e. stronger and
still FOT-sound (but this is much less efficient in strengthening effect for the added
complexity, than other possible axioms such as those listed in 1.A).
- 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 provability of FOT-soundness, but to express the FOT-soundness of a theory
requires MT or stronger framework due to truth undefinability).
The justifications to accept any strong 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.
As the T-provability of any statement A cannot be T-refuted in any
way, such as any amount of vain search for T-proofs, that means 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 (such as by finding 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
given limits of available computing resources :
As another aspect of the same fact, provability predicates are inexpressible by
bounded formulas (due to truth undefinability, as they are equivalent to truth in the
class of bounded statements).
- No limit to the expectable size of the smallest proof(s) (or example x
such that B(x) for some bounded B) can be systematically
expressed (predicted) just depending on the size of the theorem (or the size of
B, beyond the smallest ones) : 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, to interpret truth over existential
statements (or any T-provability predicate), requires a realistic
view : a use of the actual
infinity of ℕ specifically meant as its standard interpretation (which cannot be
In a kind of paradox, while the completeness theorem is proven by constructing (using actual
infinity) a counter example (model) from the fact of absence of proof, there is no
"inverse construction" which from
the fact about infinities that no system can exist with given properties, would produce any
finite witness that is its proof (which must nevertheless exist).
Instead, analyzing this
construction can reveal that the size (complexity) of a proof roughly
reflects the number of well-chosen elements that must 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 : Introduction aux