lob

Two formalizations of Löb's Theorem.

Axiomatic Formalization

In axiomatization/, an axiomatic formalization of Löb's Theorem, based on The Cartoon Guide to Löb's Theorem

Internal Formalization

In internal/, a start on a formalization based on a well-typed quine, started with the help of Benja Fallenstein at the June 2015 MIRI Workshop on Decision Theory.