相继式演算

维基百科，自由的百科全书

在证明论和数理逻辑中，相继式演算是众所周知的一阶逻辑(和作为它的特殊情况的命题逻辑)的演绎系统。这个系统也叫做 LK 系统，用以区别于后来建立的有时也叫做相继式演算的类似风格的各种其他系统。另一个给这种系统的术语是 Gentzen 系统。

因为相继式演算和与它们有关的一般概念对于整个证明论和数理逻辑领域都非常重要，下面将非常详细的解说 LK 系统。假定你熟悉谓词逻辑(特别是它的语法结构)的基本概念。

[编辑] LK 系统

在这个演算中的(形式)证明是一序列的相继式，这个的每个相继式使用下面的推理规则之一而推导自更早出现的相继式。

[编辑] 历史

相继式演算 LK 由 Gerhard Gentzen 介入为研究自然演绎的工具。它已经变成构造逻辑推导的非常有用的演算。它的名字得来自德语的 Logischer Kalkül，意思是"逻辑演算"。相继式演算是关于这个主题的很多研究所选择的方法。

[编辑] LK 系统的推理规则

将要使用下列符号:

$A$ 和 $B$ 指示一阶谓词逻辑的公式(你也可以把它限制为命题逻辑)，
$Γ$ 、 $Δ$ 、 $Σ$ 和 $Π$ 是有限的(可能为空)公式序列，也叫做上下文，
$t$ 指示一个任意的项，
$A [t]$ 指示一个公式 $A$ ，在其中项 $t$ 的某个出现是我们感兴趣的
$A [s / t]$ 指示把在 $A [t]$ 中的 $t$ 的指定出现代换为项 $s$ ，
$x$ 和 $y$ 指示变量，
一个变量被称为在一个公式中自由出现，如果它只出现于不在量词 $\forall$ 或 $\exist$ 作用域内的公式中，
$W L$ 和 $W R$ 表示弱化左/右， $C L$ 和 $C R$ 表示紧缩左/右，而 $P L$ 和 $P R$ 表示排列左/右。

公理:	切:
$\cfrac{\qquad }{ A \vdash A} \quad (I)$	$\cfrac{\Gamma \vdash A, \Delta \qquad \Sigma, A \vdash \Pi} {\Gamma, \Sigma \vdash \Delta, \Pi} \quad (\mathit{Cut})$

左逻辑规则:	右逻辑规则:
$\cfrac{\Gamma, A \vdash \Delta} {\Gamma, A \and B \vdash \Delta} \quad ({\and}L_1)$	$\cfrac{\Gamma \vdash A, \Delta}{\Gamma \vdash A \or B, \Delta} \quad ({\or}R_1)$
$\cfrac{\Gamma, B \vdash \Delta}{\Gamma, A \and B \vdash \Delta} \quad ({\and}L_2)$	$\cfrac{\Gamma \vdash B, \Delta}{\Gamma \vdash A \or B, \Delta} \quad ({\or}R_2)$
$\cfrac{\Gamma, A \vdash \Delta \qquad \Sigma, B \vdash \Pi}{\Gamma, \Sigma, A \or B \vdash \Delta, \Pi} \quad ({\or}L)$	$\cfrac{\Gamma \vdash A, \Delta \qquad \Sigma \vdash B, \Pi}{\Gamma, \Sigma \vdash A \and B, \Delta, \Pi} \quad ({\and}R)$
$\cfrac{\Gamma \vdash A, \Delta}{\Gamma, \lnot A \vdash \Delta} \quad ({\lnot}L)$	$\cfrac{\Gamma, A \vdash \Delta}{\Gamma \vdash \lnot A, \Delta} \quad ({\lnot}R)$
$\cfrac{\Gamma \vdash A, \Delta \qquad \Sigma, B \vdash \Pi}{\Gamma, \Sigma, A\rightarrow B \vdash \Delta, \Pi} \quad ({\rightarrow }L)$	$\cfrac{\Gamma, A \vdash B, \Delta}{\Gamma \vdash A \rightarrow B, \Delta} \quad ({\rightarrow}R)$
$\cfrac{\Gamma, A[t] \vdash \Delta}{\Gamma, \forall x A[x/t] \vdash \Delta} \quad ({\forall}L)$	$\cfrac{\Gamma \vdash A[t], \Delta}{\Gamma \vdash \exist x A[x/t], \Delta} \quad ({\exist}R)$
$\cfrac{\Gamma, A[y] \vdash \Delta}{\Gamma, \exist x A[x/y] \vdash \Delta} \quad ({\exist}L)$	$\cfrac{\Gamma \vdash A[y], \Delta}{\Gamma \vdash \forall x A[x/y], \Delta} \quad ({\forall}R)$

