MODEL COMPLETIONS FOR UNIVERSAL CLASSES OF ALGEBRAS: NECESSARY AND SUFFICIENT CONDITIONS

Abstract

Necessary and sufficient conditions are presented for the (first-order) theory of a universal class of algebraic structures (algebras) to have a model completion, extending a characterization provided by Wheeler. For varieties of algebras that have equationally definable principal congruences and the compact intersection property, these conditions yield a more elegant characterization obtained (in a slightly more restricted setting) by Ghilardi and Zawadowski. Moreover, it is shown that under certain further assumptions on congruence lattices, the existence of a model completion implies that the variety has equationally definable principal congruences. This result is then used to provide necessary and sufficient conditions for the existence of a model completion for theories of Hamiltonian varieties of pointed residuated lattices, a broad family of varieties that includes lattice-ordered abelian groups and MV-algebras. Notably, if the theory of a Hamiltonian variety of pointed residuated lattices has a model completion, it must have equationally definable principal congruences. In particular, the theories of lattice-ordered abelian groups and MV-algebras do not have a model completion, as first proved by Glass and Pierce, and Lacava, respectively. Finally, it is shown that certain varieties of pointed residuated lattices generated by their linearly ordered members, including lattice-ordered abelian groups and MV-algebras, can be extended with a binary operation to obtain theories that do have a model completion.

1 Introduction

The main aim of this paper is to understand what it means in algebraic terms for the (first-order) theory of a universal class of algebraic structures (algebras) to have a model completion. For classes that have finite presentations—including all quasivarieties, but not, for example, ordered abelian groups—a complete characterization was provided by Wheeler in [38] (see also [39]) using the well-studied properties of amalgamation and coherence together with a more complicated property referred to as the conservative congruence extension property. However, as we show in Section 3, replacing coherence and the conservative congruence extension property with a variable projection property and conservative model extension property yields necessary and sufficient conditions for all universal classes of algebras (Theorem 3.2).

Although the mentioned properties can be used to confirm that the theories of ordered abelian groups and linearly ordered MV-algebras have a model completion [29, 36], the conservative model extension property is, in general, rather difficult to prove or refute. We therefore also provide, in Section 4, a more elegant characterization for varieties (equational classes) of algebras that have equationally definable principal congruences and the compact intersection property, where the conservative model extension property is replaced by a more amenable equational variable restriction property (Theorem 4.5). This result generalizes slightly a characterization given by Ghilardi and Zawadowski in [19] (see also [20]) by covering varieties such as lattice-ordered abelian groups for which there exists no equation that entails all other equations.

In Section 5, we prove that for any congruence distributive variety $\mathsf {V}$ that has both the congruence extension property and a “guarded” deduction theorem, if the theory of $\mathsf {V}$ has a model completion, then $\mathsf {V}$ has equationally definable principal congruences (Theorem 5.7). Our approach is inspired by the work of Glass and Pierce on lattice-ordered abelian groups in [22] and indeed yields both their result that the theory of this variety does not have a model completion, and the same result for MV-algebras, first proved by Lacava in [28]. More generally, in Section 6, we use this theorem to show that the theory of a Hamiltonian variety of pointed residuated lattices—spanning varieties of algebras for substructural logics as well as lattice-ordered abelian groups and MV-algebras (see, e.g., [5, 16, 31])—has a model completion if, and only if, the variety is coherent and has equationally definable principal congruences, the amalgamation property, and the equational variable restriction property (Theorem 6.6).

Finally, in Section 7, we associate with any variety $\mathsf {V}$ generated by a class of linearly ordered pointed residuated lattices, a variety $\mathsf {V_\rhd }$ of algebras with an additional binary operation that has equationally definable principal congruences and the same universal theory as $\mathsf {V}$ in the original language. We then show that if $\mathsf {V}$ satisfies a certain syntactic condition, the theory of $\mathsf {V_\rhd }$ has a model completion (Theorem 7.6). Notably, this is the case for lattice-ordered abelian groups and MV-algebras, the second case yielding an alternative proof of the fact that the theory of MV $_{\Delta }$ -algebras has a model completion, first announced by X. Caicedo at a conference in 2008.

2 Algebraic properties

Let us first recall some elementary material on universal algebra, referring to [7] for proofs and references. For convenience, we will assume throughout this paper that $\mathcal {L}$ is an algebraic language (i.e., a first-order language with no relation symbols) containing at least one constant symbol c and that an $\mathcal {L}$ -algebra $\mathbf{A}$ is an $\mathcal {L}$ -structure with universe A, calling $\mathbf{A}$ trivial if $|A| = 1$ . We denote by $\operatorname {{\textrm {Con}}}{\mathbf{A}}$ the congruence lattice of $\mathbf{A}$ , and by $\mathrm{Cg}_{{\mathbf{A}}}(S)$ the congruence of $\mathbf{A}$ generated by $S\subseteq A^2$ .

The term algebra $\textbf {Tm}_{\mathcal {L}}(\overline {x})$ for $\mathcal {L}$ over a set $\overline {x}$ is an $\mathcal {L}$ -algebra with universe $\textrm {Tm}_{\mathcal {L}}(\overline {x})$ consisting of $\mathcal {L}$ -terms with variables in $\overline {x}$ , such that for any $\mathcal {L}$ -algebra $\mathbf{A}$ and map $f\colon \overline {x}\to A$ , there exists a unique homomorphism $\tilde {f}\colon \textbf {Tm}_{\mathcal {L}}(\overline {x})\to \mathbf{A}$ extending f. Atomic $\mathcal {L}$ -formulas are $\mathcal {L}$ -equations, written $s \approx t$ , and $\mathcal {L}$ -equations and their negations are $\mathcal {L}$ -literals. Conjunctions, disjunctions, negations, implications, and bi-implications of $\mathcal {L}$ -formulas are built using the symbols $\mathbin {\&}$ , $\curlyvee $ , $\neg $ , $\to $ , and $\leftrightarrow $ , respectively, with $\top := c\approx c$ and $\bot := \neg \top $ . An $\mathcal {L}$ -quasiequation is an $\mathcal {L}$ -formula $\pi \to \varepsilon $ , where $\pi $ is a conjunction of $\mathcal {L}$ -equations and $\varepsilon $ is an $\mathcal {L}$ -equation, assuming that the empty conjunction is $\top $ . For an $\mathcal {L}$ -term t or $\mathcal {L}$ -formula $\alpha $ , we denote by $t(\overline {x})$ or $\alpha (\overline {x})$ that its free variables belong to the set $\overline {x}$ , and for a conjunction of $\mathcal {L}$ -literals $\xi $ , we write $\xi ^+$ and $\xi ^-$ for the conjunctions of $\mathcal {L}$ -equations occurring in $\xi $ positively and negatively, respectively.

Let $\mathbb {H}$ , $\mathbb {I}$ , $\mathbb {S}$ , $\mathbb {P}$ , and $\mathbb {P}_U$ denote the class operators of taking homomorphic images, isomorphic images, subalgebras, products, and ultraproducts, respectively. A class of $\mathcal {L}$ -algebras $\mathsf {K}$ is called a variety if it is closed under $\mathbb {H}$ , $\mathbb {S}$ , and $\mathbb {P}$ , and a quasivariety if is closed under $\mathbb {I}$ , $\mathbb {S}$ , $\mathbb {P}$ , and $\mathbb {P}_U$ . The class $\mathsf {K}$ is a variety if, and only if, it is an equational class, and a quasivariety if, and only if, it is a quasiequational class. Moreover, $\mathsf {K}$ is a universal class if, and only if, it is closed under $\mathbb {I}$ , $\mathbb {S}$ , and $\mathbb {P}_U$ , and a positive universal class if, and only if, it is closed under $\mathbb {H}$ , $\mathbb {S}$ , and $\mathbb {P}_U$ .

The variety and quasivariety generated by a class of $\mathcal {L}$ -algebras $\mathsf {K}$ are, respectively, the smallest variety $\mathbb {HSP}(\mathsf {K})$ and quasivariety $\mathbb {ISPP}_U(\mathsf {K})$ of $\mathcal {L}$ -algebras containing $\mathsf {K}$ . An $\mathcal {L}$ -equation is valid in $\mathsf {K}$ if, and only if, it is valid in $\mathbb {HSP}(\mathsf {K})$ , and an $\mathcal {L}$ -quasiequation is valid in $\mathsf {K}$ if, and only if, it is valid in $\mathbb {ISPP}_U(\mathsf {K})$ . For future reference, let us note also that any class of $\mathcal {L}$ -algebras $\mathsf {K}$ that is closed under taking finite products satisfies the following disjunction property: for any conjunctions of $\mathcal {L}$ -equations $\varphi ,\pi _1,\dots ,\pi _n$ ,

For a variety of $\mathcal {L}$ -algebras $\mathsf {V}$ , the $\mathsf {V}$ -free algebra $\mathbf{F}_{\mathsf {V}}(\overline {x})$ over a set $\overline {x}$ may be identified with the quotient $\textbf {Tm}_{\mathcal {L}}(\overline {x}) / \theta _{\mathsf {V}}(\overline {x})$ , where $\theta _{\mathsf {V}}(\overline {x}):= \bigcap \{\theta \in \operatorname {{\textrm {Con}}}{\textbf {Tm}_{\mathcal {L}}(\overline {x})} \mid \textbf {Tm}_{\mathcal {L}}(\overline {x}) / \theta \in \mathsf {V}\}$ . For any $\mathcal {L}$ -equation $\varepsilon \in \textrm {Tm}_{\mathcal {L}}(\overline {x})^2$ , we let $\widehat {\varepsilon }$ denote its image under the natural surjection $\textbf {Tm}_{\mathcal {L}}(\overline {x})^2\twoheadrightarrow \mathbf{F}_{\mathsf {V}}(\overline {x})^2$ . The following useful lemma shows that the valid $\mathcal {L}$ -quasiequations of $\mathsf {V}$ can be described in terms of congruences of $\mathsf {V}$ -free algebras.

Lemma 2.1 (cf. [30, Lemma 2])

For any variety of $\mathcal {L}$ -algebras $\mathsf {V}$ , conjunction of $\mathcal {L}$ -equations $\pi (\overline {x})$ , and $\mathcal {L}$ -equation $\varepsilon (\overline {x})$ ,

$$ \begin{align*} \mathsf{V}\models \pi\to \varepsilon \iff \widehat{\varepsilon}\in\mathrm{Cg}_{{\mathbf{F}_{\mathsf{V}}(\overline{x})}}(\{\widehat{\sigma}\mid \sigma \text{ is an equation of } \pi\}). \end{align*} $$

A variety $\mathsf {V}$ has the congruence extension property if for all $\mathbf{A}\in \mathsf {V}$ , any congruence of a subalgebra of $\mathbf{A}$ extends to a congruence of $\mathbf{A}$ . The following lemma provides a useful equivalent characterization of this property in terms of congruences of $\mathsf {V}$ -free algebras.

Lemma 2.2 (cf. [30, Lemma 17])

A variety $\mathsf {V}$ has the congruence extension property if, and only if, for any $\theta \in \operatorname {{\mathrm{Con}}}{\mathbf{F}_{\mathsf {V}}(\overline {x})}$ and $\theta '\in \operatorname {{\mathrm{Con}}}{\mathbf{F}_{\mathsf {V}}(\overline {x},\overline {y})}$ ,

$$ \begin{align*} (\theta'\vee\mathrm{Cg}_{{\mathbf{F}_{\mathsf{V}}(\overline{x},\overline{y})}}(\theta))\cap\mathrm{F}_{\mathsf{V}}(\overline{x})^2 = (\theta'\cap\mathrm{F}_{\mathsf{V}}(\overline{x})^2)\vee\theta. \end{align*} $$

In what follows, we will omit mention of the language $\mathcal {L}$ , assuming throughout that a class of algebras $\mathsf {K}$ is a class of $\mathcal {L}$ -algebras, and that terms, equations, formulas, etc. are defined over this language.

2.1 The variable projection property and coherence

Let us say that a class of algebras $\mathsf {K}$ has the variable projection property if for any finite set $\overline {x},y$ and conjunction of equations $\varphi (\overline {x},y)$ , there exists a quantifier-free formula $\xi (\overline {x})$ such that $\mathsf {K}\models \varphi \to \xi $ and for any equation $\varepsilon (\overline {x})$ ,

$$ \begin{align*} \mathsf{K}\models \varphi\to \varepsilon \:\Longrightarrow\:\mathsf{K}\models \xi\to\varepsilon. \end{align*} $$

If $\xi (\overline {x})$ is required to be a conjunction of equations for each $\varphi (\overline {x},y)$ , we say that $\mathsf {K}$ has the equational variable projection property.

Remark 2.3. Since $\mathsf {K}$ satisfies the same quasiequations as the quasivariety $\mathbb {ISPP}_U(\mathsf {K})$ that it generates, $\mathsf {K}$ has the equational variable projection property if, and only if, $\mathbb {ISPP}_U(\mathsf {K})$ has this property.

For varieties, the variable projection property is equivalent both to the equational variable projection property and to the widely studied algebraic property of coherence. A variety $\mathsf {V}$ is said to be coherent if every finitely generated subalgebra of a finitely presented member of $\mathsf {V}$ is finitely presented.

Proposition 2.4. The following statements are equivalent for any variety $\mathsf {V}$ :

1. (1) $\mathsf {V}$ is coherent.

2. (2) $\mathsf {V}$ has the equational variable projection property.

3. (3) $\mathsf {V}$ has the variable projection property.

Proof. The equivalence of (1) and (2) is established in [27, Theorem 2.3], and (3) is an immediate consequence of (2). To show that (3) implies (2), we fix a finite set $\overline {x},y$ and a conjunction of equations $\varphi (\overline {x},y)$ , and let $\xi (\overline {x})$ be a quantifier-free formula such that $\mathsf {V}\models \varphi \to \xi $ and for any equation $\varepsilon (\overline {x})$ , we have $\mathsf {V}\models \varphi \to \varepsilon \: \Longrightarrow \: \mathsf {V}\models \xi \to \varepsilon $ . Since $\varphi $ is satisfiable in $\mathsf {V}$ (e.g., in any trivial algebra), we can assume without loss of generality that $\xi =\xi _1\curlyvee \cdots \curlyvee \xi _m$ , where $\xi _1,\dots ,\xi _m$ are conjunctions of literals satisfiable in $\mathsf {V}$ .

Since $\mathsf {V}\models \varphi \to \xi $ , also . By the disjunction property for varieties, $\mathsf {V}\models \varphi \to \xi ^+_i$ for some $i\in \{1,\dots ,m\}$ . Let $\sigma _1,\dots ,\sigma _n$ be the equations of $\xi ^-_i$ and consider any equation $\varepsilon (\overline {x})$ such that $\mathsf {V}\models \varphi \to \varepsilon $ . By assumption, $\mathsf {V}\models \xi \to \varepsilon $ , so $\mathsf {V}\models \xi _i\to \varepsilon $ . Hence and, by the disjunction property for varieties, either $\mathsf {V}\models \xi ^+_i\to \varepsilon $ or $\mathsf {V}\models \xi _i\to \bot $ . But $\xi _i$ is satisfiable in $\mathsf {V}$ , so $\mathsf {V}\models \xi ^+_i\to \varepsilon $ .⊣

Following this last proposition, we will refer to a variety throughout this paper as coherent whenever it has the (equational) variable projection property.

Remark 2.5. An algebra $\mathbf{A}$ is locally finite if every finitely generated subalgebra of $\mathbf{A}$ is finite, and a class of algebras $\mathsf {K}$ is locally finite if each $\mathbf{A}\in \mathsf {K}$ is locally finite. Since any finitely presented algebra of a locally finite variety is finite and any finite algebra of a locally finite variety is finitely presented, every locally finite variety is coherent.

Below we introduce some well-known classes of algebras that will be employed as running examples throughout the paper. These algebras all possess definable binary operations $\wedge $ and $\vee $ such that $a \le b \: :\Longleftrightarrow \: a\wedge b = a$ defines a lattice order with binary meets and joins given by $\wedge $ and $\vee $ , respectively.

Example 2.6. Linear orders with endpoints may be considered as bounded lattices $\langle L,\wedge ,\vee ,0,1\rangle $ where the defined lattice order is linear. The class $\mathsf {DL^c}$ of linear orders with endpoints is then a positive universal class of algebras that generates the variety $\mathsf {DL}$ of bounded distributive lattices as a quasivariety. Since $\mathsf {DL}$ is locally finite, it is coherent, and, by Remark 2.3, the class $\mathsf {DL^c}$ has the equational variable projection property.

Example 2.7. A Heyting algebra is an algebra $\langle H,\wedge ,\vee ,\supset ,0,1\rangle $ such that the reduct $\langle H,\wedge ,\vee ,0,1 \rangle $ is a bounded distributive lattice and $\supset $ is the right residual of $\wedge $ ; that is, $a \le b\supset c$ if, and only if, $a \wedge b \le c$ for all $a,b,c\in H$ . The fact that the variety $\mathsf {HA}$ of Heyting algebras is coherent is a direct consequence of Pitts’ uniform interpolation theorem for intuitionistic propositional logic [35].

Example 2.8. A lattice-ordered abelian group is an algebra $\langle L,\wedge ,\vee ,+,-,0 \rangle $ such that $\langle L,+,-,0 \rangle $ is an abelian group, $\langle L,\wedge ,\vee \rangle $ is a lattice, and $a\leq b$ implies $a+c\leq b+c$ for all $a,b,c\in L$ . Lattice-ordered abelian groups form a variety $\mathsf {LA}$ that is coherent (see [27]) and generated as a quasivariety by the positive universal class $\mathsf {LA^c}$ of ordered abelian groups, i.e., the class of linearly ordered members of $\mathsf {LA}$ (see, e.g., [1]). It follows from Remark 2.3 that $\mathsf {LA^c}$ has the equational variable projection property.

Example 2.9. An MV-algebra is an algebra $\langle M,\oplus ,\lnot ,0\rangle $ satisfying the equations

$$ \begin{align*} {\begin{array}{rlc@{}rl} \textrm{(MV1)} & x\oplus(y\oplus z)\approx(x\oplus y)\oplus z, & & \textrm{(MV4)} & \lnot\lnot x\approx x,\\ \textrm{(MV2)} & x\oplus y\approx y\oplus x, & & \textrm{(MV5)} & x\oplus\lnot0 \approx\lnot 0,\\ \textrm{(MV3)} & x\oplus0\approx x, & & \textrm{(MV6)} & \lnot(\lnot x\oplus y)\oplus y\approx\lnot(\lnot y\oplus x)\oplus x. \end{array}} \end{align*} $$

The variety $\mathsf {MV}$ of MV-algebras is coherent (see [27]), and generated as a quasivariety by the positive universal class $\mathsf {MV^c}$ of MV-algebras that are linearly ordered with respect to the defined lattice operations $x\wedge y:=\lnot (\lnot x \oplus \lnot (\lnot x \oplus y))$ and $x\vee y:= \lnot (\lnot x \oplus y)\oplus y$ (see, e.g., [10]). Again, it follows from Remark 2.3 that $\mathsf {MV^c}$ has the equational variable projection property.

Notable varieties that are not coherent include the varieties of lattices, semigroups, groups, and modal algebras (see [27] for proofs and references).

2.2 The conservative model extension property

Let us say that a class of algebras $\mathsf {K}$ has the conservative model extension property if for any finite set $\overline {x},y$ and conjunction of literals $\psi (\overline {x},y)$ , there exists a quantifier-free formula $\chi (\overline {x})$ satisfying

1. (i) $\mathsf {K}\models \psi \to \chi $ and

2. (ii) for any $\mathbf{A} \in \mathsf {K}$ generated by $\overline {a}\in A^{\overline {x}}$ such that $\mathbf{A}\models \chi (\overline {a})$ and for any equation $\varepsilon (\overline {x})$ ,

   $$ \begin{align*} \mathsf{K}\models\psi^+\to\varepsilon \:\Longrightarrow\: \mathbf{A}\models\varepsilon(\overline{a}), \end{align*} $$
   there exist an algebra $\mathbf{B}\in \mathsf {K}$ extending $\mathbf{A}$ and $b \in B$ such that $\mathbf{B}\models \psi (\overline {a},b)$ .

Remark 2.10. In the previous definition, we may assume without loss of generality that $\psi $ is satisfiable in $\mathsf {K}$ . Just observe that if this is not the case, then $\mathsf {K}\models \psi \leftrightarrow \bot $ and we can let $\chi := \bot $ . Moreover, if there is precisely one definable constant in $\mathsf {K}$ (which is the case, e.g., for lattice-ordered abelian groups), we can assume that $\overline {x}$ is non-empty. To see this, suppose that $\overline {x}=\emptyset $ and let $\chi := \top $ . Then (i) is clearly satisfied and for (ii), any $\mathbf{A}\in \mathsf {K}$ generated by $\emptyset $ is trivial and satisfies all equations, so, since $\psi $ is satisfiable in $\mathsf {K}$ , we can choose an algebra $\mathbf{B}\in \mathsf {K}$ extending $\mathbf{A}$ and $b\in B$ such that $\mathbf{B}\models \psi (b)$ .

In the case where $\mathsf {K}$ is a universal class of algebras admitting finite presentations (in particular, any quasivariety), the conservative model extension property is implied by the conservative congruence extension property introduced by Wheeler in [38] (see Proposition 8.3). The following proposition, proved here for the sake of completeness, is then a direct consequence of [38, Corollary 1, p. 319].

Proposition 2.11. Every locally finite variety has the conservative model extension property.

Proof. Let $\mathsf {V}$ be a locally finite variety and consider a finite set $\overline {x},y$ and conjunction of literals $\psi (\overline {x},y)$ . We can assume that $\psi $ is satisfiable in $\mathsf {V}$ . Since $\mathsf {V}$ is locally finite, the finitely generated free algebra $\mathbf{F}_{\mathsf {V}}(\overline {x})$ is finite and has finitely many congruences $\theta _1,\dots ,\theta _m$ . For each $w\in \textrm {F}_{\mathsf {V}}(\overline {x})^2$ , choose an equation $\varepsilon _{w}$ such that $\widehat {\varepsilon }_w=w$ . Now, for each $j\in \{1,\dots ,m\}$ , let $\psi _j(\overline {x})$ be the conjunction of literals in the set $\{\varepsilon _{w}\mid w\in \theta _j\}\cup \{\neg \varepsilon _{w}\mid w\notin \theta _j\}$ . Then, for any algebra $\mathbf{A}\in \mathsf {V}$ generated by a tuple $\overline {a}\in A^{\overline {x}}$ , we have $\mathbf{A}\models \psi _j(\overline {a})$ if, and only if, the homomorphism $\mathbf{F}_{\mathsf {V}}(\overline {x})/\theta _j\to \mathbf{A}$ mapping $\overline {x}_j$ to $\overline {a}$ , where $\overline {x}_j$ is the image of the tuple $\overline {x}$ under the composite map $\textbf {Tm}(\overline {x})\twoheadrightarrow \mathbf{F}_{\mathsf {V}}(\overline {x})\twoheadrightarrow \mathbf{F}_{\mathsf {V}}(\overline {x})/\theta _j$ , is an isomorphism.

