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

[[分类:证明论]]{{DEFAULTSORT:fitch shi4zi4ran2yan3yi4}}
{{#seo:
|keywords=费奇式自然演绎
|description=费奇式自然演绎是自然演绎系统的一种记号，本文介绍了这种记号的写法，以及用于命题逻辑、谓词逻辑时的推理规则。
|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
|published_time=2026-01-16
}}
{{InfoBox
|name=费奇式自然演绎
|eng_name=Fitch's natural deduction
|aliases=Fitch's notation
}}
'''Fitch 式自然演绎'''('''Fitch's natural deduction''')是逻辑领域[[形式化公理系统（逻辑）|形式化公理系统]]中 Gentzen 式系统中[[自然演绎系统]]的一种。其中每行都是一个公式，这些公式会标注出其使用的规则以及依赖的公式，以反映公式间的变形关系。 Fitch 式自然演绎的特征是各行之间书写成一个并列、有行号的列表，各行之间的依赖关系通过注明依赖行号表达； Fitch 式自然演绎通过子证明表达假言推理，并且子证明构成层级关系。

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

== 描述 ==

以下是 <math>p\rightarrow q\rightarrow p</math> 的一个证明。

<pre>
  |---------
1 | | p     hyp
  | |-------
2 | | | q   hyp
  | | |-----
3 | | | p   reit,1
  | |
4 | | q→p  →I,2,3
  |
5 | p→q→p →I,1,4
</pre>

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

<pre>
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>q</math> 的依赖为 4,5 而 4 是一个 hyp ， 5 依赖 3 、 3 依赖 1 、 1 是一个 hyp ，因此所依赖的前提是第 1 行和第 4 行，即 <math>q</math> 在条件 <math>p\rightarrow q, p</math> 下成立。

== 记号约定 ==

=== 公式描述 ===

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

=== 命题描述 ===

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

=== 变形规则描述 ===

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

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

== 变形规则 ==

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

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

=== 命题逻辑 ===

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

=== 谓词逻辑 ===

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


{{证明论}}