证明：修订间差异

2026年1月22日 (四) 04:23的最新版本

证明
术语名称	证明
英语名称	proof

可证明的
术语名称	可证明的
英语名称	provable

定理
术语名称	定理
英语名称	theorem
别名	thesis

证明(proof)指某个推理系统的变形规则下，从空前提到某一结论的步骤。对应地，这个步骤的存在性被称为可证明(provable)。定理(theorem)即该系统中任一可证明的公式。

在证明论以外的语境下，无论有无前提均称为证明。但是在证明论中，与其范围一致的概念是演绎，只有其中无前提的部分才叫做证明。

定义

在指定形式化公理系统 [math]\displaystyle{ \mathbf{H} }[/math] 中，从空集 [math]\displaystyle{ \varnothing }[/math] 到公式 [math]\displaystyle{ \phi }[/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{ \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{ \phi }[/math] 的一个证明(proof)。

对任意公式 [math]\displaystyle{ \phi }[/math] ，以下条件等价：

公式 [math]\displaystyle{ \phi }[/math] 可从空集演绎（[math]\displaystyle{ \varnothing \vdash \phi }[/math]）；
存在从空集到 [math]\displaystyle{ \phi }[/math]的演绎；
存在 [math]\displaystyle{ \mathbf{H} }[/math] 中 [math]\displaystyle{ \phi }[/math] 的证明。

此时称 [math]\displaystyle{ \phi }[/math] 是 [math]\displaystyle{ \mathbf{H} }[/math] 中 可证明的(provable)，记作 [math]\displaystyle{ \vdash \phi }[/math] ，并称 [math]\displaystyle{ \phi }[/math] 为 [math]\displaystyle{ \mathbf{H} }[/math] 中的定理(theorem, thesis)。

性质

演绎定理的特例： [math]\displaystyle{ A\vdash B }[/math] 当且仅当 [math]\displaystyle{ \vdash A\rightarrow B }[/math] 。
作为特殊的演绎，在各推理系统中公式序列的表现：
- Hilbert 表示：在演绎过程中仅会出现公理及其直接变形，不存在提及假设的步骤。
- Gentzen 式自然演绎：证明树中所有叶结点都是公理或被解除的假设。
- Fitch 式自然演绎：根证明中不存在前提，子证明中的假设都随着子证明结束而解除。
- Suppes–Lemmon 式自然演绎：结论依赖的行都是公理。
- Gentzen 式相继式演算：证明数中所有叶结点都是公理，通常是 [math]\displaystyle{ A\vdash A }[/math] 的形式。

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

@@ 第1行： / 第1行： @@
-[[分类:证明论]]
+[[分类:证明论]]{{DEFAULTSORT:zheng4ming2}}
+{{#seo:
+|keywords=证明论, 证明, 可证明, 定理
+|description=证明论中，证明指不给定前提，仅从公理和推导规则推导出结论的推理结构，其结论称为定理。本文介绍了证明的定义、性质及其与演绎的关系。
+|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
+|published_time=2023-07-01
+}}
 {{InfoBox
 |name=证明
@@ 第16行： / 第22行： @@
 对应地，这个步骤的存在性被称为'''可证明'''('''provable''')。
 '''定理'''('''theorem''')即该系统中任一可证明的公式。
+<blockquote>
+在证明论以外的语境下，无论有无前提均称为证明。但是在证明论中，与其范围一致的概念是[[演绎]]，只有其中无前提的部分才叫做证明。
+</blockquote>
 == 定义 ==
@@ 第27行： / 第37行： @@
 对任意公式 <math>\phi</math> ，以下条件等价：
-* 公式 <math>\phi</math> 可从空集演绎（<math>\varnothing \vdash \phi</math>），
+* 公式 <math>\phi</math> 可从空集演绎（<math>\varnothing \vdash \phi</math>）；
-* 存在从空集到 <math>\phi</math>的演绎，
+* 存在从空集到 <math>\phi</math>的演绎；
-* 存在 <math>\mathbf{H}</math> 中 <math>\phi</math> 的证明，
+* 存在 <math>\mathbf{H}</math> 中 <math>\phi</math> 的证明。
-此时称 <math>\phi</math> 是 <math>\mathbf{H}</math> 中 '''可证明的'''('''provable''')，记作 <math>\vdash \phi</math>。
+此时称 <math>\phi</math> 是 <math>\mathbf{H}</math> 中 '''可证明的'''('''provable''')，记作 <math>\vdash \phi</math> ，并称 <math>\phi</math> 为 <math>\mathbf{H}</math> 中的'''定理'''('''theorem''', thesis)。
-此时 <math>\phi</math> 称为 <math>\mathbf{H}</math> 中的'''定理'''('''theorem''', thesis)。
+== 性质 ==
+* [[演绎定理]]的特例： <math>A\vdash B</math> 当且仅当 <math>\vdash A\rightarrow B</math> 。
+* 作为特殊的演绎，在各推理系统中公式序列的表现：
+** [[Hilbert 表示]]：在演绎过程中仅会出现公理及其直接变形，不存在提及假设的步骤。
+** [[Gentzen 式自然演绎]]：证明树中所有叶结点都是公理或被解除的假设。
+** [[Fitch 式自然演绎]]：根证明中不存在前提，子证明中的假设都随着子证明结束而解除。
+** [[Suppes–Lemmon 式自然演绎]]：结论依赖的行都是公理。
+** [[Gentzen 式相继式演算]]：证明数中所有叶结点都是公理，通常是 <math>A\vdash A</math> 的形式。
 {{证明论}}