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)。除最外层外，竖线的右侧总是伸出一条横线。这条横线上方仅有一行，是当前子证明的假设。极端情况下，子证明可以只有一行假设没有其他行（一般仅用于得到 [math]\displaystyle{ \phi\rightarrow\phi }[/math] ）。
  • 最外层证明若有横线，上方为整个演绎过程中的前提，可能有多行；若为无前提证明，则不需要绘制横线。
• 每行右侧有这一行使用的变形规则及其依赖行号，或仅指出这是一个假设而非变形结果。

特征

• 每行都是形式语言中的一个公式。
• 每个行或者是假设，或者依赖一个或多个其他行。
• 证明中的每行都在这一行所依赖的前提下为真。其中所依赖的前提指所依赖的行中是前提的那些，而所依赖的行指这行所在的子证明及其右侧给出的依赖行号，及其间接再依赖的行号。如上例中第 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/hypothesis 或 ass/assumption 或不写右侧。有的材料中前提的右侧可能改为写 premise 。
• 重复：可以重复当前上一层证明（仅一层）中在当前子证明开始前的任意一行。记为 r/reit/reiteration 并依赖被重复行。
• 应用某种规则，从当前子证明中的几个公式得到新的公式。如果需要外层的公式，需要逐层使用重复规则，如上述例子中的 3、5 行将第 1 行的假设一路复制到最内层。

命题逻辑

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

• 否定引入（[math]\displaystyle{ \lnot_I }[/math] 或 [math]\displaystyle{ \lnot }[/math]-int）：一个假设为 [math]\displaystyle{ \phi }[/math] 的子证明中出现了 [math]\displaystyle{ \psi }[/math] 和 [math]\displaystyle{ \lnot\psi }[/math] ，可结束子证明在上一层证明中得到 [math]\displaystyle{ \lnot\phi }[/math] 。
• 否定消去([math]\displaystyle{ \lnot_E }[/math] 或 [math]\displaystyle{ \lnot }[/math]-elim)或双重否定消去（[math]\displaystyle{ \lnot\lnot_E }[/math] 或 [math]\displaystyle{ \lnot\lnot }[/math]-elim）：从 [math]\displaystyle{ \lnot\lnot \phi }[/math] 可推出 [math]\displaystyle{ \phi }[/math] 。
• 合取引入（[math]\displaystyle{ \land_I }[/math] 或 [math]\displaystyle{ \land }[/math]-int）：从 [math]\displaystyle{ \phi }[/math] 和 [math]\displaystyle{ \psi }[/math] 可推出 [math]\displaystyle{ \phi\land\psi }[/math] 。
• 合取消去（[math]\displaystyle{ \land_E }[/math] 或 [math]\displaystyle{ \land }[/math]-elim）：从 [math]\displaystyle{ \phi\land\psi }[/math] 可推出 [math]\displaystyle{ \phi }[/math] 、从 [math]\displaystyle{ \phi\land\psi }[/math] 可推出 [math]\displaystyle{ \psi }[/math]。
• 析取引入（[math]\displaystyle{ \lor_I }[/math] 或 [math]\displaystyle{ \lor }[/math]-int）：从 [math]\displaystyle{ \phi }[/math] 可推出 [math]\displaystyle{ \phi\lor\psi }[/math] 、从 [math]\displaystyle{ \phi }[/math] 可推出 [math]\displaystyle{ \psi\lor\phi }[/math]。
• 析取消去（[math]\displaystyle{ \lor_E }[/math] 或 [math]\displaystyle{ \lor }[/math]-elim）：从 [math]\displaystyle{ \phi\lor\psi }[/math] 和两个子证明 [math]\displaystyle{ \phi }[/math] 推出 [math]\displaystyle{ \chi }[/math] 、 [math]\displaystyle{ \psi }[/math] 推出 [math]\displaystyle{ \chi }[/math] 可推出 [math]\displaystyle{ \chi }[/math] 。
• 双条件引入（[math]\displaystyle{ \leftrightarrow_I }[/math] 或 [math]\displaystyle{ \leftrightarrow }[/math]-int）：从 [math]\displaystyle{ \phi\rightarrow\psi }[/math] 和 [math]\displaystyle{ \psi\rightarrow\phi }[/math] 可推出 [math]\displaystyle{ \phi\leftrightarrow\psi }[/math] 。也指通过两个子证明从 [math]\displaystyle{ \phi }[/math] 推出 [math]\displaystyle{ \psi }[/math] 、从 [math]\displaystyle{ \psi }[/math] 推出 [math]\displaystyle{ \phi }[/math] ，则可在结束两个子证明后在其上一层证明中得到 [math]\displaystyle{ \phi\leftrightarrow\psi }[/math] 。
• 双条件消去（[math]\displaystyle{ \leftrightarrow_E }[/math] 或 [math]\displaystyle{ \leftrightarrow }[/math]-elim）：从 [math]\displaystyle{ \phi\leftrightarrow\psi }[/math] 可推出 [math]\displaystyle{ \phi\rightarrow\psi }[/math] 、 从 [math]\displaystyle{ \phi\leftrightarrow\psi }[/math] 可推出 [math]\displaystyle{ \psi\rightarrow\phi }[/math] 。也指从 [math]\displaystyle{ \phi\leftrightarrow\psi }[/math] 和 [math]\displaystyle{ \phi }[/math] 可推出 [math]\displaystyle{ \psi }[/math] ，从 [math]\displaystyle{ \phi\leftrightarrow\psi }[/math] 和 [math]\displaystyle{ \psi }[/math] 可推出 [math]\displaystyle{ \phi }[/math] 。
• 条件引入（[math]\displaystyle{ \rightarrow_E }[/math] 或 [math]\displaystyle{ \rightarrow }[/math]-int）：引入一个由假设开始的子证明，假定 [math]\displaystyle{ \phi }[/math] 为真后演绎出 [math]\displaystyle{ \psi }[/math] ，可结束子证明在上一层证明中得到 [math]\displaystyle{ \phi\rightarrow\psi }[/math] 。
• 条件消去（[math]\displaystyle{ \rightarrow_E }[/math] 或 [math]\displaystyle{ \rightarrow }[/math]-elim）：从 [math]\displaystyle{ \phi\rightarrow\psi }[/math] 和 [math]\displaystyle{ \phi }[/math] 可推出 [math]\displaystyle{ \psi }[/math]。

