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

[[分类:证明论]]{{DEFAULTSORT:gentzen shi4zi4ran2yan3yi4}}
{{#seo:
|keywords=根岑式自然演绎
|description=根岑式自然演绎是自然演绎系统的一种记号，本文介绍了这种记号的写法，以及用于命题逻辑、谓词逻辑时的推理规则。
|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
|published_time=2026-01-16
}}
{{InfoBox
|name=根岑式自然演绎
|eng_name=Gentzen's natural deduction
|aliases=Gentzen's tree notation,Gentzen's system NK
}}
'''Gentzen 式自然演绎'''('''Gentzen's natural deduction''')是逻辑领域[[形式化公理系统（逻辑）|形式化公理系统]]中 Gentzen 式系统中[[自然演绎系统]]的一种。其中每行都是一个公式，这些公式通过树状的记号组织，以反映公式间的变形关系。

说明： Gentzen 最初使用的表示[[逻辑联结词]]（包括零元的[[假]]）的记号与现今标准记号有差异，以下均按照现代记号表示。<ref>原始记号见 https://hsm.stackexchange.com/a/17970 。</ref>

== 描述 ==

以下是无前提的 <math>(p\rightarrow q)\land(\lnot r\rightarrow \lnot q)\rightarrow (p\rightarrow r)</math> 的一个证明。<ref>摘抄自 https://plato.stanford.edu/entries/natural-deduction/ ，格式有改动。</ref>

<math>
\dfrac{
\dfrac{[\lnot r]^3 \qquad \dfrac{[(p\rightarrow q)\land(\lnot r\rightarrow \lnot q)]^1}{\lnot r\rightarrow \lnot q}\land_{E_2}}{\lnot q}\rightarrow_E \qquad
\dfrac{\dfrac{[(p\rightarrow q)\land(\lnot r\rightarrow \lnot q)]^1}{p\rightarrow q}\land_{E_1} \qquad [p]^2}{q}\rightarrow_E
}
{\dfrac{\dfrac{\dfrac{\dfrac{\bot}{\lnot\lnot r}\lnot_{I^3}}{r}\lnot\lnot_E}{p\rightarrow r}\rightarrow _{I^2}}{\blacksquare\quad (p\rightarrow q) \land (\lnot r\rightarrow \lnot q)\rightarrow (p\rightarrow r)}\rightarrow_{I^1}} \rightarrow_E
</math>

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

* 部分材料中，记号可能有微小差异，请以具体记号为准。
* 证明中的每一个公式称为一'''行'''('''line''')。
* 每条横线代表一个变形。横线右侧是使用的变形规则名称；上方有一个或多个公式，公式（及其证明）间用空白隔开；下方必须有且仅有一个公式。
* 每行根据是否有头顶横线及横线上其他公式、是否有方括号分为三种：
** 无头顶横线、无括号：这一行是证明中的一个'''前提'''('''premise''')。如给定甲、乙、丙求证丁中，丙是一个前提。
** 有括号：这是一个'''假设'''('''assumption''')_。假设是证明中途根据需要任意进行的，相当于一般证明中的“若……”“设……”。如上例中的 <math>[p]</math> 代表假设 <math>p</math> 为真。正常情况下，由证明者提出的假设需要在得出结论前消去，以完成证明。
** 有头顶横线：这一行在证明中由横线上的一个或多个公式变形得出。如上例中的 <math>\lnot q</math> 头上有一横线，这条横线上有两个公式 <math>\lnot r, \lnot r\rightarrow \lnot q</math> 、右侧有名称 <math>\rightarrow_E</math> ，代表从 <math>\lnot r</math> 和 <math>\lnot r\rightarrow \lnot q</math> 根据规则蕴涵消去推出了<math>\lnot q</math> 。
* 最后一行有 <math>\blacksquare</math> （Q.E.D.）符号，代表证明结束，这一行是'''结论'''('''conclusion''')。也有的材料中不写这一符号。
* 方括号的上标数字与规则的上标数字代表假设及其失效位置的对应关系，如上例中 <math>[\lnot r]^3</math> 对应 <math>\frac{\bot}{\lnot\lnot r}\lnot_{I^3}</math> ，代表我们在假设 <math>\lnot r</math> 为真时推出了矛盾，符合否定引入规则的形式，因此可以使用这一规则推出 <math>\lnot\lnot r</math> 这一行，然后这一规则要求使对应假设失效，因此从 <math>\lnot\lnot r</math> 这一行开始， <math>\lnot r</math> 为真的假设已经失效。