限制: 在规则 (∀R) 和 (∃L) 中，变量 y 一定不能在 Γ、A[x/y] 或 Δ 中自由出现。

左结构规则:	右结构规则:
$\cfrac{\Gamma \vdash \Delta}{\Gamma, A \vdash \Delta} \quad (\mathit{WL})$	$\cfrac{\Gamma \vdash \Delta}{\Gamma \vdash A, \Delta} \quad (\mathit{WR})$
$\cfrac{\Gamma, A, A \vdash \Delta}{\Gamma, A \vdash \Delta} \quad (\mathit{CL})$	$\cfrac{\Gamma \vdash A, A, \Delta}{\Gamma \vdash A, \Delta} \quad (\mathit{CR})$
$\cfrac{\Gamma_1, A, B, \Gamma_2 \vdash \Delta}{\Gamma_1, B, A, \Gamma_2 \vdash \Delta} \quad (\mathit{PL})$	$\cfrac{\Gamma \vdash \Delta_1, A, B, \Delta_2}{\Gamma \vdash \Delta_1, B, A, \Delta_2} \quad (\mathit{PR})$

[编辑] 直觉解释

上面的规则可以被分成两个主要群组: 逻辑规则和结构规则。每个逻辑规则都在十字转门 $\vdash$ 的左边或右边介入一个新的逻辑公式。相反的，结构规则操作在相继式的结构上，忽略公式的准确形状。这个一般模式的两个例外是同一性公理 (I) 和规则切 (Cut)。

尽管是以形式方式陈述的，上述规则允许用经典逻辑的方式非常直觉的读出来。比如，考虑规则 (∧L₁)。它陈述了如果你能证明 Δ 可以从包含 A 的公式序列推导出来，则你也能证明 Δ 自更强的假定，也就是 A∧B 成立。类似的，规则 (¬R) 陈述了如果 Γ 和 A 足够推导出 Δ，则从单独的 Γ 你可以要么仍然推导出 Δ 要么 A 必然为假，就是说 ¬A 成立。所有规则都可以用这种方式来解释。

对于量词规则的直觉解释，考虑规则 (∀R)。当然只从 A[y] 为真的事实推导出 ∀x A[x/y] 成立一般是不可能的。但是如果变量 y 在其他地方没有被提及(就是说，它仍可以被自由的选择，而不影响其他公式)，则你可以假定，A[y] 对 y 的任何值都成立。其他规则应当是非常直接的。

不再把规则看作是对在谓词逻辑中合法的推导的描述，你还可以把它们当作为给定陈述构造一个证明的指导。在这种情况下规则可以自底向上的读。例如，(∧R) 声称要证明 A∧B 推导自假定 Γ 和 Σ，分别证明 A 可以推导自 Γ 和 B 可以推导自 Σ 就足够了。注意，给顶某个前件，如何分解成 Γ 和 Σ 是不明确的。但是，只有有限多的可能需要检查，因为前件被假定为是有限的。这也展示了证明论如何被看作是以组合方式在证明的操作: 给定对 A 和 B 二者的证明，你可以构造一个对 A∧B 的证明。

在查找某个证明的时候，多数规则提供或多或少的如何做的处方。切规则是不同的: 它声称，在公式 A 可以被推导出来，并且这个公式也可以充当推导其他公式的前提的时候，则公式 A 可以被"切掉" 并把各自的推导连接起来。在自底向上构造一个证明的时候，这产生了猜测 A 的问题(因为它在下面根本就没有出现)。这个问题在切消定理中处理。

第二个规则有某种特殊性，它就是同一性公理 (I)。明显的直觉读为: A 证明 A。

[编辑] 例子推导

作为一个例子，下面是叫做排中律(拉丁语tertium non datur)的 $\vdash$ (A ∨ ¬A) 的序列推导。

$\cfrac {} { \qquad \cfrac {A \vdash A} { \qquad \cfrac {\vdash \lnot A,A } { \qquad \cfrac {\vdash A\lor \lnot A,A} { \qquad \cfrac {\vdash A,A\lor \lnot A} { \qquad \cfrac {\vdash A\lor \lnot A,A\lor \lnot A} {\vdash A\lor \lnot A} (CR) } ({\lor}R_1) } (PR) } ({\lor}R_2) } ({\lnot}R) } (I)$

