Trakhtenbrot’s Theorem in Coq

In the wake of the seminal discoveries concerning the undecidability of first-order logic by Turing and Church in the 1930s, a broad line of work has been pursued to characterise the border between decidable and undecidable fragments of the original decision problem. These fragments can be grouped either by syntactic restrictions controlling the allowed function and relation symbols or the quantifier prefix, or by semantic restrictions on the admitted models (see [1] for a comprehensive description).

Concerning signature restrictions, already predating the undecidability results, Löwenheim had shown in 1915 that monadic first-order logic, admitting only signatures with at most unary symbols, is decidable [15]. Therefore, the successive negative results usually presuppose non-trivial signatures containing an at least binary symbol.

Turning to semantic restrictions, Trakhtenbrot proved in 1950 that, if only admitting finite models, the satisfiability problem over non-trivial signatures is still undecidable [21]. Moreover, the situation is somewhat dual to the unrestricted case, since finite satisfiability (FSAT) is still enumerable while, in the unrestricted case, validity is enumerable. As a consequence, finite validity cannot be characterised by a complete finitary deduction system and, resting on finite model theory, various natural problems in database theory are undecidable.

Conventionally, Trakhtenbrot’s theorem is proved by (many-one) reduction from the halting problem for Turing machines (see e.g. [1, 14]). An encoding of a given Turing machine M can be given as a formula \(\varphi _M\) such that the models of \(\varphi _M\) correspond to the runs of M. Specifically, the finite models of \(\varphi _M\) correspond to terminating runs of M and so a decision procedure for finite satisfiability of \(\varphi _M\) would be enough to decide whether M terminates or not.

Although this proof strategy is in principle explainable on paper, already the formal definition of Turing machines, not to mention their encoding in first-order logic, is not ideal for mechanisation in a proof assistant. So for our Coq mechanisation of Trakhtenbrot’s theorem, we follow a different strategy by starting from the Post correspondence problem (PCP), a simple matching problem on strings. Similar to the conventional proof, we proceed by encoding every instance R of PCP as a formula \(\varphi _R\) such that R admits a solution iff \(\varphi _R\) has a finite model. Employing the framework of synthetic undecidability [8, 11], the computability of \(\varphi _R\) from R is guaranteed since all functions definable in constructive type theory are computable without reference to a concrete model of computation.

Both the conventional proof relying on Turing machines and our elaboration starting from PCP actually produce formulas in a custom signature well-suited for the encoding of the seed decision problems. The sharper version of Trakhtenbrot’s theorem, stating that a signature with at least one binary relation (or one binary function and one unary relation) is enough to turn FSAT undecidable, is in fact left as an exercise in e.g. Libkin’s book [14]. However, at least in a constructive setting, this generalisation is non-trivial and led us to mechanising a chain of signature transformations eliminating and compressing function and relation symbols step by step.

Complementing the undecidability result, we further formalise that FSAT is enumerable for enumerable signatures and decidable for monadic signatures. Again, both of these standard results come with their subtleties when explored in a constructive approach of finite model theory.

In summary, the main contributions of this paper are threefold:

• we provide an axiom-free Coq mechanisation comprising a full classification of finite satisfiability with regards to the signatures allowed;^{Footnote 1}

• we present a streamlined proof strategy for Trakhtenbrot’s theorem well-suited for mechanisation and simple to explain informally, basing on PCP;

• we give a constructive account of signature transformations and the treatment of interpreted equality typically neglected in a classical development.

The rest of the paper is structured as follows. We first describe the type-theoretical framework for undecidability proofs and the representation of first-order logic in Sect. 2. We then outline our variant of Trakhtenbrot’s theorem for a custom signature in Sect. 3. This is followed by a development of enough constructive finite model theory (Sect. 4) to conclude some decidability results (Sect. 5) as well as the final classification (Sect. 6). We end with a brief discussion of the Coq development and future work in Sect. 7.

In order to make this paper accessible to readers unfamiliar with constructive type theory, we outline the required features of Coq’s underlying type theory, the synthetic treatment of computability available in constructive mathematics, some properties of finite types, as well as our representation of first-order logic.

2.1 Basics of Constructive Type Theory

We work in the framework of a constructive type theory such as the one implemented in Coq, providing a predicative hierarchy of type universes \(\mathbb {T} \) above a single impredicative universe \(\mathbb {P} \) of propositions. On type level, we have the unit type with a single element , the void type , function spaces \(X\rightarrow Y\), products \(X\times Y\), sums \(X+Y\), dependent products \(\forall x:X.\,F\,x\), and dependent sums \(\{{x:X}\mid {F\,x}\}\). On propositional level, these types are denoted using the usual logical notation (\(\top \), \(\bot \), \(\rightarrow \), \(\wedge \), \(\vee \), \(\forall \), and \(\exists \)).

We employ the basic inductive types of Booleans (\(\mathbb {B} \mathbin {::=}\mathsf {tt}\mid \mathsf {ff}\)), of Peano natural numbers (\(n:\mathbb {N} \mathbin {::=}0\mid \mathsf {S}\,n\)), the option type (\(\mathbb {O}\,X\mathbin {::=}\ulcorner x\urcorner \mid \emptyset \)), and lists (). We write for the length of a list, for the concatenation of l and m, \(x\in l\) for membership, and simply \(f\,[x_1;\ldots ;x_n]\mathbin {:=}[f\,x_1;\ldots ;f\,x_n]\) for the map function. We denote by \(X^n\) the type of vectors of length \(n:\mathbb {N} \) and by \(\mathbb {F} _{n}\) the finite types understood as indices \(\{0,\ldots ,n-1\}\). The definitions/notations for lists are shared with vectors \(\varvec{v}:X^n\). Moreover, when \(i:\mathbb {F} _{n}\) and x : X, we denote by \(\varvec{v}_i\) the i-th component of \(\varvec{v}\) and by \({\varvec{v}}[{x}/{i}]\) the vector \(\varvec{v}\) with i-th component updated to value x.

2.2 Synthetic (Un-)decidability

We review the main ingredients of our synthetic approach to decidability and undecidability [7, 8, 10, 11, 13, 19], based on the computability of all functions definable in constructive type theory.^{Footnote 2} We first introduce standard notions of computability theory without referring to a formal model of computation, e.g. Turing machines.

Definition 1

A problem or predicate \(p:X\rightarrow \mathbb {P} \) is

• decidable if there is \(f:X \rightarrow \mathbb {B} \) with \(\forall x.\,p\,x\mathrel \leftrightarrow f\,x=\mathsf {tt}\).

• enumerable if there is \(f:\mathbb {N} \rightarrow \mathbb {O}\,X\) with \(\forall x.\,p\,x\mathrel \leftrightarrow \exists n.\, f\,n=\ulcorner x\urcorner \).

