直観主義命題論理の選言特性
References
としていたが上2つの証明には微妙にギャップがあって証明できていない
Memo
詳しくは↓の辺りを参考にして下さい.
$ w \leq vのとき,$ w \Vdash^\mathcal{M} \varphi \implies v \Vdash^\mathcal{M} \psi
$ \vdash_\mathrm{Int} \varphi \lor \psiならば$ \vdash_\mathrm{Int} \varphiまたは$ \vdash_\mathrm{Int} \psi
proof
対偶を示す.$ \nvdash \varphiかつ$ \nvdash \psiとし,$ \nvdash \varphi \lor \psiを示す.
このとき,以下のモデルと世界$ \mathcal{M}_1 = \lang W_1,\mathbin{\leq_1},V_1\rang,w_1 \in W_1及び$ \mathcal{M}_2 = \lang W_2,\mathbin{\leq_2},V_2\rang,w_2 \in W_2が存在する
$ w_1 \nVdash^{\mathcal{M}_1} \varphi
$ w_2 \nVdash^{\mathcal{M}_2} \psi
$ \mathcal{M}_1,\mathcal{M}_2のモデルを合体させて新しいモデルを作る.$ \mathcal{M} = \lang W,\mathbin{\leq},V \rangを以下のように定める.
$ W := \{w_0\} \cup W_1 \sqcup W_2
ただし
$ w_0 \notin W_1かつ$ w_0 \notin W_2とし
$ W_1 \sqcup W_2は非交和を表すとする(すなわち$ w \in W_1 \implies w \notin W_2.逆も然り) memo:ここは指摘を受けてアドホックに直したのでもしかしたら間違っているかもしれない.
$ w \leq v \iff \begin{cases} w \leq_1 v & \text{if}\ w,v \in W_1 \\ w \leq_2 v & \text{if}\ w,v \in W_2 \\ w_1 \leq v & \text{if}\ w = w_1 ~\&~ v \in W_1 \\ w_2 \leq v & \text{if}\ w = w_2 ~\&~ v \in W_2 \\ w = v = w_0 & \text{otherwise} \end{cases}
直感的はこうなっていると考えよ(ただし定義域が変わるので正確ではない):
$ \mathbin{\leq} := \mathbin{\leq_1} \cup \mathbin{\leq_2} \cup \{(w_0,w_0)\} \cup \{ (w_0, v_1) \mid w_1 \leq_1 v_1 \} \cup \{(w_0,w_0)\} \cup \{ (w_0, v_2) \mid w_2 \leq_2 v_2 \}
$ V(w, a) = 1 \iff \begin{cases} V_1(w, a) = 1 & \text{if}\ w \in W_1 \\ V_2(w,a) = 1 & \text{if}\ w \in W_2 \end{cases}
$ \mathcal{M}が直観主義論理のモデルとして良いことを示す
反射律
$ w \in W_1,w \in W_2なら$ w \leq_1 w, w \leq_2 wは元のモデルの反射律より言える.
$ w = w_0のときは定義よりよい.
推移律
$ x \leq y, y \leq z \implies x \leq zについて
$ x,y,z \in W_1及び$ x,y,z \in W_2のときは元のモデルの反射律から明らか
$ w_0から派生するものを考えると以下のパターンがある
1. $ w_0 \leq w_0, w_0 \leq w_0 \implies w_0 \leq w_0は明らか
2. $ w_0 \leq v_1 \in W_1, v_1 \leq r_1 \in W_1 \implies w_0 \leq r_1
$ w_0 \leq v_1の定義より$ w_1 \leq_1 v_1
よって$ \leq_1の推移律より$ w_1 \leq_1 r_1,
したがって$ w_0 \leq r_1が成り立つ.
3. $ w_0 \leq v_2 \in W_2, v_2 \leq r_2 \in W_2 \implies w_0 \leq r_2も2と同様にやれば良い.
遺伝性
以下は$ V(w_0,a) = 0なので成り立つ.
$ w_0 \leq v_1 \in W_1のとき$ V(w_0, a) = 1 \implies V(v_1,a) = 1
$ w_0 \leq v_2 \in W_2のとき$ V(w_0, a) = 1 \implies V(v_2,a) = 1
他は元のモデルの遺伝性より明らか.
Claim: 合体モデルの保存
任意の$ w \in W_1に対して$ w \Vdash^\mathcal{M} \varphi \iff w \Vdash^{\mathcal{M}_1} \varphi
特に$ w_1 \Vdash^\mathcal{M} \varphi \iff w_1 \Vdash^{\mathcal{M}_1} \varphi
任意の$ w \in W_2に対して$ w \Vdash^\mathcal{M} \varphi \iff w \Vdash^{\mathcal{M}_2} \varphi
特に$ w_2 \Vdash^\mathcal{M} \varphi \iff w_2 \Vdash^{\mathcal{M}_2} \varphi
proof
$ \mathcal{M}_1の場合を示す.$ \mathcal{M}_2でも大体同じようにすればよい.
$ \varphiの構造帰納法で示す.
$ \varphi \equiv \botのときは明らか.
$ \varphi \equiv aのとき$ V(w,a) = V_1(w,a)より良い.
$ \varphi \equiv \varphi_1 \lor \varphi_2
$ w \Vdash^\mathcal{M} \varphi_1 \lor \varphi_2
$ \iff$ w \Vdash^{\mathcal{M}} \varphi_1または$ w \Vdash^{\mathcal{M}} \varphi_2
$ \iff$ w \Vdash^{\mathcal{M}_1} \varphi_1または$ w \Vdash^{\mathcal{M}_1} \varphi_2(帰納法の仮定より)
$ \iff$ w \Vdash^{\mathcal{M}_1} \varphi_1 \lor \varphi_2
$ \varphi \equiv \varphi_1 \land \varphi_2
$ w \Vdash^\mathcal{M} \varphi_1 \land \varphi_2
$ \iff$ w \Vdash^{\mathcal{M}} \varphi_1かつ$ w \Vdash^{\mathcal{M}} \varphi_2
$ \iff$ w \Vdash^{\mathcal{M}_1} \varphi_1かつ$ w \Vdash^{\mathcal{M}_1} \varphi_2(帰納法の仮定より)
$ \iff$ w \Vdash^{\mathcal{M}_1} \varphi_1 \land \varphi_2
$ \varphi \equiv \varphi_1 \to \varphi_2のとき
$ \implies
$ w \Vdash^{\mathcal{M}_1} \varphi_1 \to \varphi_2を示すため,$ w \leq_1 vとなる$ v \in W_1を取り,$ v \Vdash^{\mathcal{M}_1} \varphi_1と仮定する.
$ v \Vdash^{\mathcal{M}_1} \varphi_2を示す.
帰納法の仮定より$ v \Vdash^\mathcal{M} \varphi_1となる.
定義より$ w \leq_1 vより$ w \leq vであるから,元々の前提$ w \Vdash^\mathcal{M} \varphi_1 \to \varphi_2より$ v \Vdash^\mathcal{M} \varphi_2.
帰納法の仮定より$ v \Vdash^{\mathcal{M}_1} \varphi_2.よって示された.
$ \impliedby
$ w \Vdash^{\mathcal{M}} \varphi_1 \to \varphi_2を示すため,$ w \leq vとなる$ v \in Wを取り,$ v \Vdash^{\mathcal{M}} \varphi_1と仮定する.
$ v \Vdash^{\mathcal{M}_1} \varphi_2を示す.
$ \leqの定義より,$ w \in W_1で$ w \leq vならば,必ず$ v \in W_1でかつ$ w \leq_1 vである.
帰納法の仮定より$ v \Vdash^{\mathcal{M}_1} \varphi_1となる.
以上と元々の前提$ w \Vdash^{\mathcal{M}_1} \varphi_1 \to \varphi_2であるから$ v \Vdash^{\mathcal{M}_1} \varphi_2
帰納法の仮定より$ v \Vdash^{\mathcal{M}} \varphi_2.よって示された.
$ \mathcal{M}は論理式に対して遺伝的なので対偶より以下が成り立つ.
$ w_0 \leq w_1 \implies \lbrack w_1 \nVdash^\mathcal{M} \varphi \implies w_0 \nVdash^\mathcal{M} \varphi \rbrack
$ w_0 \leq w_2 \implies \lbrack w_2 \nVdash^\mathcal{M} \psi \implies w_0 \nVdash^\mathcal{M} \psi \rbrack
もともとの仮定$ w_1 \nVdash^{\mathcal{M}_1} \varphiと$ w_2 \nVdash^{\mathcal{M}_2} \varphi及びLemの対偶より$ w_0 \nVdash^\mathcal{M} \varphiと$ w_0 \nVdash^\mathcal{M} \psiが成り立ち,
$ w_0 \nVdash^\mathcal{M} \varphi \lor \psiが成り立つので
$ \nvDash \varphi \lor \psiである.
したがって健全性より$ \nvdash \varphi \lor \psiが言えるため,所望の結論が得られた.❏