序列微積分

在數理邏輯中，序列微積分是一種形式邏輯論證的風格，其中證明的每一行都是一個條件同義詞（格哈德·根岑 (GerhardGentzen)稱之為序列），而不是一個無條件同義詞。

每一個條件同義詞都是根據推理的規則和程序從形式論證中的其他條件同義詞推斷出來的，與大衛-希爾伯特早期的形式邏輯風格相比，它更接近于數學家使用的自然演繹風格，在這種風格中，每一行都是無條件的同義詞。

更微妙的區別可能存在；例如，命題可能隱含地依賴于非邏輯公理。在這種情況下，序列標志著一階語言中的條件定理，而不是條件同義詞。

序列微積分是現存的幾種用于表達逐行邏輯論證的證明微積分風格之一。

希爾伯特風格，每一行都是一個無條件的同義詞（或定理）。

根岑(Gentzen)風格，每一行都是有條件的同義詞（或定理），左邊有零個或多個條件。

自然演繹，每條（條件）線的右邊正好有一個斷言的命題。

序列微積分，每個（條件）行的右邊都有零個或更多的斷言命題。

換句話說，自然演繹和序列微積分系統是特殊的不同類型的根岑(Gentzen)式系統。希爾伯特式系統通常有非常少的推理規則，更多地依賴于公理集。根岑(Gentzen)式系統通常只有很少的公理（如果有的話），更多地依賴于規則集。與希爾伯特式系統相比，根岑式系統具有明顯的實踐和理論優勢。

例如，自然演繹和序列微積分系統都有利于消除和引入普遍的和存在的量詞，這樣就可以根據更簡單的命題微積分規則來處理未量化的邏輯表達。

在一個典型的論證中，量詞被消除了，然后命題微積分被應用于未量化的表達式（通常包含自由變量），然后量詞被重新引入。這與數學家在實踐中進行數學證明的方式非常相似。

使用這種方法，謂詞微積分的證明通常更容易發現，而且通常更短。自然演繹系統更適合于實際的定理證明。序列微積分系統更適合于理論分析。

在證明理論和數理邏輯中，序列微積分是共享某種推理風格和某些形式屬性的形式系統家族。第 一個序列計算系統，LK和LJ，由格哈德·根岑 (<SPan style="color: #262626;font-family: var(--theme-font-family)">GerhardGentzen) 在1934/1935年推出，作為研究一階邏輯自然演繹的工具（分別為經典和直覺版本）。

根岑(Gentzen)所謂的關于LK和LJ的主要定理（基本定理）是切割消除定理，這一結果具有深遠的元理論后果，包括一致性。幾年后，根岑(Gentzen)進一步證明了這一技術的威力和靈活性，他應用割除論證給出了皮亞諾 (Peano) 算術一致性的（無限）證明，對哥德爾的不完備性定理做出了令人驚訝的回應。

自這項早期工作以來，順序計算（也稱為Gentzen系統）以及與之相關的一般概念已被廣泛應用于證明理論、數理邏輯和自動演繹等領域。

對不同風格的演繹系統進行分類的一種方法是看系統中的判斷形式，即哪些事情可以作為（子）證明的結論出現。

最簡單的判斷形式被用于希爾伯特式演繹系統，其中判斷的形式為是一階邏輯（或演繹系統適用的任何邏輯，如命題微積分、高階邏輯或模態邏輯）的任何公式。定理是那些在有效證明中作為結論判斷出現的公式。

希爾伯特式的系統不需要區分公式和判斷；我們在這里做這樣的區分只是為了與后面的案例進行比較。為希爾伯特式系統的簡單語法所付出的代價是，完整的形式證明往往會變得非常長。

在這樣的系統中，關于證明的具體論證幾乎總是訴諸于演繹定理。這導致了將演繹定理作為形式規則納入系統的想法，這發生在自然演繹中。