演绎：修订间差异

2026年1月22日 (四) 05:03的最新版本

演绎
术语名称	演绎
英语名称	deduction

可演绎的
术语名称	可演绎的
英语名称	deducible

演绎(deduction)指某个推理系统的变形规则下，从一些前提到某一结论的推理步骤。对应地，这个步骤的存在性被称为可演绎(deducible)。

定义

在指定形式化公理系统 [math]\displaystyle{ \mathbf{H} }[/math] 中，对指定公式集 [math]\displaystyle{ \Gamma }[/math] 和公式 [math]\displaystyle{ \phi }[/math] ，满足下列条件的公式序列 [math]\displaystyle{ \phi_0, \phi_1, \dots, \phi_n }[/math] ：

[math]\displaystyle{ \phi_n = \phi }[/math]；
对任意 [math]\displaystyle{ k \lt n }[/math]， [math]\displaystyle{ \phi_k }[/math] 符合以下任一条件：
- 是 [math]\displaystyle{ \mathbf{H} }[/math] 中的公理；
- 是 [math]\displaystyle{ \Gamma }[/math] 中的元素；
- 能运用 [math]\displaystyle{ \mathbf{H} }[/math] 中的推理规则从 [math]\displaystyle{ \phi_0, \dots, \phi_{k-1} }[/math] 得到。

则称公式序列 [math]\displaystyle{ \phi_0, \phi_1, \dots, \phi_n }[/math] 是 [math]\displaystyle{ \mathbf{H} }[/math] 中从公式集 [math]\displaystyle{ \Gamma }[/math] 到公式 [math]\displaystyle{ \phi }[/math] 的一个演绎(deduction)。

对任意公式集 [math]\displaystyle{ \Gamma }[/math] 和公式 [math]\displaystyle{ \phi }[/math] ，若存在 [math]\displaystyle{ \mathbf{H} }[/math] 中从 [math]\displaystyle{ \Gamma }[/math] 到 [math]\displaystyle{ \phi }[/math] 的演绎，则称 [math]\displaystyle{ \phi }[/math] 是 [math]\displaystyle{ \mathbf{H} }[/math] 中从 [math]\displaystyle{ \Gamma }[/math] 可演绎的(deducible)，记作 [math]\displaystyle{ \Gamma \vdash \phi }[/math]。对 [math]\displaystyle{ \Gamma=\{\psi_1,\psi_2,\dots,\psi_m\} }[/math] 时也记作 [math]\displaystyle{ \psi_1,\psi_2,\dots,\psi_m \vdash \phi }[/math]。此时，[math]\displaystyle{ \Gamma }[/math] 的元素称为假设(hypothesis)或前提(premise)， [math]\displaystyle{ \phi }[/math] 称为[math]\displaystyle{ \mathbf{H} }[/math] 中 [math]\displaystyle{ \Gamma }[/math] 的演绎结论或演绎后承(deductive consequence)，即逻辑蕴涵关系。

性质

[math]\displaystyle{ \Gamma\vdash B }[/math] 且 [math]\displaystyle{ \Gamma\subseteq\Delta }[/math] 则 [math]\displaystyle{ \Delta\vdash B }[/math] 。
演绎定理： [math]\displaystyle{ \Gamma,A\vdash B }[/math] 当且仅当 [math]\displaystyle{ \Gamma\vdash A\rightarrow B }[/math] 。
切消定理： [math]\displaystyle{ \Gamma \vdash A }[/math] 且 [math]\displaystyle{ \Gamma,A\vdash B }[/math] 则有 [math]\displaystyle{ \Gamma\vdash B }[/math] 。
前提为空，即 [math]\displaystyle{ \Gamma=\varnothing }[/math] 时，演绎被称为证明。

证明论
形式化公理系统（形式化、公理化）
推理系统	Hilbert 风格/公理系统：Hilbert 表示
	Gentzen 风格-自然演绎系统： Gentzen 式自然演绎、 Fitch 式自然演绎、 Suppes–Lemmon 式自然演绎
	Gentzen 风格-相继式演算： Gentzen 式相继式演算
证明、演绎	演绎、可演绎、证明、可证明
命题、定理	公理/公理模式、定理、元定理、变形规则
推理规则性质	保存真实性、保存重言性
公理系统性质	可靠性、完备性/完全性、一致性、独立性

@@ 第1行： / 第1行： @@
+[[分类:证明论]]{{DEFAULTSORT:yan3yi4}}
+{{#seo:
+|keywords=证明论, 演绎, 可演绎
+|description=证明论中，演绎指从公理、前提和推导规则推导出结论的推理结构，即前提和结论间的推理关系。本文介绍了演绎的定义与常见性质。
+|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
+|published_time=2023-07-01
+}}
 {{InfoBox
 |name=演绎
@@ 第7行： / 第14行： @@
 |eng_name=deducible
 }}
-'''演绎'''('''deduction''')指某个推理系统的变形规则下，从一些前提到某一结论的一系列步骤。
+'''演绎'''('''deduction''')指某个推理系统的变形规则下，从一些前提到某一结论的推理步骤。
 对应地，这个步骤的存在性被称为'''可演绎'''('''deducible''')。
@@ 第22行： / 第29行： @@
 对任意公式集 <math>\Gamma</math> 和公式 <math>\phi</math> ，若存在 <math>\mathbf{H}</math> 中从 <math>\Gamma</math> 到 <math>\phi</math> 的演绎，则称 <math>\phi</math> 是 <math>\mathbf{H}</math> 中从 <math>\Gamma</math> '''可演绎的'''('''deducible''')，记作 <math>\Gamma \vdash \phi</math>。
 对 <math>\Gamma=\{\psi_1,\psi_2,\dots,\psi_m\}</math> 时也记作 <math>\psi_1,\psi_2,\dots,\psi_m \vdash \phi</math>。
-此时，<math>\Gamma</math> 的元素称为'''假设'''('''hypothesis''')或'''前提'''('''premise''')， <math>\phi</math> 称为<math>\mathbf{H}</math> 中 <math>\Gamma</math> 的'''演绎结论'''或'''演绎后承'''('''deductive consequence''')。
+此时，<math>\Gamma</math> 的元素称为'''假设'''('''hypothesis''')或'''前提'''('''premise''')， <math>\phi</math> 称为<math>\mathbf{H}</math> 中 <math>\Gamma</math> 的'''演绎结论'''或'''演绎后承'''('''deductive consequence''')，即[[逻辑蕴涵]]关系。
+== 性质 ==
+* <math>\Gamma\vdash B</math> 且 <math>\Gamma\subseteq\Delta</math> 则 <math>\Delta\vdash B</math> 。
+* [[演绎定理]]： <math>\Gamma,A\vdash B</math> 当且仅当 <math>\Gamma\vdash A\rightarrow B</math> 。
+* [[切消定理]]： <math>\Gamma \vdash A</math> 且 <math>\Gamma,A\vdash B</math> 则有 <math>\Gamma\vdash B</math> 。
+* 前提为空，即 <math>\Gamma=\varnothing</math> 时，演绎被称为[[证明]]。
-{{逻辑演算}}
+{{证明论}}