形式化された演繹定理
形式化された演繹定理
$ \varphi,\psiは任意の文について，
$ T \vdash \text{Pr}_T(\ulcorner \varphi \urcorner) \leftrightarrow \text{Pr}_{T+\varphi}(\ulcorner \psi \urcorner)
注意
$ TはPeano算術の$ \sf PAの再帰的公理化可能な拡大理論
$ \text{Pr}_T(x)は$ \Sigma_1論理式で，$ \text{Pr}_T(x) := \exists y. \text{Prf}_T(x,y)
$ Tの証明可能性述語．
すなわち，「$ xは証明可能である」
$ \text{Prf}_T(x,y)は「$ yは，$ xをGödel数として持つ論理式$ E_xの証明のGödel数」を表す論理式．
$ \Delta_0論理式．