1 基本概念
1.1 序列的定义
序列演算中的“序列”通常写作 Γ ⊢ Δ，表示左侧一组前提与右侧一组结论之间的推理关系。直观上，它可以理解为“只要左边的假设都成立，则右边至少有一个结论成立”或“从这些前提能够推出这些结论”。
在不同逻辑系统中，Γ 与 Δ 的具体含义会有所差别。经典逻辑中，右侧允许多个公式共同出现；而在直觉主义逻辑中，右侧往往限制为单个公式，以体现更严格的构造性要求。
1.2 逻辑直觉与形式化表达
序列演算的核心直觉，是把推理过程拆解为可检验的局部步骤。与直接给出结论不同，它强调“从哪些前提、通过什么规则、得到怎样的结果”，因此更便于分析证明的内部结构。
这种形式化表达使逻辑关系能够被清晰编码为规则系统。每条规则都对应一种逻辑联结词或推理操作，从而把日常的“如果……那么……”式推断转化为严格的数学对象。
1.3 序列演算的研究对象
序列演算主要研究命题逻辑与谓词逻辑中的可证性问题，也常被用于考察证明的结构性质。它不仅关心某个命题是否可导出，还关心导出过程是否可以规范化、是否存在冗余步骤，以及证明是否可以被机械化处理。
因此，序列演算既是逻辑系统本身，也是证明论分析工具。它在讨论一致性、完备性、切断消去等问题时，往往能提供比其他体系更细致的视角。
2 历史发展
2.1 Gentzen 的提出
序列演算通常与 Gentzen 的工作联系在一起。20 世纪 30 年代，Gentzen 为研究逻辑证明结构而引入这一体系，提出了著名的 LK 与 LJ 形式，分别对应经典逻辑与直觉主义逻辑。
他所建立的方法具有里程碑意义，不仅给出了一种新的证明框架，还通过切断消去定理展示了该框架在元理论研究中的强大力量。
2.2 早期证明论背景
序列演算的出现，植根于早期证明论对形式推理的系统化探索。此前，希尔伯特式公理系统已在逻辑基础研究中占据重要位置，但其证明往往较为压缩，不利于分析推理细节。
与此同时，自然演绎等思想也在发展之中，推动人们思考“证明应当如何展开”这一问题。序列演算正是在这种背景下，将推理步骤显式化，并为后续的证明论研究提供了更可操作的框架。
2.3 后续发展与影响
在 Gentzen 之后，序列演算不断被推广到更多逻辑体系中，包括直觉主义逻辑、模态逻辑、线性逻辑以及各类子结构逻辑。其基本思想也被引入计算机科学，用于程序语义、自动推理和类型理论。
此外，序列演算对证明搜索和形式化验证产生了持久影响。很多现代逻辑工具在设计时，都会借鉴其“规则局部化、结构清晰、便于归纳分析”的特点。
3 形式结构
3.1 序列的组成部分
一个标准序列通常由左部、右部以及中间的推导符号构成。左部放置前提，右部放置结论，两侧可以是单个公式，也可以是若干公式的集合或多重集。
这种双侧结构使序列演算与一般的“前提推出结论”模式非常贴近，但又比口语化表达更精确，适合直接纳入形式证明。
3.1.1 左部与右部
左部常被视为待使用的假设，右部则代表目标结论或可接受的结果。在经典序列演算中，右部多结论的设计使得某些规则写法更对称，也更容易处理否定与析取等联结词。
从解释上看，左部与右部并非简单的“输入”和“输出”，而是分别承载可用信息与待证明信息的不同角色。正因如此，很多规则都体现出对两侧结构的精细操作。
3.1.2 公式集合与多重集
在形式化处理中，左侧和右侧常被表示为公式集合或多重集。若采用集合，重复公式会被自动忽略；若采用多重集，则同一公式可重复出现，以便更准确地描述结构规则的作用。
多重集表示在证明论中尤为常见，因为它能更细致地刻画收缩与弱化等操作。这样做有助于区分“公式是否存在”和“公式出现了几次”这两个层面的结构信息。
3.2 结构规则
结构规则处理的不是具体联结词，而是序列中前提与结论的排列、增删和重复问题。它们反映了逻辑系统对资源和假设的基本态度。
在传统序列演算中，结构规则往往包括交换、收缩和弱化等内容。不同逻辑对这些规则的允许程度并不相同，这也构成了各类子结构逻辑的重要来源。
3.2.1 交换规则
交换规则允许公式在同一侧自由调换顺序。由于经典逻辑中前提和结论通常只关心“有哪些公式”，而不关心“排列顺序如何”，因此交换规则一般被视为自然且基础的结构操作。
在采用序列或多重集表示时，交换规则有时可被隐含地吸收，不必单独写出；但在更严格的形式系统中，它仍然是说明两侧对称性的关键规则之一。
3.2.2 收缩规则
收缩规则用于消除重复公式，即把两个相同前提或结论压缩为一个。它体现了传统逻辑中“重复使用同一信息不会改变可证性”的观念。
这一规则在证明论中十分重要，因为它关系到证明长度与证明规范化。某些非经典逻辑会限制或取消收缩，从而形成更精细的资源敏感推理结构。
3.2.3 弱化规则
弱化规则允许在序列中加入额外公式，而不影响原有推理的有效性。换言之，即使某些前提或结论并未被实际使用，系统也允许它们存在。
弱化规则反映了经典逻辑中“多余信息无害”的特征。与收缩一样，它在子结构逻辑中也可能被削弱或移除，以表达更严格的推理约束。
3.3 逻辑规则
逻辑规则直接对应具体联结词的引入与消去，是序列演算的核心组成。它们决定了合取、析取、蕴含、否定等逻辑连接如何在序列中被处理。
通常，每个联结词都在左右两侧各有相应规则，分别描述该联结词作为前提或结论时如何分解。这样的设计使得证明步骤具有较强的局部可逆性。
3.3.1 合取规则
合取规则处理“且”关系。若要在右侧证明一个合取，通常需要分别证明其两个分量；若合取出现在左侧，则可以将其拆开，分别作为可用前提。
这类规则体现了合取的“同时成立”特征。它使证明过程能够把一个复合命题拆分为更简单的部分，从而逐步推进推导。
3.3.2 析取规则
析取规则对应“或”关系。右侧的析取通常意味着只需证明其中一个分支即可，而左侧的析取则往往要求对两个可能情形分别处理，再综合得到结论。
这种规则形式清楚地表达了析取的分情况推理特点。它是序列演算中最能体现“分支证明”风格的部分之一。
3.3.3 蕴含规则
蕴含规则反映“如果……那么……”的结构。通常，在右侧证明蕴含时，需要假设前件成立并在此基础上推出后件；而在左侧使用蕴含时，则要把它作为可触发的推理资源来处理。
蕴含规则在序列演算中往往与推导方向密切相关。它不仅表现命题之间的条件关系，也体现了证明中“引入假设—消解假设”的基本模式。
3.3.4 否定规则
否定规则与矛盾、不可兼容性相关。由于否定常可理解为“推出荒谬”或“排除某种情况”，它在序列演算中常通过与空结论或特殊符号的关系来表达。
在经典逻辑中，否定规则往往与双重否定、排中等性质相互配合；而在直觉主义逻辑中，否定的处理则更为谨慎，体现出构造性限制。
3.4 切断规则
切断规则是序列演算中最具代表性的规则之一。它允许通过一个中间公式把两个证明连接起来：先证明某公式，再在另一处使用它，从而得到最终结论。
尽管切断规则在构造证明时非常方便，但其存在并非必不可少。证明论的重要目标之一，就是说明切断可以被消去，而不损失可证性。
3.4.1 切断公式
切断公式是连接两个子证明的中介命题。它在前一段证明中被导出，在后一段证明中被当作桥梁使用，因此具有明显的“过渡”性质。
从证明结构上看，切断公式类似于临时引入的中间结论。它使证明更短、更容易组织，但也可能掩盖推理的真实复杂度。
3.4.2 切断规则的作用
切断规则的主要作用，是增强证明的组合能力。借助它，可以把复杂论证拆成若干局部片段，再通过中间命题拼接起来，十分适合人工构造证明。
不过，从元理论角度看，切断也意味着证明中可能存在冗余。切断消去定理表明，任何含切断的证明都可转化为不含切断的证明，这一结果对一致性和规范化分析尤其重要。
4 命题逻辑中的序列演算
4.1 经典命题逻辑
在经典命题逻辑中，序列演算通常采用双侧、多结论形式。这样的设置与经典逻辑的真值语义高度契合，能够较自然地表达排中律、双重否定等性质。
经典命题逻辑的序列演算体系通常较为对称，规则之间联系紧密。它不仅便于证明逻辑定理，也适合展示不同联结词之间的相互定义关系。
4.2 直觉主义命题逻辑
直觉主义命题逻辑在序列演算中通常采用单结论形式，强调构造性证明。右侧最多保留一个公式，从而避免经典逻辑中某些非构造性的推理方式。
这种限制使系统更贴近“如何构造出一个对象”的思想。也正因如此，直觉主义序列演算在类型论和程序语义中具有特别重要的地位。
4.3 单结论与多结论系统
单结论系统与多结论系统的差别，主要体现在右侧是否允许多个目标同时出现。前者结构更严格，适合构造性逻辑；后者表达力更强，也更适合经典逻辑。
两者并非简单的优劣之分，而是服务于不同的逻辑哲学与应用场景。多结论体系在对称性和推理表达上更自由，单结论体系则在证明解释上更精细。
5 谓词逻辑中的序列演算
5.1 全称量词规则
在谓词逻辑中，全称量词表示“对所有对象都成立”。其序列演算规则通常要求从一个带有任意性约束的实例出发，推出带全称量词的结论，或在左侧将全称命题实例化。
这些规则必须严守变量条件，以避免把某个特殊对象的性质误当成普遍规律。因而，全称量词的处理比命题联结词更依赖形式细节。
5.2 存在量词规则
存在量词表示“至少存在一个对象满足条件”。在序列演算中，右侧引入存在量词通常需要给出某个见证项，而左侧使用存在量词则往往通过引入一个新变量来展开。
存在量词的规则体现了“见证”思想。它与构造性证明关系密切，因为证明一个存在命题，通常意味着不仅要知道它成立，还要能指出具体对象。
5.3 变元与替换条件
谓词逻辑中的规则往往伴随着严格的变元与替换条件。某些变量必须保持任意性，某些项替换必须避免捕获，才能保证推理的正确性。
这些条件看似技术化，却是序列演算能够精确表达量词语义的关键。若忽视这些限制，规则可能在形式上成立，但在语义上会导致错误推导。
5.4 自由变量与束缚变量
自由变量是尚未被量词约束的变量，束缚变量则受量词作用范围限制。二者在序列演算中承担不同角色，前者常用于表示一般性，后者用于表达局部约束。
正确区分自由变量与束缚变量，有助于避免变量混淆和范围歧义。它也是理解量词规则、替换规则和证明可变性的基础。
6 元理论性质
6.1 一致性
一致性意味着系统不会同时推出命题及其否定，或不会推出某种形式的矛盾。对于序列演算而言，一致性通常可通过证明规则的结构性质间接建立。
由于序列演算强调推理步骤的透明性，因此它常被用于展示某些逻辑体系不可能导出荒谬，从而增强基础理论的可信度。
6.2 完备性
完备性指语义上成立的公式都能在系统中被证明。序列演算的规则设计往往与真值语义或模型论紧密配合，因此能够较自然地讨论完备性问题。
在证明论中，完备性不仅说明系统“够强”，也表明其形式规则与逻辑语义之间存在良好对应。这使序列演算兼具证明工具和语义桥梁的双重意义。
6.3 可判定性
可判定性关注的是：某个公式是否能够通过有限步骤判断可证与否。序列演算由于规则明确、结构清晰，常被用于构造决策过程或半决策过程。
不过，可判定性与所研究的逻辑系统密切相关。某些命题逻辑片段可以判定，而更强的谓词逻辑通常会失去这种简单性质。
6.4 切断消去
切断消去是序列演算最著名的元理论成果之一。它说明含有切断的证明可以转化为不含切断的证明，而证明的最终结论保持不变。
这一结果不仅具有技术价值，也具有方法论意义。它表明证明并不依赖“中间捷径”，而可以被改写为更直接、更规范的推导链条。
6.4.1 消去定理的意义
切断消去定理的意义，在于揭示证明的可分解性和内在纯净性。通过消去中间公式，证明中的依赖关系被进一步暴露出来，便于分析复杂度和结构层次。
该定理还常被用来支持一致性证明与子公式性质等结果。许多重要的证明论结论，都可以借助切断消去作为基础工具。
6.4.2 证明结构的规范化
切断消去使证明更接近规范形态。消去后的证明通常只使用子公式，从而减少了不必要的跳跃和外来引入的公式。
这种规范化不仅有助于理论分析，也有利于自动化处理。对于机器证明系统而言，越规范的证明结构，通常越便于搜索与检查。
7 与其他证明系统的关系
7.1 与自然演绎的比较
自然演绎强调从假设出发逐步构造结论，证明写法较接近日常数学叙述；序列演算则把证明组织成左右对称的推理片段，更强调结构分析。两者都适合表达逻辑证明，但风格不同。
一般而言，自然演绎更注重人的阅读直观，序列演算更利于元理论研究。尤其在切断消去、子公式性质和证明搜索方面，序列演算往往更具优势。
7.2 与希尔伯特系统的比较
希尔伯特系统以少量公理和推理规则为基础，形式简洁，但证明常较为浓缩。相比之下，序列演算把每一步都拆开，便于观察推理的内部机制。
因此，希尔伯特系统更像“压缩的证明语言”，而序列演算更像“展开的证明图谱”。前者适合公理化描述，后者则更适合结构化分析。
7.3 与真值语义的联系
序列演算与真值语义之间通常存在紧密对应关系。序列的左右两侧可以被解释为语义上的蕴含或满足关系，从而使证明规则反映逻辑联结词的真值条件。
这种联系使序列演算不仅是形式推导工具，也成为语义理解的桥梁。很多语义性质都可以借助序列系统中的规则来重述和证明。
8 应用
8.1 自动定理证明
序列演算为自动定理证明提供了清晰的规则基础。由于每条推理都被明确刻画，程序可以据此进行目标分解、分支搜索和证明检查。
在实际系统中，序列演算常与启发式搜索、剪枝策略结合使用。这样既能保留逻辑严谨性，也能提高证明发现的效率。
8.2 逻辑编程与程序验证
在逻辑编程中，推理与计算之间具有天然联系，序列演算可为此提供形式化背景。它帮助解释程序执行如何对应于逻辑导出过程。
在程序验证领域，序列演算则常用于描述前置条件、后置条件以及中间断言之间的关系。借助这一框架，可以更系统地检查程序是否满足规格要求。
8.3 类型系统与计算解释
序列演算与类型系统之间存在深刻联系。许多类型规则都可看作逻辑规则的对应物，从而形成“命题即类型、证明即程序”的解释路径。
在这一视角下，序列演算不仅说明某个命题能否推出，也说明某种程序结构是否可构造。它因此成为逻辑与计算之间的重要中介。
8.4 证明搜索与形式化验证
证明搜索任务依赖对规则空间的系统探索，而序列演算的局部规则结构非常适合这类任务。通过将证明拆为细粒度步骤，搜索过程可以更容易实施自动化控制。
在形式化验证中，序列演算也常作为基础推理框架，辅助检查模型、代码或数学命题的正确性。其严谨性和可机械处理性，使它在现代逻辑工具中占有重要位置。
9 代表性变体
9.1 经典序列演算
经典序列演算通常指 Gentzen 的 LK 系统及其相关变体。它采用多结论右侧结构，并允许较充分的结构规则，因此能够自然表达经典逻辑的推理特征。
该体系在表达力和对称性方面都较为强大，是研究经典逻辑证明论的基础模型之一。
9.2 直觉主义序列演算
直觉主义序列演算通常指 LJ 系统。它通过单结论限制，反映构造性逻辑的要求，并在证明解释上更贴近“构造一个对象”而非“排除所有反例”的思路。
这一变体在理论逻辑、类型论和计算解释中都极为重要，尤其适合与程序构造相联系的研究。
9.3 分层与扩展序列演算
分层与扩展序列演算是对基础体系的功能增强。它们可能加入模态算子、固定点机制、线性资源控制或其他专门规则，以适应不同逻辑场景。
这些扩展通常保持序列演算的核心风格，即通过明确规则描述推理。只是其研究对象从基本命题与谓词逻辑，进一步扩展到更复杂的形式系统。
9.4 相关的子结构逻辑体系
子结构逻辑体系是限制结构规则使用的一类逻辑。它们可能削弱交换、收缩或弱化中的某些规则，从而体现资源、顺序或相关性的不同约束。
这类体系与序列演算关系密切，因为序列结构本身就便于观察结构规则的可用范围。由此，序列演算成为研究非经典逻辑的重要通用框架。