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

- 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(∃ for some*p*,*V*(*p*,*s*))*V*(*p*,*s*) meaning that*p*is a valid proof of*s*.

- 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*
with axioms)
⊢ ∀*s*, (∃*p*, *V*(*p*,*s*)) ⇔ (∃*p*,
*V'*(*p*,*s*))

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.

If

**First incompleteness theorem.** Any algorithmically defined and consistent
theory stronger than FOT is incomplete.

Assume

*A* ⇒ (*A* is FOT-provable) ⇒ *C*(⌜*A*⌝)

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

¬*C*(⌜0⌝) ⇒ ∀*A*∈*S*, ¬*C*(⌜¬*C*⌝:*A*)

Rephrasing this by completeness, if

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

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

Any FOT-sound foundational theory (as a knowledge criterion) will always leave some existential 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 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).

Intuitively, to interpret truth over existential statements (or any

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 théorèmes d'incomplétude