这个推导还强调了语法演算的严格形式结构。例如，上述定义的右逻辑规则总是作用于右相继式的第一个公式，这使得 (PR) 的应用在形式上是需要的。这种非常严格的推理开始时可能难于理解，但是它形成了在形式逻辑中语法和语义之间非常核心的区别。尽管我们知道 A ∨ ¬A 和 ¬A ∨ A 有相同的意义，对后者的推导将不等价于上面给出的那个。但是，你可以通过介入引理而使语法推理更加方便些，就是说，预定义完成特定标准推导的方案。作为一个例子，你可以证明下列是一个合法的变换:

$\cfrac {\Gamma \vdash A \or B, \Delta} {\Gamma \vdash B \or A, \Delta}$

一旦已知一个一般的规则序列要建立这种推导，你可以使用它作为证明内的缩写。但是，当证明使用了好的引理而变得更加易读的时候，也使得推导的过程更加复杂，因为有更多可能的选择要考虑。在使用证明论(经常需要)作为自动演绎的时候这特别重要。

[编辑] 结构规则

结构规则需要某些额外的讨论。规则的名字是弱化(W)、紧缩(C)和排列(P)。紧缩和排列确保序列元素的次序(P)和多次出现(C)都不重要。就是说，你可以不把它当作序列而作为集合。

但是使用序列的额外努力是正当的，因为部分或全部的结构规则可以被忽略。这么做了就得到了所谓的亚结构逻辑。

[编辑] LK 系统的性质

这个规则系统可以被证明关于一阶逻辑是可靠的和完备的，就是说，从前提的集合 Γ 语义上得到的一个陈述 ( $\Gamma \vDash A$ )，当且仅当相继式 $\Gamma \vdash A$ 可以用上述规则推导出来。

在相继式演算中，切是可接纳的。这个结果也称为 Gentzen 的 Hauptsatz("主定理")。

[编辑] LK 系统的修改

上述规则可以以各种方式修改而不改变 LK 系统的本质。所有这些修改都仍可以叫做 LK 系统。

首先，如上面提及的，相继式可以被看做由集合或多集组成。在这种情况下，排列和(在使用集合的时候)紧缩公式的规则就可以废弃了。

弱化规则也变成是可接纳的了，在公理 (I) 被变更的时候，使得形如 Γ, A $\vdash$ A, Δ 的任何相继式都可以被得出。这意味着在任何上下文中 A 证明 A。在推导中的任何弱化因此可以在开始处正确的进行。在自底向上构造证明的时候这是个方便的变更。

独立于这些修改，你还可以在规则内上下文被分割的方式: 在 (∧R)、(∨L) 和 (→L) 的情况下，在向上走的时候，左上下文被以某种方式分割成 Γ 和 Σ。因为紧缩允许它们的重复，你可以假定全部上下文在两个推导分支中都使用。通过这么做，你能确保没有重要的前提在错误的分支中被丢失。使用弱化，上下文中无关的部分以后可以被消去。

所有这些改变生成等价的系统，这是在 LK 中的所有推导可以有效的变换因使用了替代规则的推导反之亦然的意义上。

[编辑] LJ 系统

令人惊讶的，LK 的规则的一些细小的变更就足以把它变成直觉逻辑的证明系统。你必须限制使用直觉相继式(就是说，右上下文被消去)并修改规则 (∨L) 为如下:

$\cfrac{\Gamma, A \vdash C \qquad \Sigma, B \vdash C }{\Gamma, \Sigma, A \or B \vdash C} \quad ({\or}L)$

这里的 C 是任意的公式。

结果的系统叫做 LJ 系统。它关于直觉逻辑是可靠的和完备的并且容许类似的切消证明。

[编辑] 引用

Girard，Jean-Yves; Paul Taylor, Yves Lafont [1989] (1990). Proofs and Types，Cambridge University Press (Cambridge Tracts in Theoretical Computer Science, 7). ISBN 0-521-37181-3.

[编辑] 参见

来自“http://zh.wikipedia.org../../../%E7%9B%B8/%E7%BB%A7/%E5%BC%8F/%E7%9B%B8%E7%BB%A7%E5%BC%8F%E6%BC%94%E7%AE%97.html”

页面分类: 证明论 | 數理邏輯