Let S be the set of all $j\in \{1,\dots ,m\}$ such that there exist $\mathbf{B}\in \mathsf {V}$ extending $\mathbf{F}_{\mathsf {V}}(\overline {x})/\theta _j$ and $b\in B$ satisfying $\mathbf{B}\models \psi (\overline {x}_j,b)$ . Since $\psi $ is satisfiable in $\mathsf {V}$ , there exist $\mathbf{B}\in \mathsf {V}$ and $(\overline {a},b)\in B^{\overline {x},y}$ such that $\mathbf{B}\models \psi (\overline {a},b)$ . The following claim then implies that $S\neq \emptyset $ .

Claim. Suppose that $\mathbf{B}\in \mathsf {V}$ and $\mathbf{B}\models \psi (\overline {a},b)$ for some $(\overline {a},b)\in B^{\overline {x},y}$ . Then there exist $j\in \{1,\dots ,m\}$ and an embedding $\mathbf{F}_{\mathsf {V}}(\overline {x})/\theta _j\hookrightarrow \mathbf{B}$ mapping $\overline {x}_j$ to $\overline {a}$ , and hence $j\in S$ .

Proof of Claim. By the homomorphism theorem for universal algebra (see, e.g., [7]), it suffices to observe that the image of the homomorphism $\mathbf{F}_{\mathsf {V}}(\overline {x})\to \mathbf{B}$ mapping the equivalence class of $\overline {x}$ to $\overline {a}$ is isomorphic to $\mathbf{F}_{\mathsf {V}}(\overline {x})/\theta _j$ for some $j\in \{1,\dots ,m\}$ . ⊣

We now prove that the quantifier-free formula

satisfies conditions (i) and (ii) in the definition of the conservative model extension property. For (i), we must show $\mathsf {V}\models \psi \to \chi $ . By the Claim, if $\mathbf{B}\in \mathsf {V}$ and $(\overline {a},b)\in B^{\overline {x},y}$ satisfy $\mathbf{B}\models \psi (\overline {a},b)$ , then there exist $j\in \{1,\dots ,m\}$ and an embedding $\mathbf{F}_{\mathsf {V}}(\overline {x})/\theta _j\hookrightarrow \mathbf{B}$ mapping $\overline {x}_j$ to $\overline {a}$ . So $\mathbf{B}\models \psi _j(\overline {a})$ , which implies $\mathbf{B}\models \chi (\overline {a})$ . For (ii), suppose that $\mathbf{A}\in \mathsf {V}$ is generated by a tuple $\overline {a}\in A^{\overline {x}}$ satisfying $\mathbf{A}\models \chi (\overline {a})$ . Let $k\in S$ be such that $\mathbf{A}\models \psi _k(\overline {a})$ , and recall that there is an isomorphism $\mathbf{F}_{\mathsf {V}}(\overline {x})/\theta _k\to \mathbf{A}$ mapping $\overline {x}_k$ to $\overline {a}$ . By the definition of S, there exist $\mathbf{B}\in \mathsf {V}$ extending $\mathbf{A}$ and $b\in B$ such that $\mathbf{B}\models \psi (\overline {a},b)$ . ⊣

Example 2.12. The class of ordered abelian groups $\mathsf {LA^c}$ has the conservative model extension property. Consider a finite set $\overline {x},y$ and a conjunction of literals $\psi (\overline {x},y)$ . We first assume that y appears in each literal of $\psi $ and then settle the general case. For any two terms $s,t$ , write $s<t$ for the formula $(s\leq t)\mathbin {\&} \neg (s\approx t)$ , where $\leq $ is the definable lattice order. In view of Remark 2.10, we can assume that $\overline {x}\neq \emptyset $ . Moreover, without loss of generality (because the members of $\mathsf {LA^c}$ are linearly ordered), we can assume that $\psi =\psi _1\curlyvee \cdots \curlyvee \psi _m$ and that each disjunct is a conjunction of formulas of the form

$$ \begin{align*} py\leq t,\: py\geq t, \: py< t, \: py> t, \end{align*} $$

where each t is a group term with variables in $\overline {x}=x_1,\dots ,x_n$ , and p is a fixed non-zero natural number (e.g., the least common multiple of the coefficients of y in the conjuncts). Let $t_{j_1}(\overline {x}),\dots ,t_{j_u}(\overline {x})$ be the terms appearing in $\psi _j$ and let $\chi (\overline {x})$ be the formula

Clearly, $\mathsf {LA^c}\models \psi \to \chi $ , so condition (i) of the conservative model extension property is satisfied. For (ii), consider $\mathbf{A}\in \mathsf {LA^c}$ together with a tuple $\overline {a}\in A^{\overline {x}}$ such that $\mathbf{A}\models \chi (\overline {a})$ . If $\mathbf{A}$ is the one-element group and there is no $\mathbf{B}\in \mathsf {LA^c}$ satisfying (ii), then

. So

by the definition of $\chi $ , contradicting the fact that $\mathbf{A}\models \chi (\overline {a})$ . If $\mathbf{A}$ is non-trivial, let $\mathbf{B}$ be the divisible hull of $\mathbf{A}$ and note that $\mathbf{B}$ is an infinite member of $\mathsf {LA^c}$ . We claim that there is a $b\in B$ such that $\mathbf{B}\models \psi (\overline {a},b)$ . If no such b exists, then, for each $1\leq j\leq m$ , a pair of inequations $t_{j_i}(\overline {a}){\vartriangle } py$ and $py{\vartriangle } t_{j_k}(\overline {a})$ of $\psi _j(\overline {a},y)$ is unsatisfiable, for ${\vartriangle }\in \{<,\leq \}$ . We settle the case where all these inequations are of the form $t_{j_i}(\overline {a})< py$ and $py< t_{j_k}(\overline {a})$ , the other cases being very similar. Since $\mathbf{B}$ is divisible and every divisible ordered abelian group is densely ordered, we get $t_{j_k}(\overline {a})\leq t_{j_i}(\overline {a})$ . Moreover, $t_{j_i}<py$ and $py< t_{j_k}$ entail $t_{j_i}<t_{j_k}$ , and hence

. But then $\mathbf{A}\models \chi (\overline {a})$ implies $t_{j_i}(\overline {a})<t_{j_k}(\overline {a})$ for some $1\leq j\leq m$ , a contradiction.

Finally, if we have a conjunction of literals of the form $\psi (\overline {x},y)\mathbin {\&} \psi '(\overline {x})$ , where $\psi '$ is any conjunction of literals, the quantifier-free formula $\chi \mathbin {\&} \psi '$ satisfies the conditions for the conservative model extension property.

Example 2.13. The positive universal class $\mathsf {DL^c}$ of linear orders with endpoints, in the language of bounded lattices, has the conservative model extension property. Consider a finite set $\overline {x},y$ and a conjunction of literals $\psi (\overline {x},y)$ satisfiable in $\mathsf {DL^c}$ . Suppose that $\overline {x}=\emptyset $ . If there is a non-trivial member of $\mathsf {DL^c}$ satisfying $\psi $ , then the formula $\chi := \neg (0\approx 1)$ satisfies the conditions for the conservative model extension property. On the other hand, if $\psi $ is satisfied only by the trivial algebra, we can set $\chi := 0\approx 1$ .

Hence, let $\overline {x}\neq \emptyset $ . We assume that y appears in all literals of $\psi $ ; the general case then follows by reasoning as in Example 2.12. Since the members of $\mathsf {DL^c}$ are linearly ordered, $\psi $ is equivalent to a formula $\psi _1\curlyvee \cdots \curlyvee \psi _m$ , where each $\psi _j$ is a conjunction of formulas of the form $y\leq x$ , $y\geq x$ , $ y< x$ , or $y> x$ with $x\in \overline {x}=x_1,\dots ,x_n$ .

Assume first that the trivial algebra satisfies $\psi $ and let $\chi (\overline {x})$ be the formula

Reasoning as in Example 2.12, it is not difficult to see that $\chi $ satisfies the conditions for the conservative model extension property. Just replace the divisible hull of an ordered abelian group with any dense linear order with endpoints that extends the given linear order with endpoints $\mathbf{A}\in \mathsf {DL^c}$ (e.g., there is an embedding of $\mathbf{A}$ into the lexicographic product of $\mathbf{A}$ and $[0,1]$ which preserves the bounds).

In the case where $\psi $ is not satisfied in the trivial algebra, we replace $\chi $ by $\chi \mathbin {\&} \neg (0\approx 1)$ .

3 Model completions

Let us first recall some relevant model-theoretic notions, referring to [9, Section 3.5] for further details. By a theory we will always mean a first-order theory, i.e., a set of sentences over some first-order language $\mathcal {L}$ . We let $\textrm {Th}(\mathsf {K})$ denote the theory of a class $\mathsf {K}$ of $\mathcal {L}$ -structures, i.e., the set of $\mathcal {L}$ -sentences that are satisfied by all members of $\mathsf {K}$ . Two theories T and $T'$ are called co-theories if they entail the same universal sentences. Semantically, $T'$ is a co-theory of T if, and only if, every model of T embeds into a model of $T'$ and vice versa. A theory $T^*$ is model complete if every formula is equivalent over $T^*$ to an existential formula; that is, model complete theories are those in which alternations of quantifiers can be eliminated. Semantically, a theory $T^*$ is model complete if, and only if, every embedding between models of $T^*$ is elementary. A theory $T^*$ is a model companion of a theory T if it is a model complete co-theory of T. A model completion of a theory T is a model companion $T^*$ of T such that for any model M of T, the theory of $T^*$ together with the diagram of M is complete.

Let us also recall that a class $\mathsf {K}$ of $\mathcal {L}$ -structures has the amalgamation property if given any $\mathbf{A},\mathbf{B},\textbf {C}\in \mathsf {K}$ and embeddings $f\colon \mathbf{A}\to \mathbf{B}$ and $g\colon \mathbf{A}\to \textbf {C}$ , there exist $\textbf {D}\in \mathsf {K}$ and embeddings $h\colon \mathbf{B}\to \textbf {D}$ and $k\colon \textbf {C}\to \textbf {D}$ satisfying $hf = kg$ .

Below, we collect some useful facts related to model completions.

Proposition 3.1 (cf. [9, Propositions 3.5.13, 3.5.15, 3.5.18, and 3.5.19])

1. (a) A theory has at most one model companion up to logical equivalence.

2. (b) If a $\forall \exists $ -theory T has a model companion $T^*$ , then $T^*$ is logically equivalent to the theory of the existentially closed models of T.

3. (c) If $T^*$ is a model companion of a theory T, then $T^*$ is a model completion of T if, and only if, the class of models of T has the amalgamation property.

4. (d) A theory $T^*$ is a model completion of a universal theory T if, and only if, $T^*$ is a co-theory of T that admits quantifier elimination.

Our aim in this section is to prove the following characterization of universal classes of algebras whose theories have a model completion.

Theorem 3.2. Let $\mathsf {K}$ be a universal class of algebras. The theory of $\mathsf {K}$ has a model completion if, and only if, $\mathsf {K}$ has the amalgamation property, variable projection property, and conservative model extension property.

For universal classes of algebras with finite presentations, Theorem 3.2 specializes to [38, Theorem 5] (see Section 8). Observe also that for locally finite varieties, Remark 2.5 and Proposition 2.11 yield the following simpler characterization.

Corollary 3.3 [38, Corollary 1, p. 319]

Let $\mathsf {V}$ be a locally finite variety. Then the theory of $\mathsf {V}$ has a model completion if, and only if, $\mathsf {V}$ has the amalgamation property.

We first settle the “if” part of Theorem 3.2.

Proposition 3.4. Let $\mathsf {K}$ be a universal class of algebras. If $\mathsf {K}$ has the amalgamation property, variable projection property, and conservative model extension property, then the theory of $\mathsf {K}$ has a model completion.

Proof. Fix a countably infinite set of variables $\overline {z}$ and let

$$ \begin{align*} J := \{(\psi,y) \mid \psi \text{ is a conjunction of literals with variables in } \overline{z}, \text{ and } y \in \overline{z}\}. \end{align*} $$

Consider $j = (\psi ,y) \in J$ . Let $\overline {x}$ be the set of variables occurring in $\psi $ different from y. Since $\mathsf {K}$ has the variable projection property, there exists a quantifier-free formula $\xi _j(\overline {x})$ such that $\mathsf {K}\models \psi ^+\to \xi _j$ and for every equation $\varepsilon (\overline {x})$ ,

(1) $$ \begin{align} \mathsf{K}\models \psi^+\to \varepsilon \:\Longrightarrow\: \mathsf{K}\models \xi_j\to \varepsilon. \end{align} $$

Since $\mathsf {K}$ has the conservative model extension property, there also exists a quantifier-free formula $\chi _j(\overline {x})$ satisfying the following conditions:

1. (i) $\mathsf {K}\models \psi \to \chi _j$ and

2. (ii) for any $\mathbf{A} \in \mathsf {K}$ generated by $\overline {a}\in A^{\overline {x}}$ such that $\mathbf{A}\models \chi _j(\overline {a})$ and for any equation $\varepsilon (\overline {x})$ ,

   $$ \begin{align*} \mathsf{K}\models\psi^+\to\varepsilon \:\Longrightarrow\: \mathbf{A}\models\varepsilon(\overline{a}), \end{align*} $$
   there exist an algebra $\mathbf{B}\in \mathsf {K}$ extending $\mathbf{A}$ and $b \in B$ such that $\mathbf{B}\models \psi (\overline {a},b)$ .

We define the first-order sentence

$$ \begin{align*} \tau_j:=\forall\overline{x} \, [(\xi_j\mathbin{\&} \chi_j) \to \exists y.\psi]. \end{align*} $$

Let $T:= \textrm {Th}(\mathsf {K})$ be the theory of $\mathsf {K}$ and set $T^* := T \cup \{\tau _j \mid j \in J\}$ . We claim that $T^*$ is a model completion of T. In view of Proposition 3.1(d), it suffices to show that $T^*$ has quantifier elimination and is a co-theory of T.

$T^*$ has quantifier elimination. We prove that for any $ (\psi ,y) \in J$ ,

(2) $$ \begin{align} T \vdash \forall \overline{x} \, [(\exists y.\psi )\to (\xi_j\mathbin{\&} \chi_j)]. \end{align} $$

It follows then from the definition of $T^*$ and (2) that $T^*$ entails that any formula $\exists y.\psi $ , where $\psi $ is a conjunction of literals with variables in $\overline {z}$ and $y\in \overline {z}$ , is equivalent to a quantifier-free formula. So $T^*$ has quantifier elimination (see, e.g., [37, Lemma 3.2.4]).

For the proof of (2), fix an arbitrary $j = (\psi ,y) \in J$ . It suffices to show that for any algebra $\mathbf{A}\in \mathsf {K}$ and map $g \colon \overline {x} \to A$ ,

$$ \begin{align*} \mathbf{A}, g \models \exists y. \psi \:\Longrightarrow\: \mathbf{A}, g \models \xi_j\mathbin{\&} \chi_j. \end{align*} $$

Suppose that $\mathbf{A}, g \models \exists y. \psi $ . Then $\mathbf{A}, f \models \psi $ for some map $f \colon \overline {x},y \to A$ extending g. Moreover, since $\mathsf {K}\models \psi ^+\to \xi _j$ and $\mathsf {K}\models \psi \to \chi _j$ , it follows that $\mathbf{A}, f \models \xi _j$ and $\mathbf{A}, f\models \chi _j$ . But $\xi _j$ and $\chi _j$ have variables in $\overline {x}$ , so $\mathbf{A}, g\models \xi _j$ and $\mathbf{A}, g\models \chi _j$ , yielding $\mathbf{A}, g \models \xi _j\mathbin {\&} \chi _j$ .

$T^*$ is a co-theory of T. Since $T \subseteq T^*$ , it suffices to show that any universal sentence entailed by $T^*$ is entailed by T. First we show that for any $j = (\psi ,y) \in J$ , algebra $\mathbf{A}\in \mathsf {K}$ , and map $g \colon \overline {x} \to A$ ,

(3) $$ \begin{align} \mathbf{A}, g \models \xi_j\mathbin{\&} \chi_j \:\Longrightarrow\: \text{there exist } \mathbf{B}\in \mathsf{K} \text{ and }\iota \colon \mathbf{A} \hookrightarrow \mathbf{B} \text{ such that } \mathbf{B}, \iota g \models \exists y. \psi. \end{align} $$

Suppose that $\mathbf{A}, g \models \xi _j\mathbin {\&} \chi _j$ . We will assume first that the unique homomorphism $\tilde {g} \colon \textbf {Tm}(\overline {x}) \to \mathbf{A}$ extending g is surjective, and hence that $\mathbf{A}$ is generated by the image $\overline {a}$ of $\overline {x}$ under g. Note that $\mathbf{A} \models \chi _j(\overline {a})$ . Moreover, if $\varepsilon (\overline {x})$ is any equation such that $\mathsf {K}\models \psi ^+\to \varepsilon $ , then (1) yields $\mathsf {K}\models \xi _j\to \varepsilon $ and, since $\mathbf{A} \models \xi _j(\overline {a})$ , also $\mathbf{A}\models \varepsilon (\overline {a})$ . Hence, by (ii), there exist an algebra $\mathbf{B}$ in $\mathsf {K}$ extending $\mathbf{A}$ and $b\in B$ such that $\mathbf{B} \models \psi (\overline {a},b)$ . So $\mathbf{B}, \iota g \models \exists y. \psi $ , where $\iota \colon \mathbf{A}\hookrightarrow \mathbf{B}$ is the inclusion map.

For the general case of (3), let $\mathbf{A}'$ be the image of $\textbf {Tm}(\overline {x})$ under $\tilde {g}$ in $\mathbf{A}$ . Since $\mathsf {K}$ is a universal class and $\mathbf{A}'$ embeds into $\mathbf{A}$ , also $\mathbf{A}'\in \mathsf {K}$ . By the previous argument, there exist $\mathbf{B}'\in \mathsf {K}$ and $\iota ' \colon \mathbf{A}' \hookrightarrow \mathbf{B}'$ such that $\mathbf{B}', \iota 'g \models \exists y. \psi $ , witnessed by $b \in B'$ , say. Since $\mathsf {K}$ has the amalgamation property, we obtain for the injection $\iota '$ and the inclusion $\mathbf{A}' \hookrightarrow \mathbf{A}$ , an extension $\iota \colon \mathbf{A} \hookrightarrow \mathbf{B}$ with $\mathbf{B}\in \mathsf {K}$ and an embedding $\lambda \colon \mathbf{B}' \hookrightarrow \mathbf{B}$ such that the following diagram commutes:

Since $\psi $ is quantifier-free, we have $\mathbf{B}, \iota g \models \exists y. \psi $ witnessed by $\lambda (b)$ .

To conclude the proof, let $\alpha $ be a universal sentence such that $T^* \vdash \alpha $ . By the compactness theorem of first-order logic, there exists a finite subset $F \subseteq J$ such that $T \cup \{\tau _j \mid j \in F\} \vdash \alpha $ . We prove that, in fact, $T \vdash \alpha $ . Consider any $\mathbf{A}\in \mathsf {K}$ . Let $\overline {w}$ be the set of variables appearing in the scope of the universal quantifier in one of the sentences $\{\tau _j \mid j \in F\}$ and let $g \colon \overline {w} \to A$ be any map. By repeatedly applying (3), we obtain $\mathbf{B}\in \mathsf {K}$ and $\iota \colon \mathbf{A} \hookrightarrow \mathbf{B}$ such that $\mathbf{B}, \iota g \models \tau _j$ for each $j \in F$ . Now, since $T \cup \{\tau _j \mid j \in F\} \vdash \alpha $ , we have $\mathbf{B}, \iota g \models \alpha $ . But $\mathbf{A}$ is a subalgebra of $\mathbf{B}$ and $\alpha $ is universal, so $\mathbf{A}, g\models \alpha $ . Hence $T \vdash \alpha $ as required.⊣

Example 3.5. The positive universal class $\mathsf {LA^c}$ of ordered abelian groups, defined over the algebraic language with operation symbols $\wedge ,\vee ,+,-,0$ , has the amalgamation property [34], variable projection property (see Example 2.8), and conservative model extension property (see Example 2.12). Hence Proposition 3.4 yields the well-known fact that the theory of $\mathsf {LA^c}$ has a model completion [36]. ¹ Similarly, the class $\mathsf {MV^c}$ of linearly ordered MV-algebras satisfies the conditions of Proposition 3.4 and its theory therefore has a model completion [29].

Example 3.6. The positive universal class $\mathsf {DL^c}$ of linear orders with endpoints, defined over the algebraic language of bounded lattices, has the amalgamation property, variable projection property (see Example 2.6), and conservative model extension property (see Example 2.13). Hence Proposition 3.4 yields the well-known fact that the theory of $\mathsf {DL^c}$ has a model completion (see, e.g., [9]). It also follows easily that the theory of the positive universal class $\mathsf {HA^c}$ of linearly ordered Heyting algebras has a model completion. Note that any linear order with endpoints $\mathbf{A}\in \mathsf {DL^c}$ can be expanded to a linearly ordered Heyting algebra by defining $a \supset b := 1$ if $a \le b$ and $a \supset b := b$ otherwise. Indeed, the theory of $\mathsf {HA^c}$ is a definitional extension of the theory of $\mathsf {DL^c}$ (in the sense of, e.g., [24]), where the binary function symbol $\supset $ is defined by the formula

$$ \begin{align*} \xi(x,y,z):= (x\leq y \mathbin{\&} z\approx 1) \, \curlyvee \, (y<x \mathbin{\&} z\approx y). \end{align*} $$

Using the fact that $\xi $ is quantifier-free, the existence of a model completion for the theory of $\mathsf {HA^c}$ follows directly from the existence of a model completion for the theory of $\mathsf {DL^c}$ .

We now prove the “only if” part of Theorem 3.2. Note first that if $\mathsf {K}$ is a universal class of algebras whose theory has a model completion, then $\mathsf {K}$ has the amalgamation property by Proposition 3.1(c). Next, we consider the variable projection property.

Proposition 3.7. Let $\mathsf {K}$ be a universal class of algebras. If the theory of $\mathsf {K}$ has a model completion, then $\mathsf {K}$ has the variable projection property.

Proof. Let $T:= \textrm {Th}(\mathsf {K})$ be the theory of $\mathsf {K}$ , and let $T^*$ be a model completion of T. Fix a finite set $\overline {x},y$ and conjunction of equations $\varphi (\overline {x},y)$ . Since $T^*$ has quantifier elimination, there exists a quantifier-free formula $\xi (\overline {x})$ such that

(4) $$ \begin{align} T^*\vdash \forall \overline{x} \, [(\exists y.\varphi)\leftrightarrow \xi]. \end{align} $$

It follows from (4) that $T^*\vdash \forall \overline {x},y \, (\varphi \to \xi )$ and, since T and $T^*$ have the same universal consequences, $T\vdash \forall \overline {x},y \, (\varphi \to \xi )$ . That is, $\mathsf {K}\models \varphi \to \xi $ . It remains to show that for any equation $\varepsilon (\overline {x})$ satisfying $\mathsf {K}\models \varphi \to \varepsilon $ , also $\mathsf {K}\models \xi \to \varepsilon $ . ²

