\(\Pi_1\)-完全な理論

以降では \(T, U\) を \({\sf PA}\) の無矛盾拡大理論とする．

証明.
\(\mathbb{N} \models \pi\) となる任意の \(\Pi_1\) 文 \(\pi\) をとる． \({\sf PA}' \vdash \pi\) となることを示せばよい． \(\pi\) はある \(\Delta_0\) 論理式 \(\delta(x)\) について \(\forall x \delta(x)\) という形であるとしてよい． 不動点定理より \[ {\sf PA} \vdash \psi \leftrightarrow \exists x(\neg \delta(x) \land \forall y \leq x \neg {\rm Prf}_T(\ulcorner \psi \urcorner, y)) \] を満たす \(\Sigma_1\) 文 \(\psi\) がとれる．

• \(T \vdash \psi\) と仮定すると \(T\) における \(\psi\) の証明 \(p\) がとれる．このとき \[ {\sf PA} \vdash \forall x(\overline{p} \leq x \to \exists y \leq x {\rm Prf}_T(\ulcorner \psi \urcorner, y)) \] が成り立つ． \(\mathbb{N} \models \varphi\) なので特に \(\mathbb{N} \models \forall x < \overline{p} \delta(x)\) であるから \({\sf PA} \vdash \forall x < \overline{p} \delta(x)\) となる．すなわち \[ {\sf PA} \vdash \forall x(\neg \delta(x) \to \overline{p} \leq x) \] が成り立つ．したがって \[ {\sf PA} \vdash \forall x(\neg \delta(x) \to \exists y \leq x {\rm Prf}_T(\ulcorner \psi \urcorner, y)) \] つまり \({\sf PA} \vdash \neg \psi\) となるため \(T\) の無矛盾性に反する． 以上より \(T \nvdash \psi\) である．
• \({\sf PA}'\) の定め方より \({\sf PA}' \vdash \neg {\rm Pr}_T(\ulcorner \psi \urcorner)\) である．
• \(\psi\) の取り方より \({\sf PA} \vdash \neg \pi \land \neg {\rm Pr}_T(\ulcorner \psi \urcorner) \to \psi\) である． \(\psi\) は \(\Sigma_1\) なので \({\sf PA} \vdash \psi \to {\rm Pr}_T(\ulcorner \psi \urcorner)\) となるため，\({\sf PA} \vdash \neg \pi \land \neg {\rm Pr}_T(\ulcorner \psi \urcorner) \to {\rm Pr}_T(\ulcorner \psi \urcorner)\) である． したがって \({\sf PA} \vdash \neg {\rm Pr}_T(\ulcorner \psi \urcorner) \to \pi\) である．
• 以上の議論より \({\sf PA}' \vdash \pi\) となることが分かった．

この議論は次のように拡張することができる．

証明.
\(\mathbb{N} \models \pi\) となる \(\Pi_1\) 文 \(\pi\) をとる．\(\pi\) はある \(\Delta_0\) 論理式 \(\delta(x)\) について \(\forall x \delta(x)\) という形をしているといてよい． \[ {\sf PA} \vdash \xi \leftrightarrow \exists x((\neg \delta(x) \lor {\rm Prf}_U(\ulcorner \neg \xi \urcorner, x) \lor {\rm Prf}_T(\ulcorner\neg {\rm Pr}_U(\ulcorner \xi \urcorner) \urcorner, x)) \land \forall y \leq x (\neg {\rm Prf}_U(\ulcorner \xi \urcorner, y) \land \neg {\rm Prf}_T(\ulcorner \neg {\rm Pr}_U(\ulcorner \neg \xi \urcorner) \urcorner, y))) \] となる \(\Sigma_1\) 文 \(\xi\) をとる． \(\Sigma_1\) 文 \(\eta\) を \[ \eta \equiv \exists y(({\rm Prf}_U(\ulcorner \xi \urcorner, y) \lor {\rm Prf}_T(\ulcorner \neg {\rm Pr}_U(\ulcorner \neg \xi \urcorner) \urcorner, y)) \land \forall x < y(\delta(x) \land \neg {\rm Prf}_U(\ulcorner \neg \xi \urcorner, x) \land \neg {\rm Prf}_T(\ulcorner \neg {\rm Pr}_U(\ulcorner \xi \urcorner)\urcorner, x))) \] とする． このとき \({\sf PA} \vdash \neg \xi \lor \neg \eta\), \({\sf PA} \vdash \neg \pi \to \xi \lor \eta\), \({\sf PA} \vdash \neg \pi \to {\rm Pr}_U(\ulcorner \xi \urcorner) \lor {\rm Pr}_U(\ulcorner \eta \urcorner)\) となる． まず初めに \(\xi\) が \(U\) において決定不能であることを示す．

• いま \(U \vdash \xi\) であると仮定すると，\(U\) における \(\xi\) の証明 \(p\) がとれる．このとき \[ {\sf PA} \vdash \forall x(\overline{p} \leq x \to \exists y \leq x ({\rm Prf}_U(\ulcorner \xi \urcorner, y) \lor {\rm Prf}_T(\ulcorner \neg {\rm Pr}_U(\ulcorner \neg \xi \urcorner) \urcorner, y)) \] である． このとき \(U \nvdash \neg \xi\) である． また \(T \vdash {\rm Pr}_U(\ulcorner \xi \urcorner)\) なので \(T \nvdash \neg {\rm Pr}_U(\ulcorner \xi \urcorner)\) であるから，\(\mathbb{N} \models \forall x \delta(x)\) であることを合わせると \[ {\sf PA} \vdash \forall x((\neg \delta(x) \lor {\rm Prf}_T(\ulcorner\neg {\rm Pr}_U(\ulcorner \xi \urcorner) \urcorner, x)) \to \overline{p} \leq x) \] を得る． したがって \[ {\sf PA} \vdash \forall x((\neg \delta(x) \lor {\rm Prf}_T(\ulcorner\neg {\rm Pr}_U(\ulcorner \xi \urcorner) \urcorner, x)) \to \exists y \leq x ({\rm Prf}_U(\ulcorner \xi \urcorner, y) \lor {\rm Prf}_T(\ulcorner \neg {\rm Pr}_U(\ulcorner \neg \xi \urcorner) \urcorner, y)) \] すなわち \({\sf PA} \vdash \neg \xi\) となりおかしい． 以上より \(U \nvdash \xi\) であることが分かった．
• \(U \vdash \neg \xi\) であると仮定すると，\(U \nvdash \xi\) かつ \(T \nvdash \neg {\rm Pr}_U(\ulcorner \neg \xi \urcorner)\) であるから \(\xi\) の取り方より \({\sf PA} \vdash \xi\) となりおかしい． したがって \(U \nvdash \neg \xi\) である.

続いて \(T^* \vdash \pi\) となることを示す．

• \(T \vdash \neg {\rm Pr}_U(\ulcorner \xi \urcorner)\) かつ \(T \nvdash \neg {\rm Pr}_U(\ulcorner \neg \xi \urcorner)\) のとき：\(U \nvdash \xi\) より \(\xi\) の取り方から \({\sf PA} \vdash \xi\) となる． このとき \(T \vdash {\rm Pr}_U(\ulcorner \xi \urcorner)\) となるため矛盾．この場合はあり得ない．
• \(T \nvdash \neg {\rm Pr}_U(\ulcorner \xi \urcorner)\) かつ \(T \vdash \neg {\rm Pr}_U(\ulcorner \neg \xi \urcorner)\) のとき：\(\mathbb{N} \models \pi\) かつ \(U \nvdash \neg \xi\) なので \(\mathbb{N} \models \eta\)，つまり \({\sf PA} \vdash \eta\) であり，\({\sf PA} \vdash \neg \xi\) なので \(U \vdash {\rm Pr}_U(\ulcorner \neg \xi \urcorner)\) となり矛盾．この場合もあり得ない．
• \(T \vdash \neg {\rm Pr}_U(\ulcorner \xi \urcorner)\) かつ \(T \vdash \neg {\rm Pr}_U(\ulcorner \neg \xi \urcorner)\) のとき：\({\sf PA} \vdash {\rm Pr}_U(\ulcorner \eta \urcorner) \to {\rm Pr}_U(\ulcorner \neg \xi \urcorner)\) なので \(T \vdash \neg {\rm Pr}_U(\ulcorner \eta \urcorner)\) である． また \({\sf PA} \vdash \neg \pi \to {\rm Pr}_U(\ulcorner \xi \urcorner) \lor {\rm Pr}_U(\ulcorner \eta \urcorner)\) なので \(T \vdash \pi\) となる． \(T \subseteq T^*\) なので \(T^* \vdash \pi\).
• \(T \nvdash \neg {\rm Pr}_U(\ulcorner \xi \urcorner)\) かつ \(T \nvdash \neg {\rm Pr}_U(\ulcorner \neg \xi \urcorner)\) のとき：\(U \nvdash \xi\) かつ \(U \nvdash \neg \xi\) なので \(T^*\) の定め方から \(T^* \vdash \neg {\rm Pr}_U(\ulcorner \xi \urcorner)\) となる． またこのとき \(T \nvdash \neg {\rm Pr}_U(\ulcorner \neg \xi \urcorner)\) かつ \(T \nvdash \neg {\rm Pr}_U(\ulcorner \neg \neg \xi \urcorner)\) でもあるので \(T^* \vdash \neg {\rm Pr}_U(\ulcorner \neg \xi \urcorner)\). したがって \(T^* \vdash \neg {\rm Pr}_U(\ulcorner \xi \urcorner) \land \neg {\rm Pr}_U(\ulcorner \eta \urcorner)\) であり，\(T^* \vdash \pi\) となる．

2018/05/31