61、证明理论与不一致理论的探索

证明理论与不一致理论的探索

1. 证明理论基础

证明理论在数学推理中起着关键作用。Herbrand定理在定理证明程序设计方面具有一定优势，尽管Herbrand证明可能比常规证明更长，但基于搜索项和测试命题有效性来构建定理证明程序似乎更容易。同时，Herbrand定理还用于证明挖掘，例如H. Luckhardt对Roth定理的“Herbrand分析”，通过该分析改进了已知的界限。

Roth定理是数论中的一个结果，对于每个无理代数数 $a$ 和 $\varepsilon > 0$，不等式 $\left|a - \frac{p}{q}\right| < \frac{1}{q^{2 + \varepsilon}}$ 只有有限个互质整数解 $p$ 和 $q$。这意味着无理代数数不能用误差渐近小于分母平方倒数的分数来近似。

2. 相继式演算与切割消除

Gerhard Gentzen发明了将一般证明转化为直接证明的另一种方法——相继式演算。他最初研究自然演绎演算，为了便于逻辑研究，逐渐简化系统，最终得到相继式演算。该演算的关键思想是仅使用引入规则，从简单公式逐步推导出复杂公式。

例如，合取和析取的自然规则如下：
- 从 $A$ 和 $B$ 推导出 $A \land B$；
- 从 $A$ 推导出 $A \lor B$；
- 从 $B$ 推导出 $A \lor B$。

然而，这个想法需要对系统进行技术修改。Gentzen引入了相继式的概念，即一步证明可以由多个公式组成，相继式的含义是其中公式的析取。在相继式演算中，对一个或多个相继式中的固定少量公式（通常仅一个）应用规则，其余相继式直接复制到