相继式演算

相继式演算
术语名称	相继式演算
英语名称	sequent calculus

相继式演算是逻辑领域形式化公理系统的一种，属于 Gentzen 式系统（可以引入假设）。相继式演算系统中包括较多的推理规则，包括左规则和右规则，这些推理规则可以将一个可演绎关系（相继式）变换为另一个可演绎关系（相继式）。 相继式演算系统中每一行都是一个相继式，表示左侧公式可以演绎出右侧公式，并通过相继式变换得到新的相继式。

描述

相继式演算是推理系统的一类。 在相继式演算系统中，推理的每一行都是一个相继式。每个相继式代表一个可演绎关系，即可以通过左侧公式演绎出右侧公式。 与基于公式变形的推理系统的不同，这种演算方式中推理的对象是从相继式到相继式的变形，因而被称为相继式演算。

常见书写规则

属于相继式演算的推理方式有多种不同书写规则，常见主要形式有：

• Gentzen 式相继式演算

证明论
研究动机与结果	Gödel 完备性定理、 Hilbert 纲领、 Gödel 不完备定理
结构化证明	推理系统 形式化公理系统 （形式化、公理化）	Hilbert 风格/公理系统（在无前提的定理间推理）： Hilbert 表示
		Gentzen 风格-自然演绎系统（在有前提、有假设的结论间推理）： Gentzen 式自然演绎、 Fitch 式自然演绎、 Suppes–Lemmon 式自然演绎
		Gentzen 风格-相继式演算（在描述可演绎关系的元定理间推理）： Gentzen 式相继式演算
	证明、演绎	演绎、可演绎、证明、可证明
	命题、定理	命题、元命题、公理/公理模式、定理、元定理
	推理规则性质描述	保存真实性、保存重言性
	推理系统性质描述	可靠性、完备性/完全性、一致性、独立性
	重要元定理	演绎定理、切消定理（切割消除定理）
		（某种推理系统的）可靠性定理、完备性定理
序数分析	证明论序数
构造性证明 程序化证明	Curry–Howard 对应
	证明复杂度理论	证明复杂度