查看“︁自然演绎”︁的源代码


在[[数理逻辑]]中，'''自然演绎'''是[[证明论]]中尝试提供象“自然”发生一样的逻辑推理形式模型的一种方式。這種方式對比於使用[[公理]]的[[公理系統]]。

== 动机 ==
自然演绎来源自对共通于[[弗雷格]]、[[罗素]]和[[希尔伯特]]系统的[[命题逻辑|判句]]公理化([[希尔伯特演绎系统]])的不满。这种公理化最著名使用是在[[罗素]]和[[怀特海]]的《[[数学原理]]》的数学论述中。在1926年由[[扬·武卡谢维奇]]在波兰发起的一系列研讨会提倡一种对逻辑的更加自然处理，[[斯坦尼斯瓦夫·亚希科夫斯基]]做了定义更自然的演绎的最早尝试，首先在1929年使用了一种图表表示法，并在1934年和1935年的一序列论文中更改了他的提议。但是他的提议没有流行起来。现代形式的自然演绎是由德国数学家[[格哈德·根岑]]于1935年在一篇提交给哥廷根大学数学系的学位论文中独立提出的。术语'''自然演绎'''就是在那篇论文中出现的:

::我首先希望构造一种尽可能地接近實際推理的形式化主義。所以提议了“'''自然演绎演算'''”。
::
::{{Lang|de|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'''“.}}
<div style="text-align: right; font-size: 80%;"> — Gentzen, 《Untersuchungen über das logische Schließen》(Mathematische Zeitschrift 39, pp.176-210, 1935)</div>

根岑被建立数论的一致性证明的目标所推动，因而找到了他的自然演绎演算的直接使用。但他不满意自己证明的复杂性，并在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''，符号化写为 "<math>A \wedge B</math>"。我们可以用推理规则的形式把它写为:
:<math>\frac{A\hbox{ prop} \qquad B\hbox{ prop}}{A \wedge B\hbox{ prop}}\ \wedge_F</math>
这个推理规则是“模式性”的: ''A'' 和 ''B'' 可以示例任何表达式。推理规则的一般形式为:

:<math>\frac{J_1 \qquad J_2 \qquad \cdots \qquad J_n}{J}\ \hbox{name}</math>

这里的每个 <math>J_i</math> 都是一个判断，而推理规则被命名为“name”。横线上的判断叫做'''前提'''，而横线下的判断叫做'''结论'''。其他常见的逻辑命题是析取(<math>A \vee B</math>)，否定(<math>\neg A</math>)，蕴涵(<math>A \supset B</math>)，和逻辑永真(<math>\top</math>) 和永假(<math>\bot</math>)。它们的形成规则如下。

:<math>
\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
</math><br /><br /><math>
\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
</math>

==介入和除去规则==

现在我们讨论“''A'' 为真(是真理)”判断。在本文余下部分中，我们将在已被理解的地方省略“prop”判断。在结论中介入逻辑连结词的推理规则叫做'''介入规则'''。要介入合取，就是说从命题 ''A'' 和 ''B'' 推导出“''A and B'' 为真” ，你需要“''A'' 为真和 ''B'' 为真”的证据。作为一个推理规则:
:<math>
\frac{A\hbox{ true} \qquad B\hbox{ true}}{A \wedge B\hbox{ true}}\ \wedge_I
</math>
上述规则实际上是省略命题判断的简写<ref>
<math>
\frac{A\hbox{ prop} \qquad B\hbox{ prop} \qquad A\hbox{ true} \qquad B\hbox{ true}}{A \wedge B\hbox{ true}}\ \wedge_I
</math>
这还可以写为:
<math>
\frac{A \wedge B\hbox{ prop} \qquad A\hbox{ true} \qquad B\hbox{ true}}{A \wedge B\hbox{ true}}\ \wedge_I
</math>
在这种形式中，第一个前提可以通过针对前面形式的前两个前提的 <math>\wedge_F</math> 形成规则来满足。</ref>。

在空无(nullary)的情况下，你可以从没有前提中推导出真理。
:<math>
\frac{\ }{\top\hbox{ true}}\ \top_I
</math>
注意在空无的情况下，对于虚假是没有介入规则的。所以你永远不能从更简单的判断推导出虚假。

如果一个命题的真实性可以通过多于一种方式来确立，则相应的连结词有多个介入规则。
:<math>
\frac{A\hbox{ true}}{A \vee B\hbox{ true}}\ \vee_{I1}
\qquad
\frac{B\hbox{ true}}{A \vee B\hbox{ true}}\ \vee_{I2}
</math>

对偶于介入规则的是描述如何把关于复合命题的信息解构为关于它的成员的信息的'''除去规则'''。因此，从“''A ∧ B'' 为真”，我们可以推导出 “''A'' 为真”和 “''B'' 为真”:
:<math>
\frac{A \wedge B\hbox{ true}}{A\hbox{ true}}\ \wedge_{E1}
\qquad
\frac{A \wedge B\hbox{ true}}{B\hbox{ true}}\ \wedge_{E2}
</math>

我们已经见到的推理不足以陈述蕴涵介入或析取除去的规则；为此我们需要'''假言推导'''的更一般的概念。

===例子===
作为推理规则的使用例子，考虑合取的交换律。如果 ''A ∧ B'' 为真，则 ''B ∧ A'' 为真；这可以通过以底下推理的前提匹配上面推理的结论的方式构成推理规则来完成这种推导。

:<math>
 \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
</math>

==假言推导==
在数理逻辑中普遍性的操作是“依据假定的推理”。例如，考虑下列推导:
:<math>
\cfrac{A \wedge \left ( B \wedge C \right ) \ true}{\cfrac{B \wedge C \ true}{B \ true} \wedge E_1} \wedge E_2
</math>
这个推导不确立 ''B'' 为真；而确立了下列事实:
:如果“A ∧ (B ∧ C) true”则“B true”。
在逻辑中，我们读做“假定 A ∧ (B ∧ C) 为真，我们证实 B 为真”；换句话说，判断“B true”依赖于假定的判断“A ∧ (B ∧ C) true”。这叫做'''假言推导'''，它可写为如下:
:<math>
\begin{matrix}
A \wedge \left ( B \wedge C \right ) \ true \\
\vdots \\
B \ true
\end{matrix}
</math>
释义为: “B true”推导自“A ∧ (B ∧ C) true”。当然，在这个特定的例子中我们实际上知道“B true”来自“A ∧ (B ∧ C) true”的推导，但是一般而言，我们不可以'''先验'''的知道这个推导。假言推导的一般形式为:
:<math>
\begin{matrix}
D_1 \quad D_2 \cdots D_n \\
\vdots \\
J
\end{matrix}
</math>
每个假言推导都有写在顶行的一组'''前件'''推导(''D<sub>i</sub>'')，和写在底行的一个'''后件'''判断(''J'')。每个前提自身都可以是一个假言推导。(出于简单性，我们把这种判断处理为无前提推导。)

===推理规则===
假言判断的概念被主观化为蕴涵的连结词。'''蕴涵介入规则'''和'''蕴涵除去规则'''如下。
:<math>
\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
</math>

在介入规则中，命名为 ''u'' 的前件被“注入”到结论中。这是界定假设的范围的机制: 它存在的唯一理由是确立 “B true”；它不能被用做任何其他目的，特别是，它不能被用在这个介入之下。作为一个例子，考虑“A <math>\supset</math> (B <math>\supset</math> (A ∧ B)) true”的推导:
:<math>
\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
</math>
这是个没有不满足前提的完整推导；但是，子推导是假设的。例如“B <math>\supset</math> (A ∧ B) true”的推导假设了前件“A true”(命名为 ''u'')。

通过假言推导，我们现在写出'''析取除去规则''':
:<math>
\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}
</math>

用口语说，如果“A ∨ B true”，并且我们可以从“A true”和“B true”二者推出“C true”，则确实“C true” 。注意这个规则不依靠于“A true”或“B true”中的任何一个。

在空无的情况下，我们得到下列有关虚假的除去规则:
:<math>
\frac{\perp true}{C \ true} \perp\!E
</math>
这读做: 如果虚假为真，则任何命题 ''C'' 为真。

'''否定介入规则'''和'''否定除去规则'''类似于蕴涵。
:<math>
\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
</math>

介入规则注入了假设 ''u'' 的名字。因为这些规则是模式性的，介入规则的释义为: 如果我们可以从“A true”推导出“P true”和“&not;P true”，就是 <math>\bot</math>；则 ''A'' 必定为假，也就是“&not;A true”。对于除去规则，如果 ''A'' 和 ''&not;A'' 二者都被证明为真，则这是个矛盾 <math>\bot</math>，在这种情况下所有命题 ''C'' 为真。因为蕴涵和否定的规则如此的类似，很容易看出 ''&not;A'' 和 ''A <math>\supset</math> ⊥'' 是等价的，就是可以相互推导的。

==一致性，完备性和规范形式==
一个[[理论]]被称为是一致(相容)的，如果虚假(从没有前提)是不能证明的，被称为是完备的，如果所有定理都可以使用这个逻辑的推理规则来证明。这是关于整体的逻辑的陈述，并通常和某种[[模型论|模型]]的概念联系在一起。但是，还有对推理规则的纯粹语法检查的一致性和完备性的局部的概念，而不需要诉诸模型。首先是局部一致性，也叫做还原性，它声称包含了一个连结词的介入、并立即跟随着它的除去的任何推导都可以被转换成不包含这种迂回的等价推导。这是对除去规则力量的检查: 它们不能强大得包含了在前提中没有包含的知识。作为一个例子，考虑合取。

{| style="margin-left: 2em;"
|-
|
<math>
\cfrac { \frac {}{A \ true}u \quad \frac {}{B \ true}w } {
\cfrac {A \land B \ true} {A \ true} \lor E_1
} \land I

</math>
|  style="width:30px; text-align:center;"| &rArr; ||
<math>
\cfrac {} {A \ true} u
</math>
|}

作为对偶，局部完备性声称除去规则足够强大来把一个连结分解成适合它的介入规则的形式。再次考虑合取:

{| style="margin-left: 2em;"
|-
|
<math>
\cfrac {} {A \land B \ true}u
</math>
|  style="width:30px; text-align:center;"| &rArr; ||
<math>
\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
</math>
|}

使用[[Curry-Howard同构]]，除去规则和介入规则分别精确的对应于[[lambda 演算]]中的 [[β-归约]]和 [[η-展开]]。通过局部完备性，我们看到所有推导都可以被转换成介入主要连结词的等价推导，实际上，如果整个推导都服从除去跟随着介入的这种次序，则可以被称为是'''规范的'''。在规范推导中，所有除去都出现在介入上面。在大多数逻辑中，所有推导都有等价的规范推导，叫做'''规范形式'''。规范形式的存在使用自然演绎自身一般是难于证明的，这种理由确实存在于文献中，其中最著名的是 [[Dag Prawitz]] 1961年的书《Natural deduction: a proof-theoretical study》，A&W Stockholm 1965,没有ISBN。通过[[切消定理|免切]][[相继式演算]]表达的方式做间接的证明是非常容易的。

==一阶扩展==
[[File:first_order_natural_deduction.png|thumb|right|一阶系统总结]]

前面章节中的逻辑是“单类”逻辑的例子，单类逻辑只带有单一一类对象: 命题。已经提出了对这个简单框架的很多扩展；在本章中我们将向它扩展上第二类对象：'''个体'''或'''项'''。更精确地说，我们将增加新的一类判断 “''t'' 是项”(或“''t term''”)，这是的 ''t'' 是模式性的。我将固定一个'''变量'''的[[可数集合]] ''V''，'''函数符号'''的可数集合 ''F''，并如下这样构造项:

{| style="margin-left: 2em;"
|-
|
<math>
\frac {v \in V}{v \ term} {var-}F
</math>
| style="width:10%;"| || 
<math>
\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
</math>
|}
对于命题，我们考虑第三个'''谓词'''的可数集合。并用如下规则定义“在项之上的原子谓词”:

{| style="margin-left: 2em;"
|-
|
<math>
\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
</math>
|}

此外，我们增加一对“量化的”命题: 全称(<math>\forall</math>)和存在(<math>\exists</math>):

{| style="margin-left: 2em;"
|-
|
<math>
\cfrac {
\begin{matrix}
\frac {}{x \ term}u \\
\vdots \\
A \ prop \\
\end{matrix}
} {\forall x. \ A \ prop }
\forall F^u
</math>
| style="width:10%;"| || 
<math>
\cfrac {
\begin{matrix}
\frac {}{x \ term}u \\
\vdots \\
A \ prop \\
\end{matrix}
} {\exists x. \ A \ prop }
\exists F^u
</math>
|}

这些量化的命题有如下的介入和除去规则。


{| style="margin-left: 2em;"
|-
|
<math>
\cfrac {
[a/x] A \ true
}
{ \forall x. \ A \ true }
\forall I^a
</math>
| style="width:10%;"| || 
<math>
\cfrac { \forall x. \ A \ true}
{ [t/x] A \ true } \forall E
</math>
|-
|
<math>
\cfrac { [t/x] A \ true}
{ \exists x. \ A \ true }
\exists I
</math>
| style="width:10%;"| || 
<math>
\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}
</math>
|}

在这些规则中，符号 [''t''/''x''] ''A'' 表示代换 ''A'' 中 ''x'' 的所有(可见)实例为 ''t''，避免它被其他量词捕获；关于这种标准操作的详细描述请参见 [[lambda 演算]]。同前面一样，名字上的上标表示被注入的成分: 在 <math>\forall I</math>的结论中不能出现项 ''a''(这种项叫做'''本征变量'''或'''参数''')，在 <math>\exists E</math>中指名为 ''u'' 的假设被局部化到假言推导的第二个前提中。尽管早先章节中的命题逻辑是[[可判定的]]，增加量词使逻辑成为不可判定的。

==高阶扩展==
迄今为止量化扩展是“一阶的”: 它们用把命题区别于在其上量化的对象的种类。高阶逻辑采用了一种不同的方式，它只有一个种类的命题，量词的量化范围是同种类的命题，反映于形成规则:

{| style="margin-left: 2em;"
|-
|
<math>
\cfrac {
\begin{matrix}
\frac {}{p \ prop}u \\
\vdots \\
A \ prop \\
\end{matrix}
} {\forall p. \ A \ prop }
\forall F^u
</math>
| style="width:10%;"| || 
<math>
\cfrac {
\begin{matrix}
\frac {}{p \ prop}u \\
\vdots \\
A \ prop \\
\end{matrix}
} {\exists p. \ A \ prop }
\exists F^u
</math>
|}
关于高阶逻辑的介入和除去规则的讨论超出了本文的范围。有介于一阶和高阶逻辑之间的逻辑。例如，二阶逻辑有两类命题，第一类量化于项，第二类量化于第一类命题之上。

==证明论==
迄今为止对自然演绎的表述集中于命题的本质而没有给出'''证明'''的形式定义。要形式化证明的概念，我们要稍微更改假言推导的表述。我们向前件标签上'''证明变量'''(来自某个变量的可数集合 ''V'')，并用实际证明装饰后件。通过'''十字转门'''(turnstile)<math>\vdash</math>的方式把前件或'''假设'''同后件分隔开。这种修改有时叫做'''局部化假设'''。下列图示总结变更。

{| style="margin-left: 2em;"
|-
|
<math>
\begin{matrix}
\frac {}{J_1}u_1 \quad \frac {}{J_2}u_2 \quad \cdots \frac {}{J_n}u_n \\
\vdots \\
J \\
\end{matrix}
</math>
|  style="width:10%; text-align:center;"| &rArr; ||
<math>
u_1:J_1, u_2:J_2, ..., u_n:J_n \vdash J</math>
|}
假设的搜集将被写为 Γ，当它们的精确内容是无关的时候。要使证明直接了当，我们把无关证明的判断“''A true''”换成判断“π 是证明(A true)”，它在符号上被写为“π : ''A true''”。服从标准方式，证明用它们自己的对“π ''proof''”的形成规则来指定。最简单的可能的证明是使用带标签的假设；在这种情况下证据是标签自身。

{| style="margin-left: 2em;"
|-
|
<math>
\frac {u \in V} {u \ proof} {proof-}F
</math>
| style="width:10%;"| || 
<math>
\frac {} {u:A \ true \vdash u : A \ true} hyp
</math>
|}
为了简短，我们在本文余下部分去掉判断标签 “true”，就写为“Γ <math>\vdash</math> π : ''A''”。让我们通过明确的证明来重新检验某些连结词。对于合取，我们查看介入规则 ∧I 来发现合取的证明形式: 它们必须是两个合取项的一对证明。就是:

{| style="margin-left: 2em;"
|-
|
<math>
\frac { \pi _1 \ proof \quad \pi _2 \ proof }
{(\pi _1, \pi _2) \ proof}{pair-}F
</math>
| style="width:10%;"| || 
<math>
\frac { \Gamma \vdash \pi _1 : A \quad \Gamma \vdash \pi _2 : B }
{ \Gamma \vdash (\pi _1, \pi _2) : A \land B } \land I
</math>
|}
除去规则 ∧E<sub>1</sub> 和 ∧E<sub>2</sub> 选择要么左面的要么右面的合取项；所以证明是一对投影 — 第一个('''fst''') 和第二个('''snd''')。

{| style="margin-left: 2em;"
|-
|
<math>
\frac
{ \pi \ proof }
{ \mathbf{fst}\ \pi \ proof }
{fst-}F
</math>
| style="width:10%;"| || 
<math>
\frac
{ \Gamma \vdash \pi : A \land B }
{ \Gamma \vdash \mathbf{fst}\ \pi : A}
\land E_1
</math>
|-
|
<math>
\frac
{ \pi \ proof }
{ \mathbf{snd}\ \pi \ proof }
{snd-}F
</math>
| style="width:10%;"| || 
<math>
\frac
{ \Gamma \vdash \pi : A \land B }
{ \Gamma \vdash \mathbf{snd}\ \pi : B }
\land E_2
</math>
|}
对于蕴涵，介入形式的局部化或约束，书写要使用 λ；这对应于注入标签。在规则“Γ, ''u'':''A''”中表示一组假设 Γ，同增补的一个假设 ''u'' 在一起。

{| style="margin-left: 2em;"
|-
|
<math>
\frac
{\pi \ proof }
{\lambda u. \pi \ proof }
{\lambda -}F
</math>
| style="width:10%;"| || 
<math>
\frac
{ \Gamma , u:A \vdash \pi : B }
{ \Gamma \vdash \lambda u. \pi : A \supset B }
\supset I
</math>
|-
|
<math>
\frac
{ \pi _1 \ proof \quad \pi _2 \ proof }
{ \pi _1 \pi _2 \ proof }
{app-}F
</math>
| style="width:10%;"| || 
<math>
\frac
{ \Gamma \vdash \pi _1 : A \supset B \quad \Gamma \vdash \pi _2 : A }
{ \Gamma \vdash \pi _1 \pi _2 : B }
\supset E
</math>
|}
通过明确可用的证明，你可以操纵和思辩证明。证明的关键操作是用一个证明去替换在另一个证明中使用的假定。这通常叫做“代换定理”，并可以通过关于第二个判断的深度(或结构)的[[数学归纳法|归纳法]]证明。

; 代换定理: 如果 <math>\Gamma \vdash \pi _1 : A</math> 并且 <math> \Gamma, u: A \vdash \pi _2 : B</math>, 则 <math>\Gamma \vdash [\pi _1/u] \pi _2 : B</math> 。

==类型论==
迄今为止判断“Γ <math>\vdash</math> π : ''A''”有一个纯逻辑释义。在[[类型论]]中，逻辑观点被调换为更加可计算的对象的观点。在逻辑释义中的命题现在被看作'''类型'''，而证明被看作使用[[lambda 演算]]写的程序。所以“π : ''A''”的释义是“程序 π 有类型 ''A''”。逻辑连结词也有不同的读法: 合取被看作乘积(×)，蕴涵被读做函数箭头(→) 等等。区别只是装饰。类型论有使用形成、介入和除去规则的自然演绎表示；事实上，读者可以用前面的章节重新构造一个“简单的类型论”。

在逻辑和类型论之间的区别主要是把焦点从类型(命题)转移到了程序(证明)。类型论主要感兴趣于程序的可转换性和可归约性。对于所有类型，都有这个类型的一个不可归约的规范程序；它们叫做“规范形式”或“值”。如果每个程序都可以归约到规范形式，则这个类型论被成为是“规范化”的(或“弱规范化”的)。如果规范形式是唯一性的，则这个理论被称为“强规范化”的。可规范化性是多数非平凡的类型论所稀有的特征，这是对逻辑世界的巨大违背。(回想起所有逻辑推导都有一个等价的正规推导)。概述其理由: 在接受递归定义的类型论中，有可能写出用不归约到一个值的程序；比如循环程序一般可以给予任何类型。特别是，有类型 ⊥ 的循环程序，尽管没有“⊥ ''true''”的逻辑证明。为此，“命题为类型；证明为程序”范例只在一个方向上成立: 把一个类型论解释为逻辑一般会给出一个不一致的逻辑。

象逻辑一样，类型论也有很多扩展和变体，包括一阶和高阶版本。叫做[[依赖类型论]]的一个有趣的类型论分支允许量词设定范围于在程序自身上。这些量化的类型被写为 Π 和 Σ 替代 <math>\forall</math> 和 <math>\exists</math>，并有如下形成规则:

{| style="margin-left: 2em;"
|-
|
<math>
\frac
{ \Gamma \vdash A \ type \quad \Gamma , x:A \vdash B \ type }
{\Gamma \vdash (\Pi x:A). B \ type }
{\Pi -}F
</math>
| style="width:10%;"| || 
<math>
\frac
{ \Gamma \vdash A \ type \quad \Gamma , x:A \vdash B \ type }
{ \Gamma \vdash (\Sigma x:A). B \ type }
{\Sigma -}F
</math>
|}
这些类型分别一般化了箭头和乘积类型，通过它们的介入和除去规则。

{| style="margin-left: 2em;"
|-
|
<math>
\frac
{ \Gamma, x:A \vdash \pi : B }
{ \Gamma \vdash \lambda x. \pi : (\Pi x:A). B }
\Pi I
</math>
| style="width:10%;"| || 
<math>
\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
</math>
|}

{| style="margin-left: 2em;"
|-
|
<math>
\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
</math>
| style="width:10%;"| || 
<math>
\frac
{ \Gamma \vdash \pi : (\Sigma x:A). B }
{ \Gamma \vdash \mathbf{fst} \ \pi : A }
\Sigma E _1
</math>
| style="width:10%;"| || 
<math>
\frac
{ \Gamma \vdash \pi : (\Sigma x:A). B }
{ \Gamma \vdash \mathbf{snd} \ \pi : [ \mathbf{fst} \ \pi /x ] B }
\Sigma E _2
</math>
|}
完全一般性的依赖类型论是非常强力的: 它可以把几乎所有程序的可想象的性质直接表达为程序的类型。这种一般性来自于高代价 — 检查一个给定程序是否有给定类型是不可判定的。为此，依赖类型理论在实践中不允许在任意程序上的量化，而是限制于给定的可判定的“索引域”的程序，例如整数，字符串或线性程序。

因为依赖类型论允许类型依赖于程序，有一个自然的问题要问，程序依赖于类型或者任何其他组合是否是可能的。对这个问题有很多种回答。类型论中一个流行的方式是允许程序量化在类型上，也叫做“参数多态”；这还有两个主要的种类: 如果类型和程序保持分离，则得到更好行为的系统，叫做“直谓多态”；如果在程序和类型之间的区别被模糊了，将得到高阶逻辑的类型论对应，叫做“非直谓多态”。文献中已经考虑了依赖性和多态性的各种组合，最著名的是 [[Henk Barendregt]] 的[[lambda立方]]。

逻辑和类型论的交集是广阔和活跃的研究领域。新逻辑通常以类型论架构来形式化，这叫做[[逻辑框架]]。流行的现代逻辑框架比如[[构造演算]]和 [[逻辑框架|LF]] 是基于高阶依赖类型论，带有在可决定性和表达能力上的各种妥协。这些逻辑框架自身总是规定为自然演绎系统，这是对自然演绎方式的多功能性的明证。

==经典逻辑==
为了简单性，迄今为止提出的逻辑都是[[直觉逻辑|直觉的]]。[[经典逻辑]]向直觉逻辑扩展了补充的[[排中律]][[公理]]或原理。

:对于任何命题 p，命题 p ∨ &not;p 为真。

这个陈述没有明显的介入和除去；实际上，它涉及两个不同连结词。Gentzen 对排中律的最初处理规定了它是下列三个(等价)的公式之一，它们在[[希尔伯特]]和 [[Arend Heyting|Heyting]] 的系统中已经已类似形式存在了:


{| style="margin-left: 2em;"
|-
|
<math>
\frac {}
{ A \lor \lnot A \ true }
XM
</math>
| style="width:5%;"| || 
<math>
\frac
{ \lnot \lnot A \ true }
{ A \ true }
\lnot \lnot _C
</math>
| style="width:5%;"| || 
<math>
\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
</math>
|}

排中律的这种处理，除了被纯粹主义者所反对之外，把额外的复杂介入到了规范形式的定义中。

相对更加另人满意的以单独的介入和除去规则处理经典自然演绎首次由 [[Michel Parigot|Parigot]] 在 1992 年提出，采用了叫做 λμ 的[[lambda 演算]]的形式。他的方式的关键性洞察是把真理中心的判断 ''A true'' 替代为更加经典的概念: 在局部化形式中，不再使用 Γ <math>\vdash</math> ''A''，他使用 Γ <math>\vdash</math> Δ，而 Δ 是类似于 Γ 的一个命题的搜集。Γ 被处理为一个合取，而 Δ 是一个析取。这种结构本质上是直接从经典的[[相继式演算]]转移过来的，但是革新为 λμ 给予了经典自然演义证明一种计算性的意义，通过在 [[LISP]] 和它的后代中可见到的 [[callcc]] 或 throw/catch 机制的方式。(参见: [[一级控制]])。

==模态逻辑==
另一个重要扩展是[[模态逻辑|模态]]和其他不只需要基本的真理判断的逻辑 。它们由 [[Dag Prawitz|Prawitz]] 在 1965 年以自然演绎的样式首次描述，并累积了大量有关的工作。给出一个简单的例子，必然性的模态逻辑需要一个新判断，“''A valid''”，它是无条件的真理:

:如果“A true”不在形如“B true”的假定之下，则“A valid”。

这个无条件判断被主观化为一元连结词 <math>\Box</math>''A''(读做“必然性的 ''A''”)，带有如下的介入和除去规则:


{| style="margin-left: 2em;"
|-
|
<math>
\frac
{ A \ valid}
{ \Box A \ true }
\Box I
</math>
| style="width:5%;"| || 
<math>
\frac
{ \Box A \ true }
{ A \ true }
\Box E
</math>
|}

注意前提“''A valid''”没有定义规则；有效性的无条件定义替代了它的位置。这个模式在局部化形式中变得更加清楚，这时假设是明确的。我们写“Ω; Γ<math>\vdash</math>''A true''”，这里的 Γ 象以前一样包含真假定，而 Ω 包含有效假定。在右面只有一个单一的判断“''A true''”；这里不需要有效性，因为“Ω<math>\vdash</math>''A valid''”被定义为同于“Ω; <math>\cdot \vdash</math> ''A true''”。介入和除去形式为:

{| style="margin-left: 2em;"
|-
|
<math>
\frac
{ \Omega; \ \cdot \vdash \pi : A \ true }
{ \Omega; \ \cdot \vdash \mathbf{box} \ \pi : \Box A \ true }
\Box I
</math>
| style="width:5%;"| || 
<math>
\frac
{ \Omega; \ \Gamma \vdash \pi : \Box A \ true }
{ \Omega; \ \Gamma \vdash \mathbf{unbox} \ \pi : A \ true }
\Box E
</math>
|}

模态假设有自己版本的假设规则和代换定理。


{| style="margin-left: 2em;"
|-
|
<math>
\frac {}
{ \Omega, u: (A \ valid) ; \Gamma \vdash u : A \ true }
{valid-}hyp
</math>
|}

; 模态代换定理: 如果 <math>\Omega \ ; \cdot \vdash \pi _1 : A \ true</math> 并且 <math>\Omega , u : (A \ valid) ; \Gamma \vdash \pi _2 : C \ true</math>, 则 <math>\Omega ; \Gamma \vdash [\pi _1/u] \pi _2 : C \ true</math>。

把判断分解到不同假设搜集中的这种框架也叫做“多区”或“多价”上下文，是非常强力和可扩展性的；它已经被用于很多不同的模态逻辑[5]，[[线性逻辑]][6]和其他[[亚结构逻辑]]中。

==同相继式演算比较==
{{Main|相继式演算}}
相继式演算是自然演绎作为[[数理逻辑]]基础的主要替代者。在自然演绎中信息流是双向的: 除去规则流向下解构，而介入规则流向上构造。所以，自然演绎证明不能纯粹自上而下或自下而上的阅读，这使得它不适于证明查找的自动化，甚至不适于证明检查(或类型论中类型检查)。为此，[[根岑]]在1935年提出了他的[[相继式演算]]，他最初打算把它作为澄清[[谓词逻辑]]的一致性的技术手段。[[克萊尼]]在 1952 年于著作《Introduction to Metamathematics》(ISBN 978-0-7204-2103-3)中，给出了相继式演算的第一个现代样式的形式化。

在相继式演算中，所有推理规则都可以纯粹的自底向上的阅读。推理规则可以应用于十字转门两侧的元素之上。(为了区分于自然演绎，本文对相继式使用双箭头 &rArr; 来替代 <math>\vdash</math>。自然演绎的介入规则被看作相继式演算中“右规则”，并且在结构上非常类似。在另一方面除去规则对应相继式演算中“左规则”。作为例子，考虑析取；右规则是常见的:

{| style="margin-left: 2em;"
|-
|
<math>
\frac
{ \Gamma \Rightarrow A }
{ \Gamma \Rightarrow A \lor B }
\lor R _1
</math>
| with="10%" | || 
<math>
\frac
{ \Gamma \Rightarrow B }
{ \Gamma \Rightarrow A \lor B }
\lor R _2
</math>
|}
而左规则:

{| style="margin-left: 2em;"
|-
|
<math>
\frac
{ \Gamma, u:A \Rightarrow C \quad \Gamma, v:B \Rightarrow C }
{ \Gamma, w: (A \lor B) \Rightarrow C }
\lor L
</math>
|}
让人想起局部化形式的自然演绎的 ∨E 规则:

{| style="margin-left: 2em;"
|-
|
<math>
\frac
{ \Gamma \vdash A \lor B \quad \Gamma, u:A \vdash C \quad \Gamma, v:B \vdash C }
{ \Gamma \vdash C }
\lor E
</math>
|}
命题 ''A ∨ B''，是在 ∨E 中的一个前提的后件，转变成在左规则 ∨ 中结论的一个假设。所以，左规则可以被看作某种反向的除去规则。

在相继式演算中，左和右规则衔接着(lock-step)进行，直到到达'''初始相继式'''，它对应于自然演绎中除去规则和介入规则的汇合点。这些初始化规则粗浅的类似于自然演绎的假设规则，但是在相继式演算中它们描述左和右命题的'''换位'''(transposition)或“握手”:

{| style="margin-left: 2em;"
|-
|
<math>
\frac {}
{ \Gamma, u:A \Rightarrow A }
init
</math>
|}
在相继式演算和自然演绎之间的对应是一对可靠性和完备性定理，它们都是可以通过归纳论证来证明的。

;<math>\Rightarrow</math> 关于 <math>\vdash</math> 的可靠性: 如果 <math>\Gamma \Rightarrow A</math>, 则 <math>\Gamma \vdash A</math>。
;<math>\Rightarrow</math> 关于 <math>\vdash</math> 的完备性: 如果 <math>\Gamma \vdash A</math>, 则 <math>\Gamma \Rightarrow A</math>。

很明显通过这些定理，相继式演算不改变真理的概念，因为同一组命题仍然是真的。所以，你可以使用同样的证明对象，如以前在相继式推导中一样。作为例子，考虑合取。右规则实质上等同于介入规则

{| style="margin-left: 2em;"
|-
! 相继式演算
|
! 自然演绎
|-
|
<math>
\frac
{ \Gamma \Rightarrow \pi _1 : A \quad \Gamma \Rightarrow \pi _2 : B }
{ \Gamma \Rightarrow (\pi _1, \pi _2) : A \land B }
\land R
</math>
| style="width:20%;"| || 
<math>
\frac
{ \Gamma \vdash \pi _1 : A  \quad \Gamma \vdash \pi _2 : B }
{ \Gamma \vdash (\pi _1, \pi _2) : A \land B }
\land I
</math>
|}
但是，左规则进行了在相应的除去规则中不进行的额外替换。

{| style="margin-left: 2em;"
|-
! 相继式演算
|
! 自然演绎
|-
|
<math>
\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
</math>
| style="width:20%;"| || 
<math>
\frac
{ \Gamma \vdash \pi : A \land B }
{ \Gamma \vdash \mathbf{fst} \ \pi : A }
\land E _1
</math>
|-
|
<math>
\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
</math>
| style="width:20%;"| || 
<math>
\frac
{ \Gamma \vdash \pi : A \land B }
{ \Gamma \vdash \mathbf{snd} \ \pi : B }
\land E _2
</math>
|}

所以在相继式演算中生成证明的种类和从自然演绎中生成的是相当不同的。相继式演算生成的证明叫做“β-正规η-长”形式，它对应于自然演绎证明的正规形式的规范表示。如果你尝试使用自然演绎自身来描述这些证明，你将得到所谓的“插入演算”(由 John Byrnes [3] 首先描述的)，它可以用来形式化的定义自然演绎的“正规形式”的概念。

自然演绎的代换定理在相继式演算中采用了[[结构规则]]或叫做'''切'''的结构定理的形式。

; 切(代换) : 如果 <math> \Gamma \Rightarrow \pi _1 : A</math> 并且 <math>\Gamma, u : A \Rightarrow \pi _2 : C</math>, 则 <math>\Gamma \Rightarrow [\pi _1/u] \pi _2 : C</math>。

在多数有良好行为的逻辑中，切作为推理规则不是必需的，尽管它仍是可证明为一个元定理；切规则的多余通常表现为一个计算过程，叫做“切除去”。这是自然演绎的一个有趣的应用；通常直接在自然演绎中证明特定性质是非常冗长的，因为有无限制数目的情况。例如，考虑证明给定的命题在自然演绎中是不可证明的。一个简单归纳论证将失败，因为规则如 ∨E 或 E，它们介入了任意的命题。但是，我们知道相继式演算关于自然演绎是完备的，所以在自然演绎中证明这中不可证明性就足够了。现在如果切不能获得为一个推理规则，则所有相继式规则要么介入一个连结词于右侧要么于左侧，所以相继式推导的深度完全受限于在最终结论中的连结词。所以，证明不可证明性是非常容易的，因为只有有限数目的情况要考虑，而每个情况都完全由结论的子公式组成的。一个简单的实例是“全局一致性”定理:“<math>\cdot \vdash \bot</math>''true''”是不可证明的。在相继式演算中，这明显为真，因为没有规则可以有“<math>\cdot \Rightarrow \bot</math>”作为结论! 由于这个性质，证明论学者经常偏好免切相继式演算公式化。

==注释==
{{reflist}}

==引用==
*[[Jon Barwise]] and [[John Etchemendy]], 2000. ''Language Proof and Logic''. CSLI (University of Chicago Press) and New York: Seven Bridges Press. A gentle introduction to [[first-order logic]] via natural deduction, by two first rate logicians.
* {{cite book en
 | author = [[Jean-Yves Girard]]
 | url = http://www.paultaylor.eu/stable/Proofs+Types.html
 | publisher = Cambridge University Press, Cambridge, England
 | series = Cambridge Tracts in Theoretical Computer Science
 | title = Proofs and Types
 | year = 1990
 | access-date = 2013-07-01
 | archive-date = 2019-10-18
 | archive-url = https://web.archive.org/web/20191018231539/http://www.paultaylor.eu/stable/Proofs+Types.html
 }} Translated and with appendices by Paul Taylor and Yves Lafont.
* {{cite journal en
 |author=[[Per Martin-Löf]] 
 |url=http://www.hf.uio.no/filosofi/njpl/vol1no1/meaning/meaning.pdf 
 |title=On the meanings of the logical constants and the justifications of the logical laws 
 |journal=Nordic Journal of Philosophical Logic 
 |volume=1 
 |issue=1 
 |year=1996 
 |pages=11-60 
 |deadurl=yes 
 |archiveurl=https://web.archive.org/web/20051217231901/http://www.hf.uio.no/filosofi/njpl/vol1no1/meaning/meaning.pdf 
 |archivedate=2005-12-17 
}} Lecture notes to a short course at Università degli Studi di Siena, April 1983.
* {{cite journal en
 | author=Frank Pfenning and Rowan Davies
 | url=https://www.cs.cmu.edu/~fp/papers/mscs00.pdf
 | title=A judgmental reconstruction of modal logic
 | journal=Mathematical Structures in Computer Science
 | volume=11
 | issue=4
 | year=2001
 | pages=511-540
 | access-date=2013-07-01
 | archive-date=2021-05-07
 | archive-url=https://web.archive.org/web/20210507051215/https://www.cs.cmu.edu/~fp/papers/mscs00.pdf
 }}

==外部链接==
* [http://www.danielclemente.com/logica/dn.en.html Introduction to natural deduction] {{Wayback|url=http://www.danielclemente.com/logica/dn.en.html |date=20201204205616 }}
* [http://www.winterdrache.de/freeware/domino/ Domino On Acid] {{Wayback|url=http://www.winterdrache.de/freeware/domino/ |date=20050623084917 }}. Natural deduction visualized as a game of dominoes.
* [http://www.sfu.ca/~jeffpell/papers/pelletierNDtexts.pdf Pelletier, Jeff, "A History of Natural Deduction and Elementary Logic Textbooks"] {{Wayback|url=http://www.sfu.ca/~jeffpell/papers/pelletierNDtexts.pdf |date=20210506182210 }}

[[Category:逻辑演算]]
[[Category:演繹]]
[[Category:证明论]]
[[Category:证明方法]]