相繼式

在證明論中，相繼式（sequent）是對在規定演繹的演算的時候經常用到的可證明性的形式陳述。

解釋

相繼式有如下形式

$\Gamma \vdash \Sigma$

這裡的Γ和Σ二者是邏輯公式的序列（就是說公式的數目和出現次序都是重要的）。符號$\vdash$通常被稱為十字轉門（turnstile）或T型符號（tee），並經常被讀做"產生"或"證明"。它不是語言中的符號，而用來討論證明的元語言中的符號。在相繼式中，Γ叫做相繼式的前件（antecedent）而Σ叫做相繼式的後繼（succedent）。

直覺意義

上面給出的那種相繼式的直覺意義是在假定了Γ推出Σ是可證明的之下的。在經典的情形下，在十字轉門左面的公式按合取解釋，而右面的公式按析取解釋。這意味着當在Γ中的所有公式成立的時候，在Σ中至少有一個公式必定是真的。如果後繼為空，則按虛假解釋，就是說$\Gamma \vdash$意味着Γ證明了虛假，並且因此是矛盾的。在另一方面，空前件被假定為真，就是說$\vdash \Sigma$意味着Σ沒有任何假定就成立，也就是說，它總是真（作為一個析取式），而且因此是一個斷言。

但是上述解釋只用於教學目的。因為在證明論中的形式證明是純粹的語法上的，相繼式的語義只由提供實際的推理規則的演算的性質給出。

剝離在上面的技術性精確定義中的任何矛盾，我們可以按它們的介紹性的邏輯形式來描述相繼式。$\Gamma$表示我們開始邏輯處理時做的假定的集合，例如"蘇格拉底是人"和"所有人都是必死的"。$\Sigma$表示從這些前提得到的邏輯結論。例如，我們希望在十字轉門的$\Sigma$端見到"蘇格拉底是必死的"。在這個意義上，$\vdash$意味着推理過程，或者英語中的"所以"。

我們對這些符號指派的意思是有所助益的。規則自身按機械性本質來運做而不承載潛在的意義。這個主題的詳情請參見哥德爾不完備定理。

例子

一個典型的相繼式：

$\phi ,\psi \vdash \alpha ,\beta$

它聲稱要麼$\alpha$要麼$\beta$可以推導自$\phi$且$\psi$。

性質

因為在（左邊的）的前件中的所有公式都必須為真來獲得在（右邊的）後繼中至少一個公式為真，向任何一端增加公式都導致一個更弱的相繼式，而從任何一端去除公式都得到更強的相繼式。

規則

多數證明系統都提供從一個相繼式到另一個相繼式的演繹方式。這些規則都寫成在橫線上下的相繼式列表。這些規則指示如果在橫線上的所有相繼式都為真，則在橫線之下的也都為真。

一個典型的規則是：

${\frac {\Gamma \vdash \Sigma }{\begin{matrix}\Gamma ,\alpha \vdash \Sigma &\alpha ,\Gamma \vdash \Sigma \end{matrix}}}$

這指示了如果我們可以演繹$\Sigma$自$\Gamma$，則我們也可以演繹它自$\Gamma$和$\alpha$一起。

注意我們通常使用大寫的希臘字母來指稱（可能為空）公式的列表。$[\Gamma ,\Sigma ]$被用來指示$\Gamma$和$\Sigma$的緊縮，就是說，這些出現在要麼$\Gamma$要麼$\Sigma$中但不重複的那些公式的列表。

變體

這裡介紹的相繼式的一般概念能以各種方式特殊化。一個相繼式被稱為是直覺相繼式，如果在後繼中有最多一個公式。這種形式是獲得直覺邏輯的演算是需要的。類似的，你可以通過要求相繼式在前件中只有一個公式來獲得雙直覺邏輯（某種次協調邏輯）的演算。

在很多情況下，相繼式還假定由多重集或集合組成。所以你可以漠視公式的次序甚至數目。對於經典命題邏輯這不導致問題，因為你能從一組前提中得出的結論不依賴於這些數據。但是在亞結構邏輯中這就變得很重要了。

一些系統只允許在右邊有一個公式。

歷史

歷史上，相繼式是格哈德·根岑介入用來規定他著名的相繼式演算。在他的德語出版物中他使用了單詞"Sequenz"。但是，在英語中，單詞"序列"已經用來翻譯德語的"Folge"並在數學中經常出現。術語"相繼式"被建立用做這個德語表達的替代翻譯。

本條目含有來自PlanetMath《Sequent》的內容，版權遵守知識共享協議：署名-相同方式共享協議。