跳转到内容

Advertising:

Gentzen 式自然演绎

来自GSXAB的知识库
Gsxab​（留言 | 贡献）2026年1月16日 (五) 14:08的版本 （→描述）
根岑式自然演绎
术语名称 根岑式自然演绎
英语名称 Gentzen's natural deduction
别名 Gentzen's tree notation, Gentzen's system NK

Gentzen 式自然演绎(Gentzen's natural deduction)是逻辑领域形式化公理系统中 Gentzen 式系统中自然演绎系统的一种。其中每行都是一个公式，这些公式通过树状的记号组织，以反映公式间的变形关系。

说明： Gentzen 最初使用的表示逻辑联结词（包括零元的假）的记号与现今标准记号有差异，以下均按照现代记号表示。[1]

描述

以下是 [math]\displaystyle{ (p\rightarrow q)\land(\lnot r\rightarrow \lnot q)\rightarrow (p\rightarrow r) }[/math] 的一个证明。[2]

[math]\displaystyle{ \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]

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

[math]\displaystyle{ \dfrac{\dfrac{\dfrac{[\lnot q]^1 \quad \dfrac{[p]^2 \quad p\rightarrow q}{q}\rightarrow_E}{\bot}\rightarrow_E}{\lnot p}\rightarrow_{I^2}}{\lnot q\rightarrow \lnot p}\rightarrow_{I^1} }[/math]

符号及术语说明

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

特征

  • 每行都是形式语言中的一个公式。
  • 每个变形上方可以有一个或多个公式，但下方必须有且仅有一个公式。换句话说，变形规则的结论必须是一个公式。
    • 这使得证明可以被看成一棵树，每个行是一个结点，其根结点为证明的结论，每个结点的父节点为前提中含有这一行的变形规则的结论，子结点为变形得到这一行所使用的前提。
  • 证明中的每行都在前提和当前有效假设下为真，其中当前有效假设指在这行所依赖的证明过程中进行过且尚未解除的假设。如上例中 [math]\displaystyle{ \lnot\lnot r }[/math] 一行依赖的证明中有 1,2,3 三个假设，而其中假设 3 [math]\displaystyle{ \lnot r }[/math] 已经解除，因此 [math]\displaystyle{ \lnot\lnot r }[/math] 在条件 [math]\displaystyle{ (p\rightarrow q)\land(\lnot r\rightarrow \lnot q), p }[/math] 下成立。如上例中 [math]\displaystyle{ q }[/math] 一行依赖的证明中有 2 一个假设（注意 1 没有被其依赖），因此 [math]\displaystyle{ p }[/math] 在前提 [math]\displaystyle{ p\rightarrow q }[/math] 和条件 [math]\displaystyle{ p }[/math] 下成立。

记号约定

公式描述

Gentzen 式自然演绎中使用的形式语言和命题语言、谓词语言的普遍定义稍有区别。这种形式语言中的公式包含：

  • 原子命题（命题逻辑为命题变元，谓词逻辑为谓词和项构成的原子命题，其中谓词和项与一般定义一致）是公式。
  • 假 [math]\displaystyle{ \bot }[/math] 是公式。
  • 若 [math]\displaystyle{ \phi,\psi }[/math] 是公式，则 [math]\displaystyle{ (\phi\land\psi) }[/math] 、 [math]\displaystyle{ (\phi\lor\psi) }[/math] 、 [math]\displaystyle{ (\phi\rightarrow\psi) }[/math] 是公式（含逻辑联结词的公式）。
  • （谓词逻辑）若 [math]\displaystyle{ x }[/math] 是个体变项， [math]\displaystyle{ \phi }[/math] 是公式，则 [math]\displaystyle{ \forall x \phi }[/math] 、 [math]\displaystyle{ \exists x \phi }[/math] 是公式（量化公式）。
  • 其他形式不是公式。

并记缩写符号：

  • [math]\displaystyle{ \lnot p := p\rightarrow \bot }[/math] 。
  • [math]\displaystyle{ \top := \bot\rightarrow\bot }[/math] 。
  • [math]\displaystyle{ \phi\leftrightarrow\psi := (\phi\rightarrow\psi)\land(\psi\rightarrow\phi) }[/math] 。

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

命题描述

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

也可以写成后继式 [math]\displaystyle{ \Gamma, \Delta, \phi \vdash \psi }[/math] 。

变形规则描述

一个变形规则总是写成形式 [math]\displaystyle{ \dfrac{H_1\quad\cdots\quad H_n}{C}R }[/math] 。其中横线上方是前提，可以包括一个至多个公式 [math]\displaystyle{ H_1,\cdots,H_n }[/math] ，若不止一个则多个前提间需用空白隔开，且多个前提间不要求顺序。横线下方是结论，只能有一个公式 [math]\displaystyle{ C }[/math] 。横线右侧是变形规则的名称 [math]\displaystyle{ R }[/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] ，其他记号也依此类推。

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

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

变形规则

命题逻辑

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

  • 合取引入： [math]\displaystyle{ \dfrac{\phi\quad\psi}{\phi\land\psi}\land_I }[/math] 。
  • 合取消去： [math]\displaystyle{ \dfrac{\phi\land\psi}{\phi}\land_{E_1} }[/math] 、 [math]\displaystyle{ \dfrac{\phi\land\psi}{\psi}\land_{E_2} }[/math] 。
  • 析取引入： [math]\displaystyle{ \dfrac{\phi}{\phi\lor\psi}\lor_{I_1} }[/math] 、 [math]\displaystyle{ \dfrac{\phi}{\psi\lor\phi}\lor_{I_2} }[/math] 。
  • 析取消去： [math]\displaystyle{ \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]\displaystyle{ \phi }[/math] 和 [math]\displaystyle{ \psi }[/math] 结合其他条件证明出 [math]\displaystyle{ \chi }[/math] ，并且这两个假设都会在执行这一步操作后解除。
  • 条件引入： [math]\displaystyle{ \dfrac{\begin{matrix}[\phi]^u\\\vdots\\\psi\end{matrix}}{\phi\rightarrow\psi} \rightarrow_{I^u} }[/math] 。横线上方也是一个从假设开始的子证明，并且解除一个假设。
  • 条件消去： [math]\displaystyle{ \dfrac{\phi\quad\phi\rightarrow\psi}{\psi} \rightarrow_E }[/math] 。
  • 矛盾消去，或爆炸律（EFQ）： [math]\displaystyle{ \dfrac{\bot}{\phi}\bot_E }[/math] 。名称也有资料写成 [math]\displaystyle{ \mathrm{EFQ} }[/math] [3] 。
  • 双重否定消去： [math]\displaystyle{ \dfrac{\lnot\lnot\phi}{\phi} }[/math] 或写成 [math]\displaystyle{ \dfrac{(\phi\rightarrow\bot)\rightarrow\bot}{\phi}\lnot\lnot_E }[/math] 。

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

另外也有一些变体规则：

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

谓词逻辑

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

  • 全称量词消去： [math]\displaystyle{ \dfrac{\forall x \phi}{\phi[t/x]}\forall_{E^t} }[/math] 。
  • 存在量词引入： [math]\displaystyle{ \dfrac{\phi[t/x]}{\exists x \phi}\exists_{I^t} }[/math] 。
  • 全称量词引入： [math]\displaystyle{ \dfrac{\phi[a/x]}{\forall x \phi}\forall_{I^a} }[/math] 。
  • 存在量词消去： [math]\displaystyle{ \dfrac{\exists x \phi \quad \begin{matrix}[\phi[a/x]]^u\\\vdots\\\psi\end{matrix}}{\psi}\exists_{E^{a,u}} }[/math] 。这里需要假设一个个体变项 [math]\displaystyle{ a }[/math] 使得 [math]\displaystyle{ \phi[a/x] }[/math] 为真，并推理出一个不含 [math]\displaystyle{ a }[/math] 的公式 [math]\displaystyle{ \psi }[/math] ，然后解除这一假设。


证明论
形式化公理系统（形式化、公理化）
形式化范式 公理系统、自然演绎系统、相继式演算
证明、演绎 证明、可证明、演绎、可演绎
命题、定理 公理、定理、元定理、变形规则
推理规则性质 保存真实性、保存重言性
公理系统性质 可靠性、完全性、一致性、独立性
  1. ↑ 原始记号见 https://hsm.stackexchange.com/a/17970 。
  2. ↑ 摘抄自 https://plato.stanford.edu/entries/natural-deduction/ ，格式有改动。
  3. ↑ https://home.mis.u-picardie.fr/~devismes/WWW/presentation/talk_Lleida.pdf
  4. ↑ https://math.stackexchange.com/a/3286149
检索自“https://knowledge.gsxab.top/index.php?title=Gentzen_式自然演绎&oldid=6526”

Advertising: