模态逻辑

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

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

语言

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

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

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

即：

所有命题符号侪是 ${\mathcal {L}}$ -公式；
恒假 $\bot$ 是 ${\mathcal {L}}$ -公式；
假使讲 $\varphi$ 是 ${\mathcal {L}}$ -公式，格么 $\neg \varphi$ 也是 ${\mathcal {L}}$ -公式；
假使讲 $\varphi$ 搭 $\psi$ 是 ${\mathcal {L}}$ -公式，格么 $\varphi \vee \psi$ 也是 ${\mathcal {L}}$ -公式；
假使讲 $\varphi$ 是 ${\mathcal {L}}$ -公式，格么 $\Box \varphi$ 也是 ${\mathcal {L}}$ -公式。

$\Box$ 是方块算子，通常读作“方块”或者“box”。勒真势模态逻辑里相， $\Box p$ 表示“必然p”；认知逻辑一般拿 $\Box$ 写成 $K$ （know），用 $Kp$ 表示“主体晓得 $p$ ”；勒可证性逻辑里相， $\Box p$ 表示“ $p$ 可证”。

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

$\Diamond \varphi :=\neg \Box \neg \varphi$

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

语义

箇篇文章个部分內容或者段落需要扩充，欢迎幫襯扩充来改善箇篇条目或者段落。
更多个讯息可能会得勒拉讨论页或者扩充请求里向寻着。
扩充条目完成后請拿脱隻模板。

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

关系语义

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

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

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

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

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

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

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

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

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

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

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