证明的定义是什么？证明的意义是什么？ 第1页

谢邀。

简单的说，证明是一串有限长的推理语句，从公理出发一直连接到待证命题。

“在研究一个问题之前，该不该先研究一下能不能用初等数学证明？“ 这种事情，其实在 数理逻辑 这个领域是有人研究的。数理逻辑下面有个学科叫 证明论，事实上知乎上就有关于证明论的讨论

证明论是把一个数学证明本身当成一个数学客体，研究 证明 本身的性质。比如其中有个分支叫 反推数学。这个分支在国内本来是没什么人知道的，但是几年前中南大学本科生刘路解决了反推数学中的西塔潘猜想被中南直聘为教授级研究员以后，一下子声名鹊起。反推数学研究的东西，简单的说，就是研究一个证明的“强度”。其实有点类似题主的说法。反推的意思是，从定理反推回公理。如果定理A能够反推回公理B，但是B推不出A，那么A严格比B强。反过来，如果公理C推出定理A，那么A比C弱。由 是否可以相互推导 得出不同公理体系之间的强度比较，这就是反推数学的核心内容。

我本来也不是做逻辑这个方向的，还是请逻辑方向的专业人士来做更为准确的介绍。反推数学的报告我其实听过两三次，但是从来没有记住过那几个常用的组合公理的记号和含义。。

不同的形式系统里，形式化证明的具体定义可能有所差别。但是差距都是不大的。

拿一阶语言举一个例子。规定一阶语言Δ的公理集是Ω。

对一个Δ中的命题A和一组Δ中的命题组成的序列，这个序列叫做A的证明序列，当且仅当:

1.这个命题序列的最后一项恰好是A

2.这个命题序列中的每一项B都符合以下四个要求之一:

①B是重言式

②B是一个公理

③存在序列中在B之前的某一项C，把C的一个原子命题全部替换成另一个命题得到的新命题恰好为B

④存在序列中在B之前的某两项，分别为P和P→B

在这个意义上，形式系统里的证明其实就是按照一定的规则对字符串进行改造。

当然具体的规则可以会比较五花八门，比如很基础的，要研究语法真和语义真的关系的时候，我们只把个别的三条重言命题作为公理。（当然其他的重言命题就不能作为进入推理序列的依据）也会有形式系统里面的推理规则要更多（我刚刚举得例子里，只有p→q加p推出q一条推理规则）也会有高阶的一些语言，加入了各种量词。

总之，形式化的证明，就是对字符串按照一定的规则进行操作。