背景与动机
在20世纪初，数学家们开始关注数学基础的可靠性问题。特别是，哥德尔不完备定理的出现对形式化系统的一致性提出了挑战。哥德尔第二不完备定理指出，一个足够强大的形式系统，如果是一致的，那么它不能在自身系统内证明它的一致性。根岑的证明试图绕过这个限制，通过发展一种不同的证明方法，来证明算术系统的一致性。
证明的核心思想
根岑的证明采用了截断推理（cut-elimination）的方法。他证明了对于一阶谓词逻辑加上算术公理的系统，所有可证明的定理都可以通过消除推理规则中的“截断”规则来证明。截断规则本质上是表示“如果A且如果A蕴含B，那么B”的推理。消除截断规则意味着证明过程可以被简化为更基本、更直观的步骤。这一过程的核心在于保证证明的结构性，从而避免了潜在的矛盾。
证明的方法
根岑的证明涉及复杂的语法分析和递归定义。他引入了序数，用于衡量证明的复杂性。通过对证明结构的仔细分析，根岑证明了，如果一个证明使用了截断规则，那么总可以找到一个等价的、不使用截断规则的证明。这表明，在原系统中，如果存在矛盾，那么一定存在一个更简单的矛盾，从而可以推导出原系统是一致的。
根岑证明的核心步骤包括：
- 形式化系统：定义了目标形式系统（例如，皮亚诺算术）。
- 结构规则：引入了证明系统的规则，特别是截断规则。
- 截断消除定理：证明了截断规则可以被消除，并且消除后不会改变证明的正确性。
- 相容性推论：基于截断消除，推出了原形式系统的一致性。
证明的意义
根岑的相容性证明是证明论的重大成就，它提供了形式算术系统一致性的一个具体的证明。它表明，尽管哥德尔不完备定理限制了形式系统自我证明的能力，但仍然存在其他方法来证明它们的一致性。该证明也促进了证明论作为数学研究领域的发展，并为后来的研究奠定了基础。
局限性
尽管根岑的证明是重要的，但它也存在一些局限性。证明本身相当复杂，不易理解。此外，根岑证明所依赖的序数，其长度超过了原系统自身的表达能力，因此从某种程度上说，它属于“外在”证明。这意味着，一致性证明是在原系统之外进行的。
结论
根岑的相容性证明是数学逻辑和证明论领域的一座里程碑。它利用截断消除技术成功证明了形式算术系统的一致性，为数学基础研究提供了重要的理论支撑。该证明展现了证明论强大的工具，并对数学的理解和发展产生了深远的影响。