These notions generalise to predicates of higher arity. Moreover, a type X is

• enumerable if there is \(f:\mathbb {N} \rightarrow \mathbb {O}\,X\) with \(\forall x. \exists n.\, f\,n=\ulcorner x\urcorner \).

• discrete if equality on X (i.e. \(\lambda xy:X.\,x=y\)) is decidable.

• a data type if it is both enumerable and discrete.

Using the expressiveness of dependent types, we equivalently tend to establish the decidability of a predicate \(p:X\rightarrow \mathbb {P} \) by giving a function \(\forall x:X.\,p\,x +\lnot p\,x\). Note that it is common to mechanise decidability results in this synthetic sense (e.g. [2, 16, 17]). Next, decidability and enumerability transport along reductions:

Definition 2

A problem \(p:X\rightarrow \mathbb {P} \) (many-one) reduces to \(q:Y\rightarrow \mathbb {P} \), written \(p\mathrel \preceq q\), if there is a function \(f: X\rightarrow Y\) such that \(p\,x\mathrel \leftrightarrow q\,(f\,x)\) for all x : X.^{Footnote 3}

Fact 3

Assume \(p:X\rightarrow \mathbb {P} \), \(q:Y\rightarrow \mathbb {P} \) and \(p\mathrel \preceq q\): (1) if q is decidable, then so is p and (2) if X and Y are data types and q is enumerable, then so is p.

Item (1) implies that we can justify the undecidability of a target problem by reduction from a seed problem known to be undecidable, such as the halting problem for Turing machines. This is in fact the closest rendering of undecidability available in a synthetic setting, since the underlying type theory is consistent with the assumption that every problem is decidable.^{Footnote 4} Nevertheless, we believe that in the intended effective interpretation for synthetic computability, a typical seed problem is indeed undecidable and so are the problems reached by verified reductions.^{Footnote 5} More specifically, since the usual seed problems are not co-enumerable, (2) implies that the reached problems are not co-enumerable either.

Given its simple inductive characterisation involving only basic types of lists and Booleans, the (binary) Post correspondence problem (\(\mathsf {BPCP}\)) is a well-suited seed problem for compact encoding into first-order logic.

Definition 4

Given a list \(R: \mathbb {L}(\mathbb {L}\,\mathbb {B} \times \mathbb {L}\,\mathbb {B})\) of pairs s/t of Boolean strings,^{Footnote 6} we define derivability of a pair s/t from R (denoted by \(R\triangleright s/t\)) and solvability (denoted by \(\mathsf {BPCP} \,R\)) by the following rules:

Fact 5

Given a list \(R:\mathbb {L}(\mathbb {L}\,\mathbb {B} \times \mathbb {L}\,\mathbb {B})\), the derivability predicate \(\lambda s\,t.R\triangleright s/t\) is decidable. However, the halting problem for Turing machines reduces to \(\mathsf {BPCP}\).

Proof

We give of proof of the decidability of \(R\triangleright s/t\) by induction on . We also provide a trivial proof of the equivalence of two definitions of \(\mathsf {BPCP}\). See [7, 10] for details on the reduction from the halting problem to \(\mathsf {BPCP}\).    \(\square \)

It might at first appear surprising that derivability \(\lambda s\,t.R\triangleright s/t\) is decidable while \(\mathsf {BPCP}\) is reducible from the halting problem (and hence undecidable). This simply illustrates that undecidability is caused by the unbounded existential quantifier in the equivalence \(\mathsf {BPCP} \,R\mathrel \leftrightarrow \exists s.\, R\triangleright s/s\).

2.3 Finiteness

Definition 6

A type X is \( finite \) if there is a list \(l_X\) with \(x\in l_X\) for all x : X and a predicate \(p:X\rightarrow \mathbb {P} \) is \( finite \) if there is a list \(l_p \) with \(\forall x.\, p\,x\mathrel \leftrightarrow x\in l_p \).

Note that in constructive settings there are various alternative characterisations of finiteness^{Footnote 7} (bijection with \(\mathbb {F} _{n}\) for some n; negated infinitude for some definition of infiniteness; etc.) and we opted for the above since it is easy to work with while transparently capturing the expected meaning. One can distinguish strong finiteness in \(\mathbb {T} \) (i.e. \(\{{l_X:\mathbb {L}\,X}\mid {\forall x.\, x\in l_X}\}\)) from weak finiteness in \(\mathbb {P} \) (i.e. \(\exists l_X:\mathbb {L}\,X.\,\forall x.\, x\in l_X\)), the list \(l_X\) being required computable in the strong case.

We present three important tools for manipulating finite types: the finite pigeon hole principle (PHP) here established without assuming discreteness, the well-foundedness of strict orders over finite types, and quotients over strongly decidable equivalences that map onto \(\mathbb {F} _{n}\). The proofs are given in Appendix A of the extended version of this paper [12].

For the finite PHP, the typical classical proof requires the discreteness of X to design transpositions/permutations. Here we avoid discreteness completely, the existence of a duplicate being established without actually computing one.

Theorem 7

(Finite PHP). Let \(R:X\rightarrow Y\rightarrow \mathbb {P} \) be a binary relation and \(l:\mathbb {L}\,X\) and \(m:\mathbb {L}\,Y\) be two lists where m is shorter than l . If R is total from l to m \((\forall x.\, x\in l \rightarrow \exists y.\, y\in m \wedge R\,x\,y)\) then the values at two distinct positions in l are related to the same y in m, i.e. there exist \(x_1,x_2\in l\) and \(y\in m\) such that l has shape .

Using the PHP, one can constructively show that, for a strict order over a finite type X, any descending chain has length bounded by the size of X.^{Footnote 8}

Fact 8

Every strict order on a finite type is well-founded.

Coq’s type theory does not provide quotients in general (see e.g. [6]) but one can build computable quotients in certain conditions, here for a decidable equivalence relation of which representatives of equivalence classes are listable.

Theorem 9

(Finite decidable quotient). Let \({\sim }:X\rightarrow X\rightarrow \mathbb {P} \) be a decidable equivalence with \(\{{l_r:\mathbb {L}\,X}\mid {\forall x\exists y.\,y\in l_r\wedge x\sim y}\}\), i.e. finitely many equivalence classes.^{Footnote 9} Then one can compute the quotient \(X/{\sim }\) onto \(\mathbb {F} _{n}\) for some n, i.e. \(n:\mathbb {N} \), \(c:X\rightarrow \mathbb {F} _{n}\) and \(r:\mathbb {F} _{n}\rightarrow X\) s.t. \(\forall p.\,c\,(r\,p) = p\) and \(\forall x \,y.\,x\sim y\mathrel \leftrightarrow c\,x = c\, y\).

