正規様相論理のメモ:2024.01.18
Def:
論理式は以下のように定義される．
$ \varphi ::= p \mid \bot \mid \varphi \to \varphi \mid \varphi \land \varphi \mid \varphi \lor \varphi \mid \Box \varphi
略記は以下とする．
$ \lnot \varphi \equiv \varphi \to \bot
$ \Diamond \varphi \equiv \lnot\Box\lnot\varphi
公理図式$ \Phiとする．ここでは，$ \bf K,B,T,D,4,5,.2,.3,Lなど． 記号の濫用として，$ \Phiが定める公理の集合もそのまま$ \Phiと書くことにする．
公理集合$ \Phi_1,\dots,\Phi_nの和集合$ \bigcup_i \Phi_iを$ \Phi_1\dots\Phi_nと書き，明記したい場合はこれを論理という．
Def:
論理$ \LambdaのHilbert流証明体系$ \mathfrak{H}_\Lambdaは古典論理のものに以下の規則$ (\Lambda)を足したものとする．
$ \varphi \in \Lambda \implies \Gamma \vdash_{\mathfrak{H}_\Lambda} \varphi
$ \Gamma =\emptysetのとき$ \Gamma \vdash \varphiを$ \vdash \varphiと書く．
Note:
非空集合$ W上と$ W上の2項関係$ R : W \times Wとする．$ F = \lang W, R \rangをKripkeフレームという． 2項関係$ Rがある性質を満足するとき，$ F=\lang W,R \rangはその性質を満足するという．
example:
$ \mathcal{F}_\mathbf{K}はすべてのフレームの集合となる．
$ \mathcal{F}_\mathbf{T}は反射的なフレームの集合となる．
$ \mathcal{F}_\mathbf{4}は推移的なフレームの集合となる．
このように$ \Phiはフレームの性質$ P_\Phiを規定するという．
$ \bf Kは何も規定しない．
$ \bf Tは対称性，$ \bf 4は推移性を規定する．
Lem
論理$ \Phi_1,\dots,\Phi_nは各々$ \Phi_iのフレームの性質をすべて満たすような性質を規定する．
example:すなわち，論理$ \bf KT4は反射的かつ推移的な，すなわち前順序性を規定する．
任意の$ F \in \mathcal{F}_\Lambdaで$ \vDash^F \varphiとなることを$ \vDash^{\mathcal{F}_\Lambda } \varphiと表記する．
$ \vdash_{\mathfrak{H}_\mathbf{\Lambda}} \varphi \implies \vDash^{\mathcal{F}_\Lambda } \varphi
proof
Hilbert流の証明に関する帰納法-
Thm. Hilbert流証明体系での論理の無矛盾性
適当なフレーム$ f \in \mathcal{F}_\Lambdaが存在してこのフレームは性質$ P_\Lambdaを満足するとする．
このとき，$ \nvdash_{\mathfrak{H}_\mathbf{\Lambda}} \bot．これを$ \mathfrak{H}_\mathbf{\Lambda}で論理$ \Lambdaは無矛盾という．
proof
健全性の対偶を取り，$ \nvDash^{\mathcal{F}_\Lambda } \botを示す．
あるフレーム$ F \in \mathcal{F}_\Lambdaが存在し$ \nvDash^F \botを示せばよいが，そのようなフレームが存在すればこれは直ちに明らかで，存在性は仮定より従う．
remark
例えば$ \forall_{w,v \in W}.wRvとした自明なフレームは$ \bf K,T,B,D,4,5で規定可能なフレームの性質を満足する．
また，$ \bf Kは何も規定しない．
そのため，$ \bf \Lambda = T4などを例とし，単に$ \nvdash_{\mathfrak{H}_\mathbf{K\Lambda}} \botと言っても良い．
Def
$ \varphiが集合$ \Gammaの
フレーム$ F上意味論的帰結である：$ \Gamma \vDash^{F} \varphiとは
任意の付値関数$ V，任意の$ w \in Wに対し，$ w \vDash^{\lang F, V\rang} \gamma \implies w \vDash^{\lang F, V\rang} \varphiが成り立つことである．
フレームクラス$ \mathcal{F}_\Lambda上意味論的帰結である：$ \Gamma \vDash^{\mathcal{F}_\Lambda} \varphiとは
任意の$ F \in \mathcal{F}_\Lambdaで$ \varphiが$ \Gammaの$ F上意味論的帰結であることを言う．
Hilbert流証明体系においてコンテクストは有限集合であるので，集合$ \Gammaに対して素朴に$ \Gamma \vdash_\mathfrak{H} \varphiとすることはできない．そのため拡張を行う．
集合$ \Gammaに対し$ \Gamma \vdash_\mathfrak{H} \varphiとは，ある有限集合$ \bar{\Gamma} \sube \Gammaが存在して$ \bar{\Gamma} \vdash_\mathfrak{H} \varphiとなることとする．
集合$ \Gammaが$ \mathfrak{H}_\mathbf{\Lambda}上で矛盾しているとは$ \Gamma \vdash_{\mathfrak{H}_\mathbf{\Lambda}} \botとなることである．
逆に$ \mathfrak{H}_\mathbf{\Lambda}無矛盾とは$ \Gamma \nvdash_{\mathfrak{H}_\mathbf{\Lambda}} \botとなることである．
すなわち，$ \mathfrak{H}_\mathbf{\Lambda}無矛盾であるとは任意の有限集合$ \bar{\Gamma} \sube \Gammaで$ \bar{\Gamma} \nvdash_{\mathfrak{H}_\mathbf{\Lambda}} \botとなることである．
Lem
$ \Gammaが$ \mathfrak{H}_\mathbf{\Lambda}無矛盾なら任意の論理式$ \varphiに対して$ \Gamma \nvdash_{ \mathfrak{H}_\mathbf{\Lambda}} \varphiまたは$ \Gamma \nvdash_{ \mathfrak{H}_\mathbf{\Lambda}} \lnot \varphi
proof
背理法．すなわち$ \Gamma \vdash_{ \mathfrak{H}_\mathbf{\Lambda}} \varphiかつ$ \Gamma \vdash_{ \mathfrak{H}_\mathbf{\Lambda}} \lnot\varphiなら$ \Gamma \vdash_{ \mathfrak{H}_\mathbf{\Lambda}} \botとなって$ \mathfrak{H}_\mathbf{\Lambda}無矛盾性に反する．
と書いたが，そう自明な結論でもない．
Lem
この補題はかなり怪しい気がする．
$ \Gammaが$ \mathfrak{H}_\mathbf{\Lambda}無矛盾のとき，$ \Gamma \cup \{\varphi\} \vdash_{ \mathfrak{H}_\mathbf{\Lambda}} \botなら$ \lnot\varphi \in \Gammaであり，よって$ \Gamma \vdash_{ \mathfrak{H}_\mathbf{\Lambda}} \lnot\varphi．
proof
$ \Gamma \nvdash_{\mathfrak{H}_\mathbf{\Lambda}} \bot
Def
集合$ \Omegaが極大$ \mathfrak{H}_\Lambda無矛盾であるとは
$ \Omegaは$ \mathfrak{H}_\Lambda無矛盾であり
任意の$ \mathfrak{H}_\Lambda無矛盾集合$ \Omega' \supe \Omega'が$ \Omega = \Omega'となることである．
Lem
$ \Omegaが極大$ \mathfrak{H}_\mathbf{\Lambda}無矛盾なら任意の論理式$ \varphiに対して$ \Omega \vdash_{ \mathfrak{H}_\mathbf{\Lambda}} \varphiまたは$ \Omega \vdash_{ \mathfrak{H}_\mathbf{\Lambda}} \lnot \varphi
proof
$ \Omegaの無矛盾性より$ \Omega \nvdash_{ \mathfrak{H}_\mathbf{\Lambda}} \varphiまたは$ \Omega \nvdash_{ \mathfrak{H}_\mathbf{\Lambda}} \lnot \varphi
$ \Omega \nvdash_{ \mathfrak{H}_\mathbf{\Lambda}} \varphiのとき
$ \Omega \cup \{\lnot\varphi\} \vdash_{ \mathfrak{H}_\mathbf{\Lambda}} \lnot\varphiなので，$ \Omega \cup \{\lnot\varphi \}が無矛盾であることを示せば$ \Omegaの極大性より$ \Omega = \Omega \cup \{\lnot\varphi \}なので$ \Omega \vdash_{ \mathfrak{H}_\mathbf{\Lambda}} \lnot\varphiが言える．
背理法で示す．$ \Omega \cup \{\lnot\varphi \}が矛盾していると仮定する．
すなわち，ある無矛盾な有限集合$ \bar{\Omega} \sube \Omegaが存在して$ \bar{\Omega} \cup \{\lnot\varphi\} \vdash_{ \mathfrak{H}_\mathbf{\Lambda}} \bot．
このとき補題より$ \bar{\Omega} \vdash_{ \mathfrak{H}_\mathbf{\Lambda}} \lnot\lnot\varphiが言えて，DNEより$ \bar{\Omega} \vdash_{ \mathfrak{H}_\mathbf{\Lambda}} \varphiだが，元々の前提より$ \bar{\Omega} \nvdash_{ \mathfrak{H}_\mathbf{\Lambda}} \varphiであるのでおかしい．
以上より仮定がおかしく$ \Omega \cup \{\lnot\varphi \}は無矛盾．
$ \Omega \nvdash_{ \mathfrak{H}_\mathbf{\Lambda}} \lnot \varphiのとき
$ \Omega \cup \{\varphi\} \vdash_{ \mathfrak{H}_\mathbf{\Lambda}} \varphiなので，$ \Omega \cup \{\varphi \}が無矛盾であることを示せば$ \Omegaの極大性より$ \Omega = \Omega \cup \{\varphi \}となって$ \Omega \vdash_{ \mathfrak{H}_\mathbf{\Lambda}} \varphiが言える．
背理法で示す．$ \Omega \cup \{\varphi \}が矛盾していると仮定する．
すなわち，ある無矛盾な有限集合$ \bar{\Omega} \sube \Omegaが存在して$ \bar{\Omega} \cup \{\varphi\} \vdash_{ \mathfrak{H}_\mathbf{\Lambda}} \bot．
このとき補題より$ \bar{\Omega} \vdash_{ \mathfrak{H}_\mathbf{\Lambda}} \lnot\varphiが言えるが，元々の前提より$ \bar{\Omega} \nvdash_{ \mathfrak{H}_\mathbf{\Lambda}} \lnot\varphiであるのでおかしい．
以上より仮定がおかしく$ \Omega \cup \{\varphi \}は無矛盾．
$ \Gammaが$ \mathfrak{H}_\mathbf{\Lambda}無矛盾なら，極大$ \mathfrak{H}_\mathbf{\Lambda}無矛盾集合$ \Gamma^+ \supe \Gammaが存在する．