2.13

\({\sf Q}\) において \(f\) を define する \(\Sigma_1\) 論理式を \(\delta_f(x, y)\) とする．

を満たす \(\Pi_1\) 文 \(\theta\) をとる．

• いま \(T | f(\theta) \vdash \theta\) と仮定すると \(T \vdash \theta\) である． また \(T \vdash \delta_f(\theta, f(\theta)) \land {\rm Pr}_{T|f(\theta)}(\theta)\) なので \(T \vdash \exists y (\delta_f(\theta, y) \land {\rm Pr}_{T|y}(\theta))\) である． つまり \(T \vdash \neg \theta\) となり矛盾する． したがって \(T | f(\theta) \nvdash \theta\) である．
• 一方 \({\sf PA}\) は essentially reflexive なので \(k > \max\{\neg \theta, f(\theta)\}\) について \(T + \neg \theta \vdash \neg {\rm Pr}_{(T + \neg \theta)|k}(0 = 1)\) である． \(k > \neg \theta\) なので \((T + \neg \theta)|k = (T|k) + \neg \theta\) であり，\(T + \neg \theta \vdash \neg {\rm Pr}_{(T | k) + \neg \theta}(0 = 1)\) となる． つまり \(T + \neg \theta \vdash \neg {\rm Pr}_{T | k}(\theta)\) である． \(k > f(\theta)\) なので \(T + \neg \theta \vdash \neg {\rm Pr}_{T | f(\theta)}(\theta)\) となる． \(T \vdash \forall y(\delta_f(\theta, y) \leftrightarrow y = f(\theta))\) なので \(T + \neg \theta \vdash \theta\)，つまり \(T \vdash \theta\) を得る．

コメント

• \(T\) が \(\Sigma_1\)-健全ならば条件を満たす \(\Sigma_1\) 文 \(\theta\) は存在しない． これは \(\Sigma_1\) 文 \(\theta\) について \(T \vdash \theta\) とすると \(T | k \vdash {\sf Q}\) となる任意の \(k\) について \(T | k \vdash \theta\) となることによる．
• 一方 \(T\) が \(\Sigma_1\)-健全でなければ条件を満たす \(\Sigma_1\) 文 \(\theta\) が次のようにとれる： \(T\) が \(\Sigma_1\)-健全でなければ，\(T \vdash \exists x \xi(x)\) であるが \(\forall x \neg \xi(x)\) が true となるような PR 論理式 \(\xi(x)\) がとれる． \({\sf Q} \vdash \theta \leftrightarrow \exists y(\delta_f(\theta, y) \land \exists x(\xi(x) \land \forall w < x \neg {\rm Prf}_{T|y}(\theta, w)))\) を満たす \(\Sigma_1\) 文 \(\theta\) をとる．
  • \(T | f(\theta) \vdash \theta\) とすると，その証明 \(p\) がとれる． \(T \vdash {\rm Prf}_{T|f(\theta)}(\theta, p)\) かつ \(T \vdash \forall x < p \neg \xi(x)\) なので \(T \vdash \neg \theta\) となるため \(T\) の無矛盾性に反する． したがって \(T | f(\theta) \nvdash \theta\) である．
  • 上で示した方法と同様にして \(T + \neg \theta \vdash \neg {\rm Pr}_{T | f(\theta)}(\theta)\) が成り立つ． \(T \vdash \exists x \xi(x)\) なので \(T + \neg \theta \vdash \exists x(\xi(x) \land \forall w < x \neg {\rm Prf}_{T|f(\theta)}(\theta, w))\) である． つまり \(T + \neg \theta \vdash \theta\) なので \(T \vdash \theta\) となる．