無矛盾性を表す文のとり方について
Introduction
すなわち$ T \vdash \mathrm{Con}_Tとなるケースがある．
原始再帰的関数
$ \mathrm{Fml}(x): $ E_xは論理式
$ \mathrm{Sent}(x): $ E_xは文
$ \mathrm{\Sigma_1Fml}(x): $ E_xは$ \Sigma_1論理式
$ \mathrm{Con}^\mathrm{L}_\Phi \equiv \lnot\Phi(\ulcorner 0 = 1 \urcorner)
$ 0 = 1の部分は算術的におかしな$ \Sigma_1文を適当に入れれば良い．$ 0 \neq 0とかでも良い．
$ T \nvdash 0 = 1
$ \mathrm{Con}^\mathrm{HB}_\Phi \equiv \forall_x\lbrack \mathrm{Fml}(x) \land \Phi(x) \to \lnot\Phi(\dot{\lnot}x) \rbrack
ただし$ \dot\lnot(x)は$ \ulcorner \lnot E_x \urcornerを計算する原始再帰関数による項とする．
任意の論理式に対し，$ T \vdash \varphiならば$ T \nvdash \lnot \varphi．
証明可能なら反証不能．
$ \mathrm{Con}^\mathrm{G}_\Phi \equiv \exists_x \lbrack \mathrm{Fml}(x) \land \lnot\Phi(x) \rbrack
$ T \nvdash \varphiな論理式$ \varphiが存在する．
$ \mathrm{Con}^{\Sigma_1}_\Phi \equiv \exists_x\lbrack \mathrm{\Sigma_1Fml}(x) \land \mathrm{Sent}(x) \land \lnot\Phi(x) \rbrack
Figure:
https://gyazo.com/1bcaa8d3c913152853aaf00ed12f70d1
1. $ \Phiが導出可能性条件$ \bf D1を満たすとき，$ \mathsf{PA} \vdash \mathrm{Con}^\mathrm{HB}_\Phi \to \mathrm{Con}^\mathrm{L}_\Phi
proof:
$ \mathsf{PA} \vdash 0 \neq 1なので$ \bf D1より$ S \vdash \Phi(\ulcorner 0 \neq 1 \urcorner)
$ \mathsf{PA} \vdash \mathrm{Con}^\mathrm{HB}_\Phi \to (\Phi(\ulcorner 0 \neq 1 \urcorner) \to \lnot\Phi(\ulcorner 0 = 1 \urcorner))
よって$ \mathsf{PA} \vdash \mathrm{Con}^\mathrm{HB}_\Phi \to \mathrm{Con}^\mathrm{L}_\Phi
2. $ \mathsf{PA} \vdash \mathrm{Con}^\mathrm{L}_\Phi \to \mathrm{Con}^{\Sigma_1}_\Phi
proof:$ 0 = 1は$ \Sigma_1文なので自明．
3. $ \mathsf{PA} \vdash \mathrm{Con}^{\Sigma_1}_\Phi \to \mathrm{Con}^\mathrm{G}_\Phi
proof:自明．
references:
導出可能性条件$ \bf D1,D2,D3を満たす証明可能性述語$ \Phi(x)で構成されたLöb無矛盾文$ \mathrm{Con}^\mathrm{L}_{\Phi}について，$ T \nvdash \mathrm{Con}^\mathrm{L}_{\Phi} proof:
References