Gentzen 式相继式演算

根岑式相继式演算
术语名称	根岑式相继式演算
英语名称	Gentzen's sequent calculus
别名	Gentzen's tree notation, Gentzen's system LK

Gentzen 式相继式演算(Gentzen's sequent calculus)是逻辑领域形式化公理系统中 Gentzen 式系统中自然演绎系统的一种。其中每行都是一个相继式，代表左侧的公式集合可演绎出右侧的公式集合，这些相继式通过树状的记号组织，以反映相继式间的变形关系。

说明： Gentzen 最初使用的表示逻辑联结词（包括零元的假）的记号与现今标准记号有差异，也有部分材料使用的记号与现代标准记号不同，以下均按照现代记号表示。

描述

以下是 [math]\displaystyle{ (p\rightarrow q)\land(\lnot r\rightarrow \lnot q)\rightarrow (p\rightarrow r) }[/math] 的一个证明。

[math]\displaystyle{ \dfrac{ \dfrac{ \dfrac{\dfrac{\dfrac{}{r\vdash r} I}{p,q,r\vdash r}WL}{p,q,\vdash r,\lnot r}\lnot R \quad \dfrac{\dfrac{\dfrac{\dfrac{}{q\vdash q}I}{q,\lnot q\vdash}\lnot L}{q, \lnot q\vdash r}WR}{p,q,\lnot q\vdash r}WL }{\lnot r \rightarrow \lnot q, p, q \vdash r}\rightarrow L \quad \dfrac{\dfrac{\dfrac{}{p \vdash p}I}{p \vdash p, r}WR}{\lnot r \rightarrow \lnot q, p \vdash p, r}WL }{ \dfrac{\dfrac{\dfrac{p \rightarrow q, \lnot r \rightarrow \lnot q, p \vdash r}{p \rightarrow q, \lnot r \rightarrow \lnot q \vdash p \rightarrow r}\rightarrow R}{(p \rightarrow q) \land (\lnot r \rightarrow \lnot q) \vdash p \rightarrow r}\wedge L}{\vdash (p \rightarrow q) \land (\lnot r \rightarrow \lnot q) \rightarrow (p \rightarrow r)}\rightarrow R }\rightarrow L }[/math]

以下是从 [math]\displaystyle{ p\rightarrow q }[/math] 到 [math]\displaystyle{ \lnot q \rightarrow \lnot p }[/math] 的一个演绎：

[math]\displaystyle{ \dfrac{ \dfrac{\dfrac{}{p\vdash p}I}{\lnot q, p \vdash p} WL \quad \dfrac{\dfrac{\dfrac{}{q\vdash q}I}{\lnot q,q,\vdash}\lnot L}{\lnot q,p,q\vdash} WL }{ \dfrac{\dfrac{p \rightarrow q, \lnot q, p \vdash }{p \rightarrow q, \lnot q \vdash \lnot p}\lnot R }{p \rightarrow q \vdash \lnot q\rightarrow \lnot p}\rightarrow R }\rightarrow L }[/math]

符号及术语说明

• 部分材料中，记号可能有微小差异，请以具体记号为准。
• 演绎过程中的每一个相继式称为一行(line)。
• 每条横线代表一个变形。横线右侧是使用的变形规则名称；上方有一个或多个相继式，相继式（及其证明）间用空白隔开；下方必须有且仅有一个相继式。
• 每行都是一个相继式。每个相继式是一个元命题，其语义为在元语言中声称这两组公式间具有左侧可演绎右侧的性质，即存在一个从左侧到右侧的演绎。更具体的语义如下：
  • 相继式代表左侧公式可以演绎出右侧公式。
  • 相继式左侧如果有多个公式，每个公式之间是合取关系，指在这些前提同时存在时可以演绎出结论。当左侧没有公式时，指哪怕没有任何前提也可以演绎出（证明出）这个结论。
  • 相继式右侧如果有多个公式，每个公式之间是析取关系，指可以前提演绎出这些结论中任意一个。考虑 [math]\displaystyle{ p\vdash p,q }[/math] ，也就是在右侧任意增加新的公式仍保证可演绎关系成立，因此当右侧没有公式时，表示其可以演绎出任意想要添加的公式，也就是当前给定的前提可以推出一切公式（参考爆炸原理）。
• 最后一行有的材料中有 [math]\displaystyle{ \blacksquare }[/math] （Q.E.D.）符号，代表证明结束，这一行是结论(conclusion)。也有的材料中不写这一符号。

特征

• 每行都是形式语言中的一个相继式。
• 每个变形上方可以有一个或多个相继式，但下方必须有且仅有一个相继式。换句话说，变形规则的结论必须是一个相继式。
  • 这使得证明可以被看成一棵树，每个行是一个结点，其根结点为证明的结论，每个结点的父节点为前提中含有这一行的变形规则的结论，子结点为变形得到这一行所使用的前提。
• 证明中的每行都在元语言中为真，也就是元命题“左侧可以演绎出右侧”总是一个元定理。

记号约定

公式描述

Gentzen 式相继式演算中使用的形式语言和命题语言、谓词语言的普遍定义稍有区别。这种形式语言中的公式包含：

• 原子命题（命题逻辑为命题变元，谓词逻辑为谓词和项构成的原子命题，其中谓词和项与一般定义一致）是公式。
• 假 [math]\displaystyle{ \bot }[/math] 是公式。
• 若 [math]\displaystyle{ \phi,\psi }[/math] 是公式，则 [math]\displaystyle{ (\phi\land\psi) }[/math] 、 [math]\displaystyle{ (\phi\lor\psi) }[/math] 、 [math]\displaystyle{ (\phi\rightarrow\psi) }[/math] 是公式（含逻辑联结词的公式）。
• （谓词逻辑）若 [math]\displaystyle{ x }[/math] 是个体变项， [math]\displaystyle{ \phi }[/math] 是公式，则 [math]\displaystyle{ \forall x \phi }[/math] 、 [math]\displaystyle{ \exists x \phi }[/math] 是公式（量化公式）。
• 其他形式不是公式。

并记缩写符号：

• [math]\displaystyle{ \lnot p := p\rightarrow \bot }[/math] 。
• [math]\displaystyle{ \top := \bot\rightarrow\bot }[/math] 。
• [math]\displaystyle{ \phi\leftrightarrow\psi := (\phi\rightarrow\psi)\land(\psi\rightarrow\phi) }[/math] 。

相继式描述

相继式从左到右依次由三部分组成：

• 假设(assumption)：零个至多个公式。若不止一个，用逗号隔开。
• 符号 [math]\displaystyle{ \vdash }[/math] (turnstile)
• 命题(proposition)：零个指多个公式。若不止一个，用逗号隔开。

命题描述

一个证明或一个需证明命题通常被写成相继式 [math]\displaystyle{ \Gamma, \Delta, \phi \vdash \Sigma, \Pi, \psi }[/math] 。

其中，小写希腊字母 [math]\displaystyle{ \phi,\psi }[/math] 表示单个公式，大写希腊字母 [math]\displaystyle{ \Gamma,\Delta }[/math] 与 [math]\displaystyle{ \Sigma,\Pi }[/math] 表示可空的公式集合。语义上可以理解为左侧的全部公式可演绎出右侧的公式之一。

变形规则描述

一个变形规则总是写成形式 [math]\displaystyle{ \dfrac{H_1\quad\cdots\quad H_n}{C}R }[/math] 。其中横线上方是前提，可以包括一个至多个相继式 [math]\displaystyle{ H_1,\cdots,H_n }[/math] ，若不止一个则多个前提间需用空白隔开，且多个前提间不要求顺序。横线下方是结论，只能有一个相继式 [math]\displaystyle{ C }[/math] 。横线右侧是变形规则的名称 [math]\displaystyle{ R }[/math] 。

每个变形规则都有一个名称。基础规则由逻辑联结词的左右侧规则构成，表示向相继式的左侧或右侧引入一个逻辑联结词所必需的符号。非基础规则也使用定理名称或缩写。具体符号不同材料中记号可能有区别。

变形规则的内容也写成横线上下的形式，如 [math]\displaystyle{ \dfrac{\Gamma,\phi\vdash\Delta\quad\Gamma,\psi\vdash\Delta}{\Gamma,\phi\lor\psi\vdash\Delta}\land L }[/math] 代表可以通过最后一行为 [math]\displaystyle{ \Gamma,\phi\vdash\Delta }[/math] 和 [math]\displaystyle{ \Gamma,\psi\vdash\Delta }[/math] 的两个可证明性的推理过程得到 [math]\displaystyle{ \Gamma,\phi\lor\psi\vdash\Delta }[/math] 的可证明性，规则名称为 [math]\displaystyle{ \land L }[/math] 。

可以简单地理解变形规则：如 [math]\displaystyle{ \dfrac{\Gamma,\phi\vdash\Delta\quad\Gamma,\psi\vdash\Delta}{\Gamma,\phi\lor\psi\vdash\Delta}\land L }[/math] 代表：我们可以通过 [math]\displaystyle{ \Gamma }[/math] 和 [math]\displaystyle{ \phi }[/math] 推出 [math]\displaystyle{ \Delta }[/math] 中的任意一个，同时可以通过 [math]\displaystyle{ \Gamma }[/math] 和 [math]\displaystyle{ \psi }[/math] 推出 [math]\displaystyle{ \Delta }[/math] 中的任意一个，那么除了 [math]\displaystyle{ \Gamma }[/math] 还给定了 [math]\displaystyle{ \phi\lor\psi }[/math] 时，一定还能推出 [math]\displaystyle{ \Delta }[/math] 中的任意一个。

若两个公式只有简写是否展开的差异，视为同一公式。对应地涉及公式对应相同的规则也是同一规则，其中前提不要求顺序。

变形规则

以下为常见的基本规则，且可能存在不必要的额外规则。变形规则一般集中于观察某一个或两个公式变形，此时其他公式被视为一个公式集，即下述 [math]\displaystyle{ \Gamma,\Delta }[/math] 等，也称为上下文(context)。

变形规则分为四部分：同一律公理模式、切消规则、结构规则（改变相继式结构，但与具体逻辑公式和逻辑符号无关）、逻辑规则（在公式内操纵逻辑符号，列举逻辑规则时通常忽略结构规则造成的影响）。

同一律公理模式

• 公理模式：同一律（I）：可以对任意公式 [math]\displaystyle{ \phi }[/math] 使用如下模式的公理。

[math]\displaystyle{ \dfrac{}{\phi\vdash\phi}I }[/math]

切削规则

• 切消定理（Cut）：对任意公式 [math]\displaystyle{ \phi,\psi }[/math] 及上下文 [math]\displaystyle{ \Gamma,\Delta,\Sigma,\Pi }[/math] 有：

[math]\displaystyle{ \dfrac{\Gamma\vdash\Delta,\phi \quad \phi,\Sigma\vdash\pi}{\Gamma,\Sigma\vdash\Delta,\Pi} }[/math]

结构规则

规则中 [math]\displaystyle{ \phi,\psi }[/math] 为任意公式， [math]\displaystyle{ \Gamma,\Delta,\Sigma,\Pi }[/math] 为上下文。

• 弱化(weakening, W)：可以在单侧任意添加新公式。

• 左侧弱化：左侧添加新附加前提不影响可演绎性

[math]\displaystyle{ \dfrac{\Gamma\vdash\Delta}{\Gamma,\phi\vdash\Delta}WL }[/math]

• 右侧弱化：右侧添加新结论选项不影响可演绎性

[math]\displaystyle{ \dfrac{\Gamma\vdash\Delta}{\Gamma\vdash\Delta,\phi}WR }[/math]

• 紧缩(contraction, C)：可以去除单侧的重复公式。

• 左侧紧缩：左侧去除重复前提不影响可演绎性

[math]\displaystyle{ \dfrac{\Gamma,\phi,\phi\vdash\Delta}{\Gamma,\phi\vdash\Delta}CL }[/math]

• 右侧紧缩：右侧去除重复结论选项不影响可演绎性

[math]\displaystyle{ \dfrac{\Gamma\vdash\Delta,\phi,\phi}{\Gamma\vdash\Delta,\phi}CR }[/math]

• 排列(permutation, P)：可以修改单侧多个公式的顺序。

• 左侧排列：前提的顺序不影响可演绎性

[math]\displaystyle{ \dfrac{\Gamma,\phi,\psi,\Gamma'\vdash\Delta}{\Gamma,\psi,\phi,\Gamma'\vdash\Delta}PL }[/math]

• 右侧排列：结论选项的顺序不影响可演绎性

[math]\displaystyle{ \dfrac{\Gamma\vdash\Delta,\phi,\psi,\Delta'}{\Gamma\vdash\Delta,\psi,\phi,\Delta'}PR }[/math]

这表明了序列中的重复、顺序都是不重要的，上下文无论描述为序列还是集合都无所谓。

命题逻辑

关于命题逻辑的 Gentzen 式相继式演算系统，公理两侧只能是相同联结词，或通过弱化加入无关的联结词，想要为相关的定理引入不同联结词，需要按左右包括不同规则。由于左侧公式间是合取的、右侧公式间是析取的，两侧的规则也有对应关系。

规则中 [math]\displaystyle{ \phi,\psi }[/math] 为任意公式， [math]\displaystyle{ \Gamma,\Delta,\Sigma,\Pi }[/math] 为上下文。

• 左侧合取和右侧析取，类似弱化规则附加新公式，

• 合取，左规则：

[math]\displaystyle{ \dfrac{\Gamma,\phi\vdash\Delta}{\Gamma,\phi\land\psi\vdash\Delta}\land L_1 }[/math] 、 [math]\displaystyle{ \dfrac{\Gamma,\psi\vdash\Delta}{\Gamma,\phi\land\psi\vdash\Delta}\land L_2 }[/math] 。

• 析取，右规则：

[math]\displaystyle{ \dfrac{\Gamma\vdash\Delta,\phi}{\Gamma\vdash\Delta,\phi\lor\psi}\lor R_1 }[/math] 、 [math]\displaystyle{ \dfrac{\Gamma\vdash\Delta,\psi}{\Gamma\vdash\Delta,\phi\lor\psi}\lor R_2 }[/math] 。

• 左侧析取、右侧合取，需要保持其他上下文不变时，两个规则分别可演绎

• 析取，左规则：

[math]\displaystyle{ \dfrac{\Gamma,\phi\vdash\Delta\quad\Gamma,\psi\vdash\Delta}{\Gamma,\phi\lor\psi\vdash\Delta}\lor L }[/math] 。

• 合取，右规则：

[math]\displaystyle{ \dfrac{\Gamma\vdash\Delta,\phi\quad\Gamma\vdash\Delta,\psi}{\Gamma\vdash\Delta,\phi\land\psi}\land R }[/math] 。

• 左侧的蕴涵否定和右侧的蕴涵，相当于将蕴含式的一条前提作为结论的前提得到新结论，或蕴含式的一个结论从前提中排除得到新前提

• 蕴涵的否定，左规则：

[math]\displaystyle{ \dfrac{\Gamma,\phi\vdash\Delta,\psi}{\Gamma,\phi\nrightarrow\psi\vdash \Delta}\nrightarrow L }[/math] 。

• 蕴涵，右规则：

[math]\displaystyle{ \dfrac{\Gamma,\phi\vdash\Delta,\psi}{\Gamma\vdash\Delta,\phi\rightarrow\psi}\rightarrow R }[/math] 。

• 左侧的蕴涵和右侧的蕴涵否定需要通过联系两个不同公式完成。

• 蕴涵，左规则：

[math]\displaystyle{ \dfrac{\Gamma\vdash\Delta,\phi\quad\Sigma,\psi\vdash\Pi}{\Gamma,\Sigma,\phi\rightarrow\psi\vdash\Delta,\Pi}\rightarrow L }[/math]

• 蕴涵否定，右规则：

[math]\displaystyle{ \dfrac{\Gamma\vdash\Delta,\phi\quad\Sigma,\psi\vdash\Pi}{\Gamma,\Sigma\vdash\Delta,\Pi,\phi\nrightarrow\psi}\nrightarrow R }[/math]

• 否定：从一侧到另一侧时增加否定

[math]\displaystyle{ \dfrac{\Gamma\vdash\Delta,\phi}{\Gamma,\lnot\phi\vdash\Delta} \lnot L }[/math] 、 [math]\displaystyle{ \dfrac{\Gamma,\phi\vdash\Delta}{\Gamma\vdash\Delta,\lnot\phi} \lnot R }[/math] 。

对于经典逻辑，这一系统称为 LK （Gentzen's system LK）。 对于非经典逻辑，可以进行一些调整。在直觉主义逻辑中，相继式的右侧只能出现至多一个公式，变换后右侧需要有多个公式的右规则都不再有效，这一系统称为 LJ （Gentzen's system LJ）。

有一些变体规则：

• 通过结构规则调整逻辑规则中描述的顺序。
• 含有假和真的公理 [math]\displaystyle{ \dfrac{}{\bot\vdash} }[/math] 、 [math]\displaystyle{ \dfrac{}{\vdash\top} }[/math] 或公理模式 [math]\displaystyle{ \dfrac{}{\Gamma,\bot\vdash \Delta} }[/math] 、 [math]\displaystyle{ \dfrac{}{\Gamma\vdash\Delta,\top} }[/math] 。

谓词逻辑

关于谓词逻辑的则增加以下4条规则。其中除要求 [math]\displaystyle{ \phi,\psi }[/math] 可以代入为任意公式外，还要求 [math]\displaystyle{ t }[/math] 是项且对 [math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/math] 中可自由代入， [math]\displaystyle{ a }[/math] 是个体变项且 [math]\displaystyle{ a }[/math] 对 [math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/math] 中可自由代入。有时也可以直接选取 [math]\displaystyle{ t=x }[/math] 或 [math]\displaystyle{ a=x }[/math] 进行个体变项代入，但是由于相同变元名称存在潜在的混淆问题，建议避免。

• 全称量词左规则：

[math]\displaystyle{ \dfrac{\Gamma,\phi[t/x]\vdash\Delta}{\Gamma,\forall x\phi\vdash\Delta}\forall L }[/math] 。

• 存在量词右规则：

[math]\displaystyle{ \dfrac{\Gamma\vdash\Delta,\phi[t/x]}{\Gamma\vdash\Delta,\exists x\phi}\exists R }[/math] 。

• 存在量词左规则：要求 [math]\displaystyle{ a }[/math] 不再出现在结论相继式中的任何位置。

[math]\displaystyle{ \dfrac{\Gamma,\phi[a/x]\vdash\Delta}{\Gamma,\exists x\phi\vdash\Delta}\exists L }[/math] 。

• 全称量词右规则：要求 [math]\displaystyle{ a }[/math] 不再出现在结论相继式中的任何位置。

[math]\displaystyle{ \dfrac{\Gamma\vdash\Delta,\phi[a/x]}{\Gamma\vdash\Delta,\forall x\phi}\forall R }[/math] 。

LJ 中也不能使用右侧有多个公式的 [math]\displaystyle{ \exists R,\forall R }[/math] 规则。

证明论
形式化公理系统（形式化、公理化）
推理系统	Hilbert 风格/公理系统（在无前提的定理间推理）： Hilbert 表示
	Gentzen 风格-自然演绎系统（在有前提、有假设的结论间推理）： Gentzen 式自然演绎、 Fitch 式自然演绎、 Suppes–Lemmon 式自然演绎
	Gentzen 风格-相继式演算（在描述可演绎关系的元定理间推理）： Gentzen 式相继式演算
证明、演绎	演绎、可演绎、证明、可证明
命题、定理	公理/公理模式、定理、元定理、变形规则
推理规则性质	保存真实性、保存重言性
公理系统性质	可靠性、完备性/完全性、一致性、独立性