一阶逻辑中错误猜想的反驳与迪克森引理的形式化证明

# 一阶逻辑中错误猜想的反驳与迪克森引理的形式化证明 ## 1. 反驳错误猜想的技术 ### 1.1 抽象化方法 在一阶逻辑中，为了反驳错误猜想，采用了抽象化的核心思想。将一阶逻辑公式转换为不含后继函数的二阶一元逻辑公式，因为二阶一元逻辑是可判定的。通过一系列推导，如： \[ \begin{align*} \Gamma ', \alpha([a/x]F '_{|s\leftarrow t}), \alpha(s = t) &\Rightarrow \alpha([a/x]F '), \Delta \quad \text{I.H.}\\ \Gamma ', [[a/x]]\alpha(F '_{|s\leftarrow t}), \alpha(s = t) &\Rightarrow [[a/x]]\alpha(F '), \Delta \quad \text{Lemma 2} \times 2\\ \Gamma ', [\alpha(a)/x]\alpha(F '_{|s\leftarrow t}), \alpha(s = t) &\Rightarrow [\alpha(a)/x]\alpha(F '), \Delta \quad \text{Lemma 3} \times 2\\ \Gamma ', \forall x. \alpha(F '_{|s\leftarrow t}), [\alpha(a)/x]\alpha(F '_{|s\leftarrow t})\alpha(s = t) &\Rightarrow [\alpha(a)/x]\alpha(F '), \Delta \quad \text{weak L}\\ \Gamma ', \forall x. \alpha(F '_{|s\leftarrow t}), \alpha(s = t) &\Rightarrow [\alpha(a)/x]\alpha(F '), \Delta \quad \forall \text{L}\\ \Gamma ', \forall x. \alpha(F '_{|s\leftarrow t}), \alpha(s = t) &\Rightarrow \forall x. \alpha(F '), \Delta \quad \forall \text{R} \end{align*} \] 证明了这种抽象化是可靠的，即它保留了可证明性。如果在二阶一元逻辑中没有证明，那么最初的猜想在一阶逻辑中也是不可证明的。 ### 1.2 示例说明 例如，对于一阶逻辑公式 \(F_0 \supset \forall p. \forall p'. \forall t. \forall s. \forall s'. \text{subtree}(t, p, s) \land \text{subtree}(t, p', s') \supset s = s'\)，其抽象化后的公式为： \[ F_0 \supset \forall p. \forall p'. \forall t. \forall s. \forall s'. \text{subtree}(t) \land \text{subtree}(p) \land \text{subtree}(s) \land \text{subtree}(t) \land \text{subtree}(p') \land \text{subtree}(s') \supset (\forall X. X(s) \supset X(s')) \land (\forall X. X(s') \supset X(s)) \] 这个结果在 \(S0S\) 中不可证明，根据抽象化的可靠性定理，它在具有原始相等性的一阶逻辑中也不可证明。 ### 1.3 不可证明公式的子类 该技术可以处理一类具有无限反例模型的一阶逻辑公式。以非有效一阶逻辑公式 \(\phi := (\exists x. P(x) \land \forall x. \exists y. P(x) \supset (y > x \land P(y)) \land \forall x, y, z. (x > y \land y > z) \supset x > z \land \forall x. x \neq x) \supset \exists x. \neg P(x)\) 为例，假设 \(I\) 是一个反例模型，使得 \(I(\phi) = \bot\)，这意味着 \(I\) 验证了蕴含式的左侧，并且否定了 \(\exists x. \neg P(x)\)。由此可以推出 \(P\)、\(>\) 和 \(=\) 的解释必须是无限的。其抽象化后的公式 \(\alpha(\phi)\) 在 \(S0S\) 中也是无效的。 ### 1.4 实现 该反驳错误猜想的过程已在 \(MAYA\) 系统中实现。\(MAYA\) 是一个用于结构化规范的大型验证工具，基于开发图的概念，能够在规范更改时有效管理和调整证明信息。具体操作步骤如下： 1. 抽象定义理论公理的一阶逻辑子集 \(\Phi\) 为二阶一元逻辑。 2. 为了反驳错误猜想 \(\psi\)，检查 \(S0S\) 公式 \(\alpha(\Phi \supset \psi)\) 的有效性。 3. 为了决定 \(S0S\) 公式的有效性，将 \(MAYA\) 与 \(MONA\) 系统链接。虽然 \(MONA\) 仅实现了弱二阶一元逻辑的决策过程，但它在没有后继函数的完整二阶一元逻辑上是保守的，在 \(MONA\) 中找到的反例模型在更一般的情况下也是反例模型。 ## 2. 迪克森引理在 ACL2 中的形式化证明 ### 2.1 背景与动机 迪克森引理是证明布赫伯格算法终止的关键结果。由于 \(ACL2\) 逻辑的表达能力有限，经典的非构造性证明无法在 \(ACL2\) 中完成。因此，采用了基于良序关系的多重集扩展的构造性证明方法。 ### 2.2 ACL2 逻辑概述 \(ACL2\) 逻辑是一种无量词的一阶逻辑，具有等式和归纳证明原则。新函数定义只有在存在一个度量，使得每个递归调用的参数相对于良序关系递减时，才被