微分方程公理化：微分幽灵的惊人威力

我们证明了微分方程不变量公理化的完备性。首先，我们表明微分动态逻辑中的微分方程公理对所有代数不变量是完备的。我们的证明利用了微分幽灵，其引入可沿新微分方程自由演化的附加变量。巧妙选取的微分幽灵是暗物质的证明论对应物。它们创造新的假设状态，其与原始状态变量的关系满足先前不存在的不变量。这些新不变量在原始系统中的反映进而使其分析成为可能。我们随后表明，将存在性与唯一性公理扩展至该公理化可使其对所有局部进展性质完备，并进一步以实归纳公理扩展可使其对所有实算术不变量完备。这产生了一个精简的公理化，作为推理微分方程不变量的逻辑基础。此外，我们的结果纯为公理化，故该公理化适于在基础定理证明器中可靠实现。