相繼式演算

在證明論和數理邏輯中，相繼式演算（又譯矢列演算、矢列式演算）是眾所周知的一階邏輯（和作為它的特殊情況的命題邏輯）的演繹系統。這個系統也叫做LK系統，用以區別於後來建立的有時也叫做相繼式演算的類似風格的各種其他系統。另一個給這種系統的術語是Gentzen系統。

基本介紹

• 中文名：相繼式演算
• 外文名：Sequent calculus

簡介

在證明論和數理邏輯中，相繼式演算（又譯矢列演算、矢列式演算）是眾所周知的一階邏輯（和作為它的特殊情況的命題邏輯）的演繹系統。這個系統也叫做LK系統，用以區別於後來建立的有時也叫做相繼式演算的類似風格的各種其他系統。另一個給這種系統的術語是Gentzen系統。

相繼式演算LK由Gerhard Gentzen介入為研究自然演繹的工具。它已經變成構造邏輯推導的非常有用的演算。它的名字得來自德語的Logischer Kalkül，意思是"邏輯演算"。相繼式演算是關於這個主題的很多研究所選擇的方法。

自然演繹

在數理邏輯中，自然演繹是證明論中嘗試提供象“自然”發生一樣的邏輯推理形式模型的一種方式。這種方式對比於使用公理的公理系統。

相繼式

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

相繼式有如下形式

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

參見

• 相繼式
• 自然演繹
• 切消定理