Fitch 式自然演绎

费奇式自然演绎
术语名称	费奇式自然演绎
英语名称	Fitch's natural deduction
别名	Fitch's notation

Fitch 式自然演绎(Fitch's natural deduction)是逻辑领域形式化公理系统中 Gentzen 式系统中自然演绎系统的一种。其中每行都是一个公式，这些公式会标注出其使用的规则以及依赖的公式，以反映公式间的变形关系。 Fitch 式自然演绎的特征是各行之间书写成一个并列、有行号的列表，各行之间的依赖关系通过注明依赖行号表达； Fitch 式自然演绎通过子证明表达假言推理，并且子证明构成层级关系。

说明：有部分材料使用的记号与现代标准记号不同，以下均按照现代记号表示。

描述

以下是 [math]\displaystyle{ p\rightarrow q\rightarrow p }[/math] 的一个证明。

  |---------
1 | | p     hyp
  | |-------
2 | | | q   hyp
  | | |-----
3 | | | p   reit,1
  | |
4 | | q→p  →I,2,3
  |
5 | p→q→p →I,1,4

以下是从 [math]\displaystyle{ p\rightarrow q }[/math] 到 [math]\displaystyle{ \lnot q \rightarrow \lnot p }[/math] 的一个演绎：

1 | p→q      hyp
  |----------
2 | | ¬q      hyp
  | |--------
3 | | p→q    reit, 1
  | |
4 | | | p     hyp
  | | |------
5 | | | p→q  reit, 3
  | | |
6 | | | q     →E, 4,5
  | | |
7 | | | ¬q    reit 2
  | |
8 | | ¬p      ¬I,4,6,7
  |
9 | ¬q→¬p    →I,2,8

符号及术语说明

部分材料中，记号可能有微小差异，请以具体记号为准。
演绎过程中的每一个公式称为一行(line)，且左侧有行号。
每条竖线代表一个子证明(subordinate proof)。竖线的右侧总是伸出一条横线。这条横线上方是当前子证明中的假设（若为最外层证明，则为整个演绎过程中的前提），下方为当前子证明中的变形步骤。
每行右侧有这一行使用的变形规则及其依赖行号，或仅指出这是一个假设而非变形结果。

特征

每行都是形式语言中的一个公式。
每个变形上方可以有一个或多个公式，但下方必须有且仅有一个公式。换句话说，变形规则的结论必须是一个公式。
证明中的每行都在这一行所依赖的前提下为真。其中所依赖的前提指所依赖的行中是前提的那些，而所依赖的行指这行所在的子证明及其右侧给出的依赖行号，及其间接再依赖的行号。如上例中第 6 行的 [math]\displaystyle{ q }[/math] 的依赖为 4,5 而 4 是一个 hyp ， 5 依赖 3 、 3 依赖 1 、 1 是一个 hyp ，因此所依赖的前提是第 1 行和第 4 行，即 [math]\displaystyle{ q }[/math] 在条件 [math]\displaystyle{ p\rightarrow q, p }[/math] 下成立。

记号约定

公式描述

Fitch 式自然演绎中使用的形式语言和命题语言、谓词语言的定义相同。

命题描述

一个证明或一个需证明命题通常被写成后继式 [math]\displaystyle{ \Gamma, \Delta, \phi \vdash \psi }[/math] 的形式，其中左侧可以包括前提集合 [math]\displaystyle{ \Gamma,\Delta }[/math] ，也可以包括单个前提 [math]\displaystyle{ \phi }[/math] ，不止一个则通过逗号隔开，右侧是单个结论 [math]\displaystyle{ \psi }[/math] 。

变形规则描述

一个变形规则总是写成形式 [math]\displaystyle{ H_1\quad\cdots\quad H_n\vdash C }[/math] 。其中左侧是前提，可以包括一个至多个公式 [math]\displaystyle{ H_1,\cdots,H_n }[/math] ，若不止一个则多个前提间需用逗号隔开，且多个前提间不要求顺序。右侧是结论，只能有一个公式 [math]\displaystyle{ C }[/math] 。

每个变形规则都有一个名称。基础规则由逻辑联结词的引入、消除规则构成，用逻辑联结词和 I （引入(introduction)）或 E （消去 elimination）命名。非基础规则也使用定理名称或缩写。但是不同材料中记号可能有区别，如 [math]\displaystyle{ \land_I }[/math] 可能被记作 [math]\displaystyle{ \land_\mathrm{I} }[/math] 、 [math]\displaystyle{ \land I }[/math] 、 [math]\displaystyle{ \land\mathrm{I} }[/math] ，其他记号也依此类推。

变形规则

Fitch 式自然演绎中有几个通用的规则：

进行一个公式假设，并开始一个子证明。最外层的前提允许有多个，内层的子证明都只能有一个假设。记为 hyp 。
重复：可以重复当前外一层证明（仅一层）中在当前子证明开始前的任意一行。记为 reit 并依赖被重复行。
应用某种规则，从当前子证明中的几个公式得到新的公式。如果需要外层的公式，需要逐层使用重复规则，如上述例子中的 3、5 行将第 1 行的假设一路复制到最内层。

命题逻辑

关于命题逻辑的 Fitch 式自然演绎系统，可能包括以下规则。其中 [math]\displaystyle{ \phi,\psi,\chi }[/math] 可以代入为任意公式。

谓词逻辑

关于谓词逻辑的则增加以下4条规则。其中除要求 [math]\displaystyle{ \phi,\psi }[/math] 可以代入为任意公式外，还要求 [math]\displaystyle{ t }[/math] 是项且对 [math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/math] 中可自由代入， [math]\displaystyle{ a }[/math] 是个体变项且[math]\displaystyle{ a }[/math] 对 [math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/math] 中可自由代入。有时也可以直接使用 [math]\displaystyle{ t=x }[/math] 或 [math]\displaystyle{ a=x }[/math] 进行个体变项代入，但是由于存在混淆，建议避免。

证明论
形式化公理系统（形式化、公理化）
形式化范式	公理系统、自然演绎系统、相继式演算
证明、演绎	证明、可证明、演绎、可演绎
命题、定理	公理、定理、元定理、变形规则
推理规则性质	保存真实性、保存重言性
公理系统性质	可靠性、完全性、一致性、独立性