basic constructions:
strong axioms
further
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
Löb’s theorem in its original form is a generalization of the Gödel incompleteness theorem whose formulation lends itself to the tools of type theory and modal logic.
Löb’s theorem states that to prove that a proposition is provable, it is sufficient to prove the proposition under the assumption that it is provable. Since the Curry-Howard isomorphism identifies formal proofs with abstract syntax trees of programs; Löb’s theorem implies, for total languages which validate it, that self-interpreters are impossible. (Gross-Gallagher-Fallenstein 16)
In provability logic the abstract statement is considered in itself as an axiom on a modal operator $\Box$ interpreted as the modality “is provable”. In this form the statement reads formally:
for any proposition $P$ (“Löb’s axiom”).
This reduces to an incompleteness theorem when taking $P =$ false and using that
negation is $\not P = (P \to false)$;
consistency means that $\Box P \to \not \Box \not P$
Where the last line reads in words “It is not provable that false is not provable.”
A variant of the Löb axiom is used in guarded recursion and synthetic guarded domain theory, which uses a modality $\blacktriangleright$, usually pronounced “later”. Then the Löb induction axiom is for any proposition $P$,
In a setting with the principle of unique choice, this can be used to prove the existence of all guarded fixed points.
Note that the assumptions about the later modality $\blacktriangleright$ are usually quite different from the provability modality $\Box$. For instance, $\Box$ is usually assumed to have some subset of the properties of a comonadic modality, but $\blacktriangleright$ typically satisfies $P \to \blacktriangleright P$.
Jason Gross, Jack Gallagher, Benya Fallenstein, Löb’s theorem – A functional pearl of dependently typed quining, 2016 (pdf)
Neelakantan Krishnaswami, Löb’s theorem is (almost) the Y-combinator, 2016
Jason Gross, MO comment on incompletenss theorems in type theory, 2017
See also
Unified proof of Löb's theorem and Gödel's second incompleteness theorem via essentially algebraic theories, modal logic and arithmetic universes:
Last revised on November 4, 2023 at 15:11:32. See the history of this page for a list of all contributions to it.