1.C. Introduction to incompleteness
Existential classes
Let 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:
- 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).
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.
Provability predicates
Provability concepts are linked to existential classes
as follows.
- 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.
Usual existential classes of "theorems" among first-order statements with a given
language, are formed in 2 steps:
- 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.
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
symbols τ,
L, X), they give the same theorems :
FOT (+ symbols τ, L, X
with axioms)
⊢ ∀s, (∃p, V(p,s)) ⇔ (∃p,
V'(p,s))
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.
A theory T stronger than FOT will be qualified as FOT-sound if, on the
class of FOT-statements, T-provability implies truth (in the standard model of FOT).
The diversity of non-standard models
Beyond the simple fact of existence of models, the diverse ways to construct them
and their use cases (theories) will provide a diversity of models, including
non-standard models of foundational theories, more or less similar to standard ones.
Even with identical first-order properties (a condition we can adopt by taking as
"axioms" all true statements from a given model, while this is not TT-invariant
for standard models of theories containing TT),
models can differ by meta-level properties : this will be seen
for arithmetic in 4.9,
and for any theory with an infinite model by the Löwenheim-Skolem theorem.
But truth undefinability implies that some constructed models also differ from the
standard one by first-order properties, because of their invariance.
This still goes for "almost complete" foundational theories (e.g.
approaching a complete
second-order theory by second-order universal elimination).
All foundational theories being FOT-invariant, have models with FOT-invariant
properties, thus non-standard already on FOT-properties.
Any consistent MT-invariant T stronger than MT, has MT-invariant,
MT-interpretable models (in particular, any FOT-invariant model is MT-interpretable),
thus with a non-standard class of MT-properties (once a
concept of "standard model of MT" would be clarified...). Now if T is FOT-sound,
adding all true FOT-statements to axioms still forms a consistent and MT-invariant
theory, giving models of T with the standard class of FOT-properties despite
non-standard other MT-properties (and a most likely non-standard FOT-model).
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
(leaving undecidable some 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:
- 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.
(The
literature reports possibilities to prove both incompleteness theorems from the Berry paradox,
but these seem very complicated, beyond the scope of this introduction.)
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
summed up
by the case A=⌜0⌝, namely C(⌜¬C(⌜0⌝)⌝) ⇒ C(⌜0⌝)
i.e. the consistency of T, if true, is T-unprovable.
Rephrasing this
by completeness, if T has no standard contradiction then it has a model which contains
a non-standard contradiction (and thus contains 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).
Proving times
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 :
- 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
speed-up theorem).
- 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).
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).
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
completely axiomatized).
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.
Other languages:
FR : Introduction aux
théorèmes d'incomplétude