Suppose that $\mathsf {K}\not \models \xi \to \varepsilon $ . Then there is an algebra $\mathbf{A}$ in $\mathsf {K}$ and a tuple $\overline {a}\in A^{\overline {x}}$ such that $\mathbf{A}\models \xi (\overline {a})$ and $\mathbf{A}\not \models \varepsilon (\overline {a})$ . Since T and $T^*$ are co-theories and T is universal, there exists a model $\mathbf{B}$ of $T^*$ extending $\mathbf{A}$ such that $\mathbf{B}\in \mathsf {K}$ . Moreover, $\mathbf{A}\models \xi (\overline {a})$ implies $\mathbf{B}\models \xi (\overline {a})$ , and hence $\mathbf{B}\models \exists y. \varphi (\overline {a},y)$ by (4). Pick $b\in B$ such that $\mathbf{B}\models \varphi (\overline {a},b)$ . Since $\mathbf{A}\not \models \varepsilon (\overline {a})$ , we get $\mathbf{B}\not \models \varepsilon (\overline {a})$ . Hence $\mathsf {K}\not \models \varphi \to \varepsilon $ as required.

To complete the proof of Theorem 3.2, it remains to prove that whenever the theory of a universal class of algebras has a model completion, this class has the conservative model extension property. In fact, we will show below that the existence of a model completion is equivalent to a stronger property that directly implies the conservative model extension property. This stronger property is difficult to check in concrete cases, but will be useful in Section 5 for establishing consequences of the existence of a model completion for the definability of principal congruences.

Proposition 3.8. Let $\mathsf {K}$ be a universal class of algebras. The theory of $\mathsf {K}$ has a model completion if, and only if, for any finite sets $\overline {x},\overline {y}$ and conjunction of literals $\psi (\overline {x},\overline {y})$ , there is a quantifier-free formula $\chi (\overline {x})$ satisfying the following conditions:

1. (i) $\mathsf {K}\models \psi \to \chi $ and

2. (ii) for any $\mathbf{A}\in \mathsf {K}$ and tuple $\overline {a}\in A^{\overline {x}}$ satisfying $\mathbf{A}\models \chi (\overline {a})$ , there exist $\mathbf{B}\in \mathsf {K}$ extending $\mathbf{A}$ and $\overline {b} \in B^{\overline {y}}$ such that $\mathbf{B}\models \psi (\overline {a},\overline {b})$ .

In particular, if the theory of $\mathsf {K}$ has a model completion, then $\mathsf {K}$ has the conservative model extension property.

Proof. Let $T:= \textrm {Th}(\mathsf {K})$ be the theory of $\mathsf {K}$ , and suppose that $T^*$ is a model completion of T. Fix finite sets $\overline {x},\overline {y}$ and a conjunction of literals $\psi (\overline {x},\overline {y})$ . Since $T^*$ admits quantifier elimination, there exists a quantifier-free formula $\chi (\overline {x})$ such that

(5) $$ \begin{align} T^*\vdash \forall \overline{x} \, [(\exists \overline{y}.\psi)\leftrightarrow \chi]. \end{align} $$

It follows that $T^*\vdash \forall \overline {x},\overline {y} \, (\psi \to \chi )$ , and since T and $T^*$ are co-theories,

(6) $$ \begin{align} T\vdash \forall \overline{x},\overline{y} \, (\psi\to \chi). \end{align} $$

We show now that $\chi $ satisfies (i) and (ii).

Condition (i) is an immediate consequence of (6). For (ii), fix an algebra $\mathbf{A}\in \mathsf {K}$ and a tuple $\overline {a}\in A^{\overline {x}}$ such that $\mathbf{A}\models \chi (\overline {a})$ . Since T and $T^*$ are co-theories and T is universal, there exists a model $\mathbf{B} \in \mathsf {K}$ of $T^*$ that extends $\mathbf{A}$ . Since $\mathbf{B}\models \chi (\overline {a})$ , it follows by (5) that there is a tuple $\overline {b}\in B^{\overline {y}}$ such that $\mathbf{B}\models \psi (\overline {a},\overline {b})$ . This settles (ii).

For the converse direction, we only sketch the proof, as it is an easy modification of the proof of Proposition 3.4. As before, we consider the theory $T^* := T \cup \{\tau _j \mid j \in J\}$ , but in this case $\tau _j$ is defined as $\forall \overline {x} \, (\chi _j \to \exists y.\psi )$ , where the quantifier-free formula $\chi _j$ satisfies (i) and (ii). To show that $T^*$ has quantifier elimination, it suffices to show that $T \vdash \forall \overline {x} \, (\exists y.\psi \to \chi _j)$ for all $j=(\psi ,y) \in J$ , which follows by (i) (cf. the proof of Proposition 3.4). On the other hand, (ii) yields the following property similar to (3): if $\mathbf{A}, g \models \chi _j$ , then there exist $\mathbf{B}\in \mathsf {K}$ and $\iota \colon \mathbf{A} \hookrightarrow \mathbf{B}$ such that $\mathbf{B}, \iota g \models \exists y. \psi $ . Reasoning as in the last part of the proof of Proposition 3.4, we conclude that T and $T^*$ are co-theories. It follows then by Proposition 3.1(d) that $T^*$ is a model completion of T.⊣

Remark 3.9. The first part of Proposition 3.8 admits the following reformulation. Let $\mathsf {K}$ be a universal class of algebras and let $T:= \textrm {Th}(\mathsf {K})$ be its first-order theory. Then the following statements are equivalent:

1. (1) T has a model completion.

2. (2) For any finite sets $\overline {x},\overline {y}$ and conjunction of literals $\psi (\overline {x},\overline {y})$ , there is a quantifier-free formula $\chi (\overline {x})$ with the same universal consequences, with respect to T, as $\exists \overline {y}.\psi $ .

This equivalence was established (for arbitrary first-order languages) by Millar in [32, Theorem 3.1] (see also [9, Theorem 3.5.20] for a related result) and has recently been considered in the context of the verification of data-aware processes [8, Theorem 3.2].

4 Compact congruences

In this section, we show that for varieties of algebras satisfying certain congruence lattice conditions, the rather complicated conservative model extension property appearing in Theorem 3.2 can be replaced by a more amenable equational variable restriction property. The resulting characterization is a slightly more general version of a theorem proved by Ghilardi and Zawadowski in [19, Theorem 4].

Recall that the compact (equivalently, finitely generated) congruences of an algebra $\mathbf{A}$ ordered by set-theoretic inclusion always form a join-semilattice. A class of algebras $\mathsf {K}$ is said to have the compact intersection property if the join-semilattice of compact congruences of each $\mathbf{A}\in \mathsf {K}$ forms a lattice, i.e., the intersection of any two compact congruences of $\mathbf{A}$ is compact. Recall also that $\mathsf {K}$ is said to be congruence distributive if the congruence lattice of each $\mathbf{A}\in \mathsf {K}$ is distributive. The following lemma describes a useful syntactic consequence of these two properties.

Lemma 4.1. Let $\mathsf {V}$ be a congruence distributive variety that has the compact intersection property. For any finite set $\overline {x}$ and conjunctions of equations $\varphi _1(\overline {x}),\varphi _2(\overline {x})$ , there exists a conjunction of equations $\pi (\overline {x})$ such that for any equation $\varepsilon (\overline {x},\overline {y})$ ,

$$ \begin{align*} \mathsf{V}\models (\varphi_1\curlyvee \varphi_2)\to\varepsilon\iff\mathsf{V}\models \pi\to \varepsilon. \end{align*} $$

Proof. Let $\overline {x}$ be any finite set and let $\varphi _1(\overline {x}),\varphi _2(\overline {x})$ be conjunctions of equations. We fix $\overline {z}$ to be any countably infinite set with $\overline {x}\cap \overline {z}=\emptyset $ and define $\theta _i:= \textrm { Cg}_{{\mathbf{F}_{\mathsf {V}}(\overline {x},\overline {z})}}(\{\widehat {\sigma }\mid \sigma \text { is an equation of } \varphi _i\})$ for $i\in \{1,2\}$ . Since $\theta _1$ and $\theta _2$ are compact, so, by assumption, is their intersection; that is, there exist a finite set $\overline {w}\subseteq \overline {z}$ and equations $\sigma _1(\overline {x},\overline {w}),\dots ,\sigma _n(\overline {x},\overline {w})$ such that $\{\widehat {\sigma }_1,\dots ,\widehat {\sigma }_n\}$ generates $\theta _1\cap \theta _2$ . Let $f\colon \overline {x},\overline {z}\to \textrm {F}_{\mathsf {V}}(\overline {x},\overline {z})$ be a map sending each $x\in \overline {x}$ to x and each $w\in \overline {w}$ to some $u\in \textrm {F}_{\mathsf {V}}(\overline {x})$ , such that the image of f contains $\overline {x},\overline {z}$ . Clearly, the unique homomorphism $g\colon \mathbf{F}_{\mathsf {V}}(\overline {x},\overline {z})\to \mathbf{F}_{\mathsf {V}}(\overline {x},\overline {z})$ extending f is surjective. Define $g^*\colon \operatorname {{\textrm {Con}}}{\mathbf{F}_{\mathsf {V}}(\overline {x},\overline {z})}\to \operatorname {{\textrm {Con}}}{\mathbf{F}_{\mathsf {V}}(\overline {x},\overline {z})}$ by $g^*(\theta ):=\mathrm{Cg}_{{\mathbf{F}_{\mathsf {V}}(\overline {x},\overline {z})}}(\{(g(a),g(b)) \mid (a,b)\in \theta \})$ . Since $\mathsf {V}$ is congruence distributive and g is surjective, $g^*$ is a lattice homomorphism (cf. [2, Lemma 1.11]) and, in particular, $g^*(\theta _1\cap \theta _2)=g^*(\theta _1)\cap g^*(\theta _2)=\theta _1\cap \theta _2$ . Hence also $\{g(\widehat {\sigma }_1),\dots ,g(\widehat {\sigma }_n)\}$ generates $\theta _1\cap \theta _2$ , where $g(\widehat {\sigma }_j):= (g(s),g(t))$ for each $\widehat {\sigma }_j=(s,t)$ , and we let $\pi (\overline {x})$ be the conjunction of the equations $\sigma _1(\overline {x},u,\dots ,u),\dots ,\sigma _n(\overline {x},u,\dots ,u)$ .

For any equation $\varepsilon (\overline {x},\overline {y})$ , we may assume without loss of generality that $\overline {y}\subseteq \overline {z}$ and use Lemma 2.1 to obtain

$$ \begin{align*} \mathsf{V}\models (\varphi_1\curlyvee \varphi_2)\to \varepsilon &\iff\mathsf{V}\models \varphi_1\to\varepsilon\:\text{ and }\:\mathsf{V}\models \varphi_2\to \varepsilon\\ &\iff\widehat{\varepsilon}\in\theta_1\:\text{ and }\:\widehat{\varepsilon}\in\theta_2\\ &\iff\widehat{\varepsilon}\in\theta_1\cap \theta_2\\ &\iff\mathsf{V}\models\pi\to\varepsilon. & \\[-32pt]\end{align*} $$

⊣

Remark 4.2. The previous lemma can also be deduced from the fact that a variety is congruence distributive and has the compact intersection property if, and only if, it has equationally definable principal meets (cf. [4, Theorem 1.5]).

Recall next that a class of algebras $\mathsf {K}$ has first-order definable principal congruences if there exists a formula $\alpha (x_1,x_2,y_1,y_2)$ satisfying for all $\mathbf{A}\in \mathsf {K}$ and $a_1,a_2,b_1,b_2\in A$ ,

$$ \begin{align*} (a_1,a_2)\in\mathrm{Cg}_{{\mathbf{A}}}(b_1,b_2) \iff \mathbf{A}\models \alpha(a_1,a_2,b_1,b_2), \end{align*} $$

where $\mathrm{Cg}_{{\mathbf{A}}}(b_1,b_2):=\mathrm{Cg}_{{\mathbf{A}}}(\{(b_1,b_2)\})$ is the smallest congruence of $\mathbf{A}$ containing the pair $(b_1,b_2)$ . If $\alpha $ can be chosen to be a quantifier-free formula or conjunction of equations, then $\mathsf {K}$ is said to have, respectively, quantifier-free definable principal congruences or equationally definable principal congruences. For a variety $\mathsf {V}$ , it is known that having equationally definable principal congruences corresponds to a property of the associated consequence relation of $\,\mathsf {V}$ (often referred to as a deduction theorem) and a property of the join-semilattices of compact congruences of members of $\mathsf {V}$ .

Proposition 4.3 [26, Theorems 5 and 8], [3, Theorem 1.7]

The following statements are equivalent for any variety $\mathsf {V}$ :

1. (1) $\mathsf {V}$ has equationally definable principal congruences.

2. (2) There exists a conjunction of equations $\varphi (x_1,x_2,y_1,y_2)$ such that for any terms $s_1,s_2,t_1,t_2$ and conjunction of equations $\pi $ ,

   $$ \begin{align*} \mathsf{V} \models (\pi \mathbin{\&} (s_1\approx s_2)) \to (t_1 \approx t_2) \iff \mathsf{V} \models \pi \to \varphi(s_1,s_2,t_1,t_2). \end{align*} $$

3. (3) The join-semilattice of compact congruences of each $\mathbf{A}\in \mathsf {V}$ is dually Brouwerian, i.e., for any compact congruences $\theta _1,\theta _2$ of $\mathbf{A}$ , there exists a compact congruence $\theta _1-\theta _2$ of $\mathbf{A}$ such that for every compact congruence $\theta _3$ of $\mathbf{A}$ ,

   $$ \begin{align*} \theta_1-\theta_2 \subseteq \theta_3\iff\theta_1 \subseteq \theta_1\vee\theta_2. \end{align*} $$

Equationally definable principal congruences imply two further useful properties.

Proposition 4.4 [12, Corollary 2], [26, Corollary 6]

If a variety has equationally definable principal congruences, then it has the congruence extension property and is congruence distributive.

We say next that a class of algebras $\mathsf {K}$ has the equational variable restriction property if for any finite set $\overline {x},y$ and conjunction of equations $\gamma (\overline {x},y)$ , there exists a formula $\pi (\overline {x})$ that is either $\bot $ or a conjunction of equations such that $\mathsf {K}\models \pi \to \gamma $ and for any conjunction of equations $\varphi (\overline {x})$ ,

$$ \begin{align*} \mathsf{K}\models\varphi\to\gamma \:\Longrightarrow\: \mathsf{K}\models \varphi\to \pi. \end{align*} $$

The main result of this section is the following characterization theorem.

Theorem 4.5. Let $\mathsf {V}$ be a variety that has the compact intersection property and equationally definable principal congruences. The theory of $\mathsf {V}$ has a model completion if, and only if, $\mathsf {V}$ is coherent and has the amalgamation property and equational variable restriction property.

Remark 4.6. Theorem 4.5 provides a slightly more general algebraic reformulation of [19, Theorem 4], which requires that the join-semilattice of compact congruences of each algebra $\mathbf{A}\in \mathsf {V}$ has a bottom element, or, equivalently, that there is a variable-free conjunction of equations $\pi $ such that $\mathsf {V}\models \pi \to \varepsilon $ for every equation $\varepsilon $ . This condition is not satisfied by all the varieties of interest in this paper, in particular, the variety of lattice-ordered abelian groups.

We show first that the right-to-left direction of Theorem 4.5 holds even in the absence of the compact intersection property.

Proposition 4.7. Let $\mathsf {V}$ be a variety that has equationally definable principal congruences. If $\mathsf {V}$ is coherent and has the amalgamation property and the equational variable restriction property, then the theory of $\mathsf {V}$ has a model completion.

Proof. Using Theorem 3.2, it suffices to prove that $\mathsf {V}$ has the conservative model extension property. Consider a finite set $\overline {x},y$ and conjunction of literals $\psi (\overline {x},y)$ , assuming without loss of generality that $\psi $ is satisfiable in $\mathsf {V}$ (cf. Remark 2.10). By coherence, there exists a conjunction of equations $\varphi (\overline {x})$ such that $\mathsf {V}\models \psi ^+ \to \varphi $ and for any equation $\varepsilon (\overline {x})$ ,

$$ \begin{align*} \mathsf{V}\models \psi^+\to \varepsilon \:\Longrightarrow\: \mathsf{V}\models \varphi\to \varepsilon. \end{align*} $$

Let $\sigma _1,\dots ,\sigma _m$ be the equations of $\psi ^-$ . Since $\mathsf {V}$ has equationally definable principal congruences, it follows by Proposition 4.3 that for each $i\in \{1,\dots ,m\}$ , there exists a conjunction of equations $\pi _i(\overline {x},y)$ such that for any conjunction of equations $\gamma (\overline {x},y)$ ,

(7) $$ \begin{align} \mathsf{V}\models (\gamma \mathbin{\&} \psi^+)\to \sigma_i \iff \mathsf{V}\models \gamma\to \pi_i. \end{align} $$

The equational variable restriction property yields a formula $\pi ^{\prime }_i(\overline {x})$ for each $i\in \{1,\dots ,m\}$ that is either $\bot $ or a conjunction of equations such that $\mathsf {V}\models \pi ^{\prime }_i\to \pi _i$ and for any conjunction of equations $\varphi '(\overline {x})$ ,

(8) $$ \begin{align} \mathsf{V}\models \varphi'\to \pi_i \:\Longrightarrow\: \mathsf{V}\models \varphi'\to \pi^{\prime}_i. \end{align} $$

We claim that the quantifier-free formula $\chi := \varphi \mathbin {\&}\neg \pi ^{\prime }_1\mathbin {\&}\cdots \mathbin {\&}\neg \pi ^{\prime }_m$ satisfies the conditions in the definition of conservative model extension property.

Note first that, since $\mathsf {V}\models \psi \to \psi ^+$ and $\mathsf {V}\models \psi ^+\to \varphi $ , also $\mathsf {V}\models \psi \to \varphi $ . To conclude that $\mathsf {V}\models \psi \to \chi $ , it remains to show that $\mathsf {V}\models \psi \to \neg \pi ^{\prime }_i$ for each $i\in \{1,\dots ,m\}$ . Let $i\in \{1,\dots ,m\}$ . Since $\mathsf {V}\models \pi ^{\prime }_i\to \pi _i $ and $\mathsf {V}\models (\pi _i \mathbin {\&} \psi ^+)\to \sigma _i$ , also $\mathsf {V}\models (\pi ^{\prime }_i \mathbin {\&} \psi ^+)\to \sigma _i$ . But then $\mathsf {V}\models (\neg \sigma _i\mathbin {\&} \psi ^+)\to \neg \pi ^{\prime }_i$ and hence $\mathsf {V}\models \psi \to \neg \pi ^{\prime }_i$ as required.

Now, consider an algebra $\mathbf{A}\in \mathsf {V}$ generated by $\overline {a}\in A^{\overline {x}}$ such that $\mathbf{A}\models \chi (\overline {a})$ and for any equation $\varepsilon (\overline {x})$ ,

(9) $$ \begin{align} \mathsf{V}\models \psi^+ \to \varepsilon \:\Longrightarrow\: \mathbf{A}\models \varepsilon(\overline{a}). \end{align} $$

Let $f\colon \mathbf{F}_{\mathsf {V}}(\overline {x})\twoheadrightarrow \mathbf{A}$ be the surjective homomorphism mapping the generators of $\mathbf{F}_{\mathsf {V}}(\overline {x})$ to the elements of $\overline {a}$ . Considering $\mathbf{F}_{\mathsf {V}}(\overline {x})$ as a subalgebra of $\mathbf{F}_{\mathsf {V}}(\overline {x},y)$ , we define

$$ \begin{align*} \theta':=\mathrm{Cg}_{{\mathbf{F}_{\mathsf{V}}(\overline{x},y)}}(\{\widehat{\sigma}\mid \sigma \text{ is an equation of } \psi^+\}) \enspace\text{and}\enspace \theta:=\theta'\vee\mathrm{Cg}_{{\mathbf{F}_{\mathsf{V}}(\overline{x},y)}}(\ker{f}). \end{align*} $$

Let $\mathbf{B}:= \mathbf{F}_{\mathsf {V}}(\overline {x},y)/\theta $ and let g be the natural homomorphism from $\mathbf{F}_{\mathsf {V}}(\overline {x},y)$ onto $\mathbf{B}$ . Since $\ker {f}\subseteq \theta \cap \textrm {F}_{\mathsf {V}}(\overline {x})^2$ , the inclusion $\mathbf{F}_{\mathsf {V}}(\overline {x})\hookrightarrow \mathbf{F}_{\mathsf {V}}(\overline {x},y)$ yields a homomorphism $\mathbf{A}\to \mathbf{B}$ mapping $f(x)$ to $g(x)$ for each $x\in \overline {x}$ , as illustrated by the following diagram:

To prove that this homomorphism is an embedding, it suffices to show that $\theta \cap \textrm {F}_{\mathsf {V}}(\overline {x})^2\subseteq \ker {f}$ . Since $\mathsf {V}$ has equationally definable principal congruences, by Proposition 4.4, it has the congruence extension property. Hence, by Lemma 2.2,

$$ \begin{align*} \theta \cap \mathrm{F}_{\mathsf{V}}(\overline{x})^2 =(\theta'\vee\mathrm{Cg}_{{\mathbf{F}_{\mathsf{V}}(\overline{x},y)}}(\ker{f}))\cap \mathrm{F}_{\mathsf{V}}(\overline{x})^2 =(\theta' \cap \mathrm{F}_{\mathsf{V}}(\overline{x})^2)\vee\ker{f}. \end{align*} $$

It therefore suffices to prove that $\theta ' \cap \textrm {F}_{\mathsf {V}}(\overline {x})^2\subseteq \ker {f}$ . Consider any equation $\varepsilon (\overline {x})$ such that $\widehat {\varepsilon }\in \theta ' \cap \textrm {F}_{\mathsf {V}}(\overline {x})^2$ . An application of Lemma 2.1 yields $\mathsf {V}\models \psi ^+\to \varepsilon $ and, by (9), we obtain $\mathbf{A}\models \varepsilon (\overline {a})$ . Hence $\widehat {\varepsilon }\in \ker {f}$ as required.

To conclude the proof, we show that $\mathbf{B}\models \psi (\overline {a},b)$ , where b is the image under g of the equivalence class of y. Since $\theta ' \subseteq \theta =\ker {g}$ , we have $\mathbf{B}\models \psi ^+(\overline {a},b)$ . Suppose toward a contradiction that $\mathbf{B}\models \sigma _i(\overline {a},b)$ for some $i\in \{1,\dots ,m\}$ . Then $\widehat {\sigma }_i\in \theta $ , and so $\mathsf {V}\models (\psi ^+\mathbin {\&} \gamma )\to \sigma _i$ for some conjunction $\gamma (\overline {x})$ of equations in $\ker {f}$ . By (7), we have $\mathsf {V}\models \gamma \to \pi _i$ and hence, by (8), also $\mathsf {V}\models \gamma \to \pi ^{\prime }_i$ . Together with $\mathbf{A}\models \gamma (\overline {a})$ , this entails $\mathbf{A}\models \pi ^{\prime }_i(\overline {a})$ , contradicting the fact that $\mathbf{A}\models \chi (\overline {a})$ .

