直観主義命題論理のプライム性を用いたKripke完全性定理
Memo
ので,少し違う方法で構成する.
Memo
形式化,というか参考文献のものをLean 4で書き直しました. 参考文献
持っていないのでコードから推察したりする
プライム拡大補題の証明で参考にしたところ,Clearly showedと書いてあるが全く明らかではなく,というか多分少し間違っている. おそらく形式化において少し修正が加えられている.
逆に寛大なモーダスポネンスでは帰納法の仮定が狂って証明が煩雑(というか出来ない?)
Memo
普通はこっちのほうが良いと思う.
どこかに転がっていると思う
論理式集合(以下,理論)$ \Gammaについて
以下を満たすとき,$ \Gammaは選言的(disjunctive)という.
$ \varphi \lor \psi \in \Gamma \implies \varphi \in \Gamma ~\text{or}~ \psi \in \Gamma
以下を満たすとき,$ \Gammaは演繹的に閉じている(deductive closed)という.
$ \Gamma \vdash \varphi \implies \varphi \in \Gamma
以下を満たすとき,$ \Gammaは無矛盾という
$ \Gamma \nvdash \bot
上3つ,すなわち選言的で / 演繹的に閉じている / 無矛盾な理論のことを,プライムな理論という.
$ \Gamma \nvdash \varphiのとき,プライムな理論$ \Gamma^P \supe \Gammaが存在し,$ \Gamma^P \nvdash \varphi
proof
全ての論理式$ \psi_0,\psi_1,\cdotsは列挙可能とする.
ただし$ \cdots,\psi,\cdots,\xi,\cdots,\psi \lor \xi,\cdotsとする.すなわち論理式を選言で結んだ論理式は必ずどちらの論理式よりも後に現れるものとする.
$ \Gammaに対して,
添字集合族$ \Gamma^I_iを以下のように定める.
$ \Gamma^I_0 := \Gamma
$ \psi_k \equiv \psi_{k,1} \lor \psi_{k,2}とする.$ \Gamma^I_{k+1}を
$ \Gamma^I_k \vdash \psi_{k,1} \lor \psi_{k,2}のとき
$ \Gamma^I_{k} \cup \{\psi_1\} \nvdash \varphi \implies \Gamma^I_{k+1} := \Gamma^I_k \cup \{\psi_1\}
$ \Gamma^I_{k} \cup \{\psi_1\} \vdash \varphi \implies \Gamma^I_{k+1} := \Gamma^I_k \cup \{\psi_2\}
$ \Gamma^I_k \nvdash \psi_{k,1} \lor \psi_{k,2}のとき$ \Gamma^I_{k+1} := \Gamma^I_k
$ \Gamma^I := \bigcup_{i \in \N} \Gamma^I_iとする.
添字集合族$ \Gamma^P_iを以下のように定める.
$ \Gamma^P_0 := \Gamma
$ \Gamma^P_{k+1} := \bigcup_{i \in \N} (\Gamma^P_k)^I_i
$ \Gamma^P := \bigcup_{i \in \N} \Gamma^P_iとする.
lemlem: $ \Gamma^I_iに関する補題
I.1. $ \Gamma \nvdash \varphiならば,任意の$ kで$ \Gamma^I_k \nvdash \varphi
proof
$ kに関する帰納法.$ k =0のときは明らか.
$ \Gamma^I_k \nvdash \varphiとしたとき$ \Gamma^I_{k+1}について.
定義に沿って分解した時自明ではないのは,$ \Gamma^I_k \vdash \psi_1 \lor \psi_2かつ$ \Gamma^I_{k} \cup \{\psi_1\} \vdash \varphiのときに$ \Gamma^I_{k+1} := \Gamma^I_k \cup \{\psi_2\}のとき.
それ以外は明らか.
$ \Gamma^I_{k} \cup \{\psi_2\} \vdash \varphiと仮定しておかしいことを示す.
$ \Gamma^I_k \vdash \psi_1 \to \varphi
$ \Gamma^I_k \vdash \psi_2 \to \varphi
$ \Gamma^I_k \vdash \psi_1 \lor \psi_2に注意するとこのとき$ \Gamma^I_k \vdash \varphiとなる.これは帰納法の仮定よりおかしい.よって$ \Gamma^I_{k} \cup \{\psi_2\} = \Gamma^I_{k+1} \nvdash \varphi.
I.1'. $ \Gamma^I_k \vdash \varphi \implies \Gamma \vdash \varphi
proof:I,1の対偶.
I.2. $ \Gamma^I \vdash \varphiならば,ある$ kで$ \Gamma^I_k \vdash \varphi.
proof
演繹$ \vdashに関する帰納法.
lemlem: $ \Gamma^P_iに関する補題
P.1. $ \Gamma^P_{k+1} \vdash \psiなら,ある$ mで$ (\Gamma^P_k)^I_m \vdash \psi
proof
$ \Gamma^P_{k + 1} = (\Gamma^P_k)^Iということに注意すればI.2より従う.
P.2. $ \Gamma^P_k \vdash \varphiならば,$ \Gamma \vdash \varphi.
proof:
$ kについての帰納法.$ k = 0のときは明らか
$ \Gamma^P_k \vdash \varphi \implies \Gamma \vdash \varphiのとき$ \Gamma^P_{k+1} \vdash \varphiについては
P.1.より$ (\Gamma^P_k)^I_m \vdash \varphi.
I.1'より$ \Gamma^P_k \vdash \varphi.
帰納法の仮定より良い.
lemlem: $ \Gamma^Pに関する補題
PP.1. $ \Gamma^P \vdash \psiなら,ある$ mで$ \Gamma^P_m \vdash \psi.
proof:演繹に関する帰納法
$ \Gamma^Pは選言的である
前提として$ k番目の論理式は選言の形をしている$ \psi_k \equiv \psi_{k,1} \lor \psi_{k,2}とし,$ \psi_{k,1} \lor \psi_{k,2} \in \Gamma^Pとする.
このとき,ある$ mで$ \psi_{k,1} \lor \psi_{k,2} \in \Gamma^P_mであり,よって$ \Gamma^P_m \vdash \psi_{k,1} \lor \psi_{k,2}である.
$ \Gamma^P_mに対して$ (\Gamma^P_m)^I_iを考えると,
$ \Gamma^P_m = (\Gamma^P_m)^I_0 \vdash \psi_{k,1} \lor \psi_{k,2}及び$ (\Gamma^P_m)^I_0 \sube (\Gamma^P_m)^I_kより$ (\Gamma^P_m)^I_k \vdash \psi_{k,1} \lor \psi_{k,2}であるため
$ (\Gamma^P_m)^I_{k+1} = (\Gamma^P_m)^I_{k} \cup \{\psi_{k,1}\}または$ (\Gamma^P_m)^I_{k+1} = (\Gamma^P_m)^I_{k} \cup \{\psi_{k,2}\}のどちらかが言えて,
$ \psi_{k,1} \in (\Gamma^P_m)^I_{k+1}または$ \psi_{k,2} \in (\Gamma^P_m)^I_{k+1}のどちらかが成り立つ.
以上より$ \psi_{k,1} \in \Gamma^Pまたは$ \psi_{k,2} \in \Gamma^Pが成り立つ.題意は示された.
$ \Gamma^Pは閉じている
前提として$ \Gamma^P \vdash \psiとする.
直ちに$ \Gamma^P \vdash \varphi \lor \psiが成り立つ.$ \psi_k \equiv \varphi \lor \psiとする.
lemlem PP.1より,ある$ mで$ \Gamma^P_m \vdash \varphi \lor \psiが成り立つ.
$ (\Gamma^P_m)^I_iを考えると,
選言的の際と同じような議論より$ (\Gamma^P_m)^I_k \vdash \varphi \lor \psiであり,
$ (\Gamma^P_m)^I_k \cup \{ \varphi \} \vdash \varphiだから$ (\Gamma^P_m)^I_{k+1} = (\Gamma^P_m)^I_k \cup \{\psi\}となる.
よって$ \psi \in (\Gamma^P_m)^I_{k + 1}
以上より$ \psi \in \Gamma^P(定義に沿ってバラせば確かめられる).題意は示された.
$ \Gamma^P \nvdash \varphi
背理法で示す.$ \Gamma^P \vdash \varphiとする.
lemlem PP.1より,ある$ mで$ \Gamma^P_m \vdash \varphi.
元々の前提$ \Gamma \nvdash \varphiとlemlem P.2の対偶より,任意の$ kで$ \Gamma^P_k \nvdash \varphiだから,特に$ \Gamma^P_m \nvdash \varphi,
よっておかしい.$ \Gamma^P \nvdash \varphi.
$ \Gamma^Pは無矛盾である
$ \Gamma^P \vdash \botとすると爆発律より$ \Gamma^P \vdash \varphiが導出されるが,これはおかしいことを上で確認した. $ \Gamma \sube \Gamma^P
$ \Gamma = \Gamma^P_0 \sube \Gamma^Pより良い.
以上より$ \Gamma^+ \nvdash \varphi,$ \Gamma \sube \Gamma^Pかつ$ \Gamma^+はプライム(選言的 / 演繹的に閉じている / 無矛盾)である.
カノニカルモデル$ \mathcal{M}^+ = \lang W^+, \rightsquigarrow^+, V^+ \rangと定める.
$ W^+ = \{ \Omega \mid \text{$\Omega$ is prime and consistent} \}
$ \Omega_1 \rightsquigarrow^+ \Omega_2 \iff \Omega_1 \sube \Omega_2
$ V^+(\Omega, a) \iff a \in \Omega
Lem 1
proof
$ \rightsquigarrow^+が推移律,反射律を満たすことは包含関係の性質より明らか 遺伝性:$ \Omega_1 \rightsquigarrow^+ \Omega_2(すなわち$ \Omega_1 \sube \Omega_2)な任意の$ \Omega_1,\Omega_2に対して$ V^+(\Omega_1, a) \implies V^+(\Omega_2, a)である 要するに$ a \in \Omega_1 \sube \Omega_2で$ a \in \Omega_2を示せば良いが,明らか.
$ \Omegaはプライム理論とする.$ \Omega \Vdash_{\mathcal{M}^+} \varphi \iff \Omega \vdash \varphi
proof
$ \varphiの構造帰納法.
$ \varphi \equiv a,\bot, \psi \land \xi, \psi \lor \xiのときはほとんど明らか
$ \varphi \equiv \psi \lor \xiの場合
$ \impliesの場合はほとんど明らか.
$ \impliedbyについて
$ \Omegaのプライム性より
closed:$ \psi \lor \xi \in \Omega
disjunctive: $ \psi \in \Omegaまたは$ \xi \in \Omega
どちらだとしても帰納法の仮定より良い.
$ \varphi \equiv \psi \to \xiの場合
$ \impliedbyを示す.
$ \Omega \vdash \psi \to \xi と仮定する.
$ \Omega \Vdash_{\mathcal{M}^+} \psi \to \xiすなわち,任意のプライム理論$ \Omega' \supe \Omegaで$ \Omega' \nVdash_{\mathcal{M}^+} \psiまたは$ \Omega' \Vdash_{\mathcal{M}^+} \xiを示す.
逆に,ある$ \Omega' \supe \Omegaで$ \Omega' \Vdash \psiかつ$ \Omega' \nVdash \xiだと仮定するとおかしいことを示す.
帰納法の仮定より
1. $ \Omega' \Vdash_{\mathcal{M}^+} \psi \implies \Omega' \vdash \psi(最後は演繹的に閉じていることより)
2. $ \Omega' \nVdash_{\mathcal{M}^+} \xi \implies \Omega' \nvdash \xi
3. $ \Omega \vdash \psi \to \xi \implies \Omega' \vdash \psi \to \xi
1,3より$ \Omega' \vdash \xiでありこれは2と合わせておかしい.よって仮定がおかしい.
よって示された.
$ \implies
対偶を示す.すなわち$ \Omega \nvdash \psi \to \xiを仮定して$ \Omega \nVdash_{\mathcal{M}^+} \psi \to \xiを示す.
$ \Omega \nVdash_{\mathcal{M}^+} \psi \to \xi$ \iffあるプライムな理論$ \Omega' \supe \Omegaで$ \Omega' \Vdash_{\mathcal{M}^+} \psiかつ$ \Omega' \nVdash_{\mathcal{M}^+} \xiを示す.
演繹定理より$ \Omega \nvdash \psi \to \xi \implies \Omega \cup \{\psi\} \nvdash \xi プライム拡大補題より$ \Omega \cup \{\psi\}に対してプライムな理論$ \Omega^+ \cup \{\psi\} \supe \Omega \cup \{\psi\}が存在して$ \Omega^+ \cup \{\psi\} \nvdash \xi 今$ \Omega' := \Omega^+ \cup \{\psi\}として取れば要件を満たす.
$ \Omega^+ \cup \{\psi\} \supe \Omega \cup \{\psi\} \supe \Omega
それぞれ帰納法の仮定
$ \Omega^+ \cup \{\psi\} \vdash \psi \implies \Omega^+ \cup \{\psi\} \Vdash_{\mathcal{M}^+} \psi
$ \Omega^+ \cup \{\psi\} \nvdash \xi \implies \Omega^+ \cup \{\psi\} \nVdash_{\mathcal{M}^+} \xi
memo
多くの本では証明が略されているが,少なくとも$ \toに関してはそれほど自明ではない.
$ \Gamma \vDash \varphi \implies \Gamma \vdash \varphi.
proof
対偶$ \Gamma \nvdash \varphi \implies \Gamma \nvDash \varphiを示す.
プライム拡大補題より$ \Gamma^+ \nvdash \varphiなプライム理論$ \Gamma^P \supe \Gammaが存在する. $ \Gamma^P \nvdash \varphiと真理補題より$ \Gamma^P \nVdash_{\mathcal{M}^+} \varphi 今$ \Gamma \vDash \varphiと仮定するとおかしくなることを示す.
$ \Gamma \vDash \varphi$ \iff任意のモデル$ \mathcal{M}と世界$ wで$ w \Vdash_\mathcal{M} \Gamma \implies w \Vdash_\mathcal{M} \varphi
$ w \Vdash_\mathcal{M} \Gamma$ \iff任意の$ \gamma \in \Gammaで$ w \Vdash_\mathcal{M} \gamma
今$ \mathcal{M}としてカノニカルモデル,$ wとして$ \Gamma^Pを取ってくる. $ \psi \in \Gamma^P \implies \Gamma^P \vdash \psi \implies \Gamma^P \Vdash_\mathcal{M^+} \psi
deductive closed, truthlemma
よって$ \Gamma^P \Vdash_\mathcal{M} \varphiが成り立つ.しかしこれはおかしい.よって$ \Gamma \nvDash \varphi.❏