望“模态逻辑”个源码

'''模态逻辑'''是现代[[逻辑]]个一个主要分支，用来刻画搭模态搭界个推理。所谓模态指个是一只[[命题]]为真个方式。常见个模态包括[[形而上学]]可能性（可能搭必然，如“苏格拉底'''可能'''是哲学家”）、认知（信念搭知识，如“我'''晓得'''苏格拉底是哲学家）、道义（许可搭义务，如“侬'''应该'''遵纪守法”）、时态（过去、现在搭未来，如“我'''过去'''是学生”）等等。相对应个，就有[[真势模态逻辑]]、[[认知逻辑]]、[[道义逻辑]]、[[时态逻辑]]等模态逻辑分支。

模态逻辑要用到[[逻辑运算符]]，勒[[哲学]]、[[数学]]、[[语言学]]、[[计算机科学]]里向侪有蛮多应用个。相比[[一阶逻辑]]搭[[二阶逻辑]]，模态逻辑常常好勒表达力搭[[计算复杂性]]之间取得更好个平衡，故咾来勒计算机个应用弗少。

== 语言 ==
模态逻辑用个[[形式语言]]通常是勒[[命题逻辑]]或者[[一阶逻辑]]个语言个基础丄加上[[模态算子]]个产物。

令<math>\mathbf{Prop}</math>为一只[[可数无穷]]个命题符号集合。'''基本模态语言'''<math>\mathcal{L}</math>个公式由以下[[BNF范式]]生成：

<math>\varphi ::= p \in \mathbf{Prop} \mid \bot \mid \neg \varphi \mid \varphi \vee \varphi \mid \Box \varphi</math>

即：

# 所有命题符号侪是<math>\mathcal{L}</math>-公式；
# 恒假<math>\bot</math>是<math>\mathcal{L}</math>-公式；
# 假使讲<math>\varphi</math>是<math>\mathcal{L}</math>-公式，格么<math>\neg \varphi</math>也是<math>\mathcal{L}</math>-公式；
# 假使讲<math>\varphi</math>搭<math>\psi</math>是<math>\mathcal{L}</math>-公式，格么<math>\varphi \vee \psi</math>也是<math>\mathcal{L}</math>-公式；
# 假使讲<math>\varphi</math>是<math>\mathcal{L}</math>-公式，格么<math>\Box \varphi</math>也是<math>\mathcal{L}</math>-公式。
<math>\Box</math>是方块算子，通常读作“方块”或者“box”。勒[[真势模态逻辑]]里相，<math>\Box p</math>表示“必然p”；[[认知逻辑]]一般拿<math>\Box</math>写成<math>K</math>（know），用<math>Kp</math>表示“主体晓得<math>p</math>”；勒[[可证性逻辑]]里相，<math>\Box p</math>表示“<math>p</math>可证”。

就像[[一阶逻辑]]里相存在量词<math>\exists</math>拨定义成全称量词<math>\forall</math>个[[对偶]]，基本模态逻辑通过下头个公式定义<math>\Box</math>个对偶算子<math>\Diamond</math>：

<math>\Diamond \varphi := \neg \Box \neg \varphi</math>

<math>\Diamond</math>通常读作“菱形”或者“diamond”。[[真势模态逻辑]]用<math>\Diamond p</math>表示“可能p”，而<math>\Box p</math>（必然<math>p</math>）就逻辑等价于<math>\neg \Diamond \neg p</math>（弗可能非<math>p</math>）。

== 语义 ==
{{expand}}
模态逻辑个语义主要有关系语义（又叫[[克里普克]]语义）、邻域语义、拓扑语义搭仔代数语义四种。其中，关系语义最直观，邻域语义搭拓扑语义是关系语义个一般化，代数语义最抽象。

=== 关系语义 ===
关系语义基于关系结构。[[关系结构]]是由论域搭伊上头个关系组成个元组。关系结构勒数学里相邪气常见，几乎所有阿拉熟悉个数学结构（譬如讲[[代数]]结构、[[图论|图]]）侪可以拨当成关系结构；计算机科学、哲学、语言学、经济学等学科也常常用着关系结构。（Blackburn, de Rijke and Venema, 2001）

