2.34

そのような原始再帰的関数 \(g(x)\) がとれるとする. \(g(x)\) を関数記号としてもっているとし,更に \(T \vdash \forall x (g(x) = 0 \lor g(x) = 1)\) となるとしてよい. 次を満たす \(\Sigma_1\) 文 \(\psi_0\) と \(\psi_1\) をとる: \[ T \vdash \psi_0 \leftrightarrow \exists y({\rm Prf}^\mu({\rm Pr}(\psi_0) \lor {\rm Pr}(\psi_1), y) \land g(y) = 1), \] \[ T \vdash \psi_1 \leftrightarrow \exists y({\rm Prf}^\mu({\rm Pr}(\psi_0) \lor {\rm Pr}(\psi_1), y) \land g(y) = 0). \] \(T \vdash g(x) = 1 \to \neg g(y) = 0\) なので,\(T \vdash \neg \psi_0 \lor \neg \psi_1\) である. \(\psi_0\) と \(\psi_1\) は \(\Sigma_1\) なので, \begin{align*} T \vdash {\rm Prf}^\mu({\rm Pr}(\psi_0) \lor {\rm Pr}(\psi_1), y) \land g(y) = 1 & \to \psi_0 \\ & \to {\rm Pr}(\psi_0)\\ T \vdash {\rm Prf}^\mu({\rm Pr}(\psi_0) \lor {\rm Pr}(\psi_1), y) \land g(y) = 0 & \to \psi_1 \\ & \to {\rm Pr}(\psi_1) \end{align*} である. よって \[ T \vdash \exists y({\rm Prf}^\mu({\rm Pr}(\psi_0) \lor {\rm Pr}(\psi_1), y) \land (g(y) = 0 \lor g(y) = 1)) \to {\rm Pr}(\psi_0) \lor {\rm Pr}(\psi_1) \] である. \(T \vdash \forall y(g(y) = 0 \lor g(y) = 1)\) なので \[ T \vdash \exists y{\rm Prf}^\mu({\rm Pr}(\psi_0) \lor {\rm Pr}(\psi_1), y) \to {\rm Pr}(\psi_0) \lor {\rm Pr}(\psi_1) \] となる. \(T \vdash {\sf PA}\) なので \(T \vdash {\rm Pr}({\rm Pr}(\psi_0) \lor {\rm Pr}(\psi_1)) \to \exists y{\rm Prf}^\mu({\rm Pr}(\psi_0) \lor {\rm Pr}(\psi_1), y)\) だから \[ T \vdash {\rm Pr}({\rm Pr}(\psi_0) \lor {\rm Pr}(\psi_1)) \to {\rm Pr}(\psi_0) \lor {\rm Pr}(\psi_1) \] である. Löb の定理より \(T \vdash {\rm Pr}(\psi_0) \lor {\rm Pr}(\psi_1)\) である.

\(T\) における \({\rm Pr}(\psi_0) \lor {\rm Pr}(\psi_1)\) の最小の証明 \(p\) をとる.

  • \(g(p)=0\) ならば \(g\) の取り方より \(T \vdash \psi_0\) であるが,\(\psi_1\) の取り方より \(T \vdash \psi_1\) となるため \(T \vdash \neg \psi_0 \lor \neg \psi_1\) に反する.
  • \(g(p)=1\) ならば \(g\) の取り方より \(T \vdash \psi_1\) であるが,\(T \vdash \psi_0\) となるためおかしい.

いずれの場合も矛盾する. したがってそのような原始再帰的関数 \(g(x)\) は存在しない.