查看“︁证明”︁的源代码

[[分类:证明论]]{{DEFAULTSORT:zheng4ming2}}
{{#seo:
|keywords=证明论, 证明, 可证明, 定理
|description=证明论中，证明指不给定前提，仅从公理和推导规则推导出结论的推理结构，其结论称为定理。本文介绍了证明的定义、性质及其与演绎的关系。
|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
|published_time=2023-07-01
}}
{{InfoBox
|name=证明
|eng_name=proof
}}
{{InfoBox
|name=可证明的
|eng_name=provable
}}
{{InfoBox
|name=定理
|eng_name=theorem
|aliases=thesis
}}
'''证明'''('''proof''')指某个推理系统的变形规则下，从空前提到某一结论的步骤。
对应地，这个步骤的存在性被称为'''可证明'''('''provable''')。
'''定理'''('''theorem''')即该系统中任一可证明的公式。

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

== 定义 ==

在指定[[形式化公理系统（逻辑）|形式化公理系统]] <math>\mathbf{H}</math> 中，从[[空集]] <math>\varnothing</math> 到公式 <math>\phi</math> 的一个演绎，即对公式 <math>\phi</math> ，满足下列条件的公式序列 <math>\phi_0, \phi_1, \dots, \phi_n</math> ：
* <math>\phi_n = \phi</math>；
* 对任意 <math>k < n</math>， <math>\phi_k</math> 符合以下任一条件：
** 是 <math>\mathbf{H}</math> 中的公理；
** 能运用 <math>\mathbf{H}</math> 中的推理规则从 <math>\phi_0, \dots, \phi_{k-1}</math> 得到。
这样的公式序列 <math>\phi_0, \phi_1, \dots, \phi_n</math> 是 <math>\mathbf{H}</math> 中公式 <math>\phi</math> 的一个'''证明'''('''proof''')。

对任意公式 <math>\phi</math> ，以下条件等价：
* 公式 <math>\phi</math> 可从空集演绎（<math>\varnothing \vdash \phi</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> 中的'''定理'''('''theorem''', thesis)。

== 性质 ==

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


{{证明论}}