查看“︁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> 的一个证明。<ref>此处右侧注解的假设、重复记号使用徐明《符号逻辑讲义》的版本且进行了简化，部分材料使用的不同。</ref>

<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
</pre>

=== 符号及术语说明 ===

* 部分材料中，记号可能有微小差异，请以具体记号为准。
* 演绎过程中的每一个公式称为一'''行'''('''line''')，且左侧有行号。
* 每条竖线代表一个'''子证明'''('''subordinate proof''')。除最外层外，竖线的右侧总是伸出一条横线。这条横线上方仅有一行，是当前子证明的假设。极端情况下，子证明可以只有一行假设没有其他行（一般仅用于得到 <math>\phi\rightarrow\phi</math> ）。
** 最外层证明若有横线，上方为整个演绎过程中的前提，可能有多行；若为无前提证明，则不需要绘制横线。
* 每行右侧有这一行使用的变形规则及其依赖行号，或仅指出这是一个假设而非变形结果。

=== 特征 ===

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

=== 命题逻辑 ===

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

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

=== 谓词逻辑 ===

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

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

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

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


{{证明论}}