Formal Arithmetic & Incompleteness

← Back to Domain-Specific Families

Abstractions about the limits and comparative strength of formal arithmetic theories — incompleteness and undefinability results such as the Gödel sentence, Tarski's undefinability theorem, and the Paris–Harrington theorem, and theories calibrated to feasible or self-verifying reasoning like bounded arithmetic and self-verifying theories.

6 abstractions in this family — domain-specific abstractions that sit near one another in structural-signature space (k-means over structural-signature embeddings). Each is shown with its short description.

• Bounded arithmetic — A family of weak arithmetic theories whose bounded quantifiers and restricted induction calibrate feasible reasoning, linking provably total functions and proofs to computational-complexity classes and propositional proof systems.
• Cointerpretability — Compare formal theories by a logic-preserving translation in the reverse language direction that reflects the translated theory's theorems, a dual of interpretability tied to Σ₁-conservativity for suitable arithmetical theories.
• Gödel sentence — The unprovable statement referred to by the theorem is often referred to as "the Gödel sentence" for the system .
• Paris–Harrington theorem — A strengthened finite Ramsey statement that is true in the standard natural numbers but not provable in first-order Peano arithmetic.
• Self-verifying theories — Weak consistent first-order arithmetical systems constructed to prove an internal statement of their own consistency without containing enough arithmetic for Gödel's second incompleteness theorem to apply in its usual form.
• Tarski's undefinability theorem — A limit theorem stating that sufficiently strong consistent formal systems cannot define within themselves the full truth predicate for their standard arithmetic interpretation.