We now complete the proof of Theorem 4.5 by establishing the necessity of the stated conditions, recalling that a variety that has equationally definable principal congruences is congruence distributive (Proposition 4.4).

Proposition 4.8. Let $\mathsf {V}$ be a congruence distributive variety that has the compact intersection property. If the theory of $\mathsf {V}$ has a model completion, then $\mathsf {V}$ is coherent and has the amalgamation property and equational variable restriction property.

Proof. If the theory of $\mathsf {V}$ has a model completion, then $\mathsf {V}$ is coherent and has the amalgamation property by Theorem 3.2. Hence, it remains to settle the equational variable restriction property. To this end, consider a finite set $\overline {x},y$ and conjunction of equations $\gamma (\overline {x},y)$ . We must find a formula $\pi (\overline {x})$ that is either $\bot $ or a conjunction of equations such that $\mathsf {V}\models \pi \to \gamma $ and for any conjunction of equations $\varphi (\overline {x})$ ,

$$ \begin{align*} \mathsf{V}\models\varphi\to\gamma \:\Longrightarrow\: \mathsf{V}\models \varphi\to \pi. \end{align*} $$

Let $T:= \textrm {Th}(\mathsf {V})$ be the theory of $\mathsf {V}$ , and let $T^*$ be a model completion of T. Since $T^*$ has quantifier elimination, there exists a quantifier-free formula $\xi (\overline {x})$ satisfying

$$ \begin{align*} T^*\vdash \forall \overline{x} \, [(\forall y. \gamma)\leftrightarrow \xi]. \end{align*} $$

So $T^*\vdash \forall \overline {x},y \, (\xi \to \gamma )$ and, since T and $T^*$ are co-theories, $T\vdash \forall \overline {x},y \, (\xi \to \gamma )$ . Assume without loss of generality that $\xi =\xi _1\curlyvee \cdots \curlyvee \xi _m$ where each $\xi _i$ is a conjunction of literals. For each $i\in \{1,\dots ,m\}$ , we have $\mathsf {V}\models \xi _i\to \gamma $ and so, by the disjunction property for varieties, either $\mathsf {V}\models \xi _i^+\to \gamma $ or $\mathsf {V}\models \neg \xi _i$ .

Now let $J:= \{i\in \{1,\dots ,m\}\mid \xi _i\text { is satisfiable in } \mathsf {V}\}$ . Then

, noting that

for $J=\emptyset $ . By Lemma 4.1, or taking $\bot $ if $J=\emptyset $ , there exists a formula $\pi (\overline {x})$ that is either $\bot $ or a conjunction of equations such that for any equation $\varepsilon (\overline {x},\overline {z})$ ,

In particular, $\mathsf {V}\models \pi \to \gamma $ . Now let $\varphi (\overline {x})$ be any conjunction of equations such that $\mathsf {V}\models \varphi \to \gamma $ . Then $T\vdash \forall \overline {x} \, [\varphi \to (\forall y.\gamma )]$ and, since T and $T^*$ are co-theories, $T^*\vdash \forall \overline {x} \, [\varphi \to (\forall y.\gamma )]$ . Hence $T^*\vdash \forall \overline {x} \, (\varphi \to \xi )$ and, again using the fact that T and $T^*$ are co-theories, $T\vdash \forall \overline {x} \, (\varphi \to \xi )$ , yielding $\mathsf {V}\models \varphi \to \xi $ . But then

and, since

, by the above equivalence, $\mathsf {V}\models \varphi \to \pi $ as required.⊣

Finally, in this section, we show that for varieties that have the congruence extension property, a small generalization of the equational variable restriction property implies the amalgamation property. Let us first recall the following well-known relationship between amalgamation and deductive interpolation.

Proposition 4.9 (cf. [30, Theorem 22])

Let $\mathsf {V}$ be a variety that has the congruence extension property. $\mathsf {V}$ has the amalgamation property if, and only if, it has the deductive interpolation property; that is, for any finite sets $\overline {x},\overline {y},\overline {z}$ and conjunctions of equations $\varphi (\overline {x},\overline {y})$ , $\gamma (\overline {x},\overline {z})$ satisfying $\mathsf {V}\models \varphi \to \gamma $ , there exists a conjunction of equations $\pi (\overline {x})$ such that $\mathsf {V}\models \varphi \to \pi $ and $\mathsf {V}\models \pi \to \gamma $ .

It follows easily that the amalgamation property and equational variable restriction property can be combined into a single “uniform interpolation” property.

Corollary 4.10. Let $\mathsf {V}$ be a variety that has the congruence extension property. Then the following statements are equivalent:

1. (1) $\mathsf {V}$ has the amalgamation property and the equational variable restriction property.

2. (2) For any finite set $\overline {x},y$ and conjunction of equations $\gamma (\overline {x},y)$ , there exists a formula $\pi (\overline {x})$ that is either $\bot $ or a conjunction of equations such that $\mathsf {V}\models \pi \to \gamma $ and for any conjunction of equations $\varphi (\overline {x},\overline {z})$ ,

   $$ \begin{align*} \mathsf{V}\models\varphi\to\gamma \:\Longrightarrow\: \mathsf{V}\models \varphi\to \pi.\\[-17pt] \end{align*} $$

Proof. $(1)\Rightarrow (2)$ Suppose that $\mathsf {V}$ has the amalgamation property and the equational variable restriction property, and consider a finite set $\overline {x},y$ and conjunction of equations $\gamma (\overline {x},y)$ . By the equational variable restriction property, there exists a formula $\pi (\overline {x})$ that is either $\bot $ or a conjunction of equations such that $\mathsf {V}\models \pi \to \gamma $ and for any conjunction of equations $\varphi (\overline {x})$ ,

$$ \begin{align*} \mathsf{V}\models\varphi\to\gamma \:\Longrightarrow\: \mathsf{V}\models \varphi\to \pi.\\[-17pt] \end{align*} $$

Now consider a conjunction of equations $\varphi (\overline {x},\overline {z})$ satisfying $\mathsf {V}\models \varphi \to \gamma $ . Since $\mathsf {V}$ has the congruence extension property and the amalgamation property, by Proposition 4.9, there exists a conjunction of equations $\pi '(\overline {x})$ such that $\mathsf {V}\models \varphi \to \pi '$ and $\mathsf {V}\models \pi '\to \gamma $ . By the above implication, $\mathsf {V}\models \pi '\to \pi $ and hence also $\mathsf {V}\models \varphi \to \pi $ as required.

$(2)\Rightarrow (1)$ The amalgamation property and the equational variable restriction property both follow directly from condition (2) and Proposition 4.9.⊣

Relationships between uniform interpolation and the existence of model completions have been investigated in some depth by Ghilardi and Zawadowski in the setting of intermediate and modal logics [19, 20]. In particular, Pitts’ uniform interpolation theorem for intuitionistic propositional logic [35] is used to deduce that the variety $\mathsf {HA}$ of Heyting algebras satisfies certain categorical conditions and therefore has a model completion. In the terminology of this section: it follows from Pitts’ theorem that $\mathsf {HA}$ is coherent and satisfies condition (2) of Corollary 4.10 and hence has the amalgamation property and the equational variable restriction property; the result then follows by Theorem 4.5 (a slight generalization of [19, Theorem 4]), since $\mathsf {HA}$ has the compact intersection property and equationally definable principal congruences. More generally, the theories of precisely eight varieties of Heyting algebras (those that have the amalgamation property) have a model completion [20]; finite axiomatizations of these model completions for the six locally finite cases are provided in [11].

5 Parametrically definable principal congruences

In this section, we show that if a variety satisfies certain congruence lattice conditions and has a model completion, then it must have equationally definable principal congruences. Our main technical tool is a weaker condition for defining principal congruences that is inspired by work of Glass and Pierce on existentially complete lattice-ordered abelian groups [22].

We say that a class of algebras $\mathsf {K}$ has parametrically definable principal congruences if there exists a quantifier-free formula $\xi (x_1,x_2,y_1,y_2,\overline {z})$ such that for each $\mathbf{A}\in \mathsf {K}$ and all $a_1,a_2,b_1,b_2\in A$ ,

$$ \begin{align*} (a_1,a_2)\in \mathrm{Cg}_{{\mathbf{A}}}(b_1,b_2) &\iff \text{any } \mathbf{B}\in\mathsf{K} \text{ extending } \mathbf{A} \text{ satisfies }\\ &\qquad\quad \mathbf{B}\models \forall \overline{z}. \xi(a_1,a_2,b_1,b_2,\overline{z}).\\[-15pt] \end{align*} $$

Clearly, if a class of algebras has equationally definable principal congruences, it has parametrically definable principal congruences. However, there are classes of algebras that have parametrically definable principal congruences but do not even have first-order definable principal congruences (see Example 5.8). The following proposition shows that this cannot be the case for a universal class of algebras whose theory has a model completion.

Proposition 5.1. Let $\mathsf {K}$ be a universal class of algebras with parametrically definable principal congruences. If the theory of $\mathsf {K}$ has a model completion, then $\mathsf {K}$ has quantifier-free definable principal congruences.

Proof. Suppose that $\mathsf {K}$ has parametrically definable principal congruences, witnessed by a quantifier-free formula $\xi (x_1,x_2,y_1,y_2,\overline {z})$ , and that the theory of $\mathsf {K}$ has a model completion. We can assume that $\neg \xi =\psi _1\curlyvee \cdots \curlyvee \psi _n$ , where each $\psi _i$ is a conjunction of literals. By Proposition 3.8, for each $i\in \{1,\dots ,n\}$ , there exists a quantifier-free formula $\chi _i(x_1,x_2,y_1,y_2)$ such that

1. (i) $\mathsf {K}\models \psi _i\to \chi _i$ and

2. (ii) for any $\mathbf{A}\in \mathsf {K}$ , and $a_1,a_2,b_1,b_2\in A$ satisfying $\mathbf{A}\models \chi _i(a_1,a_2,b_1,b_2)$ , there exists an extension $\mathbf{B}\in \mathsf {K}$ of $\mathbf{A}$ such that $\mathbf{B}\models \exists \overline {z}.\psi _i(a_1,a_2,b_1,b_2,\overline {z})$ .

We claim that for each $\mathbf{A}\in \mathsf {K}$ and all $a_1,a_2,b_1,b_2\in A$ ,

and hence that $\mathsf {K}$ has quantifier-free definable principal congruences. Suppose first that $(a_1,a_2)\in \textrm { Cg}_{{\mathbf{A}}}(b_1,b_2)$ . By assumption, any $\mathbf{B}\in \mathsf {K}$ extending $\mathbf{A}$ satisfies $\mathbf{B}\models \forall \overline {z}. \xi (a_1,a_2,b_1,b_2,\overline {z})$ and hence $\mathbf{B}\not \models \exists \overline {z}. \psi _i(a_1,a_2,b_1,b_2,\overline {z})$ for each $i\in \{1,\dots ,n\}$ . But then, by (ii), also $\mathbf{A}\models \neg \chi _i(a_1,a_2,b_1,b_2)$ for each $i\in \{1,\dots ,n\}$ . Now suppose that $(a_1,a_2)\notin \mathrm{Cg}_{{\mathbf{A}}}(b_1,b_2)$ . By assumption, there exists an extension $\mathbf{B}\in \mathsf {K}$ of $\mathbf{A}$ such that $\mathbf{B}\not \models \forall \overline {z}. \xi (a_1,a_2,b_1,b_2,\overline {z})$ , and hence $\mathbf{B}\models \exists \overline {z}. \psi _i(a_1,a_2,b_1,b_2,\overline {z})$ for some $i\in \{1,\dots ,n\}$ . But then, since $\mathsf {K}\models \psi _i\to \chi _i$ , by (i), also $\mathbf{B}\models \chi _i(a_1,a_2,b_1,b_2)$ . Finally, as $\chi _i$ is quantifier-free, it follows that $\mathbf{A}\models \chi _i(a_1,a_2,b_1,b_2)$ .⊣

Example 5.2. It is easy to see that the variety of abelian groups does not have first-order definable principal congruences. If this were the case, there would be a first-order formula $\alpha (x,y)$ such that for any abelian group $\textbf {G}$ , an element $a\in G$ belongs to the subgroup of $\textbf {G}$ generated by an element $b\in G$ if, and only if, $\textbf {G}\models \alpha (a,b)$ . But then the sentence $\exists y \forall x. \alpha (x,y)$ would define the class of cyclic groups, contradicting the fact that this class is not elementary. On the other hand, the theory of abelian groups does have a model completion (cf. [13]). Proposition 5.1 therefore tells us that the variety of abelian groups does not have parametrically definable principal congruences.

We strengthen Proposition 5.1 by exploiting the following fact, due to Fried, Grätzer, and Quackenbush [14].

Proposition 5.3 [14, Theorems 4.5 and 6.9]

Let $\mathsf {V}$ be a congruence distributive variety that has the congruence extension property. $\mathsf {V}$ has first-order definable principal congruences if, and only if, it has equationally definable principal congruences.

Combining this fact with Proposition 5.1 yields the following result.

Proposition 5.4. Let $\,\mathsf {V}$ be a congruence distributive variety that has the congruence extension property and parametrically definable principal congruences. If the theory of $\,\mathsf {V}$ has a model completion, then $\mathsf {V}$ has equationally definable principal congruences.

We now provide a sufficient syntactic condition for a variety with the congruence extension property to have parametrically definable principal congruences that is easier to establish in certain cases. We say that a variety $\mathsf {V}$ has a guarded deduction theorem if there exist conjunctions of equations $\gamma (x_1,x_2,y_1,y_2,\overline {z})$ and $\varphi (x_1,x_2,y_1,y_2,\overline {z})$ such that for any finite set $\overline {w}$ with $\overline {w}\cap \overline {z}=\emptyset $ , terms $s_1(\overline {w}),s_2(\overline {w}),t_1(\overline {w}),t_2(\overline {w})$ , and conjunction of equations $\pi (\overline {w})$ ,

1. (i) $\mathsf {V} \models (\pi \mathbin {\&} (t_1\approx t_2)) \to (s_1 \approx s_2) \iff \mathsf {V} \models \pi \to \forall \overline {z}.(\gamma \to \varphi )(s_1,s_2,t_1,t_2,\overline {z})$ and

2. (ii) $\mathsf {V} \models (\pi \mathbin {\&} \gamma (s_1,s_2,t_1,t_2,\overline {z})) \to \sigma \iff \mathsf {V}\models \pi \to \sigma $ for any equation $\sigma (\overline {w})$ .

This property has the following algebraic characterization:

Proposition 5.5. The following statements are equivalent for any variety $\mathsf {V}$ :

1. (1) $\mathsf {V}$ has a guarded deduction theorem.

2. (2) There exist conjunctions of equations $\gamma (x_1,x_2,y_1,y_2,\overline {z})$ and $\varphi (x_1,x_2,y_1,y_2,\overline {z})$ such that for any finitely generated algebra $\mathbf{A}\in \mathsf {V}$ and $a_1,a_2,b_1,b_2\in A$ , there exists an embedding of $\mathbf{A}$ into some member of $\mathsf {V}$ satisfying $\exists \overline {z}.\gamma (a_1,a_2,b_1,b_2,\overline {z})$ , and

   $$ \begin{align*} (a_1,a_2)\in \mathrm{Cg}_{{\mathbf{A}}}(b_1,b_2) \iff\: & \mathbf{B}\models \forall \overline{z}. (\gamma\to\varphi)(h(a_1),h(a_2),h(b_1),h(b_2),\overline{z})\\ & \text{for any } \mathbf{B}\in \mathsf{V} \text{ and homomorphism } h\colon \mathbf{A}\to\mathbf{B}. \end{align*} $$

Proof. $(1)\Rightarrow (2)$ Let $\gamma (x_1,x_2,y_1,y_2,\overline {z})$ and $\varphi (x_1,x_2,y_1,y_2,\overline {z})$ be conjunctions of equations satisfying the conditions for a guarded deduction theorem, and fix a finitely generated algebra $\mathbf{A}\in \mathsf {V}$ and $a_1,a_2,b_1,b_2\in A$ . We claim that $\gamma $ and $\varphi $ satisfy the equivalence given in (2).

Note first that since $\mathbf{A}$ is finitely generated, there exists a surjective homomorphism $f\colon \textbf {Tm}(\overline {w})\twoheadrightarrow \mathbf{A}$ for some finite set $\overline {w}$ with $\overline {w}\cap \overline {z}=\emptyset $ . Let $s_1,s_2,t_1,t_2$ be terms in the preimages under f of $a_1,a_2,b_1,b_2$ , respectively. Now consider $(a_1,a_2)\in \textrm { Cg}_{{\mathbf{A}}}(b_1,b_2)$ . Since $\mathbf{A}$ is isomorphic to $\textbf {Tm}(\overline {w})/\ker {f}$ , by the correspondence theorem for universal algebra, $(s_1,s_2)\in \ker {f} \vee \mathrm{Cg}_{{\textbf {Tm}(\overline {w})}}(t_1,t_2)$ . Moreover, since any congruence is the directed union of the compact congruences below it, there exists a finite subset $S\subseteq \ker {f}$ such that $(s_1,s_2)\in \textrm { Cg}_{{\textbf {Tm}(\overline {w})}}(S) \vee \mathrm{Cg}_{{\textbf {Tm}(\overline {w})}}(t_1,t_2)$ . Let $\pi (\overline {w})$ be the conjunction of the equations in S. It follows easily from Lemma 2.1 that $\mathsf {V} \models (\pi \mathbin {\&} (t_1\approx t_2)) \to (s_1 \approx s_2)$ . Hence $\mathsf {V} \models \pi \to \forall \overline {z}.(\gamma \to \varphi )(s_1,s_2,t_1,t_2,\overline {z})$ , by condition (i) in the definition of a guarded deduction theorem. But $\mathbf{A} \models \pi (f(\overline {w}))$ , so for any $\mathbf{B}\in \mathsf {V}$ and homomorphism $h\colon \mathbf{A}\to \mathbf{B}$ ,

$$ \begin{align*} \mathbf{B}\models \forall \overline{z}. (\gamma\to\varphi)(h(a_1),h(a_2),h(b_1),h(b_2),\overline{z}). \end{align*} $$

Now suppose that $\mathbf{B}\models \forall \overline {z}. (\gamma \to \varphi )(h(a_1),h(a_2),h(b_1),h(b_2),\overline {z})$ for any $\mathbf{B}\in \mathsf {V}$ and homomorphism $h\colon \mathbf{A}\to \mathbf{B}$ . Let $\mathfrak {D}^+(\mathbf{A})$ be the positive diagram of $\mathbf{A}$ , i.e., the set of all atomic sentences in the language extended with names for the elements of $\mathbf{A}$ that are satisfied in $\mathbf{A}$ . Then

$$ \begin{align*} \textrm{Th}(\mathsf{V})\cup\mathfrak{D}^+(\mathbf{A})\vdash \forall\overline{z}.(\gamma\to \varphi)(a_1,a_2,b_1,b_2,\overline{z}), \end{align*} $$

and hence, by the compactness theorem for first-order logic, there exists a finite subset $\Sigma \subseteq \mathfrak {D}^+(\mathbf{A})$ such that $\textrm {Th}(\mathsf {V})\cup \Sigma \vdash \forall \overline {z}.(\gamma \to \varphi )(a_1,a_2,b_1,b_2,\overline {z})$ . For each member of $\Sigma $ , consider an equation in its preimage under the surjection $\textbf {Tm}(\overline {w})^2\twoheadrightarrow \mathbf{A}^2$ . This yields a finite subset of $\ker {f}$ , and letting $\pi (\overline {w})$ denote the conjunction of the equations in this set, we obtain $\mathsf {V} \models \pi \to \forall \overline {z}.(\gamma \to \varphi )(s_1,s_2,t_1,t_2,\overline {z})$ . By condition (i) in the definition of a guarded deduction theorem, we obtain $\mathsf {V} \models (\pi \mathbin {\&} (t_1\approx t_2)) \to (s_1 \approx s_2)$ . Now let $q\colon \mathbf{A}\twoheadrightarrow \mathbf{A}/\mathrm{Cg}_{{\mathbf{A}}}(b_1,b_2)$ be the natural quotient map. Since $\mathbf{A}/\mathrm{Cg}_{{\mathbf{A}}}(b_1,b_2), qf\models \pi \mathbin {\&} (t_1\approx t_2)$ , we have $\mathbf{A}/\mathrm{Cg}_{{\mathbf{A}}}(b_1,b_2), q f\models s_1 \approx s_2$ , i.e., $(a_1,a_2)\in \textrm { Cg}_{{\mathbf{A}}}(b_1,b_2)$ .

To conclude, it remains to show that $\mathbf{A}$ embeds into some member of $\mathsf {V}$ satisfying $\exists \overline {z}.\gamma (a_1,a_2,b_1,b_2,\overline {z})$ . Let $\mathbf{B}$ be the quotient of $\mathbf{F}_{\mathsf {V}}(\overline {w},\overline {z})$ with respect to the congruence $\mathrm{Cg}_{{\mathbf{F}_{\mathsf {V}}(\overline {w},\overline {z})}}(\{\widehat {\varepsilon }\mid \varepsilon \in \ker {f}\}\cup \{\widehat {\sigma }\mid \sigma \text { is an equation of }\gamma (s_1,s_2,t_1,t_2,\overline {z})\})$ . Then $\mathbf{B}$ satisfies $\exists \overline {z}.\gamma (a_1,a_2,b_1,b_2,\overline {z})$ and it is not difficult to see, using condition (ii) in the definition of a guarded deduction theorem, that $\mathbf{B}$ extends $\mathbf{A}$ .

$(2)\Rightarrow (1)$ Let $\gamma (x_1,x_2,y_1,y_2,\overline {z})$ and $\varphi (x_1,x_2,y_1,y_2,\overline {z})$ be conjunctions of equations satisfying the conditions in (2). Let $\overline {w}$ be any finite set satisfying $\overline {w}\cap \overline {z}=\emptyset $ and consider terms $s_1(\overline {w}),s_2(\overline {w}),t_1(\overline {w}),t_2(\overline {w})$ and a conjunction of equations $\pi (\overline {w})$ .

