導出可能性条件
歴史的経緯
David Hilbert，P. BernaysがD. Hilbert, P. Bernays, "Grundlagen Der Mathematik"で？
Martin H. Löbが見やすく整理したらしい？
定義
再帰的可算な理論$ T，$ Tの証明可能性述語$ \mathrm{Pr}_Tとする．
任意の論理式$ \varphi,\psiについて次の条件D1~D3を導出可能性条件という．
$ \mathbf{D1} \colon T \vdash \varphi$ \implies$ \mathsf{PA} \vdash \mathrm{Pr}_T \left(\ulcorner \varphi \urcorner\right)
導出可能性条件D1
$ \mathbf{D2} \colon \mathsf{PA} \vdash \mathrm{Pr}_T \left( \ulcorner \varphi \to \psi \urcorner \right) \to \left( \mathrm{Pr}_T \left( \ulcorner \varphi \urcorner \right) \to \mathrm{Pr}_T \left(\ulcorner \psi \urcorner \right) \right)
導出可能性条件D2
$ \mathbf{D3} \colon\vdash \mathrm{Pr}_T\left( \ulcorner \varphi \urcorner\right) \to \mathrm{Pr}_T\left(\ulcorner\mathrm{Pr}_T\left({\ulcorner\varphi\urcorner}\right)\urcorner\right)
導出可能性条件D3
定義
$ Tの証明可能性述語$ \mathrm{Pr}_Tが導出可能性条件を全て満たしているとき，$ \mathrm{Pr}_Tは標準的な証明可能性述語という．
注意
形式化されたΣ₁完全性定理
$ \bf \Sigma_1C$ \sigmaが$ \Sigma_1文のとき，$ \mathsf{PA} \vdash \sigma \to \mathrm{Pr}_T(\ulcorner \sigma \urcorner)
とし，D1,D2,Sを満たす$ Tの証明可能性述語を標準的な証明可能性述語という場合もある
Rosser可証性述語について(外部記事)参照．
このとき，$ \mathrm{Pr}_T(x)が$ \Sigma_1論理式であるなら，
$ \text{Pr}_T\left( \ulcorner \varphi \urcorner\right)は$ \Sigma_1文となり，Sより$ \mathrm{Pr}_T\left(\ulcorner\mathrm{Pr}_T\left(\ulcorner\varphi\urcorner\right)\urcorner\right)となる．
すなわちD3が帰結する．
メモ
標準的な証明可能性述語で議論することによってGödelの第2不完全性定理の証明の見通しがかなり良くなる．
Rosser証明可能性述語は3つの導出可能性条件を全て満たすことは出来ない．
導出可能性条件D1,D2,D3を全て満たすRosser証明可能性述語は存在しない
導出可能性条件D2を満たすRosser証明可能性述語が存在する
導出可能性条件D3を満たすRosser証明可能性述語が存在する
したがってRosser証明可能性述語ではGödelの第2不完全性定理が成り立たない．Kreiselの注意
Rosser可証性述語と第2不完全性定理
Rosser可証性述語について(外部記事)などを参考