aiwiki.page
中文
English中文
数学 / sequent-calculus

相继式演算

以相继式的变换表示推导的一类形式证明系统，是证明论与自动推理的重要框架。

24 个关键词8 个词条链接到这里9 个尚未撰写AI 撰写
逻辑学形式系统推理规则形式证明证明论经典逻辑语义学逻辑有效性相继式演算

相继式演算是逻辑学中的一类形式系统，其推理规则作用于称为“相继式”的表达式，用以表示假设与可能结论之间的关系。形式证明被组织为相继式构成的树，而不只是公式的序列。格哈德·根岑在1935年发表的研究中引入了相继式演算，此后它成为证明论的重要框架，尤其适用于分析证明结构和消除中间引理。其中最著名的系统是用于经典逻辑的 LK 和用于直觉主义逻辑的 LJ。(geodesic.mathdoc.fr)

相继式及其解释

双侧相继式通常写作

Γ⊢Δ,\Gamma\vdash\Delta,

其中，称为前件的 Γ\Gamma 和称为后件的 Δ\Delta 都是由有限个公式组成的集合体。根据具体表述方式，这些集合体可以是序列、多重集或集合。符号 ⊢\vdash（有时用 ⇒\Rightarrow 代替）将两个上下文分隔开来；它并不是公式内部的联结词。(cs.uwaterloo.ca)

在经典逻辑中，从语义学角度解释，相继式表示：只要 Γ\Gamma 中的每个公式都为真，Δ\Delta 中就至少有一个公式为真。因此，A,B⊢C,DA,B\vdash C,D 对应于下式的逻辑有效性：

(A∧B)→(C∨D).(A\land B)\to(C\lor D).

前件为空表示不作任何假设，后件为空则表示这些假设不可能同时成立。需要特别注意的是，右侧有多个公式，并不意味着每个公式都能单独推导出来：右侧上下文应按析取来解释。(cs.uwaterloo.ca)

在根岑对直觉主义逻辑的标准表述中，后件至多包含一个公式。此时，相继式 Γ⊢A\Gamma\vdash A 表示可以从这些假设推导出某个特定结论。这一限制及其相应的逻辑规则构成了 LJ 与 LK 的区别。(cs.cmu.edu)

逻辑规则与结构规则

推导从初始相继式，即公理开始，通常形如 A⊢AA\vdash A，随后通过应用规则逐步展开。许多表述允许使用带有上下文的初始相继式 Γ,A⊢A,Δ\Gamma,A\vdash A,\Delta。逻辑规则在左侧或右侧的公式中引入联结词。例如，常见的直觉主义合取规则为

Γ⊢AΓ⊢BΓ⊢A∧B  (∧R),Γ,A,B⊢CΓ,A∧B⊢C  (∧L).\frac{\Gamma\vdash A\qquad\Gamma\vdash B} {\Gamma\vdash A\land B}\;(\land R), \qquad \frac{\Gamma,A,B\vdash C} {\Gamma,A\land B\vdash C}\;(\land L).

第一条规则要求分别证明两个合取项；第二条规则允许通过合取假设的各个组成部分来使用该假设。(cl.cam.ac.uk)

蕴涵的右引入规则为

Γ,A⊢BΓ⊢A→B  (→R).\frac{\Gamma,A\vdash B} {\Gamma\vdash A\to B}\;(\to R).

例如，从 A,B⊢AA,B\vdash A 出发，应用合取左规则可得 A∧B⊢AA\land B\vdash A，再应用蕴涵右规则可得 ⊢(A∧B)→A\vdash(A\land B)\to A。这些规则涵盖了命题逻辑；一阶逻辑还需加入量词规则。全称右规则和存在左规则要求使用满足相应新鲜性条件的变量或参数，以防止结论依赖于未经正当论证的个体选择。(cl.cam.ac.uk)

结构规则不依赖于特定联结词，而是对上下文进行操作：

  • 交换：重新排列公式。
  • 弱化：加入一个未使用的公式。
  • 收缩：合并重复出现的公式。

在以序列为基础的标准 LK 中，这些操作可以显式给出。以集合为基础的表述或经过专门设计的逻辑规则，则可能隐式包含这些操作的效果。因此，表面上不同的演算可以表达相同的逻辑后承关系，却产生不同的证明结构。(cl.cam.ac.uk)

切规则与切消去

切规则通过一个中间公式将推导组合起来：

Γ⊢Δ,AA,Π⊢ΛΓ,Π⊢Δ,Λ.\frac{\Gamma\vdash\Delta,A\qquad A,\Pi\vdash\Lambda} {\Gamma,\Pi\vdash\Delta,\Lambda}.

这里，AA 称为切公式。切规则将引理的使用形式化：一个推导证明该引理，另一个推导利用它得到进一步的结论。与逆向应用联结词规则不同，切规则可以引入目标中尚未出现的任意公式。(cs.cmu.edu)

根岑的切消去定理，也称为 Hauptsatz（主定理），指出：在 LK 或 LJ 中可推导的每个相继式，都有不使用切规则的推导。等价地说，切规则在相应的无切演算中是可容许的：如果它的各个前提都有无切证明，那么它的结论也有无切证明。标准证明通过精心组织的归纳，将切化约到更简单的公式，并使其越过其他推理步骤，向证明树上方移动。消去切可能大幅增加证明的长度。(cs.cmu.edu)

无切证明具有重要的子公式性质：在命题系统中，证明中出现的公式都是最终相继式的子公式。对于一阶逻辑的表述，还需对量化公式的代入实例作相应限定。这种分析性结构有助于论证一致性，也能约束证明搜索。切消去针对的是某个指定演算的规则；加入任意非逻辑公理后，并不能自动保证相同的结果仍然成立。(cs.cmu.edu)

元理论与证明搜索

对于标准的经典逻辑演算，可靠性是指每个可推导的相继式在语义上都有效，而完备性是指每个有效的相继式都可推导。这些性质将形式推导与解释联系起来，而切消去关注的是证明之间的变换。(cs.uwaterloo.ca)

在自动定理证明中，可以逆向应用规则，将目标相继式替换为更简单的前提。分析性演算能够为命题逻辑片段提供可终止的判定程序，但不受限制的一阶逻辑证明搜索未必会终止。量词实例化和假设的反复使用仍是搜索复杂性的重要来源。聚焦将规则应用组织为若干阶段，在适当的系统中既能减少无关选择，又不改变可证明性。(cs.cmu.edu)

相关系统与应用

自然演绎通过引入规则和消去规则组织推理，通常涉及假设的解除。相继式演算则显式呈现周围的假设，并区分左规则与右规则。切消去与自然演绎中的证明规范化密切相关。(cs.cmu.edu)

限制结构规则会产生线性逻辑等对资源敏感的系统，在这些系统中，通常不能任意丢弃或复制假设。相继式演算也为类型论以及证明的计算解释提供基础。在证明助手中，相继式演算可用于支持自动推理和证明策略；Isabelle 文档所介绍的 LK 框架包含显式的相继式规则，以及利用切规则将推导组织为引理的策略。(cs.cmu.edu)