Let $\mathbf{A}$ be the quotient of $\mathbf{F}_{\mathsf {V}}(\overline {w})$ with respect to $\textrm { Cg}_{{\mathbf{F}_{\mathsf {V}}(\overline {w})}}(\{\widehat {\varepsilon }\mid \varepsilon \text { is an equation of } \pi \})$ , with quotient map $f\colon \mathbf{F}_{\mathsf {V}}(\overline {w}) \twoheadrightarrow \mathbf{A}$ . Let $q\colon \textbf {Tm}(\overline {w})\twoheadrightarrow \mathbf{F}_{\mathsf {V}}(\overline {w})$ denote the natural quotient map and define $a_1:= f(q(s_1))$ , $a_2:= f(q(s_2))$ , $b_1:= f(q(t_1))$ , and $b_2:= f(q(t_2))$ . By Lemma 2.1, $(a_1,a_2)\in \textrm { Cg}_{{\mathbf{A}}}(b_1,b_2)$ if, and only if, $\mathsf {V} \models (\pi \mathbin {\&} (t_1\approx t_2)) \to (s_1 \approx s_2)$ . Hence, in order to settle condition (i) in the definition of a guarded deduction theorem, it remains to show that $\mathsf {V} \models \pi \to \forall \overline {z}.(\gamma \to \varphi )(s_1,s_2,t_1,t_2,\overline {z})$ if, and only if, for any $\mathbf{B}\in \mathsf {V}$ and homomorphism $h\colon \mathbf{A}\to \mathbf{B}$ ,

$$ \begin{align*} \mathbf{B}\models \forall \overline{z}. (\gamma\to\varphi)(h(a_1),h(a_2),h(b_1),h(b_2),\overline{z}). \end{align*} $$

This follows by reasoning as in the proof of $(1)\Rightarrow (2)$ .

With respect to condition (ii) in the definition of a guarded deduction theorem, let $\mathbf{B}$ denote the quotient of $\mathbf{F}_{\mathsf {V}}(\overline {w},\overline {z})$ with respect to

$$ \begin{align*} \mathrm{Cg}_{{\mathbf{F}_{\mathsf{V}}(\overline{w},\overline{z})}}&(\{\widehat{\varepsilon}\mid \varepsilon \text{ is an equation of }\pi(\overline{w})\}\\&\cup\{\widehat{\sigma}\mid \sigma \text{ is an equation of }\gamma(s_1,s_2,t_1,t_2,\overline{z})\}). \end{align*} $$

Note that there is a canonical homomorphism $k\colon \mathbf{A}\to \mathbf{B}$ . By assumption, there is an embedding $j\colon \mathbf{A} \hookrightarrow \mathbf{B}'$ with $\mathbf{B}'\in \mathsf {V}$ and $\mathbf{B}'\models \exists \overline {z}.\gamma (a_1,a_2,b_1,b_2,\overline {z})$ . It follows easily that there is a homomorphism $h\colon \mathbf{B}\to \mathbf{B}'$ such that $j=h k$ . Since j is injective, so is k. Hence, by Lemma 2.1, we have that $\mathsf {V} \models (\pi \mathbin {\&} \gamma (s_1,s_2,t_1,t_2,\overline {z})) \to \sigma '$ implies $\mathsf {V}\models \pi \to \sigma '$ for any equation $\sigma '(\overline {w})$ .⊣

Proposition 5.6. Let $\mathsf {V}$ be a variety that has the congruence extension property and a guarded deduction theorem. Then $\mathsf {V}$ has parametrically definable principal congruences.

Proof. It suffices to show that $\mathsf {V}$ has parametrically definable principal congruences whenever the property in condition (2) of Proposition 5.5 holds for some $\gamma $ and $\varphi $ . Let $\xi (x_1,x_2,y_1,y_2,\overline {z}):= \gamma \to \varphi $ . We claim that for all $\mathbf{A}\in \mathsf {V}$ and $a_1,a_2,b_1,b_2\in A$ ,

$$ \begin{align*} (a_1,a_2)\in \mathrm{Cg}_{{\mathbf{A}}}(b_1,b_2) &\iff \text{each } \mathbf{B}\in\mathsf{V} \text{ extending } \mathbf{A}\\ &\qquad\quad \text{satisfies } \mathbf{B}\models \forall \overline{z}. \xi(a_1,a_2,b_1,b_2,\overline{z}). \end{align*} $$

