Geach論理の完全性定理
References
Def
$ \mathbf{G}_{i,j,m,n} \equiv \Box^i\Diamond^m \varphi \to \Box^j\Diamond^n\varphi
$ \forall x,y,z \lbrack x \prec^i y ~\&~ x \prec^j z \implies \exists u\lbrack y \prec^m u ~\&~ z \prec^n u \rbrack \rbrack
Fact
$ \vDash^F \mathbf{G}_{i,j,m,n}$ \iff$ FはGeach合流性を満たす Memo
$ \mathcal{M}_+ = \lang W_+,\prec_+,V_+ \rangはカノニカルモデルとする． $ X,Y \in W_+とする．
Lem.1
$ \forall \varphi \lbrack \Box^n \varphi \in X \implies \varphi \in Y \rbrack \iff \forall \varphi \lbrack \varphi \in Y \implies \Diamond^n\varphi \in X \rbrack
proof
$ \Diamond^n \varphi \equiv \underbrace{\Diamond \Diamond \cdots \Diamond}_n \varphi \equiv \underbrace{(\lnot \Box \lnot) (\lnot \Box \lnot) \cdots (\lnot \Box \lnot)}_n \varphi \equiv \lnot \Box^n\lnot \varphiであることに注意する
$ \varphi \notin \Omega \iff \lnot \varphi \in \Omega
対偶を取れば，$ \varphi \in \Omega \iff \lnot\varphi \notin \Omega
$ \varphi \in \Omega \iff \lnot\lnot \varphi \in \Omega
$ \implies
$ \forall \varphi \lbrack \Box^n \varphi \in X \implies \varphi \in Y \rbrackを仮定して対偶$ \Diamond^n\varphi \notin X \implies \varphi \notin Yを示す．
$ \Diamond^n \varphi \notin Xだとする．
このとき上の注意より
$ \begin{aligned} \Diamond^n \varphi \notin X &\iff \lnot \Diamond^n \varphi \in X \\&\iff \lnot\lnot \Box^n\lnot\varphi \in X \\ &\iff \Box^n \lnot\varphi \in X \\ &\implies \lnot\varphi \in Y \\ &\iff \varphi \notin Y \end{aligned}
よってOK．
$ \impliedby
$ \forall \varphi \lbrack \varphi \in Y \implies \Diamond^n\varphi \in X \rbrackを仮定して対偶$ \varphi \notin Y \implies \Box^n\varphi \notin Xを示す．
$ \begin{aligned} \varphi \notin Y &\iff \lnot\varphi \in Y \\&\implies \Diamond^n\lnot\varphi \in X \\&\iff \lnot\Box^n\lnot\lnot\varphi \in X \\ &\iff \Box^n\lnot\lnot\varphi \notin X \\ &\iff \Box^n\varphi \notin X \end{aligned}
よってOK．
memo
この事実は次の形でも書ける．
$ \forall \varphi \lbrack \varphi \in \Box^{-n} X \implies \varphi \in Y \rbrack \iff \forall \varphi \lbrack \varphi \in Y \implies \varphi \in \Diamond^n X \rbrack
Lem.2
$ X \prec_+^n Y \iff \forall \varphi \lbrack \Box^n \varphi \in X \implies A \in Y \rbrack
proof
次のことに注意する
$ X \prec_+ Y \iff \forall \varphi \lbrack \Box\varphi \in X \implies \varphi \in Y \rbrack
$ X \prec^0_+ Y \iff X = Y
$ X \prec^{n+1}_+ Y \iff \exists Z \lbrack X \prec_+ Z ~\&~ Z \prec^n_+ Y \rbrack
$ nについての帰納法．
$ n = 0のときは明らか．
$ n = k + 1について
$ \implies
そのような$ Zを取ってきたとする．
$ \Box^{k+1} \varphi \in Xとなるような$ \varphiについて，$ \Box^k\varphi \in Zであり，帰納法の仮定より$ \varphi \in Y．よってOK
$ \impliedby
$ X \prec_+^k Y \iff \forall \varphi \lbrack \Box^k \varphi \in X \implies A \in Y \rbrack \iff \forall \varphi \lbrack \varphi \in Y \implies \varphi \in \Diamond^n X \rbrackが仮定として利用可能．
そのような$ Zの存在を示さなければならない．
$ Z^- := \Box^{-1} X \cup \Diamond^n Yとする．
$ \Box\varphi \in X \implies \varphi \in \Box^{-1}X \implies \varphi \in Z^- \implies \varphi \in Zだから$ X \prec_+ Z．
$ \varphi \in Y \implies \Diamond^k \varphi \in \Diamond^k Y \implies \Diamond^k \varphi \in Z^- \implies \Diamond^k \varphi \in Z \iff \varphi \in \Diamond^k Zより帰納法の仮定で$ Z \prec_+^k Y．
以上より$ X \prec^{k+1}_+ Yは示された．
残る点は$ Z^-が無矛盾であるかどうか．
$ Z^- \vdash \Box B_0 \land \cdots \land \Box B_b \land \Diamond^n C_0 \land \dots \land \Diamond^n C_c \to \botとなる$ \Box B_0 \dots,\Box B_b \in Xと$ C_0 \dots,C_c \in Yが存在する．
$ B \equiv \bigwedge B_bと$ C \equiv \bigwedge C_cとする．
適当に帰納法を回せば明らかに，$ \Box B \in Xおよび$ C \in Yが言える．
$ \vdash \Diamond^n C \to \Diamond^n C_0 \land \Diamond^n C_cが成り立つ．
以上より$ \vdash B \land \Diamond^n C \to \botが言える．ここから変形していくと
$ \begin{aligned} Z^- \vdash B \land \Diamond^n C \to \bot &\iff Z^- \vdash \lnot(B \land \Diamond^n C) \\&\implies Z^- \vdash \lnot B \lor \lnot \Diamond^nC \\ &\implies Z^- \vdash B \to \lnot \Diamond^nC \\ &\implies Z^- \vdash B \to \Box^n \lnot C \\ &\implies Z^- \vdash \Box B \to \Box^{n+1} \lnot C \end{aligned}
今$ \Box B \in X \iff X \vdash \Box B \implies Z^- \vdash \Box Bだから$ Z^- \vdash \Box^{n+1} \lnot C
よって$ \Box^{n+1} \lnot C \in Xであり，帰納法の仮定より$ \lnot C \in Yとなる．
$ C \in Yだったから，$ Yは矛盾する．ところが$ Yは極大無矛盾であるのでこれはおかしい．