Rosser 型の \(\Pi_1\) 反映原理について

本稿は次の論文に関連する話題について扱う．

T. Kurahashi, Henkin sentences and local reflection principles for Rosser provability, APAL, 2016.

定義.

\(\Gamma\) を論理式のクラスとする．Rosser 証明可能性述語 \(\mathrm{Pr}_T^R(x)\) について， \(\mathrm{Rfn}_{\Gamma}^R(T) : = \{\mathrm{Pr}_T^R(\ulcorner \varphi \urcorner) \to \varphi \mid \varphi\) は \(\Gamma\) 文\(\}\).

　

背景として，次の Smoryński の結果がある．

事実.

\(\mathbf{PA}\) の無矛盾な再帰的拡大理論 \(T\) に対して以下は同値： \(T\) は \(\Sigma_1\)-健全． \(T + \mathrm{Con}_T\) は \(T\) 上で \(\Sigma_1\)-保存的．

\(T + \mathrm{Rfn}_{\Sigma_1}(T) \vdash \mathrm{Con}_T\) であり，項目2の \(T + \mathrm{Con}_T\) を \(T + \mathrm{Rfn}_{\Sigma_1}(T)\) に置き換えた少し弱い主張も成立する． これに相当するものが Rosser 証明可能性述語についても成立することを上記の論文では示している（Theorem 6.2）．

事実.

\(\mathbf{PA}\) の無矛盾な再帰的拡大理論 \(T\) に対して以下は同値： \(T\) は \(\Sigma_1\)-健全． \(T + \mathrm{Rfn}_{\Sigma_1}^R(T)\) は \(T\) 上で \(\Sigma_1\)-保存的．

\(T\) 上で \(\mathrm{Con}_T\) は \(T + \mathrm{Rfn}_{\Pi_1}(T)\) と同値であるが，Rosser 証明可能性述語の場合は \(\mathrm{Rfn}_{\Pi_1}^R(T)\) が \(\mathrm{Con}_T\) と同値となる場合（Theorem 6.8）とならない場合（Corollary 5.3）がある． また，\(T + \mathrm{Rfn}_{\Sigma_1}^R(T)\) が \(\mathrm{Rfn}_{\Pi_1}^R(T)\) を証明できる場合（Theorem 6.8）とできない場合（Theorem 6.16）があって，これらの状況は \(\mathrm{Pr}_T^R(x)\) の取り方に依存する．

論文では \(\mathrm{Rfn}_{\Pi_1}^R(T)\) に関する \(\Sigma_1\)-保存性について考察していないので，ここにその証明を記しておく．

命題.

\(\mathbf{PA}\) の無矛盾な再帰的拡大理論 \(T\) に対して以下は同値： \(T\) は \(\Sigma_1\)-健全． \(T + \mathrm{Rfn}_{\Pi_1}^R(T)\) は \(T\) 上で \(\Sigma_1\)-保存的．

　

証明.
\((1 \Rightarrow 2)\): \(T + \mathrm{Con}_T \vdash \mathrm{Rfn}_{\Pi_1}^R(T)\) なので，Smoryński の結果より．

\((2 \Rightarrow 1)\): \(\Sigma_1\) 文 \(\varphi\) について \(T \vdash \varphi\) とする． 不動点補題より，次の同値性を満たす \(\Sigma_1\) 文 \(\sigma\) をとる： \[ \mathbf{PA} \vdash \sigma \leftrightarrow \mathrm{Pr}_T(\ulcorner \neg \sigma \urcorner) \preccurlyeq (\varphi \lor \mathrm{Pr}_T(\ulcorner \neg \neg \sigma \urcorner)). \] また \(\Sigma_1\) 文 \(\sigma'\) を \[ (\varphi \lor \mathrm{Pr}_T(\ulcorner \neg \neg \sigma \urcorner)) \prec \mathrm{Pr}_T(\ulcorner \neg \sigma \urcorner) \] とする．

\(\sigma\) の定め方より \(\mathbf{PA} \vdash \sigma \to \mathrm{Pr}_T^R(\ulcorner \neg \sigma \urcorner)\) であり，\(T + \mathrm{Rfn}_{\Pi_1}^R(T) \vdash \mathrm{Pr}_T^R(\ulcorner \neg \sigma \urcorner) \to \neg \sigma\) なので \(T + \mathrm{Rfn}_{\Pi_1}^R(T) \vdash \sigma \to \neg \sigma\)，すなわち \(T + \mathrm{Rfn}_{\Pi_1}^R(T) \vdash \neg \sigma\) である． \(\mathbf{PA} \vdash \varphi \to \sigma \lor \sigma'\) なので \(T \vdash \sigma \lor \sigma'\) であり，\(T + \mathrm{Rfn}_{\Pi_1}^R(T) \vdash \sigma'\) となる． \(\Sigma_1\)-保存性より \(T \vdash \sigma'\) である． 一方 \(\mathbf{PA} \vdash \neg (\sigma \land \sigma')\) なので，\(T \vdash \neg \sigma\) を得る．

\(\mathbb{N} \not \models \varphi\) と仮定して矛盾を導く． ここで \(T\) における \(\neg \sigma\) の証明 \(p\) をとれば，\(T \nvdash \neg \neg \sigma\) なので，仮定と \(\sigma\) の定義より \(\mathbb{N} \models \sigma\) である． \(\Sigma_1\)-完全性より \(T \vdash \sigma\) となり \(T\) の無矛盾性に反する． したがって \(\mathbb{N} \models \varphi\) である．