Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model Theory
This work provides a constructive, mechanized approach to finite model theory, advancing formal verification in logic and computer science, though it is incremental in applying existing methods to a new setting.
The paper tackles the classification of finite first-order satisfiability (FSAT) in constructive type theory, proving Trakhtenbrot's theorem that FSAT is undecidable for signatures with at least binary relations and establishing decidability for monadic logic and enumerability for arbitrary enumerable signatures, with all results mechanized in 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.