nLab Löb's theorem

Idea

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:

$$\Box(\Box P \to P) \to \Box P$$

for any proposition $P$ (“Löb’s axiom”).

This reduces to an incompleteness theorem when taking $P =$ false and using that

1. negation is $\not P = (P \to false)$;

2. consistency means that $\Box P \to \not \Box \not P$

$$\begin{aligned} & \Box (\Box false \to false) \to \Box false \\ \Rightarrow \;\; & \Box ( \not \Box false ) \to \Box false \\ \Rightarrow \;\; & \Box ( \not \Box false ) \to \not \Box \not false \\ \Rightarrow \;\; & \Box ( \not \Box false ) \to false \\ \Rightarrow \;\; & \not \Box \not \Box false \end{aligned}$$

Where the last line reads in words “It is not provable that false is not provable.”

Guarded Recursion Variant

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$,

$$(\blacktriangleright P \to P) \to 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$.

Related concepts

• fixed-point combinator

• Lawvere's fixed point theorem

• guarded recursion

• synthetic guarded domain theory

References

• 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

• Wikipedia, Löb’s theorem