証明可能性論理GLは決定可能
References
Fact 1
Fact 2:
references
Memo
Fact1より正規様相論理の通常の方法では$ \sf GLの決定可能性は示せない． しかし，$ \sf GLは決定可能である．
Def: 2.3.6
論理式$ \varphiとし，部分論理式集合$ \Sigma \coloneqq \mathrm{Sub}(\varphi) $ \sf GLカノニカルモデル$ \mathcal{M}^\mathsf{GL} \coloneqq \lang W^\mathsf{GL}, R^\mathsf{GL}, V^\mathsf{GL} \rangに対し $ W^\mathsf{GL}_\Sigma上関係$ R^gを
$ \lbrack\Gamma\rbrack R^g \lbrack\Delta\rbrackは以下を満たす．
1. 任意の$ \Box\psi \in \Sigmaに対し$ \Box \psi \in \Gamma \implies \psi \land \Box\psi \in \Delta
2. ある$ \Box \gamma \in \Sigmaに対し$ \Box\gamma \notin \Gammaかつ$ \Box\gamma \in \Delta
$ (\mathcal{M}^\mathsf{GL}_\Sigma)^g \coloneqq \lang W^\mathsf{GL}_\Sigma, R^g, V^\mathsf{GL}_\Sigma \rangとする．
Lem 2.3.7
$ (\mathcal{M}^\mathsf{GL}_\Sigma)^g \coloneqq \lang W^\mathsf{GL}_\Sigma, R^g, V^\mathsf{GL}_\Sigma \rangについて，$ W^\mathsf{GL}_\Sigmaは有限で，$ R^gは非反射的かつ推移的 proof:
$ \Sigmaは有限なので$ W^\mathsf{GL}_\Sigmaも有限
$ R^gの定義と$ \Gammaの$ \sf GL無矛盾性より$ R^gは非反射的
$ R^gが非反射的でないとするなら，ある$ \lbrack \Gamma \rbrack \in W^\mathsf{GL}_\Sigmaに対し$ \lbrack \Gamma \rbrack R^g \lbrack \Gamma \rbrack
これは$ R^gの条件2より$ \Box\gamma \notin \Gammaかつ$ \Box\gamma \in \Gammaとなって$ \Gammaの無矛盾性に反する．
$ R^gの推移性は$ \lbrack \Gamma_1 \rbrack R^g \lbrack \Gamma_2 \rbrackと$ \lbrack \Gamma_2 \rbrack R^g \lbrack \Gamma_3 \rbrackを仮定して$ \lbrack \Gamma_1 \rbrack R^g \lbrack \Gamma_3 \rbrackを示せば良い．これを見るには$ R^gの条件1,2を精査すればよいがこれは明らか．
Lem 2.3.9
$ \Box \beta \notin \Gamma$ \implies$ \{\lnot \beta, \Box\beta\} \cup \{\gamma, \Box\gamma \mid \Box\gamma \in \Gamma \}は$ \sf GL無矛盾
Lem 2.3.10
$ \Gammaが任意の$ \sf GL極大無矛盾集合で，$ \psi \in \Sigmaとする． $ (\mathcal{M}^\mathsf{GL}_\Sigma)^g , \lbrack \Gamma \rbrack \vDash \psi \iff \psi \in \Gamma
proof:
$ \psi \equiv \Box \betaとして$ \Box \beta \in \Sigmaを仮定する．$ \beta \in \Sigmaに注意．
$ \impliedby
$ \Box \beta \in \Gammaを仮定して$ (\mathcal{M}^\mathsf{GL}_\Sigma)^g , \lbrack \Gamma \rbrack \vDash \Box \betaを示す．
$ \lbrack \Gamma \rbrack R^g \lbrack \Delta \rbrackとなる$ \Deltaを考えて$ (\mathcal{M}^\mathsf{GL}_\Sigma)^g , \lbrack \Delta \rbrack \vDash \betaを示せば良い．
$ R^gの定義1と$ \Box \beta \in \Gammaより$ \beta \in \Delta．IHより示される．
$ \implies
対偶を示す．$ \Box \beta \notin \Gammaを仮定して$ (\mathcal{M}^\mathsf{GL}_\Sigma)^g , \lbrack \Gamma \rbrack \nvDash \Box \betaを示す．
2.3.9より$ \{\lnot \beta, \Box\beta\} \cup \{\gamma, \Box\gamma \mid \Box\gamma \in \Gamma \}は$ \sf GL無矛盾
様相論理のLindenbaum補題より$ \Delta \supe \{\lnot \beta, \Box\beta\} \cup \{\gamma, \Box\gamma \mid \Box\gamma \in \Gamma \}となる$ \sf GL極大無矛盾集合$ \Deltaが存在する． 極大性と$ \lnot \beta \in \Deltaより$ \beta \notin \Delta
$ \beta \in \SigmaであるのでIHより$ (\mathcal{M}^\mathsf{GL}_\Sigma)^g , \lbrack \Delta \rbrack \nvDash \beta
$ \lbrack \Gamma \rbrack R^g \lbrack \Delta \rbrackを示せば$ (\mathcal{M}^\mathsf{GL}_\Sigma)^g , \lbrack \Gamma \rbrack \nvDash \Box \betaとなる．以下より$ \lbrack \Gamma \rbrack R^g \lbrack \Delta \rbrack．
1. 任意の$ \Box \gamma \in \Sigmaに対し$ \Box \gamma \in \Gammaと仮定すれば$ \Deltaの構成方より明らかに$ \gamma \land \Box \gamma \in \Delta
2. $ \Box \beta \in \Sigmaに対し仮定より$ \Box \beta \notin \Gammaで$ \Deltaの構成法より$ \Box \beta \in \Delta
よって示された．
$ \sf GLは非反射的で推移的な有限フレームのクラスに対し有限フレーム性がある proof
$ \sf GL無矛盾な論理式$ \varphiとする．
補題より$ \varphi \in \Gammaな$ \sf GL極大無矛盾集合$ \Gammaが存在する． 2.3.10より$ (\mathcal{M}^\mathsf{GL}_{\mathrm{Sub}(\varphi)})^g , \lbrack \Gamma \rbrack \vDash \varphi
ところで$ (\mathcal{M}^\mathsf{GL}_{\mathrm{Sub}(\varphi)})^gの定義より$ \varphiはフレーム$ \lang W^\mathsf{GL}_{\mathrm{Sub}(\varphi)}, R^g \rangで充足可能．
2.3.7より$ \lang W^\mathsf{GL}_{\mathrm{Sub}(\varphi)}, R^g \rangは非反射的推移的有限フレームである．❏ Lem 2.3.12
proof
2.3.11よりある非反射的推移的フレーム$ \mathcal{F} \coloneqq \lang W, R \rang，付値$ V\colon \mathrm{Prop} \to 2^W，$ w \in Wで$ \lang \mathcal{F}, V \rang, w \vDash \varphiと仮定する
$ \mathcal{M} = \lang \mathcal{F}, V \rangの$ w生成部分モデル$ \mathcal{M}_wを考えれば
補題2.2.6と2.2.3より$ \mathcal{M}_w, w \vDash \varphi
$ \mathrm{Tree}^{+}(\mathcal{M}_w, w)を考えれば2.2.11と2.2.6より$ \mathrm{Tree}^{+}(\mathcal{M}_w, w),w \vDash \varphi
$ Rが非反射的なら$ \mathrm{Tree}^+(\mathcal{M}_w, w)は有限モデルとなる．❏