Using Theorem 9 with identity over X as equivalence, we get bijections between finite, discrete types and the type family \((\mathbb {F} _{n})_{n:\mathbb {N}}\).^{Footnote 10}

Corollary 10

If X is a finite and discrete type then one can compute \(n:\mathbb {N} \) and a bijection from X to \(\mathbb {F} _{n}\).

2.4 Representing First-Order Logic

We briefly outline our representation of the syntax and semantics of first-order logic in constructive type theory (cf. [9]). Concerning the syntax, we describe terms and formulas as dependent inductive types over a signature \(\varSigma =(\mathcal {F} _{\varSigma }; \mathcal {P} _{\varSigma })\) of function symbols \(f:\mathcal {F} _{\varSigma }\) and relation symbols \(P:\mathcal {P} _{\varSigma }\) with arities and , using binary connectives and quantifiers :

Negation is defined as the abbreviation .

In the chosen de Bruijn representation [4], a bound variable is encoded as the number of quantifiers shadowing its binder, e.g. \(\forall x.\,\exists y.\, P\,x\,u\rightarrow P\,y\,v\) may be represented by \(\dot{\forall }\,\dot{\exists }\,P\,1\,4\,\dot{\rightarrow }\, P\,0\,5\). The variables \(2 = 4-2\) and \(3 = 5-2\) in this example are the free variables, and variables that do not occur freely are called fresh, e.g. 0 and 1 are fresh. For the sake of legibility, we write concrete formulas with named binders and defer de Bruijn representations to the Coq development. For a formula \(\varphi \) over a signature \(\varSigma \), we define the list \(\mathsf {FV}(\varphi ):\mathbb {L}\,\mathbb {N} \) of free variables, the list \(\mathcal {F} _{\varphi }: \mathbb {L}\,\mathcal {F} _{\varSigma }\) of function symbols and the list \(\mathcal {P} _{\varphi }: \mathbb {L}\,\mathcal {P} _{\varSigma }\) of relation symbols that actually occur in \(\varphi \), all by recursion on \(\varphi \).

Turning to semantics, we employ the standard (Tarski-style) model-theoretic semantics, evaluating terms in a given domain and embedding the logical connectives into the constructive meta-logic (cf. [22]):

Definition 11

A model \(\mathcal {M} \) over a domain \(D:\mathbb {T} \) is described by a pair of functions \(\forall f.\,D^{|f|}\rightarrow D\) and \(\forall P.\,D^{|P|}\rightarrow \mathbb {P} \) denoted by \(f^\mathcal {M} \) and \(P^\mathcal {M} \).

Given a variable assignment \(\rho :\mathbb {N} \rightarrow D\), we recursively extend it to a term evaluation \(\hat{\rho }:\mathsf {Term} \rightarrow D\) with \(\hat{\rho }\,x\mathbin {:=}\rho \,x\) and \(\hat{\rho }\,(f\,\varvec{v})\mathbin {:=}f^\mathcal {M} \,(\hat{\rho }\,\varvec{v})\), and to the satisfaction relation \(\mathcal {M} \vDash _\rho \varphi \) by

where each logical connective is mapped to its meta-level counterpart and where we denote by \(a\cdot \rho \) the de Bruijn extension of \(\rho \) by a, defined by \((a\cdot \rho )\,0\mathbin {:=}a\) and \((a\cdot \rho )\,(1+x)\mathbin {:=}\rho \,x\).^{Footnote 11}

A \(\varSigma \)-model is thus a dependent triple \((D,\mathcal {M},\rho )\) composed of a domain D, a model \(\mathcal {M} \) for \(\varSigma \) over D and an assignment \(\rho :\mathbb {N} \rightarrow D\). It is finite if D is finite, and decidable if \(P^\mathcal {M}:D^{|P|}\rightarrow \mathbb {P} \) is decidable for all \(P:\mathcal {P} _{\varSigma }\).

Fact 12

Satisfaction is decidable for finite, decidable \(\varSigma \)-models.

Proof

By induction on \(\varphi \); finite quantification preserves decidability.    \(\square \)

In this paper, we are mostly concerned with finite satisfiability of formulas. However, since some of the compound reductions hold for more general or more specific notions, we introduce the following variants:

Definition 13

(Satisfiability). For a formula \(\varphi \) over a signature \(\varSigma \), we write

• \(\mathsf {SAT} (\varSigma )\,\varphi \) if there is a \(\varSigma \)-model \((D,\mathcal {M},\rho )\) such that \(\mathcal {M} \vDash _\rho \varphi \);

• \(\mathsf {FSAT} (\varSigma )\,\varphi \) if additionally D is finite and \(\mathcal {M} \) is decidable;

• \(\mathsf {FSATEQ} (\varSigma ;\equiv )\,\varphi \) if the signature contains a distinguished binary relation symbol \(\equiv \) interpreted as equality, i.e. \(x\equiv ^\mathcal {M} y\mathrel \leftrightarrow x=y\) for all x, y : D.

Notice that in a classical treatment of finite model theory, models are supposed to be given in extension, i.e. understood as tables providing computational access to functions and relations values. To enable this view in our constructive setting, we restrict to decidable relations in the definition of \(\mathsf {FSAT} \), and from now on, finite satisfiability is always meant to encompass a decidable model. One could further require the domain D to be discrete to conform more closely with the classical view; discreteness is in fact enforced by \(\mathsf {FSATEQ}\). However, we refrain from this requirement and instead show in Sect. 4.1 that \(\mathsf {FSAT} \) and \(\mathsf {FSAT} \) over discrete models are constructively equivalent.

In this section, we show that \(\mathsf {BPCP}\) reduces to \(\mathsf {FSATEQ} (\varSigma _{\mathsf {BPCP}};{\equiv })\) for the special purpose signature \(\varSigma _{\mathsf {BPCP}}\mathbin {:=}(\{\star ^0, e^0, f_\mathsf {tt}^1, f_\mathsf {ff}^1\}; \{P^2, {\prec ^2},{\equiv ^2}\})\). To this end, we fix an instance \(R:\mathbb {L}\,(\mathbb {L}\,\mathbb {B} \times \mathbb {L}\,\mathbb {B})\) of \(\mathsf {BPCP} \) (to be understood as a finite set of pairs of Boolean strings) and we construct a formula \(\varphi _R\) such that \(\varphi _R\) is finitely satisfiable if and only if R has a solution.

Informally, we axiomatise a family \(\mathcal {B} _n\) of models over the domain of Boolean strings of length bounded by n and let \(\varphi _R\) express that R has a solution in \(\mathcal {B} _n\). The axioms express enough equations and inversions of the constructions included in the definition of \(\mathsf {BPCP} \) such that a solution for R can be recovered.

