自然演绎来源自对共通于弗雷格 、罗素 和希尔伯特 系统的判句 公理化(希尔伯特演绎系统 )的不满。这种公理化最著名使用是在罗素 和怀特海 的《数学原理 》的数学论述中。在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 和 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 }
(B
⊃
{\displaystyle \supset }
(A ∧ B)) true”的推导:
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 }
(A ∧ B) true”的推导假设了前件“A true”(命名为 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}}
关于高阶逻辑的介入和除去规则的讨论超出了本文的范围。有介于一阶和高阶逻辑之间的逻辑。例如,二阶逻辑有两类命题,第一类量化于项,第二类量化于第一类命题之上。