谓词逻辑

关于谓词逻辑的则增加以下规则。其中除要求 [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] 进行个体变项代入，但是由于存在混淆，建议避免。

• 全称量词消去（[math]\displaystyle{ \forall_E }[/math]，[math]\displaystyle{ \forall }[/math]-elim，US/UI）：从 [math]\displaystyle{ \forall x \phi }[/math] 可推出 [math]\displaystyle{ \phi[t/x] }[/math] 。
• 存在量词引入（[math]\displaystyle{ \exists_I }[/math]，[math]\displaystyle{ \exists }[/math]-int，EG）：从 [math]\displaystyle{ \phi[t/x] }[/math] 可推出 [math]\displaystyle{ \exists x \phi }[/math] 。
• 等词引入（[math]\displaystyle{ =_I }[/math]，[math]\displaystyle{ = }[/math]-int）：在任意地方，可以对任意项 [math]\displaystyle{ t }[/math] 得到 [math]\displaystyle{ t=t }[/math] 。
• 等词消去（[math]\displaystyle{ =_E }[/math]，[math]\displaystyle{ = }[/math]-elim）：从 [math]\displaystyle{ s=t }[/math] 或 [math]\displaystyle{ t=s }[/math]，以及 [math]\displaystyle{ \phi[s/x] }[/math] 可以得到 [math]\displaystyle{ \phi[t/x] }[/math] 。

然后还有两条规则，涉及一个自由变项。这意味着引入一个个体变项，且对这个引入项进行使用范围上的限制。 除标记规则外，还需要进行“标示”。标示记为 flag ，引入某个中间个体变项，由于这个个体变项会使几个公式不再是闭式，需要在完成当前子证明前从公式中消除掉。

• 存在量词消去（[math]\displaystyle{ \exists_E }[/math]，[math]\displaystyle{ \exists }[/math]-elim，ES/EI）：从 [math]\displaystyle{ \exists x \phi }[/math] 可推出 [math]\displaystyle{ \phi[a/x] }[/math] 且此步骤将 [math]\displaystyle{ a }[/math] 标示。
• 全称量词引入（[math]\displaystyle{ \forall_I }[/math]，[math]\displaystyle{ \forall }[/math]-int，UG）：对被标示为任意的 [math]\displaystyle{ a }[/math] 演绎出 [math]\displaystyle{ \phi[a/x] }[/math] 可推出 [math]\displaystyle{ \forall x \phi }[/math] 。

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