微分方程不变性公理系统

本文证明了由 Noetherian 函数描述的微分方程不变性公理系统的完备性。首先，微分动态逻辑的微分方程公理被证明对解析不变性的推理是完备的。完备性关键利用了微分 ghost，其引入可沿新微分方程自由演化的附加变量。巧妙选择的微分 ghost 是暗物质的证明论对应物。它们创造新的假设状态，其与原始状态变量的关系满足先前不存在的不变性。这些新不变性在原始系统中的反映进而使其分析成为可能。带有存在性与唯一性公理的扩展公理系统对所有局部进展性质是完备的，并且带有实归纳公理时，对所有半解析不变性是完备的。这一精简的公理系统作为微分方程不变性推理的逻辑基础。事实上，正是这种逻辑处理使得完备性推广到 Noetherian 情形成为可能。