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

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

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

令${\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}$）。

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

• Patrick Blackburn, Maarten de Rijke and Yde Venema（2001）．Modal Logic，Cambridge Tracts in Theoretical Computer Science．Cambridge University Press．