nLab
Löb's theorem

Context

Foundations

The basis of it all

  • ,

Foundational axioms

  • basic constructions:

  • :

  • :

  • :

  • strong axioms

  • further

Removing axioms

Type theory

,

  • ,

    • \vdash ,

(, , , )

  • ,

  • / ()

  • // ()

= + +

/-/
,
of / of
for for hom-tensor adjunction
introduction rule for for hom-tensor adjunction
( of) ( of)
into into
( of) ( of)
, ,
higher
/-//
/
, () ,
(, ) /
(absence of) (absence of)

  • ,

  • ,

    • , ,

  • ,

Contents

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:

(PP)P \Box(\Box P \to P) \to \Box P

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

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

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

  2. consistency means that PP\Box P \to P

(falsefalse)false (¬false)false (¬false)false ¬(¬false) \begin{aligned} & \Box (\Box false \to false) \to \Box false \\ \Leftrightarrow \;\; & \Box ( \not \Box false ) \to \Box false \\ \Rightarrow \;\; & \Box ( \not \Box false ) \to false \\ \Leftrightarrow \;\; & \not \Box ( \not \Box false ) \end{aligned}

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

References

See also

Created on July 8, 2017 at 09:58:37. See the history of this page for a list of all contributions to it.