Suppose first that $(a_1,a_2)\in \mathrm{Cg}_{{\mathbf{A}}}(b_1,b_2)$ . By the congruence extension property, $(a_1,a_2)\in \textrm { Cg}_{{\mathbf{A}'}}(b_1,b_2)$ , where $\mathbf{A}'$ is the subalgebra of $\mathbf{A}$ generated by $a_1,a_2,b_1,b_2$ . Since $\mathbf{A}'$ is a finitely generated member of $\mathsf {V}$ , it follows from condition (2) of Proposition 5.5 that $\mathbf{B}\models \forall \overline {z}. \xi (a_1,a_2,b_1,b_2,\overline {z})$ for every $\mathbf{B}\in \mathsf {V}$ extending $\mathbf{A}'$ , and hence, in particular, for every $\mathbf{B}\in \mathsf {V}$ extending $\mathbf{A}$ .

Now suppose that $(a_1,a_2)\notin \mathrm{Cg}_{{\mathbf{A}}}(b_1,b_2)$ . We assume first that $\mathbf{A}$ is finitely generated, and then deduce the general case. Let $\overline {w}$ be a finite set such that $\overline {w}\cap \overline {z}=\emptyset $ and there exists a surjective homomorphism $f\colon \textbf {Tm}(\overline {w})\twoheadrightarrow \mathbf{A}$ . We can assume without loss of generality that $x_1,x_2,y_1,y_2\in \overline {w}$ , and also $f(x_1)=b_1, f(x_2)=b_2, f(y_1)=a_1, f(y_2)=a_2$ . Let $\mathbf{B}:= \mathbf{F}_{\mathsf {V}}(\overline {w},\overline {z})/\theta $ , where

$$ \begin{align*} \theta:=\mathrm{Cg}_{{\mathbf{F}_{\mathsf{V}}(\overline{w},\overline{z})}}(\{\widehat{\varepsilon}\mid \varepsilon\in \ker{f}\}\cup\{\widehat{\sigma}\mid \sigma \text{ is an equation of } \gamma\}). \end{align*} $$

We claim that $\mathbf{B}$ extends $\mathbf{A}$ . Let $j\colon \mathbf{A}\to \mathbf{B}$ be the canonical homomorphism mapping $a_1,a_2,b_1,b_2$ to the equivalence classes of $x_1,x_2,y_1,y_2$ , respectively. By assumption, there exist $\mathbf{B}'\in \mathsf {V}$ and an embedding $i\colon \mathbf{A}\to \mathbf{B}'$ such that $\mathbf{B}'\models \exists \overline {z}.\gamma (a_1,a_2,b_1,b_2,\overline {z})$ . It is not difficult to see that i factors through j, and since i is injective, so is j.

Now, by assumption, there exist $\textbf {C}\in \mathsf {V}$ and a homomorphism $h\colon \mathbf{A}\to \textbf {C}$ satisfying $\textbf {C}\models \exists \overline {z}. (\gamma \mathbin {\&} \neg \varphi _i)(h(a_1),h(a_2),h(b_1),h(b_2),\overline {z})$ for some equation $\varphi _i$ of $\varphi $ . It follows that there exists a homomorphism $k\colon \textbf {Tm}(\overline {w},\overline {z})\to \textbf {C}$ which factors through the composition $g\colon \textbf {Tm}(\overline {w},\overline {z})\twoheadrightarrow \mathbf{F}_{\mathsf {V}}(\overline {w},\overline {z})\twoheadrightarrow \mathbf{B}$ and satisfies $\varphi _i\notin \ker {k}$ , as depicted in the diagram:

So $\varphi _i\notin \ker {g}$ , showing that $\mathbf{B}$ is an extension of $\mathbf{A}$ satisfying $\mathbf{B}\not \models \forall \overline {z}. \xi (a_1,a_2,b_1,b_2,\overline {z})$ .

To conclude, consider any $\mathbf{A}\in \mathsf {V}$ and suppose that $\mathbf{B}\models \forall \overline {z}. \xi (a_1,a_2,b_1,b_2,\overline {z})$ for all $\mathbf{B}\in \mathsf {V}$ extending $\mathbf{A}$ . Then $\textrm {Th}(\mathsf {V})\cup \mathfrak {D}(\mathbf{A})\vdash \forall \overline {z}. \xi (a_1,a_2,b_1,b_2,\overline {z})$ , where $\mathfrak {D}(\mathbf{A})$ is the diagram of $\mathbf{A}$ , i.e., the collection of all atomic sentences and negated atomic sentences in the language extended with names for the elements of $\mathbf{A}$ that are satisfied in $\mathbf{A}$ . By the compactness theorem for first-order logic, there is a finite subset $\Sigma \subseteq \mathfrak {D}(\mathbf{A})$ such that $\textrm {Th}(\mathsf {V})\cup \Sigma \vdash \forall \overline {z}. \xi (a_1,a_2,b_1,b_2,\overline {z})$ . Let $\mathbf{A}'$ be the subalgebra of $\mathbf{A}$ generated by $a_1,a_2,b_1,b_2$ and the elements named by $\Sigma $ . As the diagram of $\mathbf{A}'$ contains $\Sigma $ , every $\mathbf{B}'\in \mathsf {V}$ extending $\mathbf{A}'$ satisfies $\mathbf{B}'\models \forall \overline {z}. \xi (a_1,a_2,b_1,b_2,\overline {z})$ . Note that $\mathbf{A}'$ is a finitely generated member of $\mathsf {V}$ and so, by the argument above, $(a_1,a_2)\in \textrm { Cg}_{{\mathbf{A}'}}(b_1,b_2)\subseteq \mathrm{Cg}_{{\mathbf{A}}}(b_1,b_2)$ .⊣

Combining Propositions 5.4 and 5.6 yields the main result of this section.

Theorem 5.7. Let $\mathsf {V}$ be a congruence distributive variety that has the congruence extension property and a guarded deduction theorem. If the theory of $\mathsf {V}$ has a model completion, then $\mathsf {V}$ has equationally definable principal congruences.

Example 5.8. As first proved by Glass and Pierce in [22], the theory of the variety $\mathsf {LA}$ of lattice-ordered abelian groups does not have a model completion. It is well-known that $\mathsf {LA}$ is congruence distributive and has the congruence extension property, but does not have equationally (or even first-order) definable principal congruences. Hence it suffices, by Theorem 5.7, to observe that the formulas

$$ \begin{align*} \gamma &:= (x_1 - x_2) \wedge(x_2 - x_1) \wedge 0 \leq z \mathbin{\&} ((y_1-y_2)\wedge (y_2-y_1) \wedge 0)\vee z \approx 0\:\text{ and }\:\\\varphi&:= z\approx 0 \end{align*} $$

satisfy conditions (i) and (ii) in the definition of a guarded deduction theorem for $\mathsf {LA}$ .

6 Varieties of pointed residuated lattices

In this section, we apply the results of the last two sections to a family of varieties of algebras that provide algebraic semantics for substructural logics, including (up to term-equivalence) lattice-ordered groups, MV-algebras, and Heyting algebras (see, e.g., [5, 16, 31]).

A pointed residuated lattice is an algebra $\mathbf{A} = \langle A,\wedge ,\vee ,\cdot ,\backslash , / ,\textrm {e}, \textrm {0}\rangle $ such that $\langle A,\wedge ,\vee \rangle $ is a lattice, $\langle A,\cdot ,\textrm {e} \rangle $ is a monoid, and $\backslash , / $ are left and right residuals, respectively, of $\cdot $ in the underlying lattice order, i.e., for all $a,b,c\in A$ ,

$$ \begin{align*} b \le a \backslash c \iff a \cdot b \le c \iff a \le c / b. \end{align*} $$

It will be useful to define a further binary operation $x\equiv y:= (x\backslash y)\wedge (y\backslash x)\wedge \textrm {e}$ , noting that $(a\equiv b) = \textrm {e}$ for $a,b\in A$ if, and only if, $a=b$ . We also define for any $a\in A$ inductively $a^0:= \textrm {e}$ and $a^{n+1}:= a\cdot a^n$ ( $n\in \mathbb {N}$ ).

Pointed residuated lattices form a congruence distributive variety [5], and include the subvariety $\mathsf {CPRL}$ of commutative pointed residuated lattices satisfying $x \cdot y \approx y \cdot x$ . In particular, a Heyting algebra is term-equivalent to a commutative pointed residuated lattice satisfying $x\cdot y\approx x\wedge y$ and $x\wedge \textrm {0}\approx \textrm {0}$ , and a Boolean algebra is term-equivalent to a Heyting algebra satisfying $(x \backslash \textrm {0})\backslash \textrm {0} \approx x$ .

Let $\mathsf {V}$ be a variety of pointed residuated lattices. We let $\mathsf {V^c}$ denote the class of linearly ordered members of $\mathsf {V}$ , and call $\mathsf {V}$ semilinear if $\mathsf {V} = \mathbb {ISP}(\mathsf {V^c})$ . Semilinearity can also be expressed equationally; in particular, a variety of commutative pointed residuated lattices is semilinear if, and only if, it satisfies $\textrm {e} \approx ((x \backslash y) \wedge \textrm {e}) \vee ((y \backslash x) \wedge \textrm {e})$ [5].

Example 6.1. The variety $\mathsf {LA}$ of lattice-ordered abelian groups is term-equivalent to the variety of commutative pointed residuated lattices satisfying $\textrm {e}\approx \textrm {0}$ and $x\cdot (x\backslash \textrm {e})\approx ~\textrm {e}$ . More precisely, if $\langle L,\wedge ,\vee ,+,-,0 \rangle \in \mathsf {LA}$ and we define $x\cdot y:= x+y$ , $x\backslash y:= y-x$ , and $x / y:= x-y$ , then $\langle L,\wedge ,\vee ,\cdot ,\backslash , / ,0,0\rangle \in \mathsf {CPRL}$ satisfies $\textrm {e}\approx \textrm {0}$ and $x\cdot (x\backslash \textrm { e})\approx \textrm {e}$ . Conversely, if $\textbf {L}\in \mathsf {CPRL}$ satisfies $\textrm {e}\approx \textrm {0}$ and $x\cdot (x\backslash \textrm { e})\approx \textrm {e}$ and we define $x+y:= x\cdot y$ and $-x:= x\backslash \textrm {e}$ , then $\langle L,\wedge ,\vee ,+,-,\textrm { 0}\rangle \in \mathsf {LA}$ . Recall also that $\mathsf {LA} = \mathbb {ISP}(\mathsf {LA^c})$ , so the corresponding variety of pointed residuated lattices is semilinear.

Example 6.2. The variety $\mathsf {MV}$ of MV-algebras is term-equivalent to the variety of commutative pointed residuated lattices satisfying $x\vee y\approx (x\backslash y)\backslash y$ and $x\wedge \textrm {0}\approx \textrm {0}$ . More precisely, if $\langle M,\oplus ,\lnot ,0\rangle \in \mathsf {MV}$ and we define $x \cdot y := \lnot (\lnot x\oplus \lnot y)$ , $x \backslash y := \lnot x \oplus y$ , ${x / y} := x\oplus \lnot y$ , and $\textrm {e}:= \lnot 0$ , then $\langle M,\wedge ,\vee ,\cdot ,\backslash , / ,\textrm {e},\textrm { 0}\rangle \in \mathsf {CPRL}$ satisfies $x\vee y\approx (x\backslash y)\backslash y$ and $x\wedge \textrm {0}\approx \textrm {0}$ . Conversely, if $\textbf {M}\in \mathsf {CPRL}$ satisfies $x\vee y\approx (x\backslash y)\backslash y$ and $x\wedge \textrm {0}\approx \textrm {0}$ and we define $x\oplus y:= (x\backslash \textrm {0})\backslash y$ and $\lnot x:= x\backslash \textrm {0}$ , then $\langle M,\oplus ,\lnot ,\textrm { 0}\rangle \in \mathsf {MV}$ . Again, since $\mathsf {MV}=\mathbb {ISP}(\mathsf {MV^c})$ , the corresponding variety of pointed residuated lattices is semilinear.

Let us call a variety $\mathsf {V}$ of pointed residuated lattices Hamiltonian ³ if for some $k\in \mathbb {N}^{>0}$ ,

$$ \begin{align*} \mathsf{V}\models(x\wedge \textrm{e})^k \cdot y\approx y\cdot (x\wedge \textrm{e})^k. \end{align*} $$

The following proposition collects some useful facts about such varieties.

Proposition 6.3 [15, Lemmas 3.14 and 3.17 and Proposition 3.15]

Let $\mathsf {V}$ be a Hamiltonian variety of pointed residuated lattices.

1. (a) For any $\mathbf{A}\in \mathsf {V}$ and $a_1,a_2,b_1,b_2\in A$ ,

   $$ \begin{align*} (a_1,a_2)\in \mathrm{Cg}_{{\mathbf{A}}}(b_1,b_2) \iff (b_1\equiv b_2)^n\leq a_1\equiv a_2 \text{ for some }n\in\mathbb{N}. \end{align*} $$

2. (b) $\mathsf {V}$ has equationally definable principal congruences if, and only if, for some $n\in \mathbb {N}$ ,

   $$ \begin{align*} \mathsf{V}\models(x\wedge\textrm{e})^n\approx (x\wedge\textrm{e})^{n+1}. \end{align*} $$

3. (c) $\mathsf {V}$ has the congruence extension property.

We show now that every Hamiltonian variety of pointed residuated lattices has both the compact intersection property and a guarded deduction theorem, which, combined with Theorems 4.5 and 5.7, will allow us to determine which of these varieties have a theory that has a model completion.

Lemma 6.4. Let $\mathsf {V}$ be a Hamiltonian variety of pointed residuated lattices. Then $\mathsf {V}$ has the compact intersection property.

Proof. Every compact congruence of an algebra $\mathbf{A}\in \mathsf {V}$ is a finite join of principal congruences of $\mathbf{A}$ and hence, by congruence distributivity, the intersection of any two compact congruences of $\mathbf{A}$ is a finite join of intersections of principal congruences of $\mathbf{A}$ . It therefore suffices to show that for all $b_1,b_2,c_1,c_2\in A$ ,

$$ \begin{align*} \mathrm{Cg}_{{\mathbf{A}}}(b_1,b_2)\cap\mathrm{Cg}_{{\mathbf{A}}}(c_1,c_2)=\mathrm{Cg}_{{\mathbf{A}}}(\textrm{e},(b_1\equiv b_2)\vee (c_1\equiv c_2)). \end{align*} $$

Suppose first that $(a_1,a_2)\in \mathrm{Cg}_{{\mathbf{A}}}(b_1,b_2)\cap \mathrm{Cg}_{{\mathbf{A}}}(c_1,c_2)$ . Then Proposition 6.3(a) yields $(b_1\equiv b_2)^{n_1}\leq a_1\equiv a_2$ and $(c_1\equiv c_2)^{n_2}\leq a_1\equiv a_2$ for some $n_1,n_2\in \mathbb {N}$ . Let $n:= \max {(n_1,n_2)}$ . Then $(b_1\equiv b_2)^{n} \vee (c_1\equiv c_2)^{n}\leq a_1\equiv a_2$ and, using some elementary properties of pointed residuated lattices, also $((b_1\equiv b_2)\vee (c_1\equiv c_2))^{2n}\leq {a_1\equiv a_2}$ . By Proposition 6.3(a) again, $(a_1,a_2)\in \mathrm{Cg}_{{\mathbf{A}}}(\textrm {e},(b_1\equiv b_2)\vee (c_1\equiv c_2))$ . Now suppose that $(a_1,a_2)\in \mathrm{Cg}_{{\mathbf{A}}}(\textrm {e},(b_1\equiv b_2)\vee (c_1\equiv c_2))$ . It follows easily, again using some elementary properties of pointed residuated lattices, that $(a_1,a_2)\in \mathrm{Cg}_{{\mathbf{A}}}(b_1,b_2)\cap \mathrm{Cg}_{{\mathbf{A}}}(c_1,c_2)$ .⊣

Lemma 6.5. Let $\mathsf {V}$ be a Hamiltonian variety of pointed residuated lattices. Then $\mathsf {V}$ has a guarded deduction theorem.

Proof. We show that the formulas

$$ \begin{align*} \gamma:= (x_1\equiv x_2) \leq z \mathbin{\&} (y_1\equiv y_2)\vee z \approx \textrm{e} \: \text{ and } \: \varphi:= z\approx \textrm{e} \end{align*} $$

satisfy conditions (i) and (ii) in the definition of a guarded deduction theorem for a finite set $\overline {w}$ with $z\notin \overline {w}$ , terms $s_1(\overline {w}),s_2(\overline {w}),t_1(\overline {w}),t_2(\overline {w})$ , and conjunction of equations $\pi (\overline {w})$ .

For (i), suppose first that $\mathsf {V} \models (\pi \mathbin {\&} (t_1\approx t_2)) \to (s_1 \approx s_2)$ . To show that $\mathsf {V} \models \pi \to \forall z.(\gamma \to \varphi )(s_1,s_2,t_1,t_2,z)$ , consider any $\mathbf{A}\in \mathsf {V}$ and assignment $f\colon \overline {w} \to A$ such that $\mathbf{A}, f\models \pi $ , and let $g\colon \overline {w}, z\to A$ be a map extending f such that $\mathbf{A}, g\models \gamma (s_1,s_2,t_1,t_2,z)$ . Then $\mathbf{A}, g\models (s_1\equiv s_2) \leq z$ and $\mathbf{A}, g\models (t_1\equiv t_2)\vee z \approx \textrm {e}$ . It follows that also $\mathbf{A}, g\models z\leq \textrm {e}$ and hence to show that $\mathbf{A}, g\models \varphi (s_1,s_2,t_1,t_2,z)$ , it suffices to prove the following:

Claim. $\mathbf{A}, g\models \textrm {e} \leq z$ .

Proof of Claim. Let $\tilde {g}\colon \textbf {Tm}(\overline {w},z)\to \mathbf{A}$ be the unique homomorphism extending g, and define $a_1:= \tilde {g}(s_1)$ , $a_2:= \tilde {g}(s_2)$ , $b_1:= \tilde {g}(t_1)$ , $b_2:= \tilde {g}(t_2)$ , and $c:= \tilde {g}(z)$ . We prove first that $\textrm {e}\le (b_1\equiv b_2)^k \vee c$ for all $k\in \mathbb {N}^{>0}$ , proceeding by induction on k. The base case follows from the fact that $\mathbf{A}, g\models (t_1\equiv t_2)\vee z \approx \textrm {e}$ . For the inductive step, we obtain

$$ \begin{align*} \textrm{e} & \le (b_1\equiv b_2)^k \vee c && \text{by the induction hypothesis}\\ & \le (((b_1\equiv b_2) \vee c)\cdot (b_1\equiv b_2)^k) \vee c && \text{since } \textrm{e}\le(b_1\equiv b_2) \vee c\\ & = ((b_1\equiv b_2)^{k+1} \vee c\cdot (b_1\equiv b_2)^k) \vee c && \text{by the distributivity of } \cdot \text{ over } \vee\\ & \le (b_1\equiv b_2)^{k+1} \vee c && \text{since } b_1\equiv b_2\leq \textrm{e}. \end{align*} $$

Now let q denote the natural quotient map from $\mathbf{A}$ onto $\mathbf{A}/\mathrm{Cg}_{{\mathbf{A}}}(b_1,b_2)$ . By assumption, $\mathsf {V} \models (\pi \mathbin {\&} (t_1\approx t_2)) \to (s_1 \approx s_2)$ , so $\mathbf{A}/\mathrm{Cg}_{{\mathbf{A}}}(b_1,b_2), q f\models s_1\approx s_2$ , i.e., $(a_1, a_2)\in \mathrm{Cg}_{{\mathbf{A}}}(b_1,b_2)$ . By Proposition 6.3(a), we obtain $(b_1\equiv b_2)^n\leq a_1\equiv a_2$ for some $n\in \mathbb {N}$ . But $\mathbf{A}, g\models (s_1\equiv s_2) \leq z$ , so also $(a_1\equiv a_2)\leq c$ and $(b_1\equiv b_2)^n\leq c$ . Hence we get $\textrm {e}\le (b_1\equiv b_2)^n \vee c = c$ ; that is, $\mathbf{A}, g\models \textrm {e} \leq z$ .

Now suppose that $\mathsf {V} \models \pi \to \forall \overline {z}.(\gamma \to \varphi )(s_1,s_2,t_1,t_2,\overline {z})$ . To show that $\mathsf {V} \models (\pi \mathbin {\&} (t_1\approx t_2)) \to (s_1 \approx s_2)$ , consider any $\mathbf{A}\in \mathsf {V}$ and assignment $f\colon \overline {w}\to A$ such that $\mathbf{A}, f\models \pi \mathbin {\&} (t_1\approx t_2)$ . Since $z\notin \overline {w}$ , we can extend f to an assignment $g\colon \overline {w},z\to A$ by setting $g(z):= \tilde {f}(s_1\equiv s_2)$ , where $\tilde {f}\colon \textbf {Tm}(\overline {w})\to \mathbf{A}$ is the unique homomorphism extending f. Clearly, $\mathbf{A}, g\models \pi \mathbin {\&} \gamma (s_1,s_2,t_1,t_2,z)$ and hence, by assumption, $\mathbf{A}, g\models z\approx \textrm {e}$ . It follows that $\mathbf{A}, f\models (s_1\equiv s_2)\approx \textrm {e}$ , and so $\mathbf{A}, f\models s_1\approx s_2$ .

For the non-trivial direction of (ii), suppose that $\mathsf {V} \models (\pi \mathbin {\&} \gamma (s_1,s_2,t_1,t_2,\overline {z})) \to \sigma $ for some equation $\sigma (\overline {w})$ . To show that $\mathsf {V}\models \pi \to \sigma $ , consider any algebra $\mathbf{A}\in \mathsf {V}$ and assignment $f\colon \overline {w} \to A$ such that $\mathbf{A}, f\models \pi $ . Extend f to an assignment $g\colon \overline {w},z\to A$ by setting $g(z):= \textrm {e}$ . Then $\mathbf{A}, g\models \pi \mathbin {\&} \gamma (s_1,s_2,t_1,t_2,z)$ and hence, by assumption, $\mathbf{A}, f\models \sigma $ .⊣

Theorems 4.5 and 5.7 then yield the following description of Hamiltonian varieties of pointed residuated lattices whose theories have a model completion.

Theorem 6.6. Let $\mathsf {V}$ be a Hamiltonian variety of pointed residuated lattices. The theory of $\mathsf {V}$ has a model completion if, and only if, $\mathsf {V}$ is coherent and has equationally definable principal congruences, the amalgamation property, and the equational variable restriction property.

Example 6.7. Since the variety of lattice-ordered abelian groups is Hamiltonian but does not have equationally definable principal congruences, it follows directly from Theorem 6.6 that, as already mentioned in Example 5.8 and first proved in [22], its theory does not have a model completion. Similarly, the variety of MV-algebras does not have a model completion, as first proved in [28].

An analogous result to Theorem 6.6 was obtained in [27] for Hamiltonian varieties of pointed residuated lattices that are closed under canonical extensions; for this latter notion, we refer to [17, 18].

Proposition 6.8 [27, Theorem 5.11]

Let $\mathsf {V}$ be a Hamiltonian variety of pointed residuated lattices that is closed under canonical extensions. If $\mathsf {V}$ is coherent, then it has equationally definable principal congruences.

We use Proposition 6.8 to show that if a Hamiltonian semilinear variety $\mathsf {V}$ of pointed residuated lattices is closed under canonical extensions and the theory of $\mathsf {V^c}$ has a model completion, then $\mathsf {V}$ has equationally definable principal congruences.

Lemma 6.9. Let $\mathsf {V}$ be a semilinear variety of pointed residuated lattices. If $\mathsf {V^c}$ has the variable projection property, then $\mathsf {V}$ is coherent.

Proof. The claim clearly holds if $\mathsf {V^c}$ is trivial (contains only trivial algebras), so let us assume that this is not the case. Suppose that $\mathsf {V^c}$ has the variable projection property and consider a finite set $\overline {x},y$ and conjunction of equations $\varphi (\overline {x},y)$ . By assumption, there exists a quantifier-free formula $\xi (\overline {x})$ such that $\mathsf {V^c}\models \varphi \to \xi $ and for any equation $\varepsilon (\overline {x})$ ,

$$ \begin{align*} \mathsf{V^c}\models \varphi\to \varepsilon \:\Longrightarrow\: \mathsf{V^c}\models \xi\to\varepsilon. \end{align*} $$

We may assume without loss of generality that $\xi $ is a conjunction of formulas of the form $\pi \to \delta $ where $\pi $ is a (possibly empty) conjunction of equations and $\delta $ is a non-empty disjunction of equations. Using some elementary properties of pointed residuated lattices, we may also assume that $\delta $ is of the form $\textrm {e}\le s_1 \curlyvee \cdots \curlyvee \textrm {e} \le s_n$ . But also, using the fact that $\mathsf {V^c}$ consists of linearly ordered pointed residuated lattices,

$$ \begin{align*} \mathsf{V^c}\models (\textrm{e}\le s_1 \curlyvee \cdots \curlyvee \textrm{e} \le s_n) \leftrightarrow (\textrm{e} \le s_1\vee\cdots\vee s_n). \end{align*} $$

Hence we may further assume that $\xi $ is a conjunction of quasiequations. But then, since $\mathsf {V}$ and $\mathsf {V^c}$ satisfy the same quasiequations, $\mathsf {V}$ also has the variable projection property and, by Proposition 2.4, is coherent.

Proposition 6.10. Let $\mathsf {V}$ be a Hamiltonian semilinear variety of pointed residuated lattices that is closed under canonical extensions. If the theory of $\mathsf {V^c}$ has a model completion, then $\mathsf {V}$ has equationally definable principal congruences.

Proof. Suppose that the theory of $\mathsf {V^c}$ has a model completion. By Proposition 3.7, the class $\mathsf {V^c}$ has the variable projection property. Hence, by Lemma 6.9, the variety $\mathsf {V}$ is coherent and, by Proposition 6.8, has equationally definable principal congruences.⊣

Example 6.11. Consider the class $\mathsf {CRL^c}$ of linearly ordered commutative pointed residuated lattices. The variety generated by $\mathsf {CRL^c}$ is closed under canonical extensions (cf. [16, Chapter 6]) and does not have equationally definable principal congruences. So, by Proposition 6.10, the theory of $\mathsf {CRL^c}$ does not have a model completion.

Note that the Hamiltonian semilinear varieties $\mathsf {LA}$ and $\mathsf {MV}$ are coherent and do not have equationally definable principal congruences, but are not closed under canonical extensions. Moreover, as we have already seen, the theories of $\mathsf {LA^c}$ and $\mathsf {MV^c}$ have a model completion, but this is not the case for $\mathsf {LA}$ and $\mathsf {MV}$ .

7 Extending the language

Let $\mathcal {L}$ be the language of pointed residuated lattices and let $\mathcal {L}_\rhd $ be $\mathcal {L}$ extended with an additional binary operation symbol $\rhd $ . In this section, we show how to associate with any semilinear variety $\mathsf {V}$ of pointed residuated lattices, a variety $\mathsf {V_\rhd }$ of $\mathcal {L}_\rhd $ -algebras that has equationally definable principal congruences and satisfies the same universal $\mathcal {L}$ -sentences as $\mathsf {V}$ . We then show that if $\mathsf {V}$ satisfies a certain syntactic property, the theory of $\mathsf {V_\rhd }$ has a model completion. In particular, this is the case for the varieties of lattice-ordered abelian groups and MV-algebras.

Given any semilinear variety $\mathsf {V}$ of pointed residuated lattices, let $\mathsf {V^c_\rhd }$ denote the class of linearly ordered members of $\mathsf {V}$ expanded with a binary operation $\rhd $ defined by

$$ \begin{align*} x \rhd y := \begin{cases} y, & \text{if }\textrm{e} \le x,\\ \textrm{e}, & \text{otherwise.} \end{cases} \end{align*} $$

That is, $\mathsf {V^c_\rhd }$ is the positive universal class consisting of $\mathcal {L}_\rhd $ -algebras that satisfy the equational theory of $\mathsf {V}$ and the universal sentences

$$ \begin{align*} &\forall x,y \: (x\leq y \curlyvee \, y\leq x) \enspace\text{and}\enspace \\&\forall x,y \: [(\textrm{e}\leq x \, \to \, x \rhd y\approx y) \mathbin{\&} (\textrm{e}\not\leq x \, \to \, x \rhd y\approx \textrm{e}) ]. \end{align*} $$

Let $\mathsf {V_\rhd }$ be the variety generated by $\mathsf {V^c_\rhd }$ . Since $\mathsf {V^c_\rhd }$ is a positive universal class, it follows from Jónsson’s Lemma [25] that $\mathsf {V_\rhd }=\mathbb {ISP}(\mathsf {V^c_\rhd })$ . Moreover, we obtain the following conservative extension result.

Proposition 7.1. Let $\mathsf {V}$ be any semilinear variety of pointed residuated lattices. Then for any quantifier-free $\mathcal {L}$ -formula $\chi $ ,

$$ \begin{align*} \mathsf{V_\rhd} \models \chi\iff \mathsf{V} \models \chi. \end{align*} $$

Proof. Since $\mathsf {V}$ and $\mathsf {V_\rhd }$ are both varieties, they satisfy the disjunction property (see Section 2), and it therefore suffices to establish the equivalence for the case where $\chi $ is an $\mathcal {L}$ -quasiequation. Suppose first that $\mathsf {V_\rhd } \not \models \chi $ . Since the $\mathcal {L}$ -reduct of any member of $\mathsf {V_\rhd }$ belongs to $\mathsf {V}$ , also $\mathsf {V} \not \models \chi $ . Now suppose that $\mathsf {V}\not \models \chi $ . Since $\mathsf {V}$ is semilinear, $\mathsf {V}=\mathbb {ISP}(\mathsf {V^c})$ , and hence $\mathsf {V^c}\not \models \chi $ . But every member of $\mathsf {V^c}$ is the $\mathcal {L}$ -reduct of a member of $\mathsf {V_\rhd }$ , and therefore also $\mathsf {V_\rhd } \not \models \chi $ .⊣

For convenience of notation, let us define for any class $\mathsf {K}$ of algebras with a pointed residuated lattice reduct and a finite set of $\mathcal {L}$ -terms or $\mathcal {L}_\rhd $ -terms $\Gamma \cup \{t\}$ ,

It follows easily that for any conjunction of equations $\pi $ and equation $u\approx v$ ,

$$ \begin{align*} \mathsf{K}\models\pi\to u\approx v \iff \{s\equiv t \mid s\approx t \text{ is an equation of } \pi\} \models_{\mathsf{K}} u\equiv v. \end{align*} $$

We now use this notation to describe a deduction theorem for $\mathsf {V_\rhd }$ .

Proposition 7.2. Let $\mathsf {V}$ be any semilinear variety of pointed residuated lattices. Then for any finite set $\overline {x}$ and finite $\Gamma \cup \{s,t\}\subseteq \mathrm{Tm}_{{\mathcal{L}_\rhd }}(\overline {x})$ ,

$$ \begin{align*} \Gamma\cup\{s\} \models_{\mathsf{V_\rhd}} t \iff \Gamma \models_{\mathsf{V_\rhd}} s \rhd t. \end{align*} $$

Proof. Using the fact that $\mathsf {V_\rhd }=\mathbb {ISP}(\mathsf {V^c_\rhd })$ , it suffices to prove that for any finite set $\overline {x}$ and finite $\Gamma \cup \{s,t\}\subseteq \mathrm{Tm}_{\mathcal{L}_\rhd }(\overline {x})$ ,

$$ \begin{align*} \Gamma\cup\{s\} \models_{\mathsf{V^c_\rhd}} t \iff \Gamma \models_{\mathsf{V^c_\rhd}} s \rhd t. \end{align*} $$

Suppose first that $\Gamma {\cup} \{s\} \models_{\mathsf{V^c_\rhd}} t$ and consider any $\mathbf{A}{\in} \mathsf {V^c_\rhd }$ and assignment $f\colon \overline {x}{\to} A$ satisfying $\textrm {e}\le \tilde {f}(u)$ for all $u{\,\in\,} \Gamma $ . If $\tilde {f}(s){\,<\,}\textrm {e}$ , then $\textrm {e} {\,=\,}\tilde {f}(s)\rhd \tilde {f}(t) {\,=\,} \tilde {f}(s{\,\rhd\,} t)$ ; otherwise $\textrm {e}\le \tilde {f}(s)$ and, by assumption, $\textrm {e}\le \tilde {f}(t) = \tilde {f}(s)\rhd \tilde {f}(t) = \tilde {f}(s\rhd t)$ . Hence $\Gamma \models_{\mathsf{V^c_\rhd}} s \rhd t$ .

Suppose now that $\Gamma \models_{\mathsf{V^c_\rhd}} s {\,\rhd\,} t$ and consider any $\mathbf{A}{\,\in\,} \mathsf {V^c_\rhd }$ and assignment $f\colon \overline {x}{\,\to\,} A$ satisfying $\textrm {e}\le \tilde {f}(s)$ and $\textrm {e}\le \tilde {f}(u)$ for all $u\in \Gamma $ . Then, by assumption, $\textrm {e}\le \tilde {f}(s\rhd t)= \tilde {f}(s)\rhd \tilde {f}(t) = \tilde {f}(t)$ . Hence $\Gamma \cup \{s\} \models_{\mathsf{V^c_\rhd}} t$ .⊣

The next result is then a direct consequence of Proposition 4.3.

Corollary 7.3. Let $\mathsf {V}$ be any semilinear variety of pointed residuated lattices. Then $\mathsf {V_\rhd }$ has equationally definable principal congruences.

We also obtain a uniform method for transforming a disjunct in the conclusion of a consequence into a premise. For a finite set $\overline {x} = \{x_1,\dots ,x_n\}$ and $s\in \mathrm{Tm}_{\mathcal{L}_\rhd }(\overline {x})$ , let

$$ \begin{align*} \nabla s := s \rhd ((\textrm{0}\equiv\textrm{e})\wedge\!\bigwedge_{1 \le j \le n} (x_j\equiv\textrm{e})). \end{align*} $$

Lemma 7.4. Let $\mathsf {V}$ be any semilinear variety of pointed residuated lattices. Then for any finite set $\overline {x}$ and finite $\Gamma \cup \{s,t\}\subseteq \mathrm{Tm}_{\mathcal{L}_\rhd }(\overline {x})$ ,

$$ \begin{align*} \Gamma \models_{\mathsf{V_\rhd}} s\vee t \iff \Gamma\cup\{\nabla s\} \models_{\mathsf{V_\rhd}} t. \end{align*} $$

Proof. Using the fact that $\mathsf {V_\rhd }=\mathbb {ISP}(\mathsf {V^c_\rhd })$ , it suffices to prove that for any finite set $\overline {x} = \{x_1,\dots ,x_n\}$ and finite set $\Gamma \cup \{s,t\}\subseteq \mathrm{Tm}_{\mathcal{L}_\rhd }(\overline {x})$ ,

$$ \begin{align*} \Gamma \models_{\mathsf{V^c_\rhd}} s\vee t \iff \Gamma\cup\{\nabla s\} \models_{\mathsf{V^c_\rhd}} t. \end{align*} $$

Suppose first that $\Gamma \models_{\mathsf{V^c_\rhd}} s\vee t$ and consider any $\mathbf{A}\in \mathsf {V^c_\rhd }$ and assignment $f\colon \overline {x}\to A$ such that $\textrm {e}\le \tilde {f}(\nabla s)$ and $\textrm {e}\le \tilde {f}(u)$ for all $u\in \Gamma $ . Then, by assumption, $\textrm {e} \le \tilde {f}(s\vee t)$ . If $\textrm {e}\le \tilde {f}(s)$ , then $\textrm {e}\le \tilde {f}(\nabla s)=\tilde {f}((\textrm { 0}\equiv \textrm {e})\wedge \bigwedge _{1 \le j \le n} (x_j\equiv \textrm {e}))$ , yielding $\textrm {0} =\tilde {f}(x_1)=\cdots = \tilde {f}(x_n)=\textrm { e}$ and, inductively, $\tilde {f}(t)=\textrm {e}$ . Otherwise, $\textrm {e} \le \tilde {f}(t)$ . Hence $\Gamma \cup \{\nabla s\} \models_{\mathsf{V^c_\rhd}} t$ .

Suppose next that $\Gamma \cup \{\nabla s\} \models_{\mathsf{V^c_\rhd}} t$ and consider any $\mathbf{A}\in \mathsf {V^c_\rhd }$ and assignment $f\colon \overline {x}\to A$ such that $\textrm {e}\le \tilde {f}(u)$ for all $u\in \Gamma $ . If $\textrm {e} \le \tilde {f}(s)$ , then $\textrm {e}\le \tilde {f}(s\vee t)$ . Otherwise, $\tilde {f}(\nabla s)=\textrm {e}$ and, by assumption, $\textrm {e}\le \tilde {f}(t)$ , yielding $\textrm {e}\le \tilde {f}(s\vee t)$ . Hence $\Gamma \models_{\mathsf{V^c_\rhd}} s\vee t$ .⊣

The next lemma provides a uniform method for eliminating occurrences of $\rhd $ from $\mathcal {L}_\rhd $ -quasiequations while preserving validity in $\mathsf {V_\rhd }$ . To avoid multiple case distinctions, we introduce a new symbol $\Lambda $ , fixing $s\vee \Lambda := s$ , $\Lambda \vee s:= s$ , $\nabla \Lambda :=\textrm {e}$ for any $\mathcal {L}_\rhd $ -term s.

Lemma 7.5. Let $\mathsf {V}$ be any semilinear variety of pointed residuated lattices. For any finite set $\overline {x}$ , $s\in \mathrm{Tm}_{\mathcal{L}_\rhd }(\overline {x})$ , and $t\in \mathrm{Tm}_{\mathcal{L}_\rhd }(\overline {x})\cup \{\Lambda \}$ , there exist a finite non-empty set I and $s^{\prime }_i\in \mathrm{Tm}_{\mathcal {L}}(\overline {x})$ , $t^{\prime }_i\in \mathrm{Tm}_{\mathcal {L}}(\overline {x})\cup \{\Lambda \}$ for each $i\in I$ such that for any $u,v \in \mathrm{Tm}_{\mathcal{L}_\rhd}(\overline {x},\overline {y})$ ,

$$ \begin{align*} \{u \wedge s\} \models_{\mathsf{V_\rhd}} t \vee v \iff \forall i\in I\colon\{u \wedge s^{\prime}_i\} \models_{\mathsf{V_\rhd}} t^{\prime}_i \vee v. \end{align*} $$

Proof. Let $s'[t']$ denote the result of replacing some distinguished occurrence of a variable in a term $s'$ by a term $t'$ . For $s = s'[s_1\rhd s_2]$ and any $u,v \in \mathrm{Tm}_{\mathcal{L}_\rhd}(\overline {x},\overline {y})$ ,

$$ \begin{align*} \{u \wedge s\} \models_{\mathsf{V_\rhd}} t \vee v \iff & \{u \wedge s'[s_2] \wedge s_1\} \models_{\mathsf{V_\rhd}} t \vee v \:\text{ and }\: \\ &\{u \wedge s'[\textrm{e}]\} \models_{\mathsf{V_\rhd}} t \vee s_1 \vee v. \end{align*} $$

Similarly, for $t = t'[t_1\rhd t_2]$ and any $u,v \in \mathrm{Tm}_{\mathcal{L}_\rhd}(\overline {x},\overline {y})$ ,

$$ \begin{align*} \{u \wedge s\} \models_{\mathsf{V_\rhd}} t \vee v \iff & \{u \wedge s \wedge t_1\} \models_{\mathsf{V_\rhd}} t'[t_2] \vee v \:\text{ and }\:\\& \{u \wedge s\} \models_{\mathsf{V_\rhd}} t'[\textrm{e}] \vee t_1 \vee v. \end{align*} $$

Iterating these steps yields the required finite set I and $s^{\prime }_i,t^{\prime }_i\in \mathrm{Tm}_{\mathcal {L}}(\overline {x})$ for each $i\in I$ .⊣

We now provide sufficient conditions for a semilinear variety of pointed residuated lattices $\mathsf {V}$ to ensure that the theory of $\mathsf {V_\rhd }$ has a model completion.

Theorem 7.6. Let $\mathsf {V}$ be any semilinear variety of pointed residuated lattices such that for any finite set $\overline {x},y$ and $s(\overline {x},y)\in \mathrm{Tm}_{\mathcal {L}}(\overline {x},y)$ , $t(\overline {x},y)\in \mathrm{Tm}_{\mathcal {L}}(\overline {x},y)\cup \{\Lambda \}$ , there exist a finite non-empty set K and $s^{\prime }_k(\overline {x})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x})$ , $t^{\prime }_k(\overline {x})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x})\cup \{\Lambda \}$ for each $k\in K$ satisfying for any $u(\overline {x},\overline {z}),v(\overline {x},\overline {z})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x},\overline {z})$ ,

$$ \begin{align*} &\{u(\overline{x},\overline{z})\wedge s(\overline{x},y)\} \models_{\mathsf{V}} t(\overline{x},y)\vee v(\overline{x},\overline{z})\\ &\iff \forall k\in K\colon\{u(\overline{x},\overline{z})\wedge s^{\prime}_k(\overline{x})\} \models_{\mathsf{V}} t^{\prime}_k(\overline{x})\vee v(\overline{x},\overline{z}). \end{align*} $$

Then the theory of $\mathsf {V_\rhd }$ has a model completion.

Proof. From Corollary 7.3, we know that $\mathsf {V_\rhd }$ has equationally definable principal congruences. Hence, to conclude using Proposition 4.7 that the theory of $\mathsf {V_\rhd }$ has a model completion, it remains to prove that $\mathsf {V_\rhd }$ is coherent and has the amalgamation property and equational variable restriction property.

For coherence, it suffices to show that for any finite set $\overline {x},y$ and $s(\overline {x},y)\in \mathrm{Tm}_{\mathcal{L}_\rhd}(\overline {x},y)$ , there exists an $s^\star (\overline {x})\in \mathrm{Tm}_{\mathcal{L}_\rhd}(\overline {x})$ such that for any $v(\overline {x}) \in \mathrm{Tm}_{\mathcal{L}_\rhd}(\overline {x})$ ,

