相繼式- 維基百科，自由的百科全書 - Wikipedia

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

相繼式有如下形式 這裡的Γ和Σ二者是邏輯公式的序列（就是說公式的數目和出現次序都是重要的）。

符號 ⊢ {\displaystyle \vdash } 通常被稱為十字轉門（turnstile）或T型符號（tee），並經常被讀做"產生"或"證明"。

它不是語言中的符號，而用來討論證明的元語言中的符號。

在相繼式中，Γ叫做