Formally, the symbols in \(\varSigma _{\mathsf {BPCP}}\) are used as follows: the functions \(f_b\) and the constant e represent \(b\mathbin {::}(\cdot )\) and for the encoding of strings s as terms \(\overline{s}\):

The constant \(\star \) represents an undefined value for strings too long to be encoded in the finite model \(\mathcal {B} _n\). The relation P represents derivability from R (denoted \(R\triangleright \cdot /\cdot \) here) while \(\prec \) and \(\equiv \) represent strict suffixes and equality, respectively.

Expected properties of the intended interpretation can be captured formally as first-order formulas. First, we ensure that P is proper (only subject to defined values) and that \(\prec \) is a strict order (irreflexive and transitive):

Next, the image of \(f_b\) is forced disjoint from e and injective as long as \(\star \) is not reached. We also ensure that the images of \(f_\mathsf {tt}\) and \(f_\mathsf {ff}\) intersect only at \(\star \):

Furthermore, we enforce that P simulates \(R\triangleright \cdot /\cdot \), encoding its inversion principle

where \(u/v\prec x/y\) denotes \((u\prec x~\dot{\wedge }~ v\equiv y)\dot{\vee }(v\prec y~\dot{\wedge }~ u\equiv x)\dot{\vee }(u\prec x ~\dot{\wedge }~ v\prec y)\). Finally, \(\varphi _R\) is the conjunction of all axioms plus the existence of a solution:

Theorem 14

\(\mathsf {BPCP} \mathrel \preceq \mathsf {FSATEQ} (\varSigma _{\mathsf {BPCP}};{\equiv })\).

Proof

The reduction \(\lambda R.\,\varphi _R\) is proved correct by Lemmas 15 and 16.    \(\square \)

Lemma 15

\(\mathsf {BPCP} \,R\rightarrow \mathsf {FSATEQ} (\varSigma _{\mathsf {BPCP}};{\equiv })\,\varphi _R\).

Proof

Assume \(R\triangleright s/s\) holds for a string s with \(|s|= n\). We show that the model \(\mathcal {B} _n\) over Boolean strings bounded by n satisfies \(\varphi _R\). To be more precise, we choose as domain, i.e. values in \(D_n\) are either an (overflow) value \(\emptyset \) or a (defined) dependent pair \(\ulcorner (s,H_s)\urcorner \) where . We interpret the function and relation symbols of the chosen signature by

where we left out some explicit constructors and the excluded edge cases of the relations for better readability. As required, \(\mathcal {B} _n\) interprets \(\equiv \) by equality \(=_{D_n}\).

Considering the desired properties of \(\mathcal {B} _n\), first note that \(D_n\) can be shown finite by induction on n. This however crucially relies on the proof irrelevance of the \(\lambda x.\,x\le n\) predicate.^{Footnote 12} The atoms \(s\prec ^{\mathcal {B} _n} t\) and \(s\equiv ^{\mathcal {B} _n} t\) are decidable by straightforward computations on Boolean strings. Decidability of \(P^{\mathcal {B} _n}s\,t\) (i.e. \(R\triangleright s/t\)) was established in Fact 5. Finally, since \(\varphi _R\) is a closed formula, any variable assignment \(\rho \) can be chosen to establish that \(\mathcal {B} _n\) satisfies \(\varphi _R\), for instance \(\rho \mathbin {:=}\lambda x.\emptyset \). Then showing \(\mathcal {B} _n\vDash _\rho \varphi _R\) consists of verifying simple properties of the chosen functions and relations, with mostly straightforward proofs.    \(\square \)

Lemma 16

\(\mathsf {FSATEQ} (\varSigma _{\mathsf {BPCP}};{\equiv })\,\varphi _R\rightarrow \mathsf {BPCP} \,R\).

Proof

Suppose that \(\mathcal {M} \vDash _\rho \varphi _R\) holds for some finite \(\varSigma _{\mathsf {BPCP}}\)-model \((D,\mathcal {M},\rho )\) interpreting \(\equiv \) as equality and providing operations \(f^\mathcal {M} _b\), \(e^\mathcal {M} \), \(\star ^\mathcal {M} \), \(P^\mathcal {M} \) and \(\prec ^\mathcal {M} \). Again, the concrete assignment \(\rho \) is irrelevant and \(\mathcal {M} \vDash _\rho \varphi _R\) ensures that the functions/relations behave as specified and that \(P^\mathcal {M} \,x\,x\) holds for some x : D.

Instead of trying to show that \(\mathcal {M} \) is isomorphic to some \(\mathcal {B} _n\), we directly reconstruct a solution for R, i.e. we find some s with \(R\triangleright s/s\) from the assumption that \(\mathcal {M} \vDash _\rho \varphi _R\) holds. To this end, we first observe that the relation \(u/v\prec ^\mathcal {M} x/y\) as defined above is a strict order and thus well-founded as an instance of Fact 8.

Now we can show that for all x/y with \(P^\mathcal {M} \,x\,y\) there are strings s and t with \(x=\overline{s}\), \(y=\overline{t}\) and \(R\triangleright s/t\), by induction on the pair x/y using the well-foundedness of \(\prec ^\mathcal {M} \). So let us assume \(P^\mathcal {M} \,x\,y\). Since \(\mathcal {M} \) satisfies \(\varphi _\triangleright \) there are two cases:

• there is \(s/t\in R\) such that \(x=\overline{s}\) and \(y =\overline{t}\). The claim follows by \(R\triangleright s/t\);

• there are u, v : D with \(P^\mathcal {M} \,u\,v\) and \(s/t\in R\) such that , and \(u/v\prec ^\mathcal {M} x/y\). The latter makes the inductive hypothesis applicable for \(P^\mathcal {M} \,u\,v\), hence yielding \(R\triangleright s'/t'\) for some strings \(s'\) and \(t'\) corresponding to the encodings u and v. This is enough to conclude and \(R\) as wished.

Applying this fact to the assumed match \(P^\mathcal {M} \,x\,x\) yields a solution \(R\triangleright s/s\).    \(\square \)

Combined with Fact 5, Theorem 14 entails the undecidability (and non-co-enumerability) of \(\mathsf {FSATEQ}\) over a custom (both finite and discrete) signature \(\varSigma _{\mathsf {BPCP}}\). By a series of signature reductions, we generalise these results to any signature containing an at least binary relation symbol. In particular, we explain how to reduce \(\mathsf {FSAT} (\varSigma )\) to for any discrete signature \(\varSigma \), hence including \(\varSigma _{\mathsf {BPCP}}\). We also provide a reduction from to \(\mathsf {FSAT} (\{f^n\};\{P^1\})\) for \(n\ge 2\), which entails the undecidability of \(\mathsf {FSAT} \) for signatures with one unary relation and an at least binary function. But first, let us show that \(\mathsf {FSAT} \) is unaltered when further assuming discreteness of the domain.

