Skip to Main content Skip to Navigation
New interface
Journal articles

Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens

Abstract : 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 Trakthenbrot'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.
Complete list of metadata

https://hal.inria.fr/hal-03359508
Contributor : Dominique Larchey-Wendling Connect in order to contact the contributor
Submitted on : Friday, June 17, 2022 - 12:00:41 PM
Last modification on : Friday, June 17, 2022 - 12:27:47 PM

File

2104.14445v5.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Collections

Citation

Dominik Kirst, Dominique Larchey-Wendling. Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens. Logical Methods in Computer Science, 2022, 18 (2), pp.17:1-17:29. ⟨10.46298/lmcs-18(2:17)2022⟩. ⟨hal-03359508⟩

Share

Metrics

Record views

106

Files downloads

9