模态逻辑

模態邏輯是現代邏輯個一個主要分支，用來刻畫搭模態搭界個推理。所謂模態指個是一隻命題為真箇方式。常見個模態包括形而上學可能性（可能搭必然，如「蘇格拉底可能是哲學家」）、認知（信念搭知識，如「我曉得蘇格拉底是哲學家）、道義（許可搭義務，如「儂應該遵紀守法」）、時態（過去、現在搭未來，如「我過去是學生」）等等。相對應個，就有真勢模態邏輯、認知邏輯、道義邏輯、時態邏輯等模態邏輯分支。

模態邏輯要用到邏輯運算符，勒哲學、數學、語言學、計算機科學里向儕有蠻多應用個。相比一階邏輯搭二階邏輯，模態邏輯常常好勒表達力搭計算複雜性之間取得更好個平衡，故咾來勒計算機個應用弗少。

語言

模態邏輯用個形式語言通常是勒命題邏輯或者一階邏輯個語言個基礎丄加上模態算子個產物。

令${\displaystyle \mathbf {Prop} }$為一隻可數無窮個命題符號集合。基本模態語言${\displaystyle {\mathcal {L}}}$個公式由以下BNF範式生成：

${\displaystyle \varphi$ ::=p\in \mathbf {Prop} \mid \bot \mid \neg \varphi \mid \varphi \vee \varphi \mid \Box \varphi }

即：

1. 所有命題符號儕是${\displaystyle {\mathcal {L}}}$-公式；
2. 恆假${\displaystyle \bot }$是${\displaystyle {\mathcal {L}}}$-公式；
3. 假使講${\displaystyle \varphi }$是${\displaystyle {\mathcal {L}}}$-公式，格麼${\displaystyle \neg \varphi }$也是${\displaystyle {\mathcal {L}}}$-公式；
4. 假使講${\displaystyle \varphi }$搭${\displaystyle \psi }$是${\displaystyle {\mathcal {L}}}$-公式，格麼${\displaystyle \varphi \vee \psi }$也是${\displaystyle {\mathcal {L}}}$-公式；
5. 假使講${\displaystyle \varphi }$是${\displaystyle {\mathcal {L}}}$-公式，格麼${\displaystyle \Box \varphi }$也是${\displaystyle {\mathcal {L}}}$-公式。

${\displaystyle \Box }$是方塊算子，通常讀作「方塊」或者「box」。勒真勢模態邏輯里相，${\displaystyle \Box p}$表示「必然p」；認知邏輯一般拿${\displaystyle \Box }$寫成${\displaystyle K}$（know），用${\displaystyle Kp}$表示「主體曉得${\displaystyle p}$」；勒可證性邏輯里相，${\displaystyle \Box p}$表示「${\displaystyle p}$可證」。

就像一階邏輯里相存在量詞${\displaystyle \exists }$撥定義成全稱量詞${\displaystyle \forall }$個對偶，基本模態邏輯通過下頭個公式定義${\displaystyle \Box }$個對偶算子${\displaystyle \Diamond }$：

${\displaystyle \Diamond \varphi$ :=\neg \Box \neg \varphi }

${\displaystyle \Diamond }$通常讀作「菱形」或者「diamond」。真勢模態邏輯用${\displaystyle \Diamond p}$表示「可能p」，而${\displaystyle \Box p}$（必然${\displaystyle p}$）就邏輯等價於${\displaystyle \neg \Diamond \neg p}$（弗可能非${\displaystyle p}$）。

語義

模態邏輯個語義主要有關係語義（又叫克里普克語義）、鄰域語義、拓撲語義搭仔代數語義四種。其中，關係語義最直觀，鄰域語義搭拓撲語義是關係語義個一般化，代數語義最抽象。

關係語義

關係語義基於關係結構。關係結構是由論域搭伊上頭個關係組成個元組。關係結構勒數學裏相邪氣常見，幾乎所有阿拉熟悉個數學結構（譬如講代數結構、圖）儕可以撥當成關係結構；計算機科學、哲學、語言學、經濟學等學科也常常用着關係結構。（Blackburn, de Rijke and Venema, 2001）

