1 基本概念
模态逻辑是研究“必然”“可能”等模态概念的形式系统，关注命题在不同情形下的成立方式。与只讨论“真”与“假”的经典逻辑相比，它进一步描述命题在可能状态中的变化，因此更适合分析推理中的不确定性、约束性与情境差异。
1.1 模态的含义
“模态”一词通常指事物成立的方式，而不只是事物是否成立。在逻辑中，模态常用来表达必然、可能、必须、允许、知道、将要发生等意义。不同学科中的模态含义并不完全相同，但都强调命题不仅有真假，还具有成立方式上的差别。
1.2 必然与可能
必然表示某命题在所有相关情形下都成立，可能则表示至少存在一个相关情形使其成立。二者构成模态逻辑最核心的一对概念。通常，必然性比可能性要求更强，而可能性则覆盖范围更广，常用于刻画“没有矛盾地成立”这一类判断。
1.3 模态算子
模态算子是模态逻辑中表示模态意义的符号，通常放在命题前面，用以改变该命题的解释方式。它们使逻辑语言不仅能够断言事实，还能描述事实在不同可能环境中的状态。
1.3.1 □算子
□通常读作“必然”，表示其后命题在相关世界中都为真。若一个命题被□修饰，往往意味着它具有不可反驳性或普遍成立性。在不同系统中，□的精确定义会依赖具体语义框架。
1.3.2 ◇算子
◇通常读作“可能”，表示其后命题在某个相关世界中为真。它常被理解为“至少有一种情形成立”。在形式上，◇与□彼此关联，二者常可通过对偶关系互相定义。
1.4 模态逻辑与经典逻辑的关系
模态逻辑建立在经典命题逻辑之上，保留了大量经典推理规律，同时引入新的模态表达。经典逻辑主要关心命题本身的真值，而模态逻辑还关心命题在不同可能情形中的地位。因而，模态逻辑可看作对经典逻辑的扩展，而非替代。
2 历史发展
模态思想在古代哲学中已有雏形，但作为严格形式系统的模态逻辑，主要形成于20世纪。它的发展经历了哲学讨论、符号化表达、语义模型建立以及多分支扩展等阶段。
2.1 早期思想来源
关于必然与可能的讨论可追溯到古希腊哲学与中世纪经院传统。早期思想家曾从存在、因果、时间和知识等角度探讨“能够如此”与“必须如此”的差别。这些讨论虽然尚未形成现代逻辑形式，却为后来的系统化研究提供了概念基础。
2.2 现代模态逻辑的兴起
现代模态逻辑的兴起与对模态命题形式化的需要密切相关。20世纪初，逻辑学家开始尝试用符号方法表示必然和可能。随后，模态逻辑逐渐从哲学争论中的辅助工具，发展为具有自身语法、语义和定理体系的独立分支。
2.3 主要学者与贡献
现代模态逻辑的发展离不开多位学者的推动。他们分别在形式化表达、语义解释、系统公理化以及应用拓展方面作出贡献。其中，Kripke语义的提出尤为重要，它为模态逻辑提供了直观而强大的解释框架，并显著提升了该领域的研究深度。
2.4 体系化与扩展
随着研究深入，模态逻辑不再局限于“必然/可能”这一对基本算子，而是扩展出时态、认识、义务、动态行为等多种体系。不同分支共享模态思想，但各自使用不同的语义结构与公理系统，从而形成一类内容丰富的逻辑家族。
3 形式语言
模态逻辑的形式语言是表达模态命题的基础，其结构与经典命题逻辑相近，但额外加入了模态算子。通过严格的语法规则，可以构造出各种复杂表达式，并对其进行形式分析。
3.1 语法结构
模态语言通常由命题变元、逻辑连接词和模态算子构成。它的语法简洁，却能表示丰富的推理关系。由于模态算子可以层层嵌套，语言具有较强的表达能力。
3.1.1 命题变元
命题变元用于表示基本陈述，如“p”“q”“r”等。它们本身不含模态含义，只是作为公式构造的起点。通过对命题变元施加连接词和模态算子，可以生成更复杂的逻辑表达式。
3.1.2 连接词
模态逻辑沿用经典逻辑中的基本连接词，如否定、合取、析取和蕴含。它们用于组合命题，形成复合结构。连接词与模态算子结合后，可以表达例如“必然不成立”“可能成立且另一命题也成立”等更细致的命题。
3.1.3 模态算子
模态算子是模态语言的标志性成分，决定了公式的模态解释方式。它们可单独作用于一个公式，也可与其他模态算子嵌套使用。不同系统中的模态算子形式可能一致，但语义和公理约束不尽相同。
3.2 公式的构造规则
模态公式通常由递归规则生成：命题变元是公式；若A是公式，则否定A也是公式；若A、B是公式，则A与B的各种连接式也是公式；若A是公式，则□A、◇A也都是公式。这样的定义确保语言结构清晰并可机械化处理。
3.3 复合模态表达式
复合模态表达式指多个模态算子嵌套或与连接词交织形成的公式，例如□◇p、◇□q等。这类表达式可用于描述更复杂的可能性链条，如“必然可能”或“可能必然”。其意义往往依赖于所采用的语义系统。
3.4 语言的表达能力
模态语言比经典命题语言更强，能够描述情境差异、状态可达性以及不同层面的约束。不过，它的表达能力也受到语义框架限制；在某些任务中，单纯的模态语言仍不足以细致刻画对象属性，因此需要与一阶逻辑或其他扩展系统结合。
4 语义学
模态逻辑的语义学旨在说明模态公式在何种条件下为真。与经典逻辑仅依赖单一真值赋值不同，模态逻辑通常引入多个“世界”或“状态”，从而解释命题在不同场景中的成立情况。
4.1 可能世界语义
可能世界语义把逻辑分析对象看作一组可能情形，每个情形都可以被赋予真假值。命题在某个世界中为真，不意味着它在所有世界中都为真。借助这种方法，必然与可能可以被清楚地区分，并能被形式化处理。
4.2 Kripke框架
Kripke框架是模态逻辑最常用的语义结构之一，通常由世界集合与可达关系构成。它把“从一个世界看向另一个世界”的关系显式表示出来，因此非常适合解释“必然”“可能”等概念。
4.2.1 世界集合
世界集合包含所有考虑中的可能状态。每个世界对应一种完整的情形描述。某命题在不同世界中的真假可能不同，这使得模态语义能够精细地区分局部成立与全局成立。
4.2.2 可达关系
可达关系描述一个世界能够“到达”哪些其他世界。它决定了某个模态公式的评价范围。例如，□A要求A在所有可达世界中成立，而◇A只要求存在至少一个可达世界使A成立。可达关系的性质会影响整个系统的逻辑特征。
4.3 真值赋值
真值赋值规定命题变元在各个世界中的真假情况。借助赋值函数，可以递归地确定复合公式在某一世界的真值。模态逻辑的关键不在于单点赋值，而在于不同世界之间的真值分布与联系。
4.4 语义解释规则
语义解释规则说明各类公式如何在世界中被判定为真。一般而言，命题变元依赖赋值；否定、合取、析取和蕴含按经典规则解释；而模态算子则依赖可达世界的真假情况。正是这些规则共同构成模态逻辑的模型理论。
5 公理系统
公理系统从符号推演角度刻画模态逻辑，借助公理与推理规则生成可证明公式。不同系统对应不同强度的模态假设，因此适用于不同语义背景。
5.1 基本公理
模态逻辑的基本公理通常包含经典命题逻辑公理，以及若干反映模态性质的特殊公理。例如，某些公理表达“如果必然蕴含成立，则蕴含关系本身也必然成立”。这些公理为系统提供了形式推导的起点。
5.2 推理规则
推理规则决定如何从已知公式推出新公式。它们是公理系统能否有效运作的核心组成部分。通过规则的重复使用，可以构造出完整的证明过程。
5.2.1 必然化规则
必然化规则通常表示：若某公式可证明，则其必然形式也可证明。它体现了“可证明性”与“必然性”之间的联系，但通常只能在特定前提下使用，以避免推出过强结论。
5.2.2 替换规则
替换规则允许在保持等值或可证等价的条件下，用一个公式替换另一个公式。它保证了系统的形式一致性，也使复杂公式的推导更为灵活。不同模态系统对替换的适用范围可能略有差异。
5.3 常见系统
模态逻辑存在多个经典系统，每个系统都由基础公理加上额外原则构成。它们之间强弱不同，适用的语义条件也不同。
5.3.1 K系统
K系统是最基础的模态系统之一，只加入最一般的分配类公理。它适用于最宽泛的Kripke框架，因此常作为其他系统的起点。许多更强系统都可看作在K系统上增加额外约束。
5.3.2 T系统
T系统在K系统基础上增加了反映“必然性包含真实性”的公理。直观上，它要求若某事必然成立，则它确实成立。这个系统常用于可达关系具有自反性质的语义场景。
5.3.3 S4系统
S4系统进一步强化了必然性的结构特征，常对应具有自反性与传递性的框架。它能够表达更稳定的必然性判断，因此在哲学与数学中都很常见。
5.3.4 S5系统
S5系统是较强的模态系统之一，通常用于处理“等价可达”的情形。它对可达关系的要求更严格，使得必然与可能之间的联系更加紧密。该系统常被用于讨论理想化知识、同一性或全局模态结构。
6 语义性质
模态逻辑的研究不仅关心公式是否可证，还关注语义与语法之间的对应关系。健全性、完备性、紧致性和可判定性是其中最重要的性质。
6.1 健全性
健全性表示：若某公式可由系统证明，则它在所有相应模型中都有效。换言之，语法推导不会推出语义上错误的结论。健全性保证了公理系统的可靠性。
6.2 完备性
完备性表示：若某公式在所有相应模型中都有效，则它可以在系统中证明。它说明公理系统足以捕捉语义所定义的全部有效内容。健全性与完备性结合起来，构成逻辑系统良好的理论基础。
6.3 紧致性
紧致性通常指：若一个公式集合的每个有限子集都可满足，则整个集合也可满足。这一性质在模型构造和理论分析中非常重要，常用于证明存在性结果。模态逻辑中的紧致性与所采用的系统和语义框架密切相关。
6.4 可判定性
可判定性是指存在算法能够判断某个公式是否可证或可满足。许多基本模态系统具有可判定性，这使它们在计算机科学中尤具价值。不过，随着语言和语义扩展，判定问题往往会变得更复杂。
7 典型分支
模态逻辑在发展中形成了多个重要分支，它们共享相似的形式方法，但关注对象不同。每个分支都将模态思想应用于特定领域。
7.1 时态逻辑
时态逻辑研究命题在时间中的变化，适合表达“过去发生了什么”“未来会发生什么”等内容。它把时间结构视为一种模态背景，是模态逻辑最活跃的分支之一。
7.1.1 过去与未来算子
过去算子用于表示某命题曾经成立，未来算子用于表示某命题将要成立。它们使逻辑表达能够跨越时间点，从而讨论事件顺序、持续性与先后关系。
7.1.2 线性时间与分支时间
线性时间观点把时间看作单一序列，而分支时间观点则认为未来可能分叉成多个路径。前者更适合描述确定演化，后者更适合描述选择与不确定性。两种模型影响时态逻辑的解释方式与证明性质。
7.2 知识逻辑
知识逻辑研究主体“知道什么”，用模态语言表示认知状态。它常用于分析信息、信念、推理和共享知识等问题。
7.2.1 个体知识
个体知识关注单个主体在某一时刻掌握的信息。若一个命题为该主体所知，通常意味着在其可区分的可能情形中该命题都成立。这个概念常用于形式化认知推理。
7.2.2 群体知识
群体知识讨论多个主体共同拥有的信息结构，包括“所有人都知道”“人人都知道人人都知道”等层次。它在多智能体系统中非常重要，能够刻画协同、协商与信息传播过程。
7.3 义务逻辑
义务逻辑研究“应当”“允许”“禁止”等规范性概念。它试图用形式逻辑表达规则、责任和约束，因此在规范推理中具有特殊地位。
7.3.1 规范表达
规范表达用于描述行为是否符合规则，例如“应当完成某事”或“必须避免某行为”。义务逻辑并不直接评价道德内容，而是分析规范结构与推导关系。
7.3.2 许可与禁止
许可与禁止是义务逻辑中的两类基本规范关系。许可表示某行为被规则允许，禁止则表示某行为不被允许。二者常可相互关联，并与义务概念一起构成规范体系。
7.4 动态模态逻辑
动态模态逻辑关注行动、程序或信息更新对命题真值的影响。它把“做了什么”纳入逻辑分析，适合描述变化过程。
7.4.1 程序模态
程序模态把程序当作模态算子的一部分，用于表示执行某程序后某命题是否成立。它常见于程序逻辑与验证理论中，能够刻画算法执行结果。
7.4.2 动作与更新
动作与更新强调外部操作对系统状态的改变，如信息发布、状态转移或知识修正。动态模态逻辑借助这一思想，把静态命题与动态过程联系起来。
8 重要概念与定理
模态逻辑的理论核心由若干基本概念和经典定理构成，这些内容支撑了其语义解释、系统构造与应用分析。
8.1 必然命题与可能命题
必然命题指在所有相关世界中都成立的命题，可能命题则指在至少一个相关世界中成立的命题。它们并非简单的日常语义，而是严格依赖所选框架的形式概念。二者之间通过对偶关系相互联系。
8.2 有效式与可满足式
有效式是指在所有模型和所有世界中都成立的公式；可满足式则是指至少存在一个模型和一个世界使其成立。前者体现普遍真理，后者体现存在可能。很多逻辑问题都可转化为判断这两类性质。
8.3 克里普克完备性定理
克里普克完备性定理说明，某些模态系统的语法可证明性与其Kripke语义有效性完全一致。这一定理奠定了模态逻辑现代研究的基础，使形式证明与模型语义能够相互印证。
8.4 对偶性原理
对偶性原理是模态逻辑中的基本关系，通常表现为“必然”和“可能”之间的互定义关系。通过否定符号，可以把□与◇转换，反映二者在逻辑上的互补性。这一原理简化了公式变形和定理证明。
8.5 模态深度与嵌套结构
模态深度指公式中模态算子嵌套的层数。深度越高，表达的情境层级越复杂。嵌套结构常用于描述多层推理，例如“某事可能是必然的”或“知道自己知道某事”，因此在理论分析中很重要。
9 应用领域
模态逻辑的应用范围较广，既包括理论研究，也包括工程实践。由于它擅长处理可能性、时间、知识和规范等概念，因此在多个学科中都具有工具价值。
9.1 哲学分析
在哲学中，模态逻辑常用于讨论必然性、可能性、同一性、反事实条件句等问题。它为抽象哲学论证提供了清晰的形式框架，使许多概念争论能够被精确化。
9.2 数学基础研究
在数学基础研究中，模态逻辑可用于探讨公理系统、结构性质和证明关系。它与集合论、证明论以及模型论等领域存在密切联系，并常被用于分析数学命题的成立方式。
9.3 计算机科学
模态逻辑在计算机科学中用途广泛，尤其适合描述状态系统、程序行为和信息变化。它为形式验证、系统设计和推理自动化提供了重要语言。
9.3.1 程序验证
程序验证关注程序是否满足预定规范。动态模态逻辑和相关形式系统常用于描述程序执行前后的性质，从而帮助检验程序正确性。
9.3.2 形式化推理
形式化推理强调以机器可处理的方式表达与证明结论。模态逻辑的精确定义和可判定片段，使其成为自动推理系统中的常用工具之一。
9.4 语言学
语言学中，模态逻辑可用于分析句子中的情态意义，例如“必须”“可以”“可能”等表达。它帮助研究语义结构、句法对应关系以及语用层面的解释差异。
9.5 人工智能
人工智能中，模态逻辑常用于表示知识状态、行动计划和系统约束。它有助于构建多智能体推理模型，也可用于表示决策过程中的条件依赖与不确定性。
10 相关概念
模态逻辑与若干邻近领域存在紧密联系，这些概念在语义结构、表达目标或应用方式上相互交叉。
10.1 时间逻辑
时间逻辑是研究时间结构上的模态系统，强调过去、现在与未来之间的关系。它通常被看作模态逻辑的重要分支之一。
10.2 认识论逻辑
认识论逻辑研究知识、信念和信息可得性，与知识逻辑关系密切。它关心主体如何根据可区分情形形成判断。
10.3 多值逻辑
多值逻辑允许命题具有两个以上的真值。虽然它与模态逻辑的研究重点不同，但二者都试图扩展经典逻辑的表达范围，因此在某些理论和应用中可相互联系。
10.4 一阶模态逻辑
一阶模态逻辑把量词引入模态框架，能够讨论对象在不同可能世界中的性质。它比命题模态逻辑更强，但语义和推理也更复杂。
10.5 邻域语义
邻域语义是模态逻辑的一种替代语义框架，不完全依赖可达关系，而是通过邻域集合解释模态算子。它适合处理某些标准Kripke语义难以覆盖的系统。
11 研究问题与发展方向
模态逻辑仍在持续发展，新的研究往往围绕表达能力、计算复杂性、定义性以及语义扩展展开。不同方向之间既有理论联系，也面临各自的技术挑战。
11.1 表达能力比较
表达能力比较关注不同模态系统能否描述相同类型的结构与性质。研究者常通过对照定理、翻译方法和等价变换来判断系统之间的强弱差异。
11.2 复杂度问题
复杂度问题主要研究可满足性、有效性和证明搜索的计算难度。随着模态算子、量词或动态成分的加入，问题复杂度通常显著上升，因此这是理论与应用都非常关心的方向。
11.3 公理可定义性
公理可定义性探讨某些语义性质是否可以通过有限公理组准确刻画。这个问题关系到系统是否能够简洁地表达所需框架特征，也是模态逻辑元理论中的重要主题。
11.4 新型语义框架
随着应用场景增多，研究者不断提出新的语义框架，如邻域语义、双模态语义和更复杂的结构化模型。新框架的目标通常是提升表达力、适应特殊应用或解释传统框架难以处理的现象。