查看“相继式”的源代码

在[[证明论]]中，'''相继式'''（sequent）是对在规定[[演绎推理|演绎]]的[[演算]]的时候经常用到的可证明性的形式陈述。

== 解释 ==

相继式有如下形式
:<math>\Gamma\vdash\Sigma</math>

这里的Γ和Σ二者是[[符号逻辑|逻辑]]公式的[[序列]]（就是说公式的数目和出现次序都是重要的）。符号<math>\vdash</math>通常被称为十字转门（turnstile）或T型符号（tee），并经常被读做"产生"或"证明"。它不是语言中的符号，而用来讨论证明的元语言中的符号。在相继式中，Γ叫做相继式的前件（antecedent）而Σ叫做相继式的后继（succedent）。

== 直觉意义 ==
上面给出的那种相继式的直觉意义是在假定了Γ推出Σ是可证明的之下的。在经典的情形下，在十字转门左面的公式按[[逻辑合取|合取]]解释，而右面的公式按[[逻辑析取|析取]]解释。这意味着当在Γ中的所有公式成立的时候，在Σ中至少有一个公式必定是真的。如果后继为空，则按虚假解释，就是说<math>\Gamma\vdash</math>意味着Γ证明了虚假，并且因此是矛盾的。在另一方面，空前件被假定为真，就是说<math>\vdash\Sigma</math>意味着Σ没有任何假定就成立，也就是说，它总是真（作为一个析取式），而且因此是一个[[逻辑断言|断言]]。

但是上述解释只用于教学目的。因为在证明论中的形式证明是纯粹的[[语法]]上的，相继式的[[语义]]只由提供实际的[[推理规则]]的演算的性质给出。

剥离在上面的技术性精确定义中的任何矛盾，我们可以按它们的介绍性的逻辑形式来描述相继式。<math>\Gamma</math>表示我们开始逻辑处理时做的假定的集合，例如"苏格拉底是人"和"所有人都是必死的"。<math>\Sigma</math>表示从这些前提得到的逻辑结论。例如，我们希望在十字转门的<math>\Sigma</math>端见到"苏格拉底是必死的"。在这个意义上，<math>\vdash</math>意味着推理过程，或者英语中的"所以"。

我们对这些符号指派的意思是有所助益的。规则自身按机械性本质来运做而不承载潜在的意义。这个主题的详情请参见[[哥德尔不完备定理]]。

== 例子 ==
一个典型的相继式：  

:<math> \phi,\psi\vdash\alpha,\beta</math>

它声称要么<math>\alpha</math>要么<math>\beta</math>可以推导自<math>\phi</math>且<math>\psi</math>。

== 性质 ==
因为在（左边的）的前件中的所有公式都必须为真来获得在（右边的）后继中至少一个公式为真，向任何一端增加公式都导致一个更弱的相继式，而从任何一端去除公式都得到更强的相继式。

== 规则 ==
多数证明系统都提供从一个相继式到另一个相继式的演绎方式。这些规则都写成在[[横线]]上下的相继式列表。这些规则指示如果在横线上的所有相继式都为真，则在横线之下的也都为真。

一个典型的规则是：

:<math> \frac{\Gamma\vdash\Sigma}{\begin{matrix} \Gamma,\alpha\vdash\Sigma & \alpha,\Gamma\vdash\Sigma \end{matrix}}</math>

这指示-{了}-如果我们可以演绎<math>\Sigma</math>自<math>\Gamma</math>，则我们也可以演绎它自<math>\Gamma</math>和<math>\alpha</math>一起。

注意我们通常使用大写的希腊字母来指称（可能为空）公式的列表。<math>[\Gamma,\Sigma]</math>被用来指示<math>\Gamma</math>和<math>\Sigma</math>的紧缩，就是说，这些出现在要么<math>\Gamma</math>要么<math>\Sigma</math>中但不重复的那些公式的列表。

== 变体 ==
这里介绍的相继式的一般概念能以各种方式特殊化。一个相继式被称为是'''直觉相继式'''，如果在后继中有最多一个公式。这种形式是获得[[直觉逻辑]]的演算是需要的。类似的，你可以通过要求相继式在前件中只有一个公式来获得[[双直觉逻辑]]（某种[[次协调逻辑]]）的演算。

在很多情况下，相继式还假定由[[多重集]]或[[集合]]组成。所以你可以漠视公式的次序甚至数目。对于经典[[命题演算|命题逻辑]]这不导致问题，因为你能从一组前提中得出的结论不依赖于这些数据。但是在[[亚结构逻辑]]中这就变得很重要了。

一些系统只允许在右边有一个公式。

== 历史 ==
历史上，相继式是[[Gerhard Gentzen]]介入用来规定他著名的[[相继式演算]]。在他的德语出版物中他使用了单词"Sequenz"。但是，在英语中，单词"[[序列]]"已经用来翻译德语的"Folge"并在数学中经常出现。术语"相继式"被建立用做这个德语表达的替代翻译。

{{planetmath|id=3502|title=Sequent}}

[[Category:证明论]]