多谱数到非谇数谓词逻辑标准翻译的构造性证明
逻辑
2026-05-19 v2
摘要
众所周知，许多谇数逻辑可通过为每个sort添加谓词、将量词相对化到这些谓词上并添加适当公理来归约为非谇数一阶逻辑。现有关于许多谇数语言包含等号且目标非谇数计算包含常规等号规则/公理时的翻译正确性构造性证明存在缺陷。我们给出一种有效程序形式的初等证明，以闭合这一差距。作为应用，我们对van Dalen将二阶逻辑翻译为非谇数一阶逻辑的论断提供了完全语法的合理性。我们还给出一种关于Herbrand于1930年论文中所述声明的新证明：在无等号情况下，句子在许多谇数逻辑中可导与否等价于在非谇数逻辑中可导与否。我们的证明避免了后续Schmidt和Wang论证中使用的复杂工具。
关键词
引用
@article{arxiv.2603.18216,
title = {Constructive proofs for the standard translation of many-sorted to unsorted predicate logic},
author = {Hrafn Valtýr Oddsson},
journal= {arXiv preprint arXiv:2603.18216},
year = {2026}
}
备注
21 pages, revised and reorganized exposition, simplified proof of Proposition 9, results unchanged