=== 特征 ===

* 每行都是形式语言中的一个公式。
* 每个变形上方可以有一个或多个公式，但下方必须有且仅有一个公式。换句话说，变形规则的结论必须是一个公式。
* 证明中的每行都在前提和当前有效假设下为真，其中当前有效假设指在这行以上的证明中进行过且尚未失效的假设。如上例中 <math>\lnot\lnot r</math> 一行的证明中有 1,2,3 三个假设，而其中假设 3 <math>\lnot r</math> 已经失效，因此 <math>\lnot\lnot r</math> 在条件 <math>(p\rightarrow q)\land(\lnot r\rightarrow \lnot q), p</math> 下成立。

== 记号约定 ==

=== 公式描述 ===

Gentzen 式自然演绎中使用的形式语言和[[命题语言]]、[[谓词语言]]的普遍定义稍有区别。这种形式语言中的公式包含：
* [[原子命题]]（命题逻辑为命题变元，谓词逻辑为谓词和项构成的原子命题，其中谓词和项与一般定义一致）是公式。
* 假 <math>\bot</math> 是公式。
* 若 <math>\phi,\psi</math> 是公式，则 <math>(\phi\land\psi)</math> 、 <math>(\phi\lor\psi)</math> 、 <math>(\phi\rightarrow\psi)</math> 是公式（含逻辑联结词的公式）。
* （谓词逻辑）若 <math>x</math> 是个体变项， <math>\phi</math> 是公式，则 <math>\forall x \phi</math> 、 <math>\exists x \phi</math> 是公式（量化公式）。
* 其他形式不是公式。

并记缩写符号：
* <math>\lnot p := p\rightarrow \bot</math> 。
* <math>\top := \bot\rightarrow\bot</math> 。
* <math>\phi\leftrightarrow\psi := (\phi\rightarrow\psi)\land(\psi\rightarrow\phi)</math> 。

谓词逻辑中，有部分材料中需要通过 <math>t: \mathcal{T}</math> '''标示'''('''flag''') <math>t</math> 是一个项。

=== 命题描述 ===

一个证明或一个需证明命题通常被写成 <math>\dfrac{\Gamma, \Delta, \phi}{\psi}</math> 的形式，其中横线上方可以包括前提集合 <math>\Gamma,\Delta</math> ，也可以包括单个前提 <math>\phi</math> ，不止一个则通过'''逗号'''隔开，横线下方是单个结论 <math>\psi</math> 。

也可以写成'''后继式''' <math>\Gamma, \Delta, \phi \vdash \psi</math> 。

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

一个变形规则总是写成形式 <math>\dfrac{H_1\quad\cdots\quad H_n}{C}R</math> 。其中横线上方是'''前提'''，可以包括一个至多个公式 <math>H_1,\cdots,H_n</math> ，若不止一个则多个前提间需用'''空白'''隔开，且多个前提间'''不要求顺序'''。横线下方是'''结论'''，只能有一个公式 <math>C</math> 。横线右侧是变形规则的'''名称''' <math>R</math> 。

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

变形规则的内容也写成横线上下的形式，如 <math>\dfrac{\phi\quad\psi}{\phi\land\psi}\land_I</math> 代表可以通过最后一行为 <math>\phi</math> 和 <math>\psi</math> 的两个证明得到 <math>\phi\land\psi</math> ，规则名称为 <math>\land_I</math> 。

若两个公式只有简写是否展开的差异，视为同一公式。对应地涉及公式对应相同的规则也是同一规则，其中前提不要求顺序。也就是认为 <math>\dfrac{\phi\quad\psi}{\phi\land\psi}\land_I</math> 和 <math>\dfrac{\psi\quad\phi}{\phi\land\psi}\land_I</math> 是同一条规则，但是注意 <math>\dfrac{\phi\land\psi}{\phi}\land_{E_1}</math> 、 <math>\dfrac{\phi\land\psi}{\psi}\land_{E_2}</math> 这样不是多个前提交换顺序，而是改变了公式本身的，就不再是同一条规则。

== 变形规则 ==

=== 命题逻辑 ===

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

