解釈可能性に関する第二不完全性定理
$ \mathsf S^1_2は有限公理化された表示を選ぶとする． $ Uの表示は$ \Delta^b_1-論理式で与えられているとする．
定理
$ Uを無矛盾な理論とする．このとき，
$ U \not\triangleright\ \mathsf{Q} + \mathsf{Con}_U
Proof.
$ U \triangleright \mathsf{Q} + \mathsf{Con}_Uと仮定する．
$ \mathsf Q + \mathsf{Con}_U \triangleright \mathsf S^1_2 + \mathsf{Con}_Uが存在するので，interpretation $ \pi\colon U \triangleright \mathsf{S}^1_2 + \mathsf{Con}_U が存在する．
このとき，$ \mathsf S^1_2で可証性条件と$ \exists\Sigma^b_1-完全性が証明できるので， D1: $ U \vdash \varphi \implies U \vdash \mathsf{Pr}^\pi_U(\overline{\varphi})
D2: $ U \vdash \mathsf{Pr}^\pi_U(\overline{\varphi \to \psi}) \land \mathsf{Pr}^\pi_U(\overline{\varphi}) \to \mathsf{Pr}^\pi_U(\overline{\psi})
D3': $ U \vdash \mathsf{Pr}^\pi_U(\overline{\varphi}) \to \mathsf{Pr}^\pi_{\mathsf S^1_2}(\overline{\mathsf{Pr}_U(\overline{\varphi})})
不動点定理により$ U \vdash \mathsf G \leftrightarrow \lnot \mathsf{Pr}^\pi_U(\overline{\mathsf G})
このとき$ U \nvdash \mathsf G
$ U \vdash \mathsf Gならば$ U \vdash \lnot\mathsf{Pr}^\pi_U(\overline{\mathsf{G}})
一方 D1 より$ U \vdash \mathsf{Pr}^\pi_U(\overline{\mathsf G})
矛盾
一方$ U \vdash \mathsf{Con}^\pi_U \to \mathsf G
$ U \vdash \lnot \mathsf G \to \lnot \mathsf{Con}^\pi_Uを示せばよい．
$ U \vdash \lnot \mathsf G \to \mathsf{Pr}^\pi_U(\overline{\mathsf G})
$ \to \mathsf{Pr}^\pi_U(\overline{\lnot \mathsf{Pr}^\pi_U(\overline{\mathsf G})})
また
$ U \vdash \lnot \mathsf G \to \mathsf{Pr}^\pi_U(\overline{\mathsf G})
$ \to \mathsf{Pr}^\pi_{\mathsf S^1_2}(\overline{\mathsf{Pr}_U(\overline{\mathsf G})}) D3'より
$ \to \mathsf{Pr}^\pi_U(\overline{\mathsf{Pr}^\pi_U(\overline{G})}) $ \mathsf S^1_2 \vdash \mathsf{Pr}_{\mathsf S^1_2}(\psi) \to \mathsf{Pr}_U(\psi^\pi)より
よってD2より$ U \vdash \lnot \mathsf G \to \lnot \mathsf{Con}^\pi_U．
よって $ U \vdash \mathsf{Con}^\pi_Uより$ U \vdash \mathsf G．矛盾．❏ 系
$ \mathsf Q \nvdash \mathsf{Con}(\mathsf Q)
参考