驚くべき帰結2は排中律とHPM上で等価
主張
任意の$ \varphiに対して$ \vdash_\mathsf{HPM + LEM} \varphi \iff \vdash_\mathsf{HPM + CM_2} \varphi
$ \impliedbyはなかなかにムズい．おれは全然示せなくてヘルプを求めていた
準備
$ \sf HPM + CM_2で使える公理，推論規則，構文論的同値は以下とする
公理
$ \mathsf{S} \colon (\varphi \to (\psi \to \chi)) \to ((\varphi \to \psi) \to (\phi \to \chi))
$ \mathsf{K} \colon \varphi \to (\psi \to \varphi)
$ \mathsf{Elim}_\land \colon (\varphi_1 \land \varphi_2) \to \varphi_i
ただし$ i = 1,2
$ \mathsf{Inst}_\land \colon \varphi \to \psi \to \varphi \land \psi
$ \mathsf{Elim}_\lor \colon (\varphi \to \chi) \to (\psi \to \chi) \to (\varphi \lor \psi \to \chi)
$ \mathsf{Inst}_\lor \colon \varphi_i \to \varphi_1 \lor \varphi_2
ただし$ i = 1,2
$ \mathsf{CM_2} \colon (\lnot\varphi \to \varphi) \to \varphi
推論規則
$ \mathsf{MP} \colon \vdash \varphi ~\&~ \vdash \varphi \to \psi \implies \vdash \psi
構文論的同値
$ \lnot \varphi \equiv \varphi \to \bot
補題
必要なら以下を用いても構いません．
演繹定理: $ \Gamma \vdash \varphi \to \psi \iff \Gamma, \varphi \to \psi 前提弱化$ \Gamma \vdash \varphi \implies \Delta \vdash \varphi，ただし$ \Gamma \sube \Delta
特に$ \vdash \varphi \implies \Gamma \vdash \varphi
同語反復$ \Gamma \vdash \varphi \to \varphi
補足
本当は公理ではなく公理図式として用意するか，一様代入則を推論規則として入れないとダメだが察してください． $ \sf S,K,Elim_\land,Inst_\land,Elim_\lor,Inst_\lor,MPを備えた体系は最小命題論理HPMという． 議論: $ \sf LEM \implies CM_2
$ \vdash_{\mathsf{HPM + LEM}} (\lnot\varphi \to \varphi) \to \varphi
証明
演繹定理より$ \lnot\varphi \to \varphi \vdash_{\mathsf{HPM + LEM}} \varphiを示せば示せば良い．以下$ \sf HPM + LEMは省略． 1. $ \lnot\varphi \to \varphi ⊢ \varphi \lor \lnot\varphi （$ \sf LEMより）
2. $ \lnot\varphi \to \varphi ⊢ \varphi \to \varphi （同語反復より）
3. $ \lnot\varphi \to \varphi \vdash \lnot\varphi \to \varphi （前提より）
4. $ \lnot\varphi \to \varphi \vdash (\varphi \to \varphi) \to (\lnot \varphi \to \varphi) \to ((\varphi \lor \lnot \varphi) \to \varphi)（$ \sf Elim_\lorより）
5. $ \lnot\varphi \to \varphi \vdash (\varphi \lor \lnot \varphi) \to \varphi（4,2,3で$ \sf MPを2回）
6. $ \lnot\varphi \to \varphi \vdash \varphi（5と1で$ \sf MP）
議論: $ \sf CM_2 \implies LEM
排中律$ \mathsf{LEM} \equiv \varphi \lor \lnot \varphiは$ \sf HPM + CM_2で証明可能である．すなわち$ \vdash_{\mathsf{HPM + CM_2}} \varphi \lor \lnot \varphi 本当にありがとうございました．証明は下記を参考にしてください．
https://gyazo.com/f7d5c761aff019adf0dd87f9301da25c
$ CM_2 (S (K inr) (S (S (K S) (S (KK) I)) (K inl)))