\(T + {\rm Con}_T\) から \(\neg {\rm Pr}_T(\ulcorner \varphi \urcorner)\) も \(\neg {\rm Pr}_T(\ulcorner \neg \varphi \urcorner)\) も証明できない \(\varphi\)

---

このページは y. さんによる "独立命題かどうかが独立な命題について" の内容に触発されて考えたものです．

---

Artemov による "The provability of consistency" arXiv の p.18 Lemma 4 において証明されている結果の別証明を与える． Artemov の証明は GL の uniform arithmetical completeness theorem を用いたものだが，その適用には十分な算術（\(I\Delta_0 + {\sf exp}\) を含む）と十分な健全性（\(\Sigma_1\)-健全性）がいる． ここでは具体的な不動点を与えることで非常に弱い仮定の下でも主張が成立することを示す．

---

以降では \(T\) を \({\sf Q}\) の再帰的な無矛盾拡大理論とする．

命題.

\(T + {\rm Con}_T\) が無矛盾ならば，ある \(\Pi_1\) 文 \(\varphi\) が存在して，次が成り立つ： \(T + {\rm Con}_T \nvdash \neg {\rm Pr}_T(\ulcorner \varphi \urcorner)\). \(T + {\rm Con}_T \nvdash \neg {\rm Pr}_T(\ulcorner \neg \varphi \urcorner)\).

　

証明.
\(T + {\rm Con}_T\) が無矛盾とする． 不動点定理より \[ {\sf Q} \vdash \varphi \leftrightarrow \forall x({\rm Prf}_{T + {\rm Con}_T}(\ulcorner \neg {\rm Pr}_T(\ulcorner \neg \varphi \urcorner) \urcorner, x) \land \forall y \leq x \neg {\rm Prf}_{T + {\rm Con}_T}(\ulcorner \neg {\rm Pr}_T(\ulcorner \varphi \urcorner) \urcorner, y)) \] を満たす \(\Pi_1\) 文 \(\varphi\) がとれる． いま \(T + {\rm Con}_T \vdash \neg {\rm Pr}_T(\ulcorner \varphi \urcorner)\) もしくは \(T + {\rm Con}_T \vdash \neg {\rm Pr}_T(\ulcorner \neg \varphi \urcorner)\) の少なくとも一方が成立すると仮定し，矛盾を導く． \(p\) を \(T + {\rm Con}_T\) における \(\neg {\rm Pr}_T(\ulcorner \varphi \urcorner)\) か \(\neg {\rm Pr}_T(\ulcorner \neg \varphi \urcorner)\) の証明のコードの中で最小のものとする．

• \(p\) が \(\neg {\rm Pr}_T(\ulcorner \varphi \urcorner)\) の証明のコードの場合，\(q < p\) となる \(q\) は \(\neg {\rm Pr}_T(\ulcorner \neg \varphi \urcorner)\) の証明のコードではないので \[ {\sf Q} \vdash {\rm Prf}_{T + {\rm Con}_T}(\ulcorner \neg {\rm Pr}_T(\ulcorner \varphi \urcorner) \urcorner, \overline{p}) \land \forall x < \overline{p} \neg {\rm Prf}_{T + {\rm Con}_T}(\ulcorner \neg {\rm Pr}_T(\ulcorner \neg \varphi \urcorner) \urcorner, x) \] である．つまり \[ {\sf Q} \vdash \forall x(x \geq \overline{p} \to \exists y \leq x {\rm Prf}_{T + {\rm Con}_T}(\ulcorner \neg {\rm Pr}_T(\ulcorner \varphi \urcorner) \urcorner, y)) \] かつ \[ {\sf Q} \vdash \forall x ({\rm Prf}_{T + {\rm Con}_T}(\ulcorner \neg {\rm Pr}_T(\ulcorner \neg \varphi \urcorner) \urcorner, x) \to x \geq \overline{p}) \] なのでこれらを合わせると \({\sf Q} \vdash \varphi\) を得る． よって \(T \vdash \varphi\) なので \(T \vdash {\rm Pr}_T(\ulcorner \varphi \urcorner)\) である． 一方 \(T + {\rm Con}_T \vdash \neg {\rm Pr}_T(\ulcorner \varphi \urcorner)\) なので \(T + {\rm Con}_T\) の無矛盾性に反する．
• \(p\) が \(\neg {\rm Pr}_T(\ulcorner \neg \varphi \urcorner)\) の証明のコードの場合，\(q < p\) となる \(q\) は \(\neg {\rm Pr}_T(\ulcorner \varphi \urcorner)\) の証明のコードではないので \[ {\sf Q} \vdash {\rm Prf}_{T + {\rm Con}_T}(\ulcorner \neg {\rm Pr}_T(\ulcorner \neg \varphi \urcorner) \urcorner, \overline{p}) \land \forall y \leq \overline{p} \neg {\rm Prf}_{T + {\rm Con}_T}(\ulcorner \neg {\rm Pr}_T(\ulcorner \varphi \urcorner) \urcorner, y) \] である． つまり \({\sf Q} \vdash \neg \varphi\) であり，上の議論と同様に \(T + {\rm Con}_T\) が矛盾するためにおかしい．

したがっていずれの場合も矛盾するので，\(T + {\rm Con}_T\) からは \(\neg {\rm Pr}_T(\ulcorner \varphi \urcorner)\) も \(\neg {\rm Pr}_T(\ulcorner \neg \varphi \urcorner)\) も証明できない．