论文标题
Trakhtenbrot的Coq定理，这是一种有限模型理论的建设性方法
Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model Theory
论文作者
论文摘要
我们在相关类型理论的建设性环境中研究有限的一阶满足（FSAT）。使用枚举性和可决定性的综合说明，我们根据非逻辑符号的一阶标志给出了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.
