证明理论（proof theory）是一个在数学证明中的概念，大多民间研究者被冠以”民科“的一大原因就是因为他们往往用一些想当然收集到的事例来证明自己的观点或者发现，这个论证过程或者论据本身不符合研究证明的逻辑。不仅如此，只有遵循这个方法，研究者才能在法理上拥有新发现的持有权，即便观点本身正确且由该研究者首先提出。

闲言少叙，直入正题：

大体上，目前对数学证明有两种截然不同的观点。其中一种叫普识证明（哈哈，我瞎翻的）这种证明通常由自然语言描述及一些相关的符号及公式构成；而另一种则叫制式证明，制式证明只能由一系列符号以及这些符号之间明确的约束关系构成。

请看下面的例子：

1）普识证明

A和B差不多，B和C差不多，那么A和C差不多

2）制式证明

A=B && B=C  =>  A=C

这两者只是对证明的形式上有不同的规定并不一定互相排斥，其中制式证明也可以被认为是普识证明的一种表现形式。而我们讨论的证明理论仅限于制式证明，这个是需要预先明确的。

制式证明通常由下面四步

1）将与证明相关的论证基础（公理或者经过可靠证明的公理延申）符号化或者叫公式化，并保障这个理论体系的逻辑强度（必要的话补充必要的证明或者推导细节）。

2）研究这个理论体系和你需要证明的观点的逻辑关系。

3）尽可能完整这种逻辑关系里面的约束条件，尽可能量化因素(completeness & soundness)。

4）将这个逻辑证明的”关系“最优化或者最简化

这个体系有一些常见的证明方法，如经典的modus ponens

A－＞Ｂ＆　Ａ　＝＝＞　Ｂ

其中　A－＞Ｂ＆　Ａ　称为前提，而　B称为结论。

例如 axiom schema，一种公理”泛化“的规则，举个简单的例子

A是B的子集 <-> 存在一个集合C，所有属于C的元素只要属于A那么(->)必然属于B

假设 <->的两端存在一条公理，那么这个关系既可以被左边替换也可以被右侧替换（如果必要）

公理可以用规则的方式表述

借用之前表述modus ponens的方式

Null ==> axiom 不需要前提的结论（这一切都是为了能纳入证明体系）

Julian JIN

2019-4-5