勒關係語義下頭，基本模態邏輯個框架就是一隻關係結構${\displaystyle {\mathcal {F}}=(W,R)}$，其中

1. 論域${\displaystyle W}$是一隻由（可能）世界組成個非空集合，
2. 可及關係（或可通達關係，accessibility relation）${\displaystyle R\subseteq W\times W}$是${\displaystyle W}$上頭個一隻二元關係。

基本模態邏輯個模型是一隻三元組${\displaystyle {\mathcal {M}}=(W,R,V)}$，其中

1. ${\displaystyle (W,R)}$是基本模態邏輯個框架，
2. ${\displaystyle V:\mathbf {Prop} \to {\mathcal {P}}(W)}$是一隻賦值，伊搭每隻命題變元${\displaystyle p}$賦由所有${\displaystyle p}$勒里相為真箇世界組成個集合。

阿拉下頭定義哪能勒基本模態邏輯模型上頭解釋基本模態語言公式。

設${\displaystyle {\mathcal {M}}=(W,R,V)}$是一隻基本模態邏輯模型，${\displaystyle w\in W}$。阿拉搿能遞歸定義公式${\displaystyle \varphi }$勒${\displaystyle {\mathcal {M}}}$里${\displaystyle w}$丄撥滿足（或者為真）：

• ${\displaystyle {\mathcal {M}},w\models p}$ 當且僅當 ${\displaystyle w\in V(p)}$，其中${\displaystyle p\in \mathbf {Prop} }$
• ${\displaystyle {\mathcal {M}},w\models \bot }$ 永遠弗會
• ${\displaystyle {\mathcal {M}},w\models \neg \varphi }$ 當且僅當 ${\displaystyle {\mathcal {M}},w\not \models \varphi }$
• ${\displaystyle {\mathcal {M}},w\models \varphi \vee \psi }$ 當且僅當 ${\displaystyle {\mathcal {M}},w\models \varphi }$或者${\displaystyle {\mathcal {M}},w\models \psi }$

格麼${\displaystyle {\mathcal {M}},w\models \Diamond \varphi }$就當且僅當存在${\displaystyle v\in W}$使得${\displaystyle Rwv}$並且${\displaystyle {\mathcal {M}},v\models \varphi }$。

阿拉曉得，邏輯個一個主要研究對象是有效個推理。一隻公式勒一隻框架丄有效，意思是講無論儂往搿只框架上頭加啥個賦值，勒嗨所形成個模型里相，搿只公式儕是真箇。嚴格定義如下：

• 一隻公式${\displaystyle \varphi }$勒框架${\displaystyle {\mathcal {F}}}$里個世界${\displaystyle w}$丄有效（記作${\displaystyle {\mathcal {F}},w\models \varphi }$），當且僅當對任意${\displaystyle {\mathcal {F}}}$丄個賦值${\displaystyle V}$，儕有${\displaystyle ({\mathcal {F}},V),w\models \varphi }$。
• 一隻公式${\displaystyle \varphi }$勒框架${\displaystyle {\mathcal {F}}}$丄有效（記作${\displaystyle {\mathcal {F}}\models \varphi }$），當且僅當對任意${\displaystyle {\mathcal {F}}}$里個世界${\displaystyle w}$，儕有${\displaystyle {\mathcal {F}},w\models \varphi }$。
• 一隻公式${\displaystyle \varphi }$勒框架類${\displaystyle {\mathsf {F}}}$丄有效（記作${\displaystyle {\mathsf {F}}\models \varphi }$），當且僅當對任意${\displaystyle {\mathcal {F}}\in {\mathsf {F}}}$，儕有${\displaystyle {\mathcal {F}}\models \varphi }$。
• 一隻公式${\displaystyle \varphi }$有效（記作${\displaystyle \models \varphi }$），當且僅當伊勒所有框架個類丄有效。

鄰域語義

拓撲語義

代數語義

參考文獻

• Patrick Blackburn, Maarten de Rijke and Yde Venema（2001）．Modal Logic

，Cambridge Tracts in Theoretical Computer Science．Cambridge University Press．