在數理邏輯 中，自然演繹 是證明論 中嘗試提供象「自然」發生一樣的邏輯推理形式模型的一種方式。這種方式對比於使用公理 的公理系統 。
自然演繹來源自對共通於弗雷格 、羅素 和希爾伯特 系統的判句 公理化(希爾伯特演繹系統 )的不滿。這種公理化最著名使用是在羅素 和懷特海 的《數學原理 》的數學論述中。在1926年由揚·武卡謝維奇 在波蘭發起的一系列研討會提倡一種對邏輯的更加自然處理，斯坦尼斯瓦夫·亞希科夫斯基 做了定義更自然的演繹的最早嘗試，首先在1929年使用了一種圖表表示法，並在1934年和1935年的一序列論文中更改了他的提議。但是他的提議沒有流行起來。現代形式的自然演繹是由德國數學家格哈德·根岑 於1935年在一篇提交給哥廷根大學數學系的學位論文中獨立提出的。術語自然演繹 就是在那篇論文中出現的:
我首先希望構造一種儘可能地接近實際推理的形式化主義。所以提議了「自然演繹演算 」。
Ich wollte nun zunächst einmal einen Formalismus aufstellen, der dem wirklichen Schließen möglichst nahe kommt. So ergab sich ein „Kalkül des natürlichen Schließens “. — Gentzen, 《Untersuchungen über das logische Schließen》(Mathematische Zeitschrift 39, pp.176-210, 1935)
根岑被建立數論的一致性證明的目標所推動，因而找到了他的自然演繹演算的直接使用。但他不滿意自己證明的複雜性，並在1938年使用他的相繼式演算 給出了一個新的一致性證明。在1961年和1962年的一系列研討會中，Dag Prawitz 給出了自然演繹演算的全面總結，並把根岑對相繼式演算做的很多工作轉運到了自然演繹框架中。他在1965年的專著《Natural deduction: a proof-theoretical study》成為關於自然演繹的權威著作，並包括了模態 和二階邏輯 的應用。
在本文中提供的系統是根岑或 Prawitz 的公式化的一個小變體，但忠實於 Per Martin-Löf 對邏輯判斷和連結詞的描述(Martin-Lof, 1996)。
判斷 是可知的事物，就是說知識的對象。如果有人實際上知道它則它是顯然 (有證據的)的。所以"正在下雨"是一個判斷，對於知道實際上正在下雨的人而言它是顯然的；在這種情況下，你可以通過看窗外或走出屋子來輕易的找到這個判斷的證據。但是在數理邏輯中，證據通常不是直接可觀測到的，而是從更加基本的顯然判斷演繹來的。演繹的過程構成了一個證明 ；換句話說，一個判斷是顯然的，如果你有對它的證明。
在邏輯中最重要的判斷是「A 為真」這種形式的。字母 A 表示代表一個命題的任何表達式；這個真理判斷要求更基本的判斷:「A 是命題」。很多其他判斷也已經被研究了；比如「A 為假」(參見經典邏輯 )，「A 在時間 t 為真」(參見時間邏輯 )，「A 必然為真」或「A 可能為真」(參見模態邏輯 )，「程序 M 有類型 τ」(參見編程語言 和類型論 )，「A 從可用的資源是可完成的」(參見線性邏輯 )，等等。作為開始，我們先只關注最簡單的兩個判斷 「A 是命題」和「A 為真」，分別縮寫為「A prop」和「A true」。
判斷「A prop」定義了 A 的有效證明的結構，它們進而定義了命題的結構。出於這個原因，判斷的推理規則 有時叫做形成規則 。作為展示，如果我們有兩個命題 A 和 B (就是說，判斷「A prop」 和「B prop」是顯然的)，則我們形成了複合命題 A 與 B ，符號化寫為 "
A
∧
B
{\displaystyle A\wedge B}
A
prop
B
prop
A
∧
B
prop
∧
F
{\displaystyle {\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}}{A\wedge B{\hbox{ prop}}}}\ \wedge _{F}}
這個推理規則是「模式性」的: A 和 B 可以示例任何表達式。推理規則的一般形式為:
J
1
J
2
⋯
J
n
J
name
{\displaystyle {\frac {J_{1}\qquad J_{2}\qquad \cdots \qquad J_{n}}{J}}\ {\hbox{name}}}
這裡的每個
J
i
{\displaystyle J_{i}}
前提 ，而橫線下的判斷叫做結論 。其他常見的邏輯命題是析取(
A
∨
B
{\displaystyle A\vee B}
¬
A
{\displaystyle \neg A}
A
⊃
B
{\displaystyle A\supset B}
⊤
{\displaystyle \top }
⊥
{\displaystyle \bot }
A
prop
B
prop
A
∨
B
prop
∨
F
A
prop
B
prop
A
⊃
B
prop
⊃
F
{\displaystyle {\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}}{A\vee B{\hbox{ prop}}}}\ \vee _{F}\qquad {\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}}{A\supset B{\hbox{ prop}}}}\ \supset _{F}}
⊤
prop
⊤
F
⊥
prop
⊥
F
A
prop
¬
A
prop
¬
F
{\displaystyle {\frac {\hbox{ }}{\top {\hbox{ prop}}}}\ \top _{F}\qquad {\frac {\hbox{ }}{\bot {\hbox{ prop}}}}\ \bot _{F}\qquad {\frac {A{\hbox{ prop}}}{\neg A{\hbox{ prop}}}}\ \neg _{F}}
現在我們討論「A 為真(是真理)」判斷。在本文餘下部分中，我們將在已被理解的地方省略「prop」判斷。在結論中介入邏輯連結詞的推理規則叫做介入規則 。要介入合取，就是說從命題 A 和 B 推導出「A and B 為真」 ，你需要「A 為真和 B 為真」的證據。作為一個推理規則:
A
true
B
true
A
∧
B
true
∧
I
{\displaystyle {\frac {A{\hbox{ true}}\qquad B{\hbox{ true}}}{A\wedge B{\hbox{ true}}}}\ \wedge _{I}}
上述規則實際上是省略命題判斷的簡寫[ 1]
在空無(nullary)的情況下，你可以從沒有前提中推導出真理。
⊤
true
⊤
I
{\displaystyle {\frac {\ }{\top {\hbox{ true}}}}\ \top _{I}}
注意在空無的情況下，對於虛假是沒有介入規則的。所以你永遠不能從更簡單的判斷推導出虛假。
如果一個命題的真實性可以通過多於一種方式來確立，則相應的連結詞有多個介入規則。
A
true
A
∨
B
true
∨
I
1
B
true
A
∨
B
true
∨
I
2
{\displaystyle {\frac {A{\hbox{ true}}}{A\vee B{\hbox{ true}}}}\ \vee _{I1}\qquad {\frac {B{\hbox{ true}}}{A\vee B{\hbox{ true}}}}\ \vee _{I2}}
對偶於介入規則的是描述如何把關於複合命題的信息解構為關於它的成員的信息的除去規則 。因此，從「A ∧ B 為真」，我們可以推導出 「A 為真」和 「B 為真」:
A
∧
B
true
A
true
∧
E
1
A
∧
B
true
B
true
∧
E
2
{\displaystyle {\frac {A\wedge B{\hbox{ true}}}{A{\hbox{ true}}}}\ \wedge _{E1}\qquad {\frac {A\wedge B{\hbox{ true}}}{B{\hbox{ true}}}}\ \wedge _{E2}}
我們已經見到的推理不足以陳述蘊涵介入或析取除去的規則；為此我們需要假言推導 的更一般的概念。
作為推理規則的使用例子，考慮合取的交換律。如果 A ∧ B 為真，則 B ∧ A 為真；這可以通過以底下推理的前提匹配上面推理的結論的方式構成推理規則來完成這種推導。
A
∧
B
true
B
true
∧
E
2
A
∧
B
true
A
true
∧
E
1
B
∧
A
true
∧
I
{\displaystyle {\cfrac {{\cfrac {A\wedge B{\hbox{ true}}}{B{\hbox{ true}}}}\ \wedge _{E2}\qquad {\cfrac {A\wedge B{\hbox{ true}}}{A{\hbox{ true}}}}\ \wedge _{E1}}{B\wedge A{\hbox{ true}}}}\ \wedge _{I}}
在數理邏輯中普遍性的操作是「依據假定的推理」。例如，考慮下列推導:
A
∧
(
B
∧
C
)
t
r
u
e
B
∧
C
t
r
u
e
B
t
r
u
e
∧
E
1
∧
E
2
{\displaystyle {\cfrac {A\wedge \left(B\wedge C\right)\ true}{{\cfrac {B\wedge C\ true}{B\ true}}\wedge E_{1}}}\wedge E_{2}}
這個推導不確立 B 為真；而確立了下列事實:
如果「A ∧ (B ∧ C) true」則「B true」。 在邏輯中，我們讀做「假定 A ∧ (B ∧ C) 為真，我們證實 B 為真」；換句話說，判斷「B true」依賴於假定的判斷「A ∧ (B ∧ C) true」。這叫做假言推導 ，它可寫為如下:
A
∧
(
B
∧
C
)
t
r
u
e
⋮
B
t
r
u
e
{\displaystyle {\begin{matrix}A\wedge \left(B\wedge C\right)\ true\\\vdots \\B\ true\end{matrix}}}
釋義為: 「B true」推導自「A ∧ (B ∧ C) true」。當然，在這個特定的例子中我們實際上知道「B true」來自「A ∧ (B ∧ C) true」的推導，但是一般而言，我們不可以先驗 的知道這個推導。假言推導的一般形式為:
D
1
D
2
⋯
D
n
⋮
J
{\displaystyle {\begin{matrix}D_{1}\quad D_{2}\cdots D_{n}\\\vdots \\J\end{matrix}}}
每個假言推導都有寫在頂行的一組前件 推導(Di )，和寫在底行的一個後件 判斷(J )。每個前提自身都可以是一個假言推導。(出於簡單性，我們把這種判斷處理為無前提推導。)
假言判斷的概念被主觀化為蘊涵的連結詞。蘊涵介入規則 和蘊涵除去規則 如下。
A
t
r
u
e
u
⋮
B
t
r
u
e
A
⊃
B
t
r
u
e
⊃
I
u
A
⊃
B
t
r
u
e
A
t
r
u
e
B
t
r
u
e
⊃
E
{\displaystyle {\frac {\begin{matrix}{\frac {}{A\ true}}u\\\vdots \\B\ true\end{matrix}}{A\supset B\ true}}\supset I^{u}\qquad {\frac {A\supset B\ true\quad A\ true}{B\ true}}\supset E}
在介入規則中，命名為 u 的前件被「注入」到結論中。這是界定假設的範圍的機制: 它存在的唯一理由是確立 「B true」；它不能被用做任何其他目的，特別是，它不能被用在這個介入之下。作為一個例子，考慮「A
⊃
{\displaystyle \supset }
⊃
{\displaystyle \supset }
A
t
r
u
e
u
B
t
r
u
e
w
A
∧
B
t
r
u
e
B
⊃
(
A
∧
B
)
t
r
u
e
A
⊃
(
B
⊃
(
A
∧
B
)
)
t
r
u
e
⊃
I
u
⊃
I
w
∧
I
{\displaystyle {\cfrac {{\frac {}{A\ true}}u\qquad {\frac {}{B\ true}}w}{{\cfrac {A\wedge B\ true}{{\cfrac {B\supset \left(A\wedge B\right)\ true}{A\supset \left(B\supset \left(A\wedge B\right)\right)\ true}}\supset I^{u}}}\supset I^{w}}}\wedge I}
這是個沒有不滿足前提的完整推導；但是，子推導是假設的。例如「B
⊃
{\displaystyle \supset }
u )。
通過假言推導，我們現在寫出析取除去規則 :
A
∨
B
true
A
t
r
u
e
u
⋮
C
t
r
u
e
B
t
r
u
e
w
⋮
C
t
r
u
e
C
t
r
u
e
∨
E
u
,
w
{\displaystyle {\frac {A\vee B{\hbox{ true}}\quad {\begin{matrix}{\frac {}{A\ true}}u\\\vdots \\C\ true\end{matrix}}\quad {\begin{matrix}{\frac {}{B\ true}}w\\\vdots \\C\ true\end{matrix}}}{C\ true}}\vee E^{u,w}}
用口語說，如果「A ∨ B true」，並且我們可以從「A true」和「B true」二者推出「C true」，則確實「C true」 。注意這個規則不依靠於「A true」或「B true」中的任何一個。
在空無的情況下，我們得到下列有關虛假的除去規則:
⊥
t
r
u
e
C
t
r
u
e
⊥
E
{\displaystyle {\frac {\perp true}{C\ true}}\perp \!E}
這讀做: 如果虛假為真，則任何命題 C 為真。
否定介入規則 和否定除去規則 類似於蘊涵。
A
t
r
u
e
u
⋮
P
t
r
u
e
A
t
r
u
e
u
⋮
¬
P
t
r
u
e
¬
A
t
r
u
e
¬
I
u
¬
A
t
r
u
e
A
t
r
u
e
C
t
r
u
e
¬
E
{\displaystyle {\frac {{\begin{matrix}{\frac {}{A\ true}}u\\\vdots \\P\ true\end{matrix}}\quad {\begin{matrix}{\frac {}{A\ true}}u\\\vdots \\\lnot P\ true\end{matrix}}}{\lnot A\ true}}\lnot I^{u}\qquad {\frac {\lnot A\ true\quad A\ true}{C\ true}}\lnot E}
介入規則注入了假設 u 的名字。因為這些規則是模式性的，介入規則的釋義為: 如果我們可以從「A true」推導出「P true」和「¬P true」，就是
⊥
{\displaystyle \bot }
A 必定為假，也就是「¬A true」。對於除去規則，如果 A 和 ¬A 二者都被證明為真，則這是個矛盾
⊥
{\displaystyle \bot }
C 為真。因為蘊涵和否定的規則如此的類似，很容易看出 ¬A 和 A
⊃
{\displaystyle \supset }
是等價的，就是可以相互推導的。
一個理論 被稱為是一致(相容)的，如果虛假(從沒有前提)是不能證明的，被稱為是完備的，如果所有定理都可以使用這個邏輯的推理規則來證明。這是關於整體的邏輯的陳述，並通常和某種模型 的概念聯繫在一起。但是，還有對推理規則的純粹語法檢查的一致性和完備性的局部的概念，而不需要訴諸模型。首先是局部一致性，也叫做還原性，它聲稱包含了一個連結詞的介入、並立即跟隨着它的除去的任何推導都可以被轉換成不包含這種迂迴的等價推導。這是對除去規則力量的檢查: 它們不能強大得包含了在前提中沒有包含的知識。作為一個例子，考慮合取。
A
t
r
u
e
u
B
t
r
u
e
w
A
∧
B
t
r
u
e
A
t
r
u
e
∨
E
1
∧
I
{\displaystyle {\cfrac {{\frac {}{A\ true}}u\quad {\frac {}{B\ true}}w}{{\cfrac {A\land B\ true}{A\ true}}\lor E_{1}}}\land I}
⇒
A
t
r
u
e
u
{\displaystyle {\cfrac {}{A\ true}}u}
作為對偶，局部完備性聲稱除去規則足夠強大來把一個連結分解成適合它的介入規則的形式。再次考慮合取:
A
∧
B
t
r
u
e
u
{\displaystyle {\cfrac {}{A\land B\ true}}u}
⇒
A
∧
B
t
r
u
e
u
A
t
r
u
e
∧
E
1
A
∧
B
t
r
u
e
u
B
t
r
u
e
∧
E
2
A
∧
B
t
r
u
e
∧
I
{\displaystyle {\cfrac {{\cfrac {{\frac {}{A\land B\ true}}u}{A\ true}}\land E_{1}\quad {\cfrac {{\frac {}{A\land B\ true}}u}{B\ true}}\land E_{2}}{A\land B\ true}}\land I}
使用Curry-Howard同構 ，除去規則和介入規則分別精確的對應於lambda 演算 中的 β-歸約 和 η-展開 。通過局部完備性，我們看到所有推導都可以被轉換成介入主要連結詞的等價推導，實際上，如果整個推導都服從除去跟隨着介入的這種次序，則可以被稱為是規範的 。在規範推導中，所有除去都出現在介入上面。在大多數邏輯中，所有推導都有等價的規範推導，叫做規範形式 。規範形式的存在使用自然演繹自身一般是難於證明的，這種理由確實存在於文獻中，其中最著名的是 Dag Prawitz 1961年的書《Natural deduction: a proof-theoretical study》，A&W Stockholm 1965,沒有ISBN。通過免切 相繼式演算 表達的方式做間接的證明是非常容易的。
一階系統總結 前面章節中的邏輯是「單類」邏輯的例子，單類邏輯只帶有單一一類對象: 命題。已經提出了對這個簡單框架的很多擴展；在本章中我們將向它擴展上第二類對象：個體 或項 。更精確地說，我們將增加新的一類判斷 「t 是項」(或「t term 」)，這是的 t 是模式性的。我將固定一個變量 的可數集合 V ，函數符號 的可數集合 F ，並如下這樣構造項:
v
∈
V
v
t
e
r
m
v
a
r
−
F
{\displaystyle {\frac {v\in V}{v\ term}}{var-}F}
f
∈
F
t
1
t
e
r
m
t
2
t
e
r
m
.
.
.
t
n
t
e
r
m
f
(
t
1
,
t
2
,
.
.
.
,
t
n
)
t
e
r
m
a
p
p
−
F
{\displaystyle {\frac {f\in F\quad t_{1}\ term\quad t_{2}\ term\quad ...\ t_{n}\ term}{f(t_{1},t_{2},...,t_{n})\ term}}{app-}F}
對於命題，我們考慮第三個謂詞 的可數集合。並用如下規則定義「在項之上的原子謂詞」:
ϕ
∈
P
t
1
t
e
r
m
t
2
t
e
r
m
.
.
.
t
n
t
e
r
m
ϕ
(
t
1
,
t
2
,
.
.
.
,
t
n
)
p
r
o
p
p
r
e
d
−
F
{\displaystyle {\frac {\phi \in P\quad t_{1}\ term\quad t_{2}\ term\quad ...\ t_{n}\ term}{\phi (t_{1},t_{2},...,t_{n})\ prop}}{pred-}F}
此外，我們增加一對「量化的」命題: 全稱(
∀
{\displaystyle \forall }
∃
{\displaystyle \exists }
x
t
e
r
m
u
⋮
A
p
r
o
p
∀
x
.
A
p
r
o
p
∀
F
u
{\displaystyle {\cfrac {\begin{matrix}{\frac {}{x\ term}}u\\\vdots \\A\ prop\\\end{matrix}}{\forall x.\ A\ prop}}\forall F^{u}}
x
t
e
r
m
u
⋮
A
p
r
o
p
∃
x
.
A
p
r
o
p
∃
F
u
{\displaystyle {\cfrac {\begin{matrix}{\frac {}{x\ term}}u\\\vdots \\A\ prop\\\end{matrix}}{\exists x.\ A\ prop}}\exists F^{u}}
這些量化的命題有如下的介入和除去規則。
[
a
/
x
]
A
t
r
u
e
∀
x
.
A
t
r
u
e
∀
I
a
{\displaystyle {\cfrac {[a/x]A\ true}{\forall x.\ A\ true}}\forall I^{a}}
∀
x
.
A
t
r
u
e
[
t
/
x
]
A
t
r
u
e
∀
E
{\displaystyle {\cfrac {\forall x.\ A\ true}{[t/x]A\ true}}\forall E}
[
t
/
x
]
A
t
r
u
e
∃
x
.
A
t
r
u
e
∃
I
{\displaystyle {\cfrac {[t/x]A\ true}{\exists x.\ A\ true}}\exists I}
∃
x
.
A
t
r
u
e
[
a
/
x
]
A
t
r
u
e
u
⋮
C
t
r
u
e
C
t
r
u
e
∃
E
a
,
u
{\displaystyle {\cfrac {\exists x.\ A\ true\quad {\begin{matrix}{\frac {}{[a/x]A\ true}}u\\\vdots \\C\ true\end{matrix}}}{C\ true}}\exists E^{a,u}}
在這些規則中，符號 [t /x ] A 表示代換 A 中 x 的所有(可見)實例為 t ，避免它被其他量詞捕獲；關於這種標準操作的詳細描述請參見 lambda 演算 。同前面一樣，名字上的上標表示被注入的成分: 在
∀
I
{\displaystyle \forall I}
a (這種項叫做本徵變量 或參數 )，在
∃
E
{\displaystyle \exists E}
u 的假設被局部化到假言推導的第二個前提中。儘管早先章節中的命題邏輯是可判定的 ，增加量詞使邏輯成為不可判定的。
迄今為止量化擴展是「一階的」: 它們用把命題區別於在其上量化的對象的種類。高階邏輯採用了一種不同的方式，它只有一個種類的命題，量詞的量化範圍是同種類的命題，反映於形成規則:
p
p
r
o
p
u
⋮
A
p
r
o
p
∀
p
.
A
p
r
o
p
∀
F
u
{\displaystyle {\cfrac {\begin{matrix}{\frac {}{p\ prop}}u\\\vdots \\A\ prop\\\end{matrix}}{\forall p.\ A\ prop}}\forall F^{u}}
p
p
r
o
p
u
⋮
A
p
r
o
p
∃
p
.
A
p
r
o
p
∃
F
u
{\displaystyle {\cfrac {\begin{matrix}{\frac {}{p\ prop}}u\\\vdots \\A\ prop\\\end{matrix}}{\exists p.\ A\ prop}}\exists F^{u}}
關於高階邏輯的介入和除去規則的討論超出了本文的範圍。有介於一階和高階邏輯之間的邏輯。例如，二階邏輯有兩類命題，第一類量化於項，第二類量化於第一類命題之上。
迄今為止對自然演繹的表述集中於命題的本質而沒有給出證明 的形式定義。要形式化證明的概念，我們要稍微更改假言推導的表述。我們向前件標籤上證明變量 (來自某個變量的可數集合 V )，並用實際證明裝飾後件。通過十字轉門 (turnstile)
⊢
{\displaystyle \vdash }
假設 同後件分隔開。這種修改有時叫做局部化假設 。下列圖示總結變更。
J
1
u
1
J
2
u
2
⋯
J
n
u
n
⋮
J
{\displaystyle {\begin{matrix}{\frac {}{J_{1}}}u_{1}\quad {\frac {}{J_{2}}}u_{2}\quad \cdots {\frac {}{J_{n}}}u_{n}\\\vdots \\J\\\end{matrix}}}
⇒
u
1
:
J
1
,
u
2
:
J
2
,
.
.
.
,
u
n
:
J
n
⊢
J
{\displaystyle u_{1}:J_{1},u_{2}:J_{2},...,u_{n}:J_{n}\vdash J}
假設的搜集將被寫為 Γ，當它們的精確內容是無關的時候。要使證明直接了當，我們把無關證明的判斷「A true 」換成判斷「π 是證明(A true)」，它在符號上被寫為「π : A true 」。服從標準方式，證明用它們自己的對「π proof 」的形成規則來指定。最簡單的可能的證明是使用帶標籤的假設；在這種情況下證據是標籤自身。
u
∈
V
u
p
r
o
o
f
p
r
o
o
f
−
F
{\displaystyle {\frac {u\in V}{u\ proof}}{proof-}F}
u
:
A
t
r
u
e
⊢
u
:
A
t
r
u
e
h
y
p
{\displaystyle {\frac {}{u:A\ true\vdash u:A\ true}}hyp}
為了簡短，我們在本文餘下部分去掉判斷標籤 「true」，就寫為「Γ
⊢
{\displaystyle \vdash }
A 」。讓我們通過明確的證明來重新檢驗某些連結詞。對於合取，我們查看介入規則 ∧I 來發現合取的證明形式: 它們必須是兩個合取項的一對證明。就是:
π
1
p
r
o
o
f
π
2
p
r
o
o
f
(
π
1
,
π
2
)
p
r
o
o
f
p
a
i
r
−
F
{\displaystyle {\frac {\pi _{1}\ proof\quad \pi _{2}\ proof}{(\pi _{1},\pi _{2})\ proof}}{pair-}F}
Γ
⊢
π
1
:
A
Γ
⊢
π
2
:
B
Γ
⊢
(
π
1
,
π
2
)
:
A
∧
B
∧
I
{\displaystyle {\frac {\Gamma \vdash \pi _{1}:A\quad \Gamma \vdash \pi _{2}:B}{\Gamma \vdash (\pi _{1},\pi _{2}):A\land B}}\land I}
除去規則 ∧E1 和 ∧E2 選擇要麼左面的要麼右面的合取項；所以證明是一對投影 — 第一個(fst ) 和第二個(snd )。
π
p
r
o
o
f
f
s
t
π
p
r
o
o
f
f
s
t
−
F
{\displaystyle {\frac {\pi \ proof}{\mathbf {fst} \ \pi \ proof}}{fst-}F}
Γ
⊢
π
:
A
∧
B
Γ
⊢
f
s
t
π
:
A
∧
E
1
{\displaystyle {\frac {\Gamma \vdash \pi :A\land B}{\Gamma \vdash \mathbf {fst} \ \pi :A}}\land E_{1}}
π
p
r
o
o
f
s
n
d
π
p
r
o
o
f
s
n
d
−
F
{\displaystyle {\frac {\pi \ proof}{\mathbf {snd} \ \pi \ proof}}{snd-}F}
Γ
⊢
π
:
A
∧
B
Γ
⊢
s
n
d
π
:
B
∧
E
2
{\displaystyle {\frac {\Gamma \vdash \pi :A\land B}{\Gamma \vdash \mathbf {snd} \ \pi :B}}\land E_{2}}
對於蘊涵，介入形式的局部化或約束，書寫要使用 λ；這對應於注入標籤。在規則「Γ, u :A 」中表示一組假設 Γ，同增補的一個假設 u 在一起。
π
p
r
o
o
f
λ
u
.
π
p
r
o
o
f
λ
−
F
{\displaystyle {\frac {\pi \ proof}{\lambda u.\pi \ proof}}{\lambda -}F}
Γ
,
u
:
A
⊢
π
:
B
Γ
⊢
λ
u
.
π
:
A
⊃
B
⊃
I
{\displaystyle {\frac {\Gamma ,u:A\vdash \pi :B}{\Gamma \vdash \lambda u.\pi :A\supset B}}\supset I}
π
1
p
r
o
o
f
π
2
p
r
o
o
f
π
1
π
2
p
r
o
o
f
a
p
p
−
F
{\displaystyle {\frac {\pi _{1}\ proof\quad \pi _{2}\ proof}{\pi _{1}\pi _{2}\ proof}}{app-}F}
Γ
⊢
π
1
:
A
⊃
B
Γ
⊢
π
2
:
A
Γ
⊢
π
1
π
2
:
B
⊃
E
{\displaystyle {\frac {\Gamma \vdash \pi _{1}:A\supset B\quad \Gamma \vdash \pi _{2}:A}{\Gamma \vdash \pi _{1}\pi _{2}:B}}\supset E}
通過明確可用的證明，你可以操縱和思辯證明。證明的關鍵操作是用一個證明去替換在另一個證明中使用的假定。這通常叫做「代換定理」，並可以通過關於第二個判斷的深度(或結構)的歸納法 證明。
代換定理
如果
Γ
⊢
π
1
:
A
{\displaystyle \Gamma \vdash \pi _{1}:A}
Γ
,
u
:
A
⊢
π
2
:
B
{\displaystyle \Gamma ,u:A\vdash \pi _{2}:B}
Γ
⊢
[
π
1
/
u
]
π
2
:
B
{\displaystyle \Gamma \vdash [\pi _{1}/u]\pi _{2}:B}
迄今為止判斷「Γ
⊢
{\displaystyle \vdash }
A 」有一個純邏輯釋義。在類型論 中，邏輯觀點被調換為更加可計算的對象的觀點。在邏輯釋義中的命題現在被看作類型 ，而證明被看作使用lambda 演算 寫的程序。所以「π : A 」的釋義是「程序 π 有類型 A 」。邏輯連結詞也有不同的讀法: 合取被看作乘積(×)，蘊涵被讀做函數箭頭(→) 等等。區別只是裝飾。類型論有使用形成、介入和除去規則的自然演繹表示；事實上，讀者可以用前面的章節重新構造一個「簡單的類型論」。
在邏輯和類型論之間的區別主要是把焦點從類型(命題)轉移到了程序(證明)。類型論主要感興趣於程序的可轉換性和可歸約性。對於所有類型，都有這個類型的一個不可歸約的規範程序；它們叫做「規範形式」或「值」。如果每個程序都可以歸約到規範形式，則這個類型論被成為是「規範化」的(或「弱規範化」的)。如果規範形式是唯一性的，則這個理論被稱為「強規範化」的。可規範化性是多數非平凡的類型論所稀有的特徵，這是對邏輯世界的巨大違背。(回想起所有邏輯推導都有一個等價的正規推導)。概述其理由: 在接受遞歸定義的類型論中，有可能寫出用不歸約到一個值的程序；比如循環程序一般可以給予任何類型。特別是，有類型 ⊥ 的循環程序，儘管沒有「⊥ true 」的邏輯證明。為此，「命題為類型；證明為程序」範例只在一個方向上成立: 把一個類型論解釋為邏輯一般會給出一個不一致的邏輯。
象邏輯一樣，類型論也有很多擴展和變體，包括一階和高階版本。叫做依賴類型論 的一個有趣的類型論分支允許量詞設定範圍於在程序自身上。這些量化的類型被寫為 Π 和 Σ 替代
∀
{\displaystyle \forall }
∃
{\displaystyle \exists }
Γ
⊢
A
t
y
p
e
Γ
,
x
:
A
⊢
B
t
y
p
e
Γ
⊢
(
Π
x
:
A
)
.
B
t
y
p
e
Π
−
F
{\displaystyle {\frac {\Gamma \vdash A\ type\quad \Gamma ,x:A\vdash B\ type}{\Gamma \vdash (\Pi x:A).B\ type}}{\Pi -}F}
Γ
⊢
A
t
y
p
e
Γ
,
x
:
A
⊢
B
t
y
p
e
Γ
⊢
(
Σ
x
:
A
)
.
B
t
y
p
e
Σ
−
F
{\displaystyle {\frac {\Gamma \vdash A\ type\quad \Gamma ,x:A\vdash B\ type}{\Gamma \vdash (\Sigma x:A).B\ type}}{\Sigma -}F}
這些類型分別一般化了箭頭和乘積類型，通過它們的介入和除去規則。
Γ
,
x
:
A
⊢
π
:
B
Γ
⊢
λ
x
.
π
:
(
Π
x
:
A
)
.
B
Π
I
{\displaystyle {\frac {\Gamma ,x:A\vdash \pi :B}{\Gamma \vdash \lambda x.\pi :(\Pi x:A).B}}\Pi I}
Γ
⊢
π
1
:
(
Π
x
:
A
)
.
B
Γ
⊢
π
2
:
A
Γ
⊢
π
1
π
2
:
[
π
2
/
x
]
B
Π
E
{\displaystyle {\frac {\Gamma \vdash \pi _{1}:(\Pi x:A).B\quad \Gamma \vdash \pi _{2}:A}{\Gamma \vdash \pi _{1}\pi _{2}:[\pi _{2}/x]B}}\Pi E}
Γ
⊢
π
1
:
A
Γ
,
x
:
A
⊢
π
2
:
B
Γ
⊢
(
π
1
,
π
2
)
:
(
Σ
x
:
A
)
.
B
Σ
I
{\displaystyle {\frac {\Gamma \vdash \pi _{1}:A\quad \Gamma ,x:A\vdash \pi _{2}:B}{\Gamma \vdash (\pi _{1},\pi _{2}):(\Sigma x:A).B}}\Sigma I}
Γ
⊢
π
:
(
Σ
x
:
A
)
.
B
Γ
⊢
f
s
t
π
:
A
Σ
E
1
{\displaystyle {\frac {\Gamma \vdash \pi :(\Sigma x:A).B}{\Gamma \vdash \mathbf {fst} \ \pi :A}}\Sigma E_{1}}
Γ
⊢
π
:
(
Σ
x
:
A
)
.
B
Γ
⊢
s
n
d
π
:
[
f
s
t
π
/
x
]
B
Σ
E
2
{\displaystyle {\frac {\Gamma \vdash \pi :(\Sigma x:A).B}{\Gamma \vdash \mathbf {snd} \ \pi :[\mathbf {fst} \ \pi /x]B}}\Sigma E_{2}}
完全一般性的依賴類型論是非常強力的: 它可以把幾乎所有程序的可想象的性質直接表達為程序的類型。這種一般性來自於高代價 — 檢查一個給定程序是否有給定類型是不可判定的。為此，依賴類型理論在實踐中不允許在任意程序上的量化，而是限制於給定的可判定的「索引域」的程序，例如整數，字符串或線性程序。
因為依賴類型論允許類型依賴於程序，有一個自然的問題要問，程序依賴於類型或者任何其他組合是否是可能的。對這個問題有很多種回答。類型論中一個流行的方式是允許程序量化在類型上，也叫做「參數多態」；這還有兩個主要的種類: 如果類型和程序保持分離，則得到更好行為的系統，叫做「直謂多態」；如果在程序和類型之間的區別被模糊了，將得到高階邏輯的類型論對應，叫做「非直謂多態」。文獻中已經考慮了依賴性和多態性的各種組合，最著名的是 Henk Barendregt 的lambda立方 。
邏輯和類型論的交集是廣闊和活躍的研究領域。新邏輯通常以類型論架構來形式化，這叫做邏輯框架 。流行的現代邏輯框架比如構造演算 和 LF 是基於高階依賴類型論，帶有在可決定性和表達能力上的各種妥協。這些邏輯框架自身總是規定為自然演繹系統，這是對自然演繹方式的多功能性的明證。
為了簡單性，迄今為止提出的邏輯都是直覺的 。經典邏輯 向直覺邏輯擴展了補充的排中律 公理 或原理。
對於任何命題 p，命題 p ∨ ¬p 為真。 這個陳述沒有明顯的介入和除去；實際上，它涉及兩個不同連結詞。Gentzen 對排中律的最初處理規定了它是下列三個(等價)的公式之一，它們在希爾伯特 和 Heyting 的系統中已經已類似形式存在了:
A
∨
¬
A
t
r
u
e
X
M
{\displaystyle {\frac {}{A\lor \lnot A\ true}}XM}
¬
¬
A
t
r
u
e
A
t
r
u
e
¬
¬
C
{\displaystyle {\frac {\lnot \lnot A\ true}{A\ true}}\lnot \lnot _{C}}
¬
A
t
r
u
e
u
⋮
P
t
r
u
e
¬
A
t
r
u
e
u
⋮
¬
P
t
r
u
e
A
t
r
u
e
⊥
C
u
{\displaystyle {\cfrac {{\begin{matrix}{\frac {}{\lnot A\ true}}u\\\vdots \\P\ true\end{matrix}}\quad {\begin{matrix}{\frac {}{\lnot A\ true}}u\\\vdots \\\lnot P\ true\end{matrix}}}{A\ true}}\bot _{C}^{u}}
排中律的這種處理，除了被純粹主義者所反對之外，把額外的複雜介入到了規範形式的定義中。
相對更加另人滿意的以單獨的介入和除去規則處理經典自然演繹首次由 Parigot 在 1992 年提出，採用了叫做 λμ 的lambda 演算 的形式。他的方式的關鍵性洞察是把真理中心的判斷 A true 替代為更加經典的概念: 在局部化形式中，不再使用 Γ
⊢
{\displaystyle \vdash }
A ，他使用 Γ
⊢
{\displaystyle \vdash }
相繼式演算 轉移過來的，但是革新為 λμ 給予了經典自然演義證明一種計算性的意義，通過在 LISP 和它的後代中可見到的 callcc 或 throw/catch 機制的方式。(參見: 一級控制 )。
另一個重要擴展是模態 和其他不只需要基本的真理判斷的邏輯 。它們由 Prawitz 在 1965 年以自然演繹的樣式首次描述，並累積了大量有關的工作。給出一個簡單的例子，必然性的模態邏輯需要一個新判斷，「A valid 」，它是無條件的真理:
如果「A true」不在形如「B true」的假定之下，則「A valid」。 這個無條件判斷被主觀化為一元連結詞
◻
{\displaystyle \Box }
A (讀做「必然性的 A 」)，帶有如下的介入和除去規則:
A
v
a
l
i
d
◻
A
t
r
u
e
◻
I
{\displaystyle {\frac {A\ valid}{\Box A\ true}}\Box I}
◻
A
t
r
u
e
A
t
r
u
e
◻
E
{\displaystyle {\frac {\Box A\ true}{A\ true}}\Box E}
注意前提「A valid 」沒有定義規則；有效性的無條件定義替代了它的位置。這個模式在局部化形式中變得更加清楚，這時假設是明確的。我們寫「Ω; Γ
⊢
{\displaystyle \vdash }
A true 」，這裡的 Γ 象以前一樣包含真假定，而 Ω 包含有效假定。在右面只有一個單一的判斷「A true 」；這裡不需要有效性，因為「Ω
⊢
{\displaystyle \vdash }
A valid 」被定義為同於「Ω;
⋅
⊢
{\displaystyle \cdot \vdash }
A true 」。介入和除去形式為:
Ω
;
⋅
⊢
π
:
A
t
r
u
e
Ω
;
⋅
⊢
b
o
x
π
:
◻
A
t
r
u
e
◻
I
{\displaystyle {\frac {\Omega ;\ \cdot \vdash \pi :A\ true}{\Omega ;\ \cdot \vdash \mathbf {box} \ \pi :\Box A\ true}}\Box I}
Ω
;
Γ
⊢
π
:
◻
A
t
r
u
e
Ω
;
Γ
⊢
u
n
b
o
x
π
:
A
t
r
u
e
◻
E
{\displaystyle {\frac {\Omega ;\ \Gamma \vdash \pi :\Box A\ true}{\Omega ;\ \Gamma \vdash \mathbf {unbox} \ \pi :A\ true}}\Box E}
模態假設有自己版本的假設規則和代換定理。
Ω
,
u
:
(
A
v
a
l
i
d
)
;
Γ
⊢
u
:
A
t
r
u
e
v
a
l
i
d
−
h
y
p
{\displaystyle {\frac {}{\Omega ,u:(A\ valid);\Gamma \vdash u:A\ true}}{valid-}hyp}
模態代換定理
如果
Ω
;
⋅
⊢
π
1
:
A
t
r
u
e
{\displaystyle \Omega \ ;\cdot \vdash \pi _{1}:A\ true}
Ω
,
u
:
(
A
v
a
l
i
d
)
;
Γ
⊢
π
2
:
C
t
r
u
e
{\displaystyle \Omega ,u:(A\ valid);\Gamma \vdash \pi _{2}:C\ true}
Ω
;
Γ
⊢
[
π
1
/
u
]
π
2
:
C
t
r
u
e
{\displaystyle \Omega ;\Gamma \vdash [\pi _{1}/u]\pi _{2}:C\ true}
把判斷分解到不同假設搜集中的這種框架也叫做「多區」或「多價」上下文，是非常強力和可擴展性的；它已經被用於很多不同的模態邏輯[5]，線性邏輯 [6]和其他亞結構邏輯 中。
相繼式演算是自然演繹作為數理邏輯 基礎的主要替代者。在自然演繹中信息流是雙向的: 除去規則流向下解構，而介入規則流向上構造。所以，自然演繹證明不能純粹自上而下或自下而上的閱讀，這使得它不適於證明查找的自動化，甚至不適於證明檢查(或類型論中類型檢查)。為此，根岑 在1935年提出了他的相繼式演算 ，他最初打算把它作為澄清謂詞邏輯 的一致性的技術手段。克萊尼 在 1952 年於著作《Introduction to Metamathematics》(ISBN 978-0-7204-2103-3 )中，給出了相繼式演算的第一個現代樣式的形式化。
在相繼式演算中，所有推理規則都可以純粹的自底向上的閱讀。推理規則可以應用於十字轉門兩側的元素之上。(為了區分於自然演繹，本文對相繼式使用雙箭頭 ⇒ 來替代
⊢
{\displaystyle \vdash }
Γ
⇒
A
Γ
⇒
A
∨
B
∨
R
1
{\displaystyle {\frac {\Gamma \Rightarrow A}{\Gamma \Rightarrow A\lor B}}\lor R_{1}}
Γ
⇒
B
Γ
⇒
A
∨
B
∨
R
2
{\displaystyle {\frac {\Gamma \Rightarrow B}{\Gamma \Rightarrow A\lor B}}\lor R_{2}}
而左規則:
Γ
,
u
:
A
⇒
C
Γ
,
v
:
B
⇒
C
Γ
,
w
:
(
A
∨
B
)
⇒
C
∨
L
{\displaystyle {\frac {\Gamma ,u:A\Rightarrow C\quad \Gamma ,v:B\Rightarrow C}{\Gamma ,w:(A\lor B)\Rightarrow C}}\lor L}
讓人想起局部化形式的自然演繹的 ∨E 規則:
Γ
⊢
A
∨
B
Γ
,
u
:
A
⊢
C
Γ
,
v
:
B
⊢
C
Γ
⊢
C
∨
E
{\displaystyle {\frac {\Gamma \vdash A\lor B\quad \Gamma ,u:A\vdash C\quad \Gamma ,v:B\vdash C}{\Gamma \vdash C}}\lor E}
命題 A ∨ B ，是在 ∨E 中的一個前提的後件，轉變成在左規則 ∨ 中結論的一個假設。所以，左規則可以被看作某種反向的除去規則。
在相繼式演算中，左和右規則銜接着(lock-step)進行，直到到達初始相繼式 ，它對應於自然演繹中除去規則和介入規則的匯合點。這些初始化規則粗淺的類似於自然演繹的假設規則，但是在相繼式演算中它們描述左和右命題的換位 (transposition)或「握手」:
Γ
,
u
:
A
⇒
A
i
n
i
t
{\displaystyle {\frac {}{\Gamma ,u:A\Rightarrow A}}init}
在相繼式演算和自然演繹之間的對應是一對可靠性和完備性定理，它們都是可以通過歸納論證來證明的。
⇒
{\displaystyle \Rightarrow }
⊢
{\displaystyle \vdash }
如果
Γ
⇒
A
{\displaystyle \Gamma \Rightarrow A}
Γ
⊢
A
{\displaystyle \Gamma \vdash A}
⇒
{\displaystyle \Rightarrow }
⊢
{\displaystyle \vdash }
如果
Γ
⊢
A
{\displaystyle \Gamma \vdash A}
Γ
⇒
A
{\displaystyle \Gamma \Rightarrow A}
很明顯通過這些定理，相繼式演算不改變真理的概念，因為同一組命題仍然是真的。所以，你可以使用同樣的證明對象，如以前在相繼式推導中一樣。作為例子，考慮合取。右規則實質上等同於介入規則
相繼式演算
自然演繹
Γ
⇒
π
1
:
A
Γ
⇒
π
2
:
B
Γ
⇒
(
π
1
,
π
2
)
:
A
∧
B
∧
R
{\displaystyle {\frac {\Gamma \Rightarrow \pi _{1}:A\quad \Gamma \Rightarrow \pi _{2}:B}{\Gamma \Rightarrow (\pi _{1},\pi _{2}):A\land B}}\land R}
Γ
⊢
π
1
:
A
Γ
⊢
π
2
:
B
Γ
⊢
(
π
1
,
π
2
)
:
A
∧
B
∧
I
{\displaystyle {\frac {\Gamma \vdash \pi _{1}:A\quad \Gamma \vdash \pi _{2}:B}{\Gamma \vdash (\pi _{1},\pi _{2}):A\land B}}\land I}
但是，左規則進行了在相應的除去規則中不進行的額外替換。
相繼式演算
自然演繹
Γ
,
v
:
(
A
∧
B
)
,
u
:
A
⇒
π
:
C
Γ
,
v
:
(
A
∧
B
)
⇒
[
f
s
t
v
/
u
]
π
:
C
∧
L
1
{\displaystyle {\frac {\Gamma ,v:(A\land B),u:A\Rightarrow \pi :C}{\Gamma ,v:(A\land B)\Rightarrow [\mathbf {fst} \ v/u]\pi :C}}\land L_{1}}
Γ
⊢
π
:
A
∧
B
Γ
⊢
f
s
t
π
:
A
∧
E
1
{\displaystyle {\frac {\Gamma \vdash \pi :A\land B}{\Gamma \vdash \mathbf {fst} \ \pi :A}}\land E_{1}}
Γ
,
v
:
(
A
∧
B
)
,
u
:
B
⇒
π
:
C
Γ
,
v
:
(
A
∧
B
)
⇒
[
s
n
d
v
/
u
]
π
:
C
∧
L
2
{\displaystyle {\frac {\Gamma ,v:(A\land B),u:B\Rightarrow \pi :C}{\Gamma ,v:(A\land B)\Rightarrow [\mathbf {snd} \ v/u]\pi :C}}\land L_{2}}
Γ
⊢
π
:
A
∧
B
Γ
⊢
s
n
d
π
:
B
∧
E
2
{\displaystyle {\frac {\Gamma \vdash \pi :A\land B}{\Gamma \vdash \mathbf {snd} \ \pi :B}}\land E_{2}}
所以在相繼式演算中生成證明的種類和從自然演繹中生成的是相當不同的。相繼式演算生成的證明叫做「β-正規η-長」形式，它對應於自然演繹證明的正規形式的規範表示。如果你嘗試使用自然演繹自身來描述這些證明，你將得到所謂的「插入演算」(由 John Byrnes [3] 首先描述的)，它可以用來形式化的定義自然演繹的「正規形式」的概念。
自然演繹的代換定理在相繼式演算中採用了結構規則 或叫做切 的結構定理的形式。
切(代換)
如果
Γ
⇒
π
1
:
A
{\displaystyle \Gamma \Rightarrow \pi _{1}:A}
Γ
,
u
:
A
⇒
π
2
:
C
{\displaystyle \Gamma ,u:A\Rightarrow \pi _{2}:C}
Γ
⇒
[
π
1
/
u
]
π
2
:
C
{\displaystyle \Gamma \Rightarrow [\pi _{1}/u]\pi _{2}:C}
在多數有良好行為的邏輯中，切作為推理規則不是必需的，儘管它仍是可證明為一個元定理；切規則的多餘通常表現為一個計算過程，叫做「切除去」。這是自然演繹的一個有趣的應用；通常直接在自然演繹中證明特定性質是非常冗長的，因為有無限制數目的情況。例如，考慮證明給定的命題在自然演繹中是不可證明的。一個簡單歸納論證將失敗，因為規則如 ∨E 或 E，它們介入了任意的命題。但是，我們知道相繼式演算關於自然演繹是完備的，所以在自然演繹中證明這中不可證明性就足夠了。現在如果切不能獲得為一個推理規則，則所有相繼式規則要麼介入一個連結詞於右側要麼於左側，所以相繼式推導的深度完全受限於在最終結論中的連結詞。所以，證明不可證明性是非常容易的，因為只有有限數目的情況要考慮，而每個情況都完全由結論的子公式組成的。一個簡單的實例是「全局一致性」定理:「
⋅
⊢
⊥
{\displaystyle \cdot \vdash \bot }
true 」是不可證明的。在相繼式演算中，這明顯為真，因為沒有規則可以有「
⋅
⇒
⊥
{\displaystyle \cdot \Rightarrow \bot }
^
A
prop
B
prop
A
true
B
true
A
∧
B
true
∧
I
{\displaystyle {\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}\qquad A{\hbox{ true}}\qquad B{\hbox{ true}}}{A\wedge B{\hbox{ true}}}}\ \wedge _{I}}
A
∧
B
prop
A
true
B
true
A
∧
B
true
∧
I
{\displaystyle {\frac {A\wedge B{\hbox{ prop}}\qquad A{\hbox{ true}}\qquad B{\hbox{ true}}}{A\wedge B{\hbox{ true}}}}\ \wedge _{I}}
∧
F
{\displaystyle \wedge _{F}}
![{\displaystyle {\cfrac {[a/x]A\ true}{\forall x.\ A\ true}}\forall I^{a}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/55c84a6b941e1fec85e76166b84c9c4f1785cde4)
![{\displaystyle {\cfrac {\forall x.\ A\ true}{[t/x]A\ true}}\forall E}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fae665da08791eaf042af2f6036266be5c8a6aad)
![{\displaystyle {\cfrac {[t/x]A\ true}{\exists x.\ A\ true}}\exists I}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a8220b3297649aa562c716ff09b4814afb641bcc)
![{\displaystyle {\cfrac {\exists x.\ A\ true\quad {\begin{matrix}{\frac {}{[a/x]A\ true}}u\\\vdots \\C\ true\end{matrix}}}{C\ true}}\exists E^{a,u}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9a9eef1d9c05b847fb6b674ccea532c0d8234c38)
![{\displaystyle \Gamma \vdash [\pi _{1}/u]\pi _{2}:B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ecfe644785ebe59bf6cafff72e04f4a2b6ee3e5b)
![{\displaystyle {\frac {\Gamma \vdash \pi _{1}:(\Pi x:A).B\quad \Gamma \vdash \pi _{2}:A}{\Gamma \vdash \pi _{1}\pi _{2}:[\pi _{2}/x]B}}\Pi E}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7b5025bc159c0e2ed973e79a8cdda9e946f6cb65)
![{\displaystyle {\frac {\Gamma \vdash \pi :(\Sigma x:A).B}{\Gamma \vdash \mathbf {snd} \ \pi :[\mathbf {fst} \ \pi /x]B}}\Sigma E_{2}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cde4f6fd6eedfcebfc3e32af62256af212a7c498)
![{\displaystyle \Omega ;\Gamma \vdash [\pi _{1}/u]\pi _{2}:C\ true}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b6880e5d05bbc925361bdacf7d0cf0de95768e2f)
![{\displaystyle {\frac {\Gamma ,v:(A\land B),u:A\Rightarrow \pi :C}{\Gamma ,v:(A\land B)\Rightarrow [\mathbf {fst} \ v/u]\pi :C}}\land L_{1}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f02318831631f0c7bce5c1eeb03e5cd232d90dfe)
![{\displaystyle {\frac {\Gamma ,v:(A\land B),u:B\Rightarrow \pi :C}{\Gamma ,v:(A\land B)\Rightarrow [\mathbf {snd} \ v/u]\pi :C}}\land L_{2}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4deedfbd744fd16636262aa4c032f86a1fd55b4e)
![{\displaystyle \Gamma \Rightarrow [\pi _{1}/u]\pi _{2}:C}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d4a23ea989701adb0f8702971ddb57418dc93ab6)
