Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model Theory

Dominik Kirst, Dominique Larchey-Wendling

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 fu…