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., [Reference Tent and Ziegler37, 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.⊣

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 $ .Footnote ²

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.

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.⊣

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. [Reference Baker2, 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*} $$

⊣

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})$ .

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.⊣

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.⊣

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)$ .⊣

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})$ .⊣

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)$ .⊣

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)$ .⊣

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:

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 $ .⊣

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.

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.⊣