,
basic constructions:
:
:
:
strong axioms
further
,
,
(, , , )
,
/ ()
// ()
= + +
/ | -/ | |
, | ||
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) | |
,
,
, ,
,
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 P$
Where the last line reads in words “It is not provable that false is not provable.”
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
Created on July 8, 2017 at 09:58:37. See the history of this page for a list of all contributions to it.