4.1 Removing Model Discreteness and Interpreted Equality

We consider the case of models over a discrete domain D. Of course, in the case of \(\mathsf {FSATEQ} (\varSigma ;{\equiv })\) the requirement that \(\equiv \) is interpreted as a decidable binary relation which is equivalent to \(=_D\) imposes the discreteness of D. But in the case of \(\mathsf {FSAT} (\varSigma )\) nothing imposes such a restriction on D. However, as we argue here, we can always quotient D using a suitable decidable congruence, making the quotient a discrete finite type while preserving first-order satisfaction.

Definition 17

We write if \(\mathsf {FSAT} (\varSigma )\,\varphi \) on a discrete model.

Let us consider a fixed signature \(\varSigma =(\mathcal {F} _{\varSigma }; \mathcal {P} _{\varSigma })\). In addition, let us fix a finite type D and a (decidable) model \(\mathcal {M} \) of \(\varSigma \) over D. We can conceive an equivalence over D which is a congruence for all the interpretations of the symbols by \(\mathcal {M} \), namely first-order indistinguishability \(x\mathrel {\dot{=}_{\varSigma }}y~\mathbin {:=}~\forall \varphi \,\rho .\, \mathcal {M} \vDash _{x\cdot \rho }\varphi \mathrel \leftrightarrow \mathcal {M} \vDash _{y\cdot \rho }\varphi \), i.e. first-order semantics in \(\mathcal {M} \) is not impacted when switching x with y.

The facts that \(\mathrel {\dot{=}_{\varSigma }}\) is both an equivalence and a congruence are easy to prove but, with this definition, there is little hope of establishing decidability of \(\mathrel {\dot{=}_{\varSigma }}\). The main reason for this is that the signature may contain symbols of infinitely many arities. So we fix two lists \(l_\mathcal {F}: \mathbb {L}\,\mathcal {F} _{\varSigma }\) and \(l_\mathcal {P}: \mathbb {L}\,\mathcal {P} _{\varSigma }\) of function and relation symbols respectively and restrict the congruence requirement to these lists.

Definition 18

(Bounded first-order indistinguishability). We say that x and y are first-order indistinguishable up to \(l_\mathcal {F}/l_\mathcal {P} \), and we write , if for any \(\rho :\mathbb {N} \rightarrow D\) and any first-order formula \(\varphi \) built from the symbols in \(l_\mathcal {F} \) and \(l_\mathcal {P} \) only, we have \(\mathcal {M} \vDash _{x\cdot \rho }\varphi \mathrel \leftrightarrow \mathcal {M} \vDash _{y\cdot \rho }\varphi \).

Theorem 19

First-order indistinguishability \(\mathrel {\dot{=}_{}}\) up to \(l_\mathcal {F}/l_\mathcal {P} \) is a strongly decidable equivalence and a congruence for all the symbols in \(l_\mathcal {F}/l_\mathcal {P} \).

Proof

The proof is quite involved, we only give its sketch here; see Appendix B of the extended version of this paper [12] for more details. The real difficulty is to show the decidability of \(\mathrel {\dot{=}_{}}\). To this end, we characterise \(\mathrel {\dot{=}_{}}\) as a bisimulation, i.e. we show that \(\mathrel {\dot{=}_{}}\) is extensionally equivalent to Kleene’s greatest fixpoint \(\mathrm F^\omega (\lambda uv.\top )\) of some \(\omega \)-continuous operator \(\mathrm F:(D\rightarrow D\rightarrow \mathbb {P}) \rightarrow (D\rightarrow D\rightarrow \mathbb {P})\). We then show that \(\mathrm F\) preserves strong decidability. To be able to conclude, we establish that \(\mathrm F\) reaches its limit after \(l\mathbin {:=}2^{d\times d}\) iterations where \(d\mathbin {:=}\mathrm {card}\,D\), the length of a list enumerating the finite type D. To verify this upper bound, we build the weak powerset, a list of length l which contains all the weakly decidable binary predicates of type \(D\rightarrow D\rightarrow \mathbb {P} \), up to extensional equivalence. As all the iterated values \(\mathrm F^n(\lambda uv.\top )\) are strongly decidable, they all belong to the weak powerset, so by Theorem 7, a duplicate is to be found in the first \(l+1\) steps, ensuring that the sequence is stalled at l.    \(\square \)

We use the strongly decidable congruence \(\mathrel {\dot{=}_{}}\) to quotient models onto discrete ones (in fact \(\mathbb {F} _{n}\) for some n) while preserving first-order satisfaction.

Theorem 20

