Kreisel文を用いたLöbの定理の証明
Thm: Löbの定理
任意の文$ \sigmaに対して
$ T \vdash \sigma \iff T \vdash \mathrm{Pr}_T(\overline{\ulcorner \sigma \urcorner}) \to \sigma
$ \impliesは自明．
$ \impliedbyを証明する．
第2不完全性定理を用いても証明することができる(第2不完全性定理からLöbの定理を導く)が，
用いなくても証明出来る．
その場合はKreisel文と呼ばれるものをGödelの不動点補題より構成して考える．
ただし，ここで$ \mathrm{Pr}_T(x)は導出可能性条件を満たすとする．
Def: Kreisel文
任意の文$ \sigmaに対して，$ Kを（$ \sigmaに対しての）$ TのKreisel文という．
$ T \vdash K \leftrightarrow (\mathrm{Pr}_T(\overline{\ulcorner K \urcorner}) \to \sigma)
proof:
warning:後でちゃんと見た所この証明はミスがありました．
正しい証明はWikipediaを参照してください．
SnO2WMaN/lean4-modal-logicにも証明はあります．
1. $ T \vdash \mathrm{Pr}_T(\overline{\ulcorner \sigma \urcorner}) \to \sigmaを仮定する．
2. Kreisel文$ Kとして$ T \vdash K \leftrightarrow (\mathrm{Pr}_T(\overline{\ulcorner K \urcorner}) \to \sigma)をとる．
3. $ Kと導出可能性条件より，$ T \vdash \mathrm{Pr}_T(\overline{\ulcorner K \urcorner}) \to \mathrm{Pr}_T(\overline{\ulcorner \sigma \urcorner})が成り立つ．
i. $ T \vdash \mathrm{Pr}_T(\overline{\ulcorner K \urcorner}) \to \mathrm{Pr}_T(\overline{ \ulcorner \mathrm{Pr}_T(\overline{\ulcorner K \urcorner}) \to \sigma \urcorner})
$ Kと導出可能性条件D1より
$ T \vdash K \implies T \vdash \mathrm{Pr}_T(\overline{\ulcorner K \urcorner})
$ T \vdash \mathrm{Pr}_T(\overline{\ulcorner K \urcorner}) \to \sigma \implies T \vdash \mathrm{Pr}_T(\overline{\ulcorner \mathrm{Pr}_T(\overline{\ulcorner K \urcorner}) \to \sigma \urcorner})
ii. $ T \vdash \mathrm{Pr}_T(\overline{\ulcorner K \urcorner}) \to (\mathrm{Pr}_T(\overline{\ulcorner \mathrm{Pr}_T(\overline{\ulcorner K \urcorner}) \urcorner}) \to \mathrm{Pr}_T(\overline{ \ulcorner \sigma \urcorner}))
iと導出可能性条件D2より
$ T \vdash \mathrm{Pr}_T(\overline{\ulcorner \mathrm{Pr}_T(\overline{\ulcorner K \urcorner}) \to \sigma \urcorner}) \to (\mathrm{Pr}_T(\overline{\ulcorner \mathrm{Pr}_T(\overline{\ulcorner K \urcorner}) \urcorner}) \to \mathrm{Pr}_T(\overline{ \ulcorner \sigma \urcorner}))
iii. $ T \vdash \mathrm{Pr}_T(\overline{\ulcorner K \urcorner}) \to \mathrm{Pr}_T(\overline{\ulcorner \sigma \urcorner})
iiと導出可能性条件D3より
$ T \vdash \mathrm{Pr}_T(\overline{\ulcorner K \urcorner}) \to \mathrm{Pr}_T(\overline{\ulcorner \mathrm{Pr}_T(\overline{\ulcorner K \urcorner}) \urcorner})
4. 1と3より$ T \vdash \mathrm{Pr}_T(\overline{\ulcorner K \urcorner}) \to \sigma
5. 4と$ Kの定義より，$ T \vdash K
6. 5と導出可能性条件D1より$ T \vdash \mathrm{Pr}_T(\overline{\ulcorner K \urcorner})
7. 4と6より$ T \vdash \sigma．
Remark:
証明可能性述語を$ \Boxとして表したほうが証明の見た目が遥かに良い．
実際，新井敏康『数学基礎論』増補版ではそうしている
この証明は数学における証明と真理 様相論理と数学基礎論の行間を補完したものだが，非常にわかりずらかった．
Remark:
見ればわかるが，この証明に置いては導出可能性条件D1~D3を満遍なくフル活用している．
Col: Löbの定理から第2不完全性定理を導く
対偶を示す．
$ T \vdash \mathrm{Con}_Tならば$ Tは矛盾する
$ T \vdash \mathrm{Con}_Tなら$ T \vdash \mathrm{Pr}_T(\overline{\ulcorner \bot \urcorner}) \to \botが成り立つ（なぜなら$ \mathrm{Con}_T \equiv \lnot \mathrm{Pr}_T(\overline{\ulcorner \bot \urcorner})）が，Löbの定理より$ T \vdash \botとなる．よって$ Tは矛盾する．