一句话：在 Coq 中机械化有限一阶可满足性的可判定性分类，证明 Trakhtenbrot 定理并归约到分离逻辑。
本文在依赖类型论的构造性设定下研究有限一阶可满足性（FSAT），采用可枚举性与可判定性的合成式刻画，按一阶符号表对 FSAT 给出完整分类。工作核心是机械化 Trakhtenbrot 定理：只要符号表含至少二元关系符号，FSAT 不可判定；证明从 Post 对应问题出发构造多一归约链。另一方面，证明仅含至多一元函数与关系符号的 monadic 一阶逻辑中 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. 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.
@article{paperbot1694,
title = {Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens},
author = {Dominik Kirst and Dominique Larchey-Wendling},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 2},
year = {2022},
doi = {10.46298/lmcs-18(2:17)2022}
}