$$ \begin{align*} \{s(\overline{x},y)\} \models_{\mathsf{V_\rhd}} v(\overline{x}) \iff \{s^\star(\overline{x})\} \models_{\mathsf{V_\rhd}} v(\overline{x}). \end{align*} $$

By Lemma 7.5 (with $t=\Lambda $ ), there exist a finite non-empty set I and $s^{\prime }_i(\overline {x},y)\in \mathrm{Tm}_{\mathcal {L}}(\overline {x},y)$ , $t^{\prime }_i(\overline {x},y)\in \mathrm{Tm}_{\mathcal {L}}(\overline {x},y)\cup \{\Lambda \}$ ( $i\in I$ ) such that for any $v(\overline {x}) \in \mathrm{Tm}_{\mathcal{L}_\rhd}(\overline {x})$ ,

(10) $$ \begin{align} \{s(\overline{x},y)\} \models_{\mathsf{V_\rhd}} v(\overline{x}) & \iff \forall i\in I\colon\{s^{\prime}_i(\overline{x},y)\} \models_{\mathsf{V_\rhd}} t^{\prime}_i(\overline{x},y)\vee v(\overline{x}). \end{align} $$

By assumption, there exist for each $i\in I$ , a finite non-empty set $K_i$ and $s^{\prime \prime }_{i,k}(\overline {x})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x})$ , $t^{\prime \prime }_{i,k}(\overline {x})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x})\cup \{\Lambda \}$ ( $k\in K_i$ ) satisfying for any $u'(\overline {x}),v'(\overline {x})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x})$ ,

(11) $$ \begin{align} \begin{split} \{u'(\overline{x})\wedge s^{\prime}_i(\overline{x},y)\} & \models_{\mathsf{V}} t^{\prime}_i(\overline{x},y)\vee v'(\overline{x})\\ & \iff \forall k\in K_i\colon \{u'(\overline{x})\wedge s^{\prime\prime}_{i,k}(\overline{x})\} \models_{\mathsf{V}} t^{\prime\prime}_{i,k}(\overline{x})\vee v'(\overline{x}). \end{split} \end{align} $$

We define now

$$ \begin{align*} s^\star(\overline{x}):= \bigvee_{i\in I}\bigvee_{k\in K_i}\left(s^{\prime\prime}_{i,k}(\overline{x}) \wedge \nabla t^{\prime\prime}_{i,k}(\overline{x})\right). \end{align*} $$

Consider any $v(\overline {x})\in \mathrm{Tm}_{\mathcal{L}_\rhd}(\overline {x})$ . By Lemma 7.5 (with $s=\textrm {e}$ ), there exist a finite non-empty set J and $u^{\prime }_j(\overline {x})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x})$ , $v^{\prime }_j(\overline {x})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x})\cup \{\Lambda \}$ ( $j\in J$ ) such that for any $s'(\overline {x},y),t'(\overline {x},y)\in \mathrm{Tm}_{\mathcal{L}_\rhd}(\overline {x},y)$ ,

$$ \begin{align*} &\{s'(\overline{x},y)\} \models_{\mathsf{V_\rhd}} t'(\overline{x},y)\vee v(\overline{x}) \\ &\iff \forall j\in J\colon\{u^{\prime}_j(\overline{x})\wedge s'(\overline{x},y)\} \models_{\mathsf{V_\rhd}}t'(\overline{x},y)\vee v^{\prime}_j(\overline{x}). \end{align*} $$

In particular, for each $i \in I$ and $k\in K_i$ ,

(12) $$ \begin{align} &\{s^{\prime}_i(\overline{x},y)\} \models_{\mathsf{V_\rhd}} t^{\prime}_i(\overline{x},y)\vee v(\overline{x})\nonumber\\ & \iff \forall j\in J\colon\{u^{\prime}_j(\overline{x})\wedge s^{\prime}_i(\overline{x},y)\} \models_{\mathsf{V_\rhd}} t^{\prime}_i(\overline{x},y)\vee v^{\prime}_j(\overline{x}), \end{align} $$

(13) $$ \begin{align} \{s^{\prime\prime}_{i,k}(\overline{x})\} \models_{\mathsf{V_\rhd}} t^{\prime\prime}_{i,k}(\overline{x})\vee v(\overline{x}) & \iff \forall j\in J\colon\{u^{\prime}_j(\overline{x})\wedge s^{\prime\prime}_{i,k}(\overline{x})\} \models_{\mathsf{V_\rhd}} t^{\prime\prime}_{i,k}(\overline{x})\vee v^{\prime}_j(\overline{x}). \end{align} $$

Putting these equivalences together, it follows that

$$ \begin{align*} &\{s(\overline{x},y)\} \models_{\mathsf{V_\rhd}} v(\overline{x})\\ &\qquad \iff \forall i\in I\colon\{s^{\prime}_i(\overline{x},y)\} \models_{\mathsf{V_\rhd}} t^{\prime}_i(\overline{x},y) \vee v(\overline{x}) & \text{by (10)}\\ &\qquad\iff \forall i\in I,j\in J\colon\{u^{\prime}_j(\overline{x})\wedge s^{\prime}_i(\overline{x},y)\} \models_{\mathsf{V_\rhd}} t^{\prime}_i(\overline{x},y)\vee v^{\prime}_j(\overline{x}) & \text{by (12)}\\ & \qquad\iff \forall i\in I,j\in J\colon\{u^{\prime}_j(\overline{x})\wedge s^{\prime}_i(\overline{x},y)\} \models_{\mathsf{V}} t^{\prime}_i(\overline{x},y)\vee v^{\prime}_j(\overline{x}) & \text{Prop. 7.1}\\ & \qquad\iff \forall i\in I,j\in J,k\in K_i\colon\{u^{\prime}_j(\overline{x})\wedge s^{\prime\prime}_{i,k}(\overline{x})\} \models_{\mathsf{V}} t^{\prime\prime}_{i,k}(\overline{x})\vee v^{\prime}_j(\overline{x}) & \text{by (11)}\\ & \qquad\iff \forall i\in I,j\in J,k\in K_i\colon\{u^{\prime}_j(\overline{x})\wedge s^{\prime\prime}_{i,k}(\overline{x})\} \models_{\mathsf{V_\rhd}} t^{\prime\prime}_{i,k}(\overline{x})\vee v^{\prime}_j(\overline{x}) & \text{Prop. 7.1}\\ &\qquad \iff \forall i\in I,k\in K_i\colon\{s^{\prime\prime}_{i,k}(\overline{x})\} \models_{\mathsf{V_\rhd}} t^{\prime\prime}_{i,k}(\overline{x})\vee v(\overline{x}) & \text{by (13)}\\ &\qquad \iff \forall i\in I,k\in K_i\colon\{s^{\prime\prime}_{i,k}(\overline{x})\wedge \nabla t^{\prime\prime}_{i,k}(\overline{x})\} \models_{\mathsf{V_\rhd}} v(\overline{x}) & \text{Lem. 7.4}\\ &\qquad \iff \{s^\star(\overline{x})\} \models_{\mathsf{V_\rhd}} v(\overline{x}). \end{align*} $$

For the amalgamation property and equational variable restriction property, it suffices by Corollary 4.10 to show that for any finite set $\overline {x},y$ and $t(\overline {x},y)\in \mathrm{Tm}_{\mathcal{L}_\rhd}(\overline {x},y)$ , either $\{w(\overline {x})\}\not \models_{\mathsf{V_\rhd}} t(\overline {x},y)$ for all $w(\overline {x})\in \mathrm{Tm}_{\mathcal{L}_\rhd}(\overline {x})$ (taking care of the case in Corollary 4.10 where $\pi (\overline {x})$ is $\bot $ ) or there exists a $t^\star (\overline {x})\in \mathrm{Tm}_{\mathcal{L}_\rhd}(\overline {x})$ such that for any $u(\overline {x},\overline {z}) \in \mathrm{Tm}_{\mathcal{L}_\rhd}(\overline {x},\overline {z})$ ,

$$ \begin{align*} \{u(\overline{x},\overline{z})\} \models_{\mathsf{V_\rhd}} t(\overline{x},y) \iff \{u(\overline{x},\overline{z})\} \models_{\mathsf{V_\rhd}} t^\star(\overline{x}). \end{align*} $$

Suppose then that $\{w(\overline {x})\} \models_{\mathsf{V_\rhd}} t(\overline {x},y)$ for some $w(\overline {x})\in \mathrm{Tm}_{\mathcal{L}_\rhd}(\overline {x})$ . By iteratively replacing $w'[w_1\rhd w_2]$ with $w'[w_2]\wedge w_1$ , we may assume without loss of generality that $w(\overline {x})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x})$ . Next, by Lemma 7.5 (with $s=\textrm {e}$ ), there exist a finite non-empty set I and $s^{\prime }_i(\overline {x},y),t^{\prime }_i(\overline {x},y)\in \mathrm{Tm}_{\mathcal {L}}(\overline {x},y)$ ( $i\in I$ ) such that for any $u(\overline {x},\overline {z})\in \mathrm{Tm}_{\mathcal{L}_\rhd}(\overline {x},\overline {z})$ ,

(14) $$ \begin{align} \{u(\overline{x},\overline{z})\} \models_{\mathsf{V_\rhd}} t(\overline{x},y) & \iff \forall i\in I\colon\{u(\overline{x},\overline{z})\wedge s^{\prime}_i(\overline{x},y)\} \models_{\mathsf{V_\rhd}} t^{\prime}_i(\overline{x},y). \end{align} $$

Let us temporarily fix $i\in I$ . By assumption, there exist a finite non-empty set $K_i$ and $s^{\prime \prime }_{i,k}(\overline {x})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x})$ , $t^{\prime \prime }_{i,k}(\overline {x})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x})\cup \{\Lambda \}$ ( $k\in K_i$ ) such that for any $u'(\overline {x},\overline {z}),v'(\overline {x},\overline {z})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x},\overline {z})$ ,

(15) $$ \begin{align} \begin{split} \{u'(\overline{x},\overline{z}) & \wedge s^{\prime}_i(\overline{x},y)\} \models_{\mathsf{V}} t^{\prime}_i(\overline{x},y)\vee v'(\overline{x},\overline{z})\\ & \iff \forall k\in K_i\colon \{u'(\overline{x},\overline{z})\wedge s^{\prime\prime}_{i,k}(\overline{x})\} \models_{\mathsf{V}} t^{\prime\prime}_{i,k}(\overline{x})\vee v'(\overline{x},\overline{z}). \end{split} \end{align} $$

Since $\{w(\overline {x})\} \models_{\mathsf{V_\rhd}} t(\overline {x},y)$ , by (14) and Proposition 7.1, also $\{w(\overline {x})\wedge s^{\prime }_i(\overline {x},y)\} \models _{\mathsf {V}} t^{\prime }_i(\overline {x},y)$ . Let $t^{\prime \prime \prime }_{i,k}(\overline {x}) := t^{\prime \prime }_{i,k}(\overline {x}) \vee w(\overline {x})$ for each $k\in K_i$ . Then for any $u'(\overline {x},\overline {z}),v'(\overline {x},\overline {z})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x},\overline {z})$ ,

(16) $$ \begin{align} \begin{split} \{u'(\overline{x},\overline{z}) &\wedge s^{\prime}_i(\overline{x},y)\} \models_{\mathsf{V_\rhd}} t^{\prime}_i(\overline{x},y)\vee v'(\overline{x},\overline{z})\\ & \iff \forall k\in K_i\colon\{u'(\overline{x},\overline{z})\wedge s^{\prime\prime}_{i,k}(\overline{x})\} \models_{\mathsf{V_\rhd}} t^{\prime\prime\prime}_{i,k}(\overline{x})\vee v'(\overline{x},\overline{z}). \end{split} \end{align} $$

The left-to-right direction of this equivalence is immediate. For the converse direction,

$$ \begin{align*} & \forall k\in K_i\colon\{u'(\overline{x},\overline{z})\wedge s^{\prime\prime}_{i,k}(\overline{x})\} \models_{\mathsf{V_\rhd}} t^{\prime\prime\prime}_{i,k}(\overline{x})\vee v'(\overline{x},\overline{z})\\ & \Longrightarrow \forall k\in K_i\colon\{u'(\overline{x},\overline{z})\wedge s^{\prime\prime}_{i,k}(\overline{x})\} \models_{\mathsf{V}} t^{\prime\prime\prime}_{i,k}(\overline{x})\vee v'(\overline{x},\overline{z}) \kern90pt \text{Prop. 7.1}\\ & \Longrightarrow \{u'(\overline{x},\overline{z})\wedge s^{\prime}_i(\overline{x},y)\}\models_{\mathsf{V}} t^{\prime}_i(\overline{x},y)\vee w(\overline{x}) \vee v'(\overline{x},\overline{z}) \kern97pt \text{by (15)}\\ & \Longrightarrow \{u'(\overline{x},\overline{z})\wedge s^{\prime}_i(\overline{x},y)\}\models_{\mathsf{V}} t^{\prime}_i(\overline{x},y)\vee v'(\overline{x},\overline{z})\quad \ \ \text{since } \{w(\overline{x})\wedge s^{\prime}_i(\overline{x},y)\} \models_{\mathsf{V}} t^{\prime}_i(\overline{x},y)\\ & \Longrightarrow \{u'(\overline{x},\overline{z})\wedge s^{\prime}_i(\overline{x},y)\}\models_{\mathsf{V_\rhd}} t^{\prime}_i(\overline{x},y)\vee v'(\overline{x},\overline{z})\kern111pt \text{Prop. 7.1}. \end{align*} $$

We define now

$$ \begin{align*} t^\star(\overline{x}):= \bigwedge_{i\in I}\bigwedge_{k\in K_i} \left(s^{\prime\prime}_{i,k}(\overline{x}) \rhd t^{\prime\prime\prime}_{i,k}(\overline{x})\right). \end{align*} $$

Consider any $u(\overline {x},\overline {z})\in \mathrm{Tm}_{\mathcal{L}_\rhd}(\overline {x},\overline {z})$ . By Lemma 7.5 (with $t=\Lambda $ ), there exist a finite non-empty set J and $u^{\prime }_j(\overline {x},\overline {z})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x},\overline {z})$ , $v^{\prime }_j(\overline {x},\overline {z})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x},\overline {z})\cup \{\Lambda \}$ ( $j\in J$ ) such that for any $s'(\overline {x},y),t'(\overline {x},y)\in \mathrm{Tm}_{\mathcal{L}_\rhd}(\overline {x},y)$ ,

$$ \begin{align*} &\{u(\overline{x},\overline{z})\wedge s'(\overline{x},y)\} \models_{\mathsf{V_\rhd}} t'(\overline{x},y) \\&\iff \forall j\in J\colon\{u^{\prime}_j(\overline{x},\overline{z})\wedge s'(\overline{x},y)\} \models_{\mathsf{V_\rhd}}t'(\overline{x},y)\vee v^{\prime}_j(\overline{x},\overline{z}). \end{align*} $$

In particular, for each $i \in I$ and $k\in K_i$ ,

(17) $$ \begin{align} \begin{split} \{u(\overline{x},\overline{z}) \wedge s^{\prime}_i(\overline{x},y)\} & \models_{\mathsf{V_\rhd}} t^{\prime}_i(\overline{x},y)\\ & \iff \forall j\in J\colon\{u^{\prime}_j(\overline{x},\overline{z}) \wedge s^{\prime}_i(\overline{x},y)\} \models_{\mathsf{V_\rhd}} t^{\prime}_i(\overline{x},y)\vee v^{\prime}_j(\overline{x},\overline{z}), \end{split} \end{align} $$

(18) $$ \begin{align} \begin{split} \{u(\overline{x},\overline{z}) \wedge s^{\prime\prime}_{i,k}(\overline{x})\} & \models_{\mathsf{V_\rhd}} t^{\prime\prime\prime}_{i,k}(\overline{x})\\ & \iff \forall j\in J\colon\{u^{\prime}_j(\overline{x},\overline{z}) \wedge s^{\prime\prime}_{i,k}(\overline{x})\} \models_{\mathsf{V_\rhd}} t^{\prime\prime\prime}_{i,k}(\overline{x})\vee v^{\prime}_j(\overline{x},\overline{z}). \end{split} \end{align} $$

Putting these equivalences together, it follows that

$$ \begin{align*} & \{u(\overline{x},\overline{z})\} \models_{\mathsf{V_\rhd}} t(\overline{x},y)\\ & \iff \forall i\in I\colon\{u(\overline{x},\overline{z}) \wedge s^{\prime}_i(\overline{x},y)\} \models_{\mathsf{V_\rhd}} t^{\prime}_i(\overline{x},y) & \text{by (14)}\\ & \iff \forall i\in I,j\in J\colon\{u^{\prime}_j(\overline{x},\overline{z}) \wedge s^{\prime}_i(\overline{x},y)\} \models_{\mathsf{V_\rhd}} t^{\prime}_i(\overline{x},y)\vee v^{\prime}_j(\overline{x},\overline{z}) & \text{by (17)}\\ & \iff \forall i\in I,j\in J,k\in K_i\colon\{u^{\prime}_j(\overline{x},\overline{z}) \wedge s^{\prime\prime}_{i,k}(\overline{x})\} \models_{\mathsf{V_\rhd}} t^{\prime\prime\prime}_{i,k}(\overline{x})\vee v^{\prime}_j(\overline{x},\overline{z}) & \text{by (16)}\\ & \iff \forall i\in I,k\in K_i\colon\{u(\overline{x},\overline{z}) \wedge s^{\prime\prime}_{i,k}(\overline{x})\} \models_{\mathsf{V_\rhd}} t^{\prime\prime\prime}_{i,k}(\overline{x}) & \text{by (18)}\\ & \iff \forall i\in I,k\in K_i\colon\{u(\overline{x},\overline{z})\} \models_{\mathsf{V_\rhd}} s^{\prime\prime}_{i,k}(\overline{x}) \rhd t^{\prime\prime\prime}_{i,k}(\overline{x}) & \text{Prop. 7.2}\\ & \iff \{u(\overline{x},\overline{z})\} \models_{\mathsf{V_\rhd}} t^\star(\overline{x}). & \\[-32pt]\end{align*} $$

⊣

In particular, the conditions of Theorem 7.6 are satisfied when $\mathsf {V}$ is the variety $\mathsf {LA}$ of lattice-ordered abelian groups.

Theorem 7.7. The theory of $\mathsf {LA_\rhd }$ has a model completion.

Proof. Recall that $\mathsf {LA}$ is generated as a quasivariety by the lattice-ordered abelian group $\textbf {R}=\langle \mathbb {R},\min ,\max ,+,-,0\rangle $ (see, e.g., [1]). Hence, to show that $\mathsf {LA_\rhd }$ has a model completion, it suffices to check the condition of Theorem 7.6 with $\models _{\mathsf {V}}$ replaced by $\models _{\textbf {R}}$ .

We proceed in two stages. Suppose first that $\overline {x},y$ is a finite set, $s(\overline {x},y)\in \mathrm{Tm}_{\mathcal {L}}(\overline {x},y)$ is a meet of group terms, and $t(\overline {x},y)\in \mathrm{Tm}_{\mathcal {L}}(\overline {x},y)\cup \{\Lambda \}$ is $\Lambda $ or a join of group terms. We prove that there exist $s'(\overline {x})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x})$ , $t'(\overline {x})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x})\cup \{\Lambda \}$ satisfying for any $u(\overline {x},\overline {z}),v(\overline {x},\overline {z})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x},\overline {z})$ ,

$$ \begin{align*} \{u(\overline{x},\overline{z}){\wedge} s(\overline{x},y)\} \models_{\textbf{R}} t(\overline{x},y){\vee} v(\overline{x},\overline{z}){\,\iff\,} \{u(\overline{x},\overline{z}){\wedge} s'(\overline{x})\} \models_{\textbf{R}} t'(\overline{x}){\vee} v(\overline{x},\overline{z}). \end{align*} $$

It is easily checked in $\textbf {R}$ that for any $\mathcal {L}$ -terms $u,v,w$ and $k\in \mathbb {N}^{>0}$ ,

$$ \begin{align*} \{u \wedge v\} \models_{\textbf{R}} w \iff \{u \wedge kv\} \models_{\textbf{R}} w \enspace\text{and}\enspace \{u\} \models_{\textbf{R}} v \vee w \iff \{u\} \models_{\textbf{R}} v \vee kw. \end{align*} $$

Also, $\textbf {R}\models x + (y \wedge z) \approx (x+y)\wedge (x+z)$ and $\textbf {R}\models x + (y \vee z) \approx (x+y)\vee (x+z)$ . Hence, reasoning in $\textbf {R}$ , we may assume that there exist a $k\in \mathbb {N}^{>0}$ and $s_0(\overline {x}),s_1(\overline {x}),s_2(\overline {x}),t_1(\overline {x}),t_2(\overline {x})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x})$ , $t_0(\overline {x})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x})\cup \{\Lambda \}$ such that $s(\overline {x},y)$ is the meet of $s_0(\overline {x})$ and some members (possibly none) of $\{s_1(\overline {x}) +ky, s_2(\overline {x})-ky\}$ , and $t(\overline {x},y)$ is the join of $t_0(\overline {x})$ and some members (possibly none) of $\{t_1(\overline {x}) + ky,t_2(\overline {x})-ky\}$ . We construct $s'(\overline {x})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x})$ , $t'(\overline {x})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x})\cup \{\Lambda \}$ as follows. Let $s'(\overline {x}):= s_0(\overline {x}) \wedge (s_1(\overline {x})+s_2(\overline {x}))$ if $s_1(\overline {x}) +ky$ and $s_2(\overline {x})-ky$ occur in $s(\overline {x},y)$ ; otherwise $s'(\overline {x}):= s_0(\overline {x})$ . The term $t'(\overline {x})$ is the join of $t_0(\overline {x})$ and (i) $t_1(\overline {x})+t_2(\overline {x})$ if $t_1(\overline {x}) + ky$ and $t_2(\overline {x})-ky$ occur in $t(\overline {x},y)$ ; (ii) $t_1(\overline {x})-s_1(\overline {x})$ if $s_1(\overline {x}) +ky$ occurs in $s(\overline {x},y)$ and $t_1(\overline {x}) + ky$ occurs in $t(\overline {x},y)$ ; and (iii) $t_2(\overline {x})-s_2(\overline {x})$ if $s_2(\overline {x})-ky$ occurs in $s(\overline {x},y)$ and $t_2(\overline {x}) - ky$ occurs in $t(\overline {x},y)$ .