For every first-order signature \(\varSigma \) and formula \(\varphi \) over \(\varSigma \), we have \(\mathsf {FSAT} (\varSigma )\,\varphi \) iff \(\mathsf {FSAT} '(\varSigma )\,\varphi \), and as a consequence, both reductions \(\mathsf {FSAT} (\varSigma )\mathrel \preceq \mathsf {FSAT} '(\varSigma )\) and \(\mathsf {FSAT} '(\varSigma )\mathrel \preceq \mathsf {FSAT} (\varSigma )\) hold.

Proof

\(\mathsf {FSAT} (\varSigma )\,\varphi \) entails \(\mathsf {FSAT} '(\varSigma )\,\varphi \) is the non-trivial implication. Hence we consider a finite \(\varSigma \)-model \((D,\mathcal {M},\rho )\) of \(\varphi \) and we build a new finite \(\varSigma \)-model of \(\varphi \) which is furthermore discrete. We collect the symbols occurring in \(\varphi \) as the lists \(l_\mathcal {F} \mathbin {:=}\mathcal {F} _{\varphi }\) (for functions) and \(l_\mathcal {P} \mathbin {:=}\mathcal {P} _{\varphi }\) (for relations). By Theorem 19, first-order indistinguishability \({\mathrel {\dot{=}_{}}}:D\rightarrow D\rightarrow \mathbb {P} \) up to \(\mathcal {F} _{\varphi }/\mathcal {P} _{\varphi }\) is a strongly decidable equivalence over D and a congruence for the semantics of the symbols occurring in \(\varphi \). Using Theorem 9, we build the quotient \(D/{\mathrel {\dot{=}_{}}}\) on a \(\mathbb {F} _{n}\) for some \(n:\mathbb {N} \). We transport the model \(\mathcal {M} \) along this quotient and because \(\mathrel {\dot{=}_{}}\) is a congruence for the symbols in \(\varphi \), its semantics is preserved along the quotient. Hence, \(\varphi \) has a finite model over the domain \(\mathbb {F} _{n}\) which is both finite and discrete.    \(\square \)

Theorem 21

If \(\equiv \) is a binary relation symbol in the signature \(\varSigma \), one has a reduction \(\mathsf {FSATEQ} (\varSigma ;{\equiv })\mathrel \preceq \mathsf {FSAT} (\varSigma )\).

Proof

Given a list \(l_\mathcal {F} \) (resp. \(l_\mathcal {P} \)) of function (resp. relation) symbols, we construct a formula \(\psi (l_\mathcal {F},l_\mathcal {P},{\equiv })\) over the function symbols in \(l_\mathcal {F} \) and relation symbols in \(({\equiv }\mathbin {::}l_\mathcal {P})\) expressing the requirement that \(\equiv \) is an equivalence and a congruence for the symbols in \(l_\mathcal {F}/l_\mathcal {P} \). Then we show that \(\lambda \varphi .\, \varphi ~\dot{\wedge }~\psi (\mathcal {F} _{\varphi }, {\equiv }::\mathcal {P} _{\varphi },{\equiv })\) is a correct reduction, where \(\mathcal {F} _{\varphi }\) and \(\mathcal {P} _{\varphi }\) list the symbols occurring in \(\varphi \).    \(\square \)

4.2 From Discrete Signatures to Singleton Signatures

Let us start by converting a discrete signature to a finite and discrete signature.

Lemma 22

For any formula \(\varphi \) over a discrete signature \(\varSigma \), one can compute a signature \(\varSigma _{n,m}=(\mathbb {F} _{n};\mathbb {F} _{m})\), arity preserving maps \(\mathbb {F} _{n}\rightarrow \mathcal {F} _{\varSigma }\) and \(\mathbb {F} _{m}\rightarrow \mathcal {P} _{\varSigma }\) and an equi-satisfiable formula \(\psi \) over \(\varSigma _{n,m}\), i.e. \(\mathsf {FSAT} (\varSigma )\,\varphi \mathrel \leftrightarrow \mathsf {FSAT} (\varSigma _{n,m})\,\psi \).

Proof

We use the discreteness of \(\varSigma \) and bijectively map the lists of symbols \(\mathcal {F} _{\varphi }\) and \(\mathcal {P} _{\varphi }\) onto \(\mathbb {F} _{n}\) and \(\mathbb {F} _{m}\) respectively, using Corollary 10. We structurally map \(\varphi \) to \(\psi \) over \(\varSigma _{n,m}\) along this bijection, which preserves finite satisfiability.    \(\square \)

Notice that n and m in the signature \(\varSigma _{n,m}\) depend on \(\varphi \), hence the above statement cannot be presented as a reduction between (fixed) signatures.

We now erase all function symbols by encoding them with relation symbols. To this end, let \(\varSigma =(\mathcal {F} _{\varSigma }; \mathcal {P} _{\varSigma })\) be a signature, we set where \(\equiv \) is a new interpreted relation symbol of arity two and in the conversion, function symbols have arity lifted by one, hence the \(\mathcal {F} _{\varSigma }^{+1}\) notation.

Lemma 23

For any finite^{Footnote 13} type of function symbols \(\mathcal {F} _{\varSigma }\), one has a reduction .

Proof

The idea is to recursively replace a term t over \(\varSigma \) by a formula which is “equivalent” to \(x\equiv t\) (where x is a fresh variable not occurring in t) and then an atomic formula like e.g. \(P\,[t_1;t_2]\) by \(\exists \, x_1\,x_2.\, x_1\equiv t_1\,\dot{\wedge }\,x_2\equiv t_2\,\dot{\wedge }\, P\,[x_1;x_2]\). We complete the encoding with a formula stating that every function symbol \(f:\mathcal {F} _{\varSigma }\) is encoded into a total functional relation \(P_f: \mathcal {F} _{\varSigma }^{+1}\) of arity augmented by 1.    \(\square \)

Next, assuming that the function symbols have already been erased, we explain how to merge the relation symbols in a signature into a single relation symbol, provided that there is an upper bound for the arities in \(\mathcal {P} _{\varSigma }\).

Lemma 24

The reduction holds when \(\mathcal {P} _{\varSigma }\) is a finite and discrete type of relation symbols and \(|P|\le n\) holds for all \(P:\mathcal {P} _{\varSigma }\).

Proof

This comprises three independent reductions, see Fact 25 below.    \(\square \)

In the following, we denote by \(\mathcal {F} _{\varSigma }^n\) (resp. \(\mathcal {P} _{\varSigma }^n\)) the same type of function (resp. relation) symbols but where the arity is uniformly converted to n.

Fact 25

Let \(\varSigma =(\mathcal {F} _{\varSigma }; \mathcal {P} _{\varSigma })\) be a signature:

• 1. \(\mathsf {FSAT} (\mathcal {F} _{\varSigma }; \mathcal {P} _{\varSigma })\mathrel \preceq \mathsf {FSAT} (\mathcal {F} _{\varSigma }; \mathcal {P} _{\varSigma }^n)\) if \(|P|\le n\) holds for all \(P:\mathcal {P} _{\varSigma }\);

• 2. if \(\mathcal {P} _{\varSigma }\) is finite;

• 3. if \(\mathcal {F} _{\varSigma }\) is discrete.

Proof

For the first reduction, every atomic formula of the form \(P\,\varvec{v}\) with is converted to \(P\,\varvec{v}'\) with \(\varvec{v}'\mathbin {:=}\varvec{v} \mathbin {++}[x_0;\dots ;x_0]\) and for an arbitrary term variable \(x_0\). The rest of the structure of formulas is unchanged.

For the second reduction, we convert every atomic formula \(P\,\varvec{v}\) with into \(Q(P\mathbin {::}\varvec{v})\) where P now represents a constant symbol (Q is fixed).

For the last reduction, we replace every constant symbol by a corresponding fresh variable chosen above all the free variables of the transformed formula.    \(\square \)

4.3 Compressing n-ary Relations to Binary Membership

Let be a singleton signature where P is of arity n. We now show that P can be compressed to a binary relation modelling membership via a construction using hereditarily finite sets [18] (useful only when \(n\ge 3\)).

Theorem 26

.

Technically, this reduction is one of the most involved in this work, although in most presentations of Trakhtenbrot’s theorem, this is left as an “easy exercise,” see e.g. [14]. Maybe it is perceived so because it relies on the encoding of tuples in set theory, which is somehow natural for mathematicians,^{Footnote 14} but properly building the finite set model in constructive type theory was not that easy.

Here we only give an overview of the main tools. We encode an arbitrary n-ary relation \(R:X^n\rightarrow \mathbb {P} \) over a finite type X in the theory of membership over the signature . Membership is much weaker than set theory because the only required set-theoretic axiom is extensionality. Two sets are extensionally equal if their members are the same, and extensionality states that two extensionally equal sets belong to the same sets:

(1)

As a consequence, no first-order formula over \(\varSigma _2\) can distinguish two extensionally equal sets. Notice that the language of membership theory (and set theory) does not contain any function symbol, hence, contrary to usual mathematical practices, there is no other way to handle a set than via its characterising formula which makes it a very cumbersome language to work with formally. However, this is how we have to proceed in the Coq development but here, we stick to meta-level “terms” in the prose for simplicity.

The ordered pair of two sets p and q is encoded as \(({p},{q}) \mathbin {:=}\{\{p\},\{p,q\}\}\) while the n-tuple \((t_1,\ldots ,t_n)\) is encoded as \(({t_1},{(t_2,\ldots ,t_n)})\) recursively. The reduction function which maps formulas over \(\varSigma _n\) to formulas over \(\varSigma _2\) proceeds as follows. We reserve two first-order variables d (for the domain D) and r (for the relation R). We describe the recursive part of the reduction \(\varSigma _{n\rightsquigarrow 2}^r\)

ignoring the de Bruijn syntax (which would imply adding d and r as parameters). Notice that d and r should not occur freely in \(\varphi \). In addition, we require that:

This gives us the reduction function .

The completeness of the reduction \(\varSigma _{n\rightsquigarrow 2}\) is the easy part. Given a finite model of \(\varSigma _{n\rightsquigarrow 2}(\varphi )\) over \(\varSigma _2\), we recover a model of \(\varphi \) over \(\varSigma _n\) by selecting as the new domain the members of d and the interpretation of \(P\,\varvec{v}\) is given by testing whether the encoding of \(\varvec{v}\) as a n-tuple is a member of r.

The soundness of the reduction \(\varSigma _{n\rightsquigarrow 2}\) is the formally involved part, with Theorem 27 below containing the key construction.

Theorem 27

Given a decidable n-ary relation \(R:X^n\rightarrow \mathbb {P} \) over a finite, discrete and inhabited type X, one can compute a finite and discrete type Y equipped with a decidable relation \({\in }:Y\rightarrow Y\rightarrow \mathbb {P} \), two distinguished elements d, r : Y and a pair of maps \(i:X \rightarrow Y\) and \(s:Y \rightarrow X\) s.t.

Proof

We give a brief outline of this quite involved proof, referring to the Coq code for details. The type Y is built from the type of hereditarily finite sets based on [18], and when we use the word “set” below, it means hereditarily finite set. The idea is first to construct d as a transitive set of which the elements are in bijection i/s with the type X, hence d is the cardinal of X in the set-theoretic meaning. Then the iterated powersets \(\mathcal P(d), \mathcal P^2(d),\ldots ,\mathcal P^k(d)\) are all transitive as well and contain d both as a member and as a subset. Considering \(\mathcal P^{2n}(d)\) which contains all the n-tuples built from the members of d, we define r as the set of n-tuples collecting the encodings \(i(\varvec{v})\) of vectors \(\varvec{v}:X^n\) such that \(R\,\varvec{v}\). We show \(r\in p\) for p defined as \(p\mathbin {:=}\mathcal P^{2n+1}(d)\). Using the Boolean counterpart of \((\cdot )\in p\) for unicity of proofs, we then define \(Y\mathbin {:=}\{z\mid z\in p\}\), restrict membership \(\in \) to Y and this gives the finite type equipped with all the required properties. Notice that the decidability requirement for \({\in }\) holds constructively because we work with hereditarily finite sets, and would not hold with arbitrary sets.    \(\square \)

4.4 Summary: From Discrete Signatures to the Binary Signature

Combining all the previous results, we give a reduction from any discrete signature to the binary singleton signature.

Theorem 28

holds for any discrete signature \(\varSigma \).

Proof

Let us first consider the case of \(\varSigma _{n,m}=(\mathbb {F} _{n};\mathbb {F} _{m})\), a signature over the finite and discrete types \(\mathbb {F} _{n}\) and \(\mathbb {F} _{m}\). Then we have a reduction by combining Theorems 20, 21 and 26 and Lemmas 23 and 24.

Let us denote by \(f_{n,m}\) the reduction . Let us now consider a fixed discrete signature \(\varSigma \). For a formula \(\varphi \) over \(\varSigma \), using Lemma 22, we compute a signature \(\varSigma _{n,m}\) and \(\psi \) over \(\varSigma _{n,m}\) s.t. \(\mathsf {FSAT} (\varSigma )\,\varphi \mathrel \leftrightarrow \mathsf {FSAT} (\mathbb {F} _{n};\mathbb {F} _{m})\,\psi \). The map \(\lambda \varphi .f_{n,m}\,\psi \) is the required reduction.    \(\square \)

Lemma 29

when \(n\ge 2\).

Proof

We encode the binary relation \(\lambda x\,y.\,P\,[x;y]\) with \(\lambda x\,y.\,Q \bigl (f\,[x;y;\dots ]\bigr )\), using the first two parameters of f to encode pairing. But since we need to change the domain of the model, we also use a fresh variable d to encode the domain as \(\lambda x.\,Q (f\,[d;x;\dots ])\) and we restrict all quantifications to the domain similarly to the encoding \(\varSigma _{n\rightsquigarrow 2}^r\) of Sect. 4.3.    \(\square \)

We finish the reduction chains with the weakest possible signature constraints. The following reductions have straightforward proofs.

Fact 30

One has reductions for the three statements below (for \(n\ge 2\)):

• 1. ;

• 2. if \(\varSigma \) contains an n-ary relation symbol;

• 3. \(\mathsf {FSAT} (\{f^n\};\{Q^1\})\mathrel \preceq \mathsf {FSAT} (\varSigma )\) if \(\varSigma \) contains an n-ary fun. and a unary rel.

Complementing the previously studied negative results, we now examine the conditions allowing for decidable satisfiability problems.

Lemma 31

(FSAT over a fixed domain). Given a discrete signature \(\varSigma \) and a discrete and finite type D, one can decide whether or not a formula over \(\varSigma \) has a (finite) model over domain D.

Proof

By Fact 12, satisfaction in a given finite model is decidable. It is also invariant under extensional equivalence, so we only need to show that there are finitely many (decidable) models over D up to extensional equivalence.^{Footnote 15}    \(\square \)

Lemma 32

A formula over a signature \(\varSigma \) has a finite and discrete model if and only if it has a (finite) model over \(\mathbb {F} _{n}\) for some \(n:\mathbb {N} \).

Proof

If \(\varphi \) has a model over a discrete and finite domain D, by Corollary 10, one can bijectively map D to \(\mathbb {F} _{n}\) and transport the model along this bijection.    \(\square \)

Lemma 33

is decidable if \(\mathcal {P} _{\varSigma }\) is discrete with uniform arity 1.

Proof

By Lemma 22, we can assume \(\mathcal {P} _{\varSigma }=\mathbb {F} _{n}\) w.l.o.g.We show that if \(\varphi \) has a finite model then it must have a model over domain \(\{\varvec{v}:\mathbb {B} ^n\rightarrow \mathbb {B} \mid b\,\varvec{v} = \mathsf {tt}\}\) for some Boolean subset \(b:(\mathbb {B} ^n\rightarrow \mathbb {B})\rightarrow \mathbb {B} \). Up to extensional equivalence, there are only finitely many such subsets b and we conclude with Lemma 31.    \(\square \)

Lemma 34

For any finite type \(\mathcal {P} _{\varSigma }\) of relation symbols and signatures of uniform arity 1, we have a reduction .

Proof

We implemented a proof somewhat inspired by that of Proposition 6.2.7 (Grädel) in [1, pp. 251] but the invariant suggested in the iterative process described there did not work out formally and we had to proceed in a single conversion step instead, switching from single symbols to lists of symbols.    \(\square \)

If functions or relations have arity 0, one can always lift them to arity 1 using a fresh variable (of arbitrary value), like in Fact 25, item (1).

Fact 35

The reduction \(\mathsf {FSAT} (\mathcal {F} _{\varSigma };\mathcal {P} _{\varSigma })\mathrel \preceq \mathsf {FSAT} (\mathcal {F} _{\varSigma }^1;\mathcal {P} _{\varSigma }^1)\) holds when all arities in \(\varSigma \) are at most 1, where \(\mathcal {F} _{\varSigma }^1\) and \(\mathcal {P} _{\varSigma }^1\) denote arities uniformly updated to 1.

We conclude with the exact classification of \(\mathsf {FSAT} \) regarding enumerability, decidability, and undecidability depending on the properties of the signature.

Theorem 36

Given \(\varSigma =(\mathcal {F} _{\varSigma };\mathcal {P} _{\varSigma })\) where both \(\mathcal {F} _{\varSigma }\) and \(\mathcal {P} _{\varSigma }\) are data types, the finite satisfiability problem for formulas over \(\varSigma \) is enumerable.

Proof

Using Theorem 20 and Lemmas 31 and 32, one constructs a predicate \(Q:\mathbb {N} \rightarrow \mathsf {Form} _\varSigma \rightarrow \mathbb {B} \) s.t. \(\mathsf {FSAT} (\varSigma )\,\varphi \mathrel \leftrightarrow \exists n.\,Q\,n\,\varphi = \mathsf {tt}\). Then, it is easy to build a computable enumeration \(e:\mathbb {N} \rightarrow \mathbb {O}\,\mathsf {Form} _\varSigma \) of \(\mathsf {FSAT} (\varSigma ):\mathsf {Form} _\varSigma \rightarrow \mathbb {P} \).    \(\square \)

Theorem 37

\(\mathsf {FSAT} (\varSigma )\) is decidable if \(\varSigma \) is discrete with arities less or equal than 1, or if all relation symbols have arity 0.

Proof

If all arities are at most 1, then by Fact 35, we can assume \(\varSigma \) of uniform arity 1. Therefore, for a formula \(\varphi \) over \(\varSigma \) with uniform arity 1, we need to decide \(\mathsf {FSAT} \) for \(\varphi \). By Theorem 22, we can compute a signature \(\varSigma _{n,m}=(\mathbb {F} _{n};\mathbb {F} _{m})\) and a formula \(\psi \) over \(\varSigma _{n,m}\) equi-satisfiable with \(\varphi \). Using the reduction of Lemma 34, we compute a formula \(\gamma \), equi-satisfiable with \(\psi \), over a discrete signature of uniform arity 1, void of functions. We decide the satisfiability of \(\gamma \) by Lemma 33.

If all relation symbols have arity 0, regardless of \(\mathcal {F} _{\varSigma }\), no term can occur in formulas, hence neither can function symbols. Starting from \(\varphi \) over \(\varSigma =(\mathcal {F} _{\varSigma };\mathcal {P} _{\varSigma }^0)\) where only \(\mathcal {P} _{\varSigma }\) is assumed discrete, we compute an equi-satisfiable formula \(\psi \) over and we are back to the previous case.    \(\square \)

Theorem 38

(Full Trakhtenbrot). If \(\varSigma \) contains either an at least binary relation symbol or a unary relation symbol together with an at least binary function symbol, then \(\mathsf {BPCP} \) reduces to \(\mathsf {FSAT} (\varSigma )\).

Proof

By Theorems 14, 21 and 28, Lemma 29, and Fact 30.    \(\square \)

Corollary 39

For an enumerable and discrete signature \(\varSigma \) furthermore satisfying the conditions in Theorem 38, \(\mathsf {FSAT} (\varSigma )\) is both enumerable and undecidable, thus, more specifically, not co-enumerable.

Proof

Follows by Facts 3 and 5.    \(\square \)

Notice that even if the conditions on arities of Theorems 37 and 38 fully classify discrete signatures, it is not possible to decide which case holds unless the signature is furthermore finite. For a given formula \(\varphi \) though, it is always possible to render it in the finite signature of used symbols.

The main part of our Coq development directly concerned with the classification of finite satisfiability consists of 10k loc, in addition to 3k loc of (partly reused) utility libraries. Most of the code comprises the signature transformations with more than 4k loc for reducing discrete signatures to membership. Comparatively, the initial reduction from \(\mathsf {BPCP} \) to \(\mathsf {FSATEQ} (\varSigma _{\mathsf {BPCP}})\) takes less than 500 loc.

Our mechanisation of first-order logic in principle follows previous developments [8, 9] but also differs in a few aspects. Notably, we had to separate function from relation signatures to be able to express distinct signatures that agree on one sort of symbols computationally. Moreover, we found it favourable to abstract over the logical connectives in form of and to shorten purely structural definitions and proofs. Finally, we did not use the Autosubst 2 [20] support for de Bruijn syntax to avoid its current dependency on the functional extensionality axiom.

We refrained from additional axioms since we included our development in the growing Coq library of synthetic undecidability proofs [11]. In this context, we plan to generalise some of the intermediate signature reductions so that they become reusable for other undecidability proofs concerning first-order logic over arbitrary models.

As further future directions, we want to explore and mechanise the direct consequences of Trakhtenbrot’s theorem such as the undecidability of query containment and equivalence in data base theory or the undecidability of separation logic [3, 5]. Also possible, though rather ambitious, would be to mechanise the classification of first-order satisfiability with regards to the quantifier prefix as comprehensively developed in [1]. Finally, we plan to mechanise the undecidability of semantic entailment and syntactic deduction in first-order axiom systems such as ZF set theory and Peano arithmetic.