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

[[分类:证明论]]
{{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)。


{{证明论}}