相继式

在逻辑学中, 相继式 (或称假言判断、条件判断) 是描述命题之间的推理关系的表达式, 它一般是描述数学的元语言的一部分, 且会和推理规则结合使用.

相继式格式如下:

$前因 ⊢ 后果$

其中:

判断可以粗略地理解为元语言中的命题. 因此, 我们可以这样阅读它:

•	若前因成立, 那么可以证明后果.
•	前因推出后果.

等等. 若前因和后果中包含多个表达式的话, 一般认为前因是由与关系连接, 而后果是由或关系连接, 形成某种对称性.

1相关概念

•	相继式可以看作是一种压缩的推理规则: $前因 ⊢ 后果等价于 \frac{前因}{后果}$ 将推理规则压缩为相继式后, 可以把这些相继式视为命题去讨论它们之间的推理规则.

•	直觉主义相继式最多有一个后果, 这导致经典相继式演算中对排中律的证明无法生效.

最早由 Gerhard Gentzen 提出相继式的概念时, 由德语中表示 “后果” 的单词 Konsequenz 演化出 sequenz 这一称呼:

•	Gerhard Gentzen (1935). “Untersuchungen über das logische Schließen I Mathematische Zeitschrift”. Mathematische Zeitschrift. (doi)

后来才演变为今天的拼写方式. Per Martin-Löf 在作品中指出 Gentzen 的相继式中去掉前因和后果的对称性后的 “这种形式的假言判断是我需要的”:

•	Per Martin-Löf (1996). “On the Meanings of the Logical Constants and the Justifications of the Logical Laws”. Nordic Journal of Philosophical Logic. (web)

并且将判断的概念和命题分离开. 参见 Martin-Löf 类型论.

后来由 Frank Pfenning 在他的讲义中将相继式直接称为 “假言判断”:

•	Frank Pfenning, Rowan Davies (2000). “A judgemental reconstruction of modal logic”.

•	相继式演算
•	切规则

术语翻译

相继式 • 英文 sequent

假言判断 • 英文 hypothetical judgment

前因 • 英文 antecedent

后果 • 英文 succedent