勒关系语义下头，基本模态逻辑个'''框架'''就是一只关系结构<math>\mathcal{F} = (W, R)</math>，其中

# '''论域'''<math>W</math>是一只由'''（可能）世界'''组成个非空集合，
# '''可及关系'''（或可通达关系，accessibility relation）<math>R \subseteq W \times W</math>是<math>W</math>上头个一只二元关系。

基本模态逻辑个'''模型'''是一只三元组<math>\mathcal{M} = (W, R, V)</math>，其中

# <math>(W, R)</math>是基本模态逻辑个框架，
# <math>V : \mathbf{Prop} \to \mathcal{P}(W)</math>是一只'''赋值'''，伊搭每只命题变元<math>p</math>赋由所有<math>p</math>勒里相为真个世界组成个集合。

阿拉下头定义哪能勒基本模态逻辑模型上头解释基本模态语言公式。

设<math>\mathcal{M} = (W, R, V)</math>是一只基本模态逻辑模型，<math>w \in W</math>。阿拉搿能递归定义公式<math>\varphi</math>勒<math>\mathcal{M}</math>里<math>w</math>丄拨'''满足'''（或者为'''真'''）'''：'''

* <math>\mathcal{M}, w \models p</math>  当且仅当  <math>w \in V(p)</math>，其中<math>p \in \mathbf{Prop}</math>
* <math>\mathcal{M}, w \models \bot</math>  永远弗会
* <math>\mathcal{M}, w \models \neg \varphi</math>  当且仅当  <math>\mathcal{M}, w \not\models \varphi</math>
* <math>\mathcal{M}, w \models \varphi \vee \psi</math>  当且仅当  <math>\mathcal{M}, w \models \varphi</math>或者<math>\mathcal{M}, w \models \psi</math>

格么<math>\mathcal{M}, w \models \Diamond \varphi</math>就当且仅当存在<math>v \in W</math>使得<math>Rwv</math>并且<math>\mathcal{M}, v \models \varphi</math>。

阿拉晓得，逻辑个一个主要研究对象是[[有效性|有效]]个推理。一只公式勒一只框架丄有效，意思是讲无论侬往搿只框架上头加啥个赋值，勒嗨所形成个模型里相，搿只公式侪是真个。严格定义如下：

* 一只公式<math>\varphi</math>勒框架<math>\mathcal{F}</math>里个世界<math>w</math>丄'''有效'''（记作<math>\mathcal{F}, w\models \varphi</math>），当且仅当对任意<math>\mathcal{F}</math>丄个赋值<math>V</math>，侪有<math>(\mathcal{F}, V), w \models \varphi</math>。
* 一只公式<math>\varphi</math>勒框架<math>\mathcal{F}</math>丄'''有效'''（记作<math>\mathcal{F}\models \varphi</math>），当且仅当对任意<math>\mathcal{F}</math>里个世界<math>w</math>，侪有<math>\mathcal{F}, w \models \varphi</math>。
* 一只公式<math>\varphi</math>勒框架类<math>\mathsf{F}</math>丄'''有效'''（记作<math>\mathsf{F}\models \varphi</math>），当且仅当对任意<math>\mathcal{F} \in \mathsf{F}</math>，侪有<math>\mathcal{F} \models \varphi</math>。
* 一只公式<math>\varphi</math>'''有效'''（记作<math>\models \varphi</math>），当且仅当伊勒所有框架个类丄有效。

=== 邻域语义 ===

=== 拓扑语义 ===

=== 代数语义 ===

== 参考文献 ==
* {{cite book |author= Patrick Blackburn, Maarten de Rijke and Yde Venema |title = Modal Logic |year=2001 |series= Cambridge Tracts in Theoretical Computer Science |publisher=Cambridge University Press }}
[[Category:逻辑]]