\[ {\sf PA} \vdash \kappa(x) \leftrightarrow \forall y({\rm Prf}(\kappa(\dot{x}), y) \to \exists z \exists u(\langle z, u \rangle < \langle x, y \rangle \land {\rm Prf}(\kappa(\dot{z}), u)))
\] を満たす \(\Pi_1\) 論理式 \(\kappa(x)\) をとる．
- \({\sf PA} \vdash \kappa(n)\) となる \(n\) があるとすると，\(\langle k, p \rangle = \min \{\langle n, q \rangle : q\) は \({\sf PA}\) における \(\kappa(n)\) の証明\(\}\) がとれる． つまり \({\sf PA} \vdash \kappa(k)\)
であり，一方 \[ {\sf PA} \vdash {\rm Prf}(\kappa(k), p) \land \forall z \forall u (\langle z, u \rangle < \langle k, p \rangle \to \neg {\rm Prf}(\kappa(\dot{z}), u)) \] なので \(\kappa(x)\) の取り方より
\({\sf PA} \vdash \neg \kappa(k)\) となるため矛盾． したがって \({\sf PA} \vdash \kappa(n)\) となる \(n\) はない．
- \(m \neq n\) とする． \[ {\sf PA} \vdash \neg \kappa(m) \to \exists y({\rm Prf}(\kappa(m), y) \land \forall z \forall u(\langle z, u \rangle < \langle m, y \rangle \to \neg {\rm
Prf}(\kappa(\dot{z}), u))) \] であるから， \[ {\sf PA} \vdash \neg \kappa(m) \land {\rm Prf}(\kappa(n), u) \to \exists y({\rm Prf}(\kappa(m), y) \land \langle n, u \rangle \geq \langle m, y \rangle) \]
となる． また \(m \neq n\) なので \(T \vdash \langle n, u \rangle \neq \langle m, y \rangle\) である． したがって \[ {\sf PA} \vdash \neg \kappa(m) \to \forall u ({\rm Prf}(\kappa(n), u) \to \exists x \exists y
(\langle x, y \rangle < \langle n, u \rangle \land {\rm Prf}(\kappa(\dot{x}), y)) \] なので \({\sf PA} \vdash \neg \kappa(m) \to \kappa(n)\) つまり \({\sf PA} \vdash \kappa(m) \lor \kappa(n)\) がいえた．
コメント
更に \({\sf PA} \vdash \forall x \forall y(x \neq y \to \kappa(x) \lor \kappa(y))\) も成り立つ．