Löbの定理
参考文献
https://ncatlab.org/nlab/show/Löb's+theorem
数学における証明と真理 様相論理と数学基礎論及び数学における証明と真理 第2部メモ
表記
$ TはPeano算術の拡大理論とする．
導出可能性条件が成り立つ証明可能性述語$ \mathrm{Pr}_T(x)とする．
定理: Löbの定理
以下は同値．
1. $ T \vdash \varphi
2. $ T \vdash \mathrm{Pr}_T(\ulcorner \varphi \urcorner) \to \varphi
定理: 形式化されたLöbの定理
$ \mathsf{PA} \vdash \mathrm{Pr}_T \left({\ulcorner \mathrm{Pr}_T \left({\ulcorner \varphi \urcorner}\right) \to \varphi \urcorner}\right) \to \mathrm{Pr}_T \left({\ulcorner \varphi \urcorner}\right)
様相論理GL
様相論理の$ \Boxを$ Tでの証明可能性として解釈する．
すなわち$ \Box \varphiを$ T \vdash \mathrm{Pr}_T\left({\ulcorner \varphi \urcorner}\right)として解釈する．
形式化されたLöbの定理は論理式$ \Box(\Box \varphi \to \varphi) \to \varphiとして解釈することが出来る．
公理$ \mathsf{L} \equiv \Box(\Box \varphi \to \varphi) \to \varphiを$ \mathbf{K}に付け加えたものを様相論理GLと呼ぶ．