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: 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. Usual existential classes of "theorems" among first-order statements with a given language, are formed in 2 steps:
  1. Give a first-order theory with an existential class of axioms (usual ones, including all theories from our list, even have bounded definitions);
  2. 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.

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: (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⌝) ⇒ ∀AS, ¬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 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 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.

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 : 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.

Set theory and Foundations of Mathematics
1. First foundations of mathematics
1.1. Introduction to the foundations of mathematics
1.2. Variables, sets, functions and operations
1.3. Form of theories: notions,..., meta-objects
1.4. Structures of mathematical systems
1.5. Expressions and definable structures
1.6. Logical connectives
1.7. Classes in set theory
1.8. Binders in set theory
1.9. Axioms and proofs
1.10. Quantifiers
1.11. Second-order quantifiers
Philosophical aspects
1.A. Time in model theory
1.B. Truth undefinability
1.C. Introduction to incompleteness
1.D. Set theory as unified framework
2. Set theory - 3. Algebra - 4. Arithmetic - 5. Second-order foundations
Other languages:
FR : Introduction aux théorèmes d'incomplétude