We check the case where $s(\overline {x},y)= (s_1(\overline {x}) +ky)\wedge (s_2(\overline {x})-ky)$ , $t(\overline {x},y) = (t_1(\overline {x}) + ky)\vee (t_2(\overline {x})-ky)$ , $s'(\overline {x}) = s_1(\overline {x})+s_2(\overline {x})$ , and $t'(\overline {x}) = (t_1(\overline {x})+t_2(\overline {x}))\vee (t_1(\overline {x})-s_1(\overline {x}))\vee (t_2(\overline {x})-s_2(\overline {x}))$ , other cases being very similar. Let $u(\overline {x},\overline {z}),v(\overline {x},\overline {z})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x},\overline {z})$ and suppose first that $\{u(\overline {x},\overline {z})\wedge s'(\overline {x})\} \models _{\textbf {R}} t'(\overline {x})\vee v(\overline {x},\overline {z})$ . Since $\{s(\overline {x},y)\}\models _{\textbf {R}}s'(\overline {x})$ and $\{s(\overline {x})\wedge t'(\overline {x})\}\models _{\textbf {R}}t(\overline {x},y)$ , it follows that $\{u(\overline {x},\overline {z})\wedge s(\overline {x},y)\} \models _{\textbf {R}} t(\overline {x},y)\vee v(\overline {x},\overline {z})$ . Now suppose that $\{u(\overline {x},\overline {z})\wedge s'(\overline {x})\}\not \models _{\textbf {R}}t'(\overline {x})\vee v(\overline {x},\overline {z})$ ; that is, some assignment $f\colon \overline {x},\overline {z}\to \mathbb {R}$ satisfies $0\le \tilde {f}(u(\overline {x},\overline {z}))$ , $0\le \tilde {f}(s_1(\overline {x}))+ \tilde {f}(s_2(\overline {x}))$ , $\tilde {f}(t_1(\overline {x}))+\tilde {f}(t_2(\overline {x}))<0$ , $\tilde {f}(t_1(\overline {x}))<\tilde {f}(s_1(\overline {x}))$ , $\tilde {f}(t_2(\overline {x}))<\tilde {f}(s_2(\overline {x}))$ , and $\tilde {f}(v(\overline {x},\overline {z}))<0$ . We extend f to an assignment $g\colon \overline {x},y,\overline {z}\to \mathbb {R}$ by defining

$$ \begin{align*} g(y):=\frac{\min{(\tilde{f}(s_2),-\tilde{f}(t_1))}+\max{(-\tilde{f}(s_1),\tilde{f}(t_2))}}{2k}. \end{align*} $$

We obtain $0\le \tilde {g}(u(\overline {x},\overline {z}))$ , $0\le \tilde {g}(s_1(\overline {x}))+\tilde {g}(ky)$ , $\tilde {g}(ky)\le \tilde {g}(s_2(\overline {x}))$ , $\tilde {g}(t_1(\overline {x})) + \tilde {g}(ky) <0$ , $\tilde {g}(t_2(\overline {x}))<\tilde {g}(ky)$ , and $\tilde {g}(v(\overline {x},\overline {z}))<0$ . So $\{u(\overline {x},\overline {z})\wedge s(\overline {x},y)\}\not \models _{\textbf {R}}t(\overline {x},y)\vee v(\overline {x},\overline {z})$ .

We now prove that for any finite set $\overline {x},y$ and $s(\overline {x},y)\in \mathrm{Tm}_{\mathcal {L}}(\overline {x},y)$ , $t(\overline {x},y)\in \mathrm{Tm}_{\mathcal {L}}(\overline {x},y)\cup \{\Lambda \}$ , there exist a finite non-empty set K and $s^{\prime }_k(\overline {x})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x})$ , $t^{\prime }_k(\overline {x})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x})\cup \{\Lambda \}$ ( $k\in K$ ) satisfying for any $u(\overline {x},\overline {z}),v(\overline {x},\overline {z})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x},\overline {z})$ ,

$$ \begin{align*} &\{u(\overline{x},\overline{z})\wedge s(\overline{x},y)\} \models_{\textbf{R}} t(\overline{x},y)\vee v(\overline{x},\overline{z}) \\&\iff \forall k\in K\colon\{u(\overline{x},\overline{z})\wedge s^{\prime}_k(\overline{x})\} \models_{\textbf{R}} t^{\prime}_k(\overline{x})\vee v(\overline{x},\overline{z}). \end{align*} $$

By the distributivity properties of $\textbf {R}$ , we may assume that $s(\overline {x},y)$ is $s_1(\overline {x},y)\vee \cdots \vee s_n(\overline {x},y)$ , where each $s_i(\overline {x},y)$ is a meet of group terms, and that $t(\overline {x},y)$ is $t_1(\overline {x},y)\wedge \cdots \wedge t_m(\overline {x},y)$ , where either each $t_j(\overline {x},y)$ is a join of group terms or $m=1$ and $t_1(\overline {x},y)=\Lambda $ . Using the first part of this proof, for each $i\in \{1,\dots ,n\}$ and $j\in \{1,\dots ,m\}$ , there exist $s^{\prime }_{i,j}(\overline {x})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x})$ and $t^{\prime }_{i,j}(\overline {x})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x})\cup \{\Lambda \}$ satisfying for any $u(\overline {x},\overline {z}),v(\overline {x},\overline {z})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x},\overline {z})$ ,

$$ \begin{align*} &\{u(\overline{x},\overline{z})\wedge s_i(\overline{x},y)\} \models_{\textbf{R}} t_j(\overline{x},y)\vee v(\overline{x},\overline{z})\\&\iff \{u(\overline{x},\overline{z})\wedge s^{\prime}_{i,j}(\overline{x})\} \models_{\textbf{R}} t^{\prime}_{i,j}(\overline{x})\vee v(\overline{x},\overline{z}). \end{align*} $$

Hence for any $u(\overline {x},\overline {z}),v(\overline {x},\overline {z})\in \mathrm{Tm}_{\mathcal {L}}(\overline {x},\overline {z})$ ,

$$ \begin{align*} & \{u(\overline{x},\overline{z}) \wedge s(\overline{x},y)\} \models_{\textbf{R}} t(\overline{x},y) \vee v(\overline{x},\overline{z}) \\ &\ \iff \forall i\in\{1,\dots,n\},j\in\{1,\dots,m\}\colon \{u(\overline{x},\overline{z})\wedge s^{\prime}_{i,j}(\overline{x})\} \models_{\textbf{R}} t^{\prime}_{i,j}(\overline{x})\vee v(\overline{x},\overline{z}). \\[-36pt]\end{align*} $$

⊣

The variety $\mathsf {MV_\rhd }$ of MV-algebras extended with $\rhd $ is term-equivalent to the variety $\mathsf {MV}_{\!\Delta }$ of MV $_{\!\Delta }$ -algebras (see, e.g., [23, 33]), generated by linearly ordered MV-algebras extended with an additional unary operator $\Delta $ defined by

$$ \begin{align*} \Delta x := \begin{cases} 1, & \text{if }x=1,\\ 0, & \text{otherwise.} \end{cases} \end{align*} $$

For any algebra in $\mathsf {MV_\rhd }$ , we let $\Delta x:= (x\rhd 0)\rhd 0$ , and for any algebra in $\mathsf {MV}_{\!\Delta }$ , we let $x\rhd y:= \lnot \Delta x \oplus y$ . The following theorem may therefore be proved along the same lines as Theorem 7.7, using the fact that $\mathsf {MV}$ is generated as a quasivariety by the algebra $\langle [0,1],\oplus ,\lnot ,0\rangle $ , where $x\oplus y:= \min {(1,x+y)}$ and $\lnot x:=1-x$ (see, e.g., [10]).

Theorem 7.8. The theory of $\mathsf {MV}_{\!\Delta }$ has a model completion.

A different proof of this last result (obtained by giving an explicit axiomatization) was presented by X. Caicedo at the conference Residuated Structures: Algebra and Logic in 2008. Caicedo also presented a proof (again by giving an explicit axiomatization) at the Latin American Algebra Colloquium in 2019 that the theory of the class of so-called “pseudo-complemented” lattice-ordered abelian groups has a model completion, which seems to bear some relation to our Theorem 7.7.

8. Appendix. A comparison with Wheeler’s characterization theorem

In this section, we relate our results in Section 3 to the necessary and sufficient conditions provided by Wheeler in [38] (see also [39]) for the existence of model completions for universal theories with finite presentations. Let us note that Wheeler considers arbitrary first-order languages and, although we restrict ourselves here to algebraic languages, it is not difficult to see that the results of this section can be generalized to any first-order language by replacing equations with atomic formulas.

Let $\mathsf {K}$ be a universal class of algebras. Following [38, Section 3], a finite presentation of an algebra $\mathbf{A}\in \mathsf {K}$ is a pair $(\overline {a}, \pi )$ where $\overline {a}\in A^{\overline {x}}$ is a finite set of generators for $\mathbf{A}$ and $\pi (\overline {x})$ is a conjunction of equations such that $\mathbf{A}\models \pi (\overline {a})$ and for any equation $\varepsilon (\overline {x})$ ,

$$ \begin{align*} \mathbf{A}\models \varepsilon(\overline{a}) \iff \mathsf{K}\models \pi\to\varepsilon. \end{align*} $$

Observe that $(\overline {a}, \pi )$ is a finite presentation of $\mathbf{A}$ if, and only if, for any $\mathbf{B}\in \mathsf {K}$ generated by $\overline {b}\in B^{\overline {x}}$ satisfying $\mathbf{B}\models \pi (\overline {b})$ , there is a surjective homomorphism $\mathbf{A}\twoheadrightarrow \mathbf{B}$ mapping $\overline {a}$ to $\overline {b}$ . An algebra $\mathbf{A}\in \mathsf {K}$ is said to be finitely presented in $\mathsf {K}$ if it admits a finite presentation.

Remark 8.1. If $\mathsf {K}$ is a variety, then an algebra $\mathbf{A} \in \mathsf {K}$ is finitely presented in $\mathsf {K}$ if, and only if, it is finitely presented in the usual sense, i.e., $\mathbf{A}$ is isomorphic to the quotient of a finitely generated $\mathsf {K}$ -free algebra with respect to a compact congruence. Moreover, if $\mathsf {K}$ is a positive universal class and the variety $\mathsf {V}$ generated by $\mathsf {K}$ is congruence distributive, then $\mathbf{A}\in \mathsf {K}$ is finitely presented in $\mathsf {K}$ if, and only if, it is finitely presented in $\mathsf {V}$ . Just observe that by Jónsson’s Lemma [25], we have in this case $\mathsf {V}=\mathbb {ISP}(\mathsf {K})$ .

A class of algebras $\mathsf {K}$ has finite presentations if for every finite set $\overline {x}$ and conjunction of equations $\pi (\overline {x})$ that is satisfiable in $\mathsf {K}$ , there exist an algebra $\mathbf{A}\in \mathsf {K}$ and a tuple $\overline {a}\in A^{\overline {x}}$ such that $(\overline {a},\pi )$ is a presentation of $\mathbf{A}$ . All quasivarieties, and in particular all varieties, have finite presentations (cf. [38, Corollary 1, p. 315]), but this is not the case for all universal classes, as shown by the following example.

Example 8.2. The positive universal class $\mathsf {LA^c}$ of ordered abelian groups does not have finite presentations. To see this, recall that $\mathsf {LA^c}$ generates the variety $\mathsf {LA}$ of lattice-ordered abelian groups, which is congruence distributive (cf. Example 2.8). Hence, by Remark 8.1, an ordered abelian group is finitely presented in the sense of the above definition if, and only if, it is finitely presented as a lattice-ordered abelian group in the usual sense. However, any finitely presented ordered abelian group is simple (see, e.g., [21, Theorem 4.A and Corollary 5.2.3]) and there exist finitely generated ordered abelian groups that are not simple, e.g., the lexicographic product $\textbf {R}\overrightarrow {\times }\textbf {R}$ generated by $\{(1,0),(0,1)\}$ . It follows that there cannot be a $2$ -generated finitely presented ordered abelian group with presentation $\top (x_1,x_2)$ .

Let us now recall Wheeler’s conservative congruence extension property. Given any algebra $\mathbf{A}\in \mathsf {K}$ , let $\mathfrak {D}^+(\mathbf{A})$ be the positive diagram of $\mathbf{A}$ , i.e., the set of atomic sentences in the language extended with names for the elements of $\mathbf{A}$ that are satisfied in $\mathbf{A}$ . The class $\mathsf {K}$ has the conservative congruence extension property (for finite presentations) if, whenever $\mathbf{B}$ admits a finite presentation $((\overline {a},\overline {b}),\pi (\overline {x},\overline {y}))$ , $\mathbf{A}$ is the subalgebra of $\mathbf{B}$ generated by $\overline {a}$ , the tuple $\overline {b}$ does not lie in $\mathbf{A}$ , and $\rho (\overline {x},\overline {y})$ is a conjunction of negated equations such that $\mathbf{B} \models \rho (\overline {a},\overline {b})$ , there exists a quantifier-free formula $\chi (\overline {x})$ satisfying

$$ \begin{align*} \textrm{Th}(\mathsf{K})\cup\mathfrak{D}^+(\mathbf{B})\vdash \rho(\overline{a},\overline{b})\to \chi(\overline{a}), \end{align*} $$

and for every surjective homomorphism $h\colon \mathbf{A}\twoheadrightarrow \mathbf{A}'$ such that $\mathbf{A}'\in \mathsf {K}$ and $\mathbf{A}'\models \chi (h(\overline {a}))$ there exist a $\mathbf{B}'\in \mathsf {K}$ extending $\mathbf{A}'$ and a surjective homomorphism $h'\colon \mathbf{B} \twoheadrightarrow \mathbf{B}'$ whose restriction to $\mathbf{A}$ coincides with h, and such that $\mathbf{B}'\models \rho (h(\overline {a}),h'(\overline {b}))$ . ⁴

The following proposition shows that, for universal classes with finite presentations, the conservative congruence extension property is equivalent to a strengthening of the conservative model extension property where the variable y is replaced by a tuple $\overline {y}$ .

Proposition 8.3. Let $\mathsf {K}$ be a universal class of algebras with finite presentations. Then $\mathsf {K}$ has the conservative congruence extension property if, and only if, for any finite sets $\overline {x},\overline {y}$ and conjunction of literals $\psi (\overline {x},\overline {y})$ , there exists a quantifier-free formula $\chi (\overline {x})$ satisfying

1. (i) $\mathsf {K}\models \psi \to \chi $ and

2. (ii) for every $\mathbf{A} \in \mathsf {K}$ generated by $\overline {a}\in A^{\overline {x}}$ such that $\mathbf{A}\models \chi (\overline {a})$ and for any equation $\varepsilon (\overline {x})$ ,

   $$ \begin{align*} \mathsf{K}\models\psi^+\to\varepsilon \:\Longrightarrow\: \mathbf{A}\models\varepsilon(\overline{a}), \end{align*} $$
   there exist an algebra $\mathbf{B}\in \mathsf {K}$ extending $\mathbf{A}$ and $\overline {b} \in B^{\overline {y}}$ such that $\mathbf{B}\models \psi (\overline {a},\overline {b})$ .

Proof. Suppose that $\mathsf {K}$ has the conservative congruence extension property. Fix finite sets $\overline {x},\overline {y}$ and a conjunction of literals $\psi (\overline {x},\overline {y})$ . If $\psi $ is not satisfiable in $\mathsf {K}$ , we can set $\chi := \bot $ . Hence, assume that $\psi $ is satisfiable in $\mathsf {K}$ . Consider $\mathbf{B}\in \mathsf {K}$ and $(\overline {a},\overline {b})\in B^{\overline {x},\overline {y}}$ such that $((\overline {a},\overline {b}),\psi ^+)$ is a finite presentation of $\mathbf{B}$ and let $\mathbf{A}$ be the subalgebra of $\mathbf{B}$ generated by $\overline {a}$ . If there is a $b_i\in \overline {b}$ such that $b_i\in A$ , then $\mathsf {K}\models \psi ^+ \to y_i\approx t(\overline {x})$ for some term t. Replacing $y_i$ by $t(\overline {x})$ in the formula $\psi $ whenever $b_i\in A$ , we can assume that no element of $\overline {b}$ belongs to $\mathbf{A}$ . Further, if $\mathbf{B}\models \sigma (\overline {a},\overline {b})$ for some equation $\sigma $ of $\psi ^-$ , then $\mathsf {K}\models \psi ^+\to \sigma $ , contradicting the fact that $\psi $ is satisfiable in $\mathsf {K}$ . Hence $\mathbf{B}\models \rho (\overline {a},\overline {b})$ , where $\rho (\overline {x},\overline {y})$ is the conjunction of the negated equations $\neg \sigma $ for $\sigma $ ranging over the equations of $\psi ^-$ (hence, $\psi =\psi ^+\mathbin {\&}\rho $ ), and so there exists a quantifier-free formula $\chi (\overline {x})$ satisfying the conditions for the conservative congruence extension property.

We prove that $\chi $ satisfies (i) and (ii). For (i), consider any algebra $\textbf {C}\in \mathsf {K}$ and tuples $\overline {c}\in C^{\overline {x}}$ and $\overline {d}\in C^{\overline {y}}$ such that $\textbf {C}\models \psi (\overline {c},\overline {d})$ . We must prove that $\textbf {C}\models \chi (\overline {c})$ . Let $\textbf {C}'$ be the subalgebra of $\textbf {C}$ generated by $\overline {c},\overline {d}$ , and note that $\textbf {C}'\models \psi (\overline {c},\overline {d})$ as $\psi $ is quantifier-free. Since $\textbf {C}'\models \psi ^+(\overline {c},\overline {d})$ , there is a surjective homomorphism $\mathbf{B}\twoheadrightarrow \textbf {C}'$ mapping $\overline {a}$ to $\overline {c}$ and $\overline {b}$ to $\overline {d}$ . Hence, with the obvious interpretation of the new constants, $\textbf {C}'\models \mathfrak {D}^+(\mathbf{B})$ . So $\textrm {Th}(\mathsf {K})\cup \mathfrak {D}^+(\mathbf{B})\vdash \rho \to \chi $ and $\textbf {C}'\models \rho (\overline {c},\overline {d})$ entail $\textbf {C}'\models \chi (\overline {c})$ , and therefore $\textbf {C}\models \chi (\overline {c})$ .

For (ii), consider any algebra $\mathbf{A}'\in \mathsf {K}$ generated by a tuple $\overline {a}'\in (A')^{\overline {x}}$ such that $\mathbf{A}'\models \chi (\overline {a}')$ and, for all equations $\varepsilon (\overline {x})$ , $\mathsf {K}\models \psi ^+\to \varepsilon $ entails $\mathbf{A}'\models \varepsilon (\overline {a}')$ . Then there exists a (unique) homomorphism $h\colon \mathbf{A}\to \mathbf{A}'$ mapping $\overline {a}$ to $\overline {a}'$ . Just observe that, whenever $s(\overline {a})=t(\overline {a})$ for two terms $s(\overline {x}),t(\overline {x})$ , we have $\mathbf{B}\models s(\overline {a})\approx t(\overline {a})$ and hence also $\mathsf {K}\models \psi ^+\to s(\overline {x})\approx t(\overline {x})$ , which implies $\mathbf{A}'\models s(\overline {a}')\approx t(\overline {a}')$ . Moreover, h is surjective because $\overline {a}'$ generates $\mathbf{A}'$ . By the conservative congruence extension property, there exist $\mathbf{B}'\in \mathsf {K}$ extending $\mathbf{A}'$ and a surjective homomorphism $h'\colon \mathbf{B}\twoheadrightarrow \mathbf{B}'$ that extends h and satisfies $\mathbf{B}'\models \rho (\overline {a}',h'(\overline {b}))$ . Using the fact that $\mathbf{B}\models \psi ^+(\overline {a},\overline {b})$ entails $\mathbf{B}'\models \psi ^+(\overline {a}',h'(\overline {b}))$ , we conclude that $\mathbf{B}'\models \psi (\overline {a}', h'(\overline {b}))$ , as was to be proved.

For the converse direction, let $\mathbf{B}\in \mathsf {K}$ be an algebra admitting a finite presentation $((\overline {a},\overline {b}),\pi (\overline {x},\overline {y}))$ , let $\mathbf{A}$ be the subalgebra of $\mathbf{B}$ generated by $\overline {a}$ , and assume that $\overline {b}$ does not lie in $\mathbf{A}$ . Further, let $\rho (\overline {x},\overline {y})$ be a conjunction of negated equations such that $\mathbf{B} \models \rho (\overline {a},\overline {b})$ . Define the conjunction of literals $\psi (\overline {x},\overline {y}):= \pi \mathbin {\&} \rho $ . Then there exists a quantifier-free formula $\chi (\overline {x})$ satisfying the properties in (i) and (ii). Condition (i) entails easily that

$$ \begin{align*} \textrm{Th}(\mathsf{K})\cup\mathfrak{D}^+(\mathbf{B})\vdash \rho(\overline{a},\overline{b})\to \chi(\overline{a}). \end{align*} $$

Consider next a surjective homomorphism $h\colon \mathbf{A}\twoheadrightarrow \mathbf{A}'$ with $\mathbf{A}'\in \mathsf {K}$ and $\mathbf{A}'\models \chi (h(\overline {a}))$ . Note that $h(\overline {a})$ generates $\mathbf{A}'$ and, for any equation $\varepsilon (\overline {x})$ , $\mathsf {K}\models \pi \to \varepsilon $ implies $\mathbf{B}\models \varepsilon (\overline {a})$ and hence also $\mathbf{A}\models \varepsilon (\overline {a})$ and $\mathbf{A}'\models \varepsilon (h(\overline {a}))$ . By (ii), there exist $\mathbf{B}'\in \mathsf {K}$ extending $\mathbf{A}'$ and a tuple $\overline {b}' \in (B')^{\overline {y}}$ such that $\mathbf{B}'\models \psi (h(\overline {a}),\overline {b}')$ . Let $\mathbf{B}''$ be the subalgebra of $\mathbf{B}'$ generated by $h(\overline {a}),\overline {b}'$ and note that $\mathbf{B}''\in \mathsf {K}$ because $\mathsf {K}$ is a universal class. Since $\mathbf{B}''\models \pi (h(\overline {a}),\overline {b}')$ , there exists a surjective homomorphism $h'\colon \mathbf{B}\twoheadrightarrow \mathbf{B}''$ mapping $\overline {a}$ to $h(\overline {a})$ and $\overline {b}$ to $\overline {b}'$ . In particular, $h'$ extends h. Further, $\mathbf{B}''$ extends $\mathbf{A}'$ and satisfies $\mathbf{B}''\models \rho (h(\overline {a}),\overline {b}')$ . Hence $\mathsf {K}$ has the conservative congruence extension property.⊣

We are now in a position to compare Wheeler’s characterization of universal theories that have a model completion with our results from Section 3. Following Wheeler, we say that a universal class of algebras with finite presentations $\mathsf {K}$ is coherent if whenever $\mathbf{B}\in \mathsf {K}$ is finitely presented in $\mathsf {K}$ and $\mathbf{A}$ is a finitely generated subalgebra of $\mathbf{B}$ , then $\mathbf{A}$ is finitely presented in $\mathsf {K}$ . It is not difficult to see that a universal class of algebras with finite presentations is coherent if, and only if, it has the variable projection property.

In the case where $\mathsf {K}$ is a universal class of algebras, the following main result of [38] is a direct consequence of Theorem 3.2 and Propositions 3.8 and 8.3.

Proposition 8.4 [38, Theorem 5]

Let $\mathsf {K}$ be a universal class with finite presentations. The theory of $\mathsf {K}$ has a model completion if, and only if, $\mathsf {K}$ is coherent and has the amalgamation property and conservative congruence extension property.