Trakhtenbrot定理在Coq中的证明：通过构造性视角的有限模型论
Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens
AI总结：
在Coq中构造性地证明了Trakhtenbrot定理，通过多一归约链分类了FSAT的不可判定性与可判定性，并应用于分离逻辑。
摘要：
我们在依赖类型理论的构造性环境中研究有限一阶可满足性（FSAT）。利用可枚举性和可判定性的综合表述，我们根据非逻辑符号的一阶签名给出了FSAT的完整分类。一方面，我们的研究聚焦于Trakhtenbrot定理，该定理指出：只要签名包含至少一个二元关系符号，FSAT就是不可判定的。我们的证明通过从Post对应问题出发的多一归约链进行。另一方面，我们建立了单子一阶逻辑（即签名仅包含至多一元函数和关系符号）中FSAT的可判定性，以及任意可枚举签名下FSAT的可枚举性。为了展示Trakhtenbrot定理的一个应用，我们继续我们的归约链，给出了从FSAT到分离逻辑的多一归约。我们所有的结果都在一个不断增长的Coq综合不可判定性证明库框架中被机械化实现。
英文摘要：
We study finite first-order satisfiability (FSAT) in the constructive setting of dependent type theory. Employing synthetic accounts of enumerability and decidability, we give a full classification of FSAT depending on the first-order signature of non-logical symbols. On the one hand, our development focuses on Trakhtenbrot's theorem, stating that FSAT is undecidable as soon as the signature contains an at least binary relation symbol. Our proof proceeds by a many-one reduction chain starting from the Post correspondence problem. On the other hand, we establish the decidability of FSAT for monadic first-order logic, i.e. where the signature only contains at most unary function and relation symbols, as well as the enumerability of FSAT for arbitrary enumerable signatures. To showcase an application of Trakhtenbrot's theorem, we continue our reduction chain with a many-one reduction from FSAT to separation logic. All our results are mechanised in the framework of a growing Coq library of synthetic undecidability proofs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
