Coq中的Trakhtenbrot定理，有限模型理论的构造性方法
Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model Theory
摘要：
本文在相依类型论的构造性背景下研究有限一阶可满足性。利用可枚举性和可判定性的综合考虑，我们根据非逻辑符号的一阶签名给出了FSAT的完整分类。一方面，我们的发展集中在Trakhtenbrot的定理，指出FSAT是不可判定的，只要签名包含至少一个二元关系符号。我们的证明收益从邮政对应问题的多一个减少链。另一方面，我们建立了一元一阶逻辑的FSAT的可判定性，即签名最多只包含一元函数和关系符号，以及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. All our results are mechanised in the framework of a growing Coq library of synthetic undecidability proofs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