* 合取引入： <math>\dfrac{\phi\quad\psi}{\phi\land\psi}\land_I</math> 。
* 合取消去： <math>\dfrac{\phi\land\psi}{\phi}\land_{E_1}</math> 、 <math>\dfrac{\phi\land\psi}{\psi}\land_{E_2}</math> 。
* 析取引入： <math>\dfrac{\phi}{\phi\lor\psi}\lor_{I_1}</math> 、 <math>\dfrac{\phi}{\psi\lor\phi}\lor_{I_2}</math> 。
* 析取消去： <math>\dfrac{\phi\lor\psi \quad \begin{matrix}[\phi]^u\\\vdots\\\chi\end{matrix} \quad \begin{matrix}[\psi]^v\\\vdots\\\chi\end{matrix}}{\chi}\lor_{E^{u,v}}</math> 。横线上方右侧的记号表示这里需要两个带有新假设的子证明，分别从 <math>\phi</math> 和 <math>\psi</math> 结合其他条件证明出 <math>\chi</math> ，并且这两个假设都会在执行这一步操作后失效。
* 条件引入： <math>\dfrac{\begin{matrix}[\phi]^u\\\vdots\\\psi\end{matrix}}{\phi\rightarrow\psi} \rightarrow_{I^u}</math> 。横线上方也是一个从假设开始的子证明。
* 条件消去： <math>\dfrac{\phi\quad\phi\rightarrow\psi}{\psi} \rightarrow_E</math> 。
* 矛盾消去，或爆炸律（EFQ）： <math>\dfrac{\bot}{\phi}\bot_E</math> 。名称也有资料写成 <math>\mathrm{EFQ}</math> <ref>https://home.mis.u-picardie.fr/~devismes/WWW/presentation/talk_Lleida.pdf</ref> 。
* 双重否定消去： <math>\dfrac{\lnot\lnot\phi}{\phi}</math> 或写成 <math>\dfrac{(\phi\rightarrow\bot)\rightarrow\bot}{\phi}\lnot\lnot_E</math> 。

对于经典逻辑，这一系统称为 NK （'''Gentzen's system NK'''）。
对于非经典逻辑，可以进行一些调整。在直觉主义逻辑中，去除双重否定消去规则，称为 NJ （'''Gentzen's system NJ'''）。

另外也有一些变体规则：
* 双重否定消去可能被替换为反证法 <math>\dfrac{\begin{matrix}[\phi\rightarrow\bot]^u\\\vdots\\\bot\end{matrix}}{\phi} \mathrm{RAA}^u</math> 。
* 后件 <math>\psi</math> 取 <math>\bot</math> 的条件引入也被称为否定引入 <math>\dfrac{\begin{matrix}[\phi]^u\\\vdots\\\bot\end{matrix}}{\lnot\phi} \lnot_{I^u}</math> 。
* 后件 <math>\psi</math> 取 <math>\bot</math> 的条件消去也被称为否定消去 <math>\dfrac{\phi\quad\lnot\phi}{\bot}\lnot_E</math> 。有时也称为矛盾引入，但因为一般情况下 <math>\bot</math> 除了否定引入外，几乎不会作为独立的公式出现，较少使用。
* 对于 <math>\leftrightarrow</math> ，看作简写并遵守 <math>\land</math> 的规则。
* 对于 <math>\top</math> ，看作简写并遵守 <math>\rightarrow</math> 的规则。常用规则中只有矛盾消去而没有矛盾引入，代表“假推出任意”，理论上对应地只存在一个重言引入而没有重言消去，代表“任意推出真” <math>\dfrac{}{\top}\top_I</math> 。但是因为没有实用价值，一般不列出<ref>https://math.stackexchange.com/a/3286149</ref>。

=== 谓词逻辑 ===

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

* 全称量词消去： <math>\dfrac{\forall x \phi}{\phi[t/x]}\forall_{E^t}</math> 。
* 存在量词引入： <math>\dfrac{\phi[t/x]}{\exists x \phi}\exists_{I^t}</math> 。
* 全称量词引入： <math>\dfrac{\phi[a/x]}{\forall x \phi}\forall_{I^a}</math> 。
* 存在量词消去： <math>\dfrac{\exists x \phi \quad \begin{matrix}[\phi[a/x]]^u\\\vdots\\\psi\end{matrix}}{\psi}\exists_{E^{a,u}}</math> 。 


{{证明论}}