is at least one non-redundant atom $\phi$ in the freest model $F_{C}(R^{+})$
that discriminates $r$. If $\phi^{|Q}$ is a non-redundant atom of
$F_{C}(R^{+})^{|Q}$ then $\phi^{|Q}$ cannot be an atom of any $F_{S}^{|Q}$
(otherwise $R\wedge{\bf{\varphi_{S}}}\vdash r^{-}$) and then $\phi^{|Q}$ is a
residual atom of the embedding. The atom $\phi^{|Q}$ may, however, be
redundant in $F_{C}(R^{+})^{|Q}$. If $\phi^{|Q}$ is redundant with
$F_{C}(R^{+})^{|Q}$ then there should be some non-redundant atom $\alpha$ in
$F_{C}(R^{+})^{|Q}$ that discriminates $r$. From theorem 12 we know that
$\alpha$ is the restriction of at least one non-redundant atom $\beta$ in
$F_{C}(R^{+})$. Since $F_{S}^{|Q}\models r^{+}$ then $\alpha=\beta^{|Q}$
cannot be in any $F^{|Q}_{S}$ and $\alpha$ is a residual atom of the
embedding. ∎

######  Theorem 14.

(i) An embedding that has no residual atoms is complete.
(ii) An embedding that is complete and concise has no residual atoms.

###### Proof.

Theorem 13 says that an embedding of a problem $P$ has a residual atom if and
only if $\exists r((R\not\vdash r^{+})\wedge\forall
S(R\wedge{\bf{\varphi_{S}}}\vdash r^{+}))$ where $r$ is a duple over the
embedding constants $Q$ and the universal quantifier runs along the solutions
$S$ of $P$.
i) If an embedding has no residual atoms then $\forall r((R\vdash
r^{+})\vee\exists S(R\wedge{\bf{\varphi_{S}}}\not\vdash r^{+}))$. Since
$\exists S(R\wedge{\bf{\varphi_{S}}}\not\vdash r^{+})$ implies $\exists
S({\bf{\varphi_{S}}}\not\vdash r^{+})$ then $\forall r((R\vdash
r^{+})\vee\exists S({\bf{\varphi_{S}}}\not\vdash r^{+}))$ which is the
definition of a complete embedding.
ii) If an embedding is concise then $R\wedge{\bf{\varphi_{S}}}\vdash r^{+}$
implies ${\bf{\varphi_{S}}}\vdash r^{+}$ when $r$ is a duple over $Q$. If the
model is also complete then $\forall S({\bf{\varphi_{S}}}\vdash r^{+})$
implies $R\vdash r^{+}$, in other words $\forall r(\forall
S(R\wedge{\bf{\varphi_{S}}}\vdash r^{+})\Rightarrow(R\vdash r^{+}))$ and then
theorem 13 tells us that the embedding has no residual atoms. ∎

######  Theorem 15.

Two concise and complete embeddings with embedding constants $C_{1}$ and
$C_{2}$ respectively sharing the same interpretation
$(Q,{\bf{\varphi}},\Gamma)$ have the same non-redundant atoms restricted to
$Q$, i.e $F_{C1}(R_{1}^{+})^{|Q}=F_{C2}(R_{2}^{+})^{|Q}$.

###### Proof.

From theorem 9 we know that in a concise embedding $F_{S}^{|Q}=F_{Q}(S)$ and
then $F^{|Q}=\cup_{S}F_{Q}(S)$. Since embeddings 1 and 2 are both concise then
$F_{1}^{|Q}=\cup_{S}F_{Q}(S)=F_{2}^{|Q}$. Theorem 14 proves that our two
embeddings have no residual atoms and then theorem 12 (iii) shows that
$F_{1}^{|Q}=F_{C1}(R^{+})^{|Q}$ and $F_{2}^{|Q}=F_{C2}(R^{+})^{|Q}$. Putting
all together
$F_{C1}(R^{+})^{|Q}=F_{1}^{|Q}=\cup_{S}F_{Q}(S)=F_{2}^{|Q}=F_{C2}(R^{+})^{|Q}$
as we wanted to prove. ∎

######  Theorem 16.

Consider two embeddings $1$ and $2$ of a problem $P$ with the same
interpretation $(Q,{\bf{\varphi}},\Gamma)$ and let $R_{1}$ and $R_{2}$ be the
embeddings sets and $C_{1}$ and $C_{2}$ the embedding constants. Let $\eta$ be
a non-redundant atom of $F_{1S}^{|Q}$ where $S$ is a solution of $P$.
i) If both embeddings are concise then $\eta$ is a non-redundant atom of
$F_{2S}^{|Q}$.
ii) If both embeddings are concise and tight there are non-redundant atoms
$\phi_{1}\in F_{C1}(R_{1}^{+})$ and $\phi_{2}\in F_{C2}(R_{2}^{+})$ such that
$\phi_{1}^{|Q}=\phi_{2}^{|Q}=\eta$.

###### Proof.

(i) Since the embeddings are concise in agreement with theorem 9 so, since
$\eta$ is a non-redundant atom of $F_{1S}^{|Q}$ then it is also a non-
redundant atom of $F_{2S}^{|Q}$.
(ii) If the embeddings are tight every non-redundant atom $\eta$ of
$F_{1S}^{|Q}$ is equal to the the restriction to $Q$ of at least one non-
redundant atom $\phi_{1}$ of $F_{C1}(R_{1}^{+})$. From prop. i there is also
at least one non-redundant atom $\phi_{2}$ of $F_{C2}(R_{2}^{+})$ with
restriction equal to $\eta$. ∎

######  Theorem 17.

Consider two embeddings $1$ and $2$ of a problem $P$ with the same
interpretation $(Q,{\bf{\varphi}},\Gamma)$ and let $R_{1}$ and $R_{2}$ be the
embeddings sets and $C_{1}$ and $C_{2}$ the embedding constants. Let
$\phi_{1}$ be a non-redundant atom of $F_{1S}$ where $S$ is a solution of $P$.
i) If both embeddings are concise then $\phi_{1}^{|Q}$ is either redundant
with both $F_{1S}^{|Q}$ and $F_{2S}^{|Q}$ or is a non-redundant atom in
$F_{1S}^{|Q}$ and in $F_{2S}^{|Q}$.
ii) If both embeddings are concise and tight either $\phi_{1}^{|Q}$ is
redundant with $F_{1S}^{|Q}$ or there is a non-redundant atom $\phi_{2}\in
F_{C2}(R_{2}^{+})$ such that $\phi_{1}^{|Q}=\phi_{2}^{|Q}$.

###### Proof.

Suppose $\phi_{1}^{|Q}$ is redundant with $F_{1S}^{|Q}$. Because the
embeddings are concise $F_{1S}^{|Q}=F_{2S}^{|Q}$ and then $\phi_{1}^{|Q}$ is
redundant with $F_{2S}^{|Q}$. If, on the other hand, $\phi_{1}^{|Q}$ is non-
redundant in $F_{1S}^{|Q}$ make $\eta$ in theorem 16 equal to $\phi_{1}^{|Q}$.
∎

######  Theorem 18.

Consider two embeddings $1$ and $2$ of a problem $P$ with the same
interpretation $(Q,{\bf{\varphi}},\Gamma)$ and let $R_{1}$ and $R_{2}$ be the
embeddings sets and $C_{1}$ and $C_{2}$ the embedding constants. Let
$\phi_{1}$ be a non-redundant atom of $F_{1}$.
i) If both embeddings are concise there is some solution $S$ where
$\phi_{1}^{|Q}$ is either redundant with both $F_{1S}^{|Q}$ and $F_{2S}^{|Q}$
or is a non-redundant atom in $F_{1S}^{|Q}$ and in $F_{2S}^{|Q}$.
ii) If both embeddings are concise and tight either $\phi_{1}^{|Q}$ is
redundant with $F_{1S}^{|Q}$ for some solution $S$ or there is a non-redundant
atom $\phi_{2}\in F_{C2}(R_{2}^{+})$ such that $\phi_{1}^{|Q}=\phi_{2}^{|Q}$.

###### Proof.

If $\phi_{1}$ is non-redundant in $F_{1}=\cup_{S}F_{S1}$ then it is non-
redundant in at least one $F_{1S}$. Apply theorem 17 to $\phi_{1}$ non-
redundant in $F_{1S}$. ∎

######  Theorem 19.

An embedding is strongly complete if and only if
$F\equiv\cup_{S}F_{S}=F_{C}(R^{+})$.

###### Proof.

Since $F_{C}(R^{+})$ is freer than every freest solution $F_{S}$ it follows
that $F\equiv\cup_{S}F_{S}\subset F_{C}(R^{+})$. In the other direction, let
$\phi$ be non-redundant in $F_{C}(R^{+})$ and external to $F$. Then there is
at least one duple $r$ over the embedding constants $C$ that is discriminated
only by $\phi$. Since $\phi$ is external to $F$ it must be external to each
$F_{S}$ and, hence, $F_{S}\models r^{+}$ for every solution $S$ while
$F_{C}(R^{+})\models r^{-}$ contradicting the assumption that the embedding is
strongly complete. ∎

######  Theorem 20.

Consider two embeddings $1$ and $2$ of a problem $P$ with the same
interpretation $(Q,{\bf{\varphi}},\Gamma)$ and let $R_{1}$ and $R_{2}$ be the
embeddings sets and $C_{1}$ and $C_{2}$ the embedding constants. Let
$\phi_{1}$ be a non-redundant atom of $F_{C1}(R_{1}^{+})$ and assume embedding
1 is strongly complete.
i) If both embeddings are concise there is some solution $S$ where
$\phi_{1}^{|Q}$ is either redundant with both $F_{1S}^{|Q}$ and $F_{2S}^{|Q}$
or is a non-redundant atom in $F_{1S}^{|Q}$ and in $F_{2S}^{|Q}$.
ii) If both embeddings are concise and tight either $\phi_{1}^{|Q}$ is
redundant with $F_{1S}^{|Q}$ for some solution $S$ or there is a non-redundant
atom $\phi_{2}\in F_{C2}(R_{2}^{+})$ such that $\phi_{1}^{|Q}=\phi_{2}^{|Q}$.

###### Proof.

If embedding 1 is strongly complete, theorem 19 tells us that
$F_{1}=F_{C1}(R_{1}^{+})$. Therefore, $\phi_{1}$ is a non-redundant atom of
$F_{1}$ and we can apply theorem 18. ∎

######  Theorem 21.

An explicit embedding is tight.

###### Proof.

An embedding is explicit if for each solution $S$ there is a subset $K_{S}$ of
the constants $Q\subseteq K_{S}\subset C$ such that the freest solution model
for $S$ is $F_{S}=F_{C}(R^{+})^{{}^{\vee}K_{S}}\oplus F_{C-K_{S}}(\emptyset)$.
Since the set of constants in $F_{C}(R^{+})^{{}^{\vee}K_{S}}$ and
$F_{C-K_{S}}(\emptyset)$ are disjoint, theorem 3 tells us that
$F_{S}=F_{C}(R^{+})^{{}^{\vee}K_{S}}+F_{C-K_{S}}(\emptyset)$. Theorem 6 shows
that $F_{C}(R^{+})^{{}^{\vee}K_{S}}\sqsubset F_{C}(R^{+})$, i.e. the non-
redundant atoms of $F_{C}(R^{+})^{{}^{\vee}K_{S}}$ are all non-redundant atoms
of $F_{C}(R^{+})$. Regarding the rest of the atoms of $F_{S}$, i.e the atoms
in the set $F_{C-K_{S}}(\emptyset)$, consider that it follows from
$F_{S}\equiv F_{C}(R^{+}\cup S)$ that $F_{S}\subset F_{C}(R^{+})$. Therefore,
$F_{C-K_{S}}(\emptyset)\subset F_{C}(R^{+})$ and, since a non-redundant atom
$\phi$ in $F_{C-K_{S}}(\emptyset)$ has a single constant in its upper constant
segment it can be redundant with no model, so $\phi$ should be a non-redundant
atom of both $F_{S}$ and $F_{C}(R^{+})$. We have shown the non-redundant atoms
of $F_{C-K_{S}}(\emptyset)$ and the non-redundant atoms of
$F_{C}(R^{+})^{{}^{\vee}K_{S}}$ are non-redundant atoms of $F_{C}(R^{+})$ so
we can write $F_{S}\sqsubset F_{C}(R^{+})$ for every solution $S$ of $P$ and
the embedding is tight. ∎

######  Lemma 10.1.

Let M be a semilattice model with constants $C$ and let $R$ be a set of
positive duples over $C$. Let $M_{R}\equiv F_{C}(Th^{+}_{0}(M)\cup R^{+})$,
i.e. the freest extension of $M$ that satisfies $R^{+}$. Let $C^{\prime}$ be a
superset of $C$ with a constant $g_{\sigma}$ for each atomic sentence $\sigma$
of $R$. For a duple $\sigma\equiv(a\leq b)$ define
$\sigma^{\prime}\equiv(a\leq b\odot g_{\sigma})$. Let $M_{R^{\prime}}\equiv
F_{C^{\prime}}(Th^{+}_{0}(M)\cup_{i:(\sigma_{i}\in
R)}\\{\sigma^{\prime}_{i}\\})$. The set of non-redundant atoms of $M_{R}$ is a
subset of the set of non-redundant atoms of $M_{R^{\prime}}$, written
$M_{R}\sqsubset M_{R^{\prime}}$. In addition, the restriction to $C$ satisfies
$M_{R^{\prime}}^{|C}\approx M$ and grounded to $C$ satisfies
$M_{R^{\prime}}^{{}^{\vee}C}\approx M_{R}$.

${M_{R}}$${M_{R^{\prime}}}$${M}$$\sqsubset$$\scriptstyle{{}^{\vee}C}$$\scriptstyle{|C}$$\scriptstyle{\square_{R}}$

###### Proof.

$M_{R^{\prime}}$ can be calculated by starting with model $M$ and enforcing
each duple of $\sigma^{\prime}_{i}$ one by one, in any order, using full
crossing. Assume first that $R$ contains a single duple $\sigma\equiv(a\leq
b)$ and consider the following two models: the model $M_{\sigma}\equiv
F_{C}(Th^{+}_{0}(M)\cup\\{\sigma\\})=\square_{\sigma}M\equiv(M-{\bf{dis}}_{M}(a,b))\,\cup\,({\bf{L}}^{a}(b)\bigtriangledown{\bf{dis}}_{M}(a,b))$
resulting from full-crossing $\sigma$ over $M$, and the model
$M_{\sigma^{\prime}}\equiv
F_{C\cup\\{g_{\sigma}\\}}(Th^{+}_{0}(M)\cup\\{\sigma^{\prime}\\})$ obtained
from the full-crossing of $\sigma^{\prime}$ over a model atomized by the atoms
of $M$ plus an additional atom $\phi_{\sigma}$ with upper constant segment
$U^{c}(\phi_{\sigma})=\\{g_{\sigma}\\}$.
From the definition of full crossing follows that
$M_{\sigma^{\prime}}=M_{\sigma}\cup\\{\phi_{\sigma}\\}\cup(\phi_{\sigma}\bigtriangledown{\bf{dis}}_{M}(a,b))$,
where we are using the same symbols for models and their atomizations. It
follows that the atoms of $M_{\sigma}$ are a subset of the atoms of
$M_{\sigma^{\prime}}$. In addition, each atom of $M_{\sigma^{\prime}}$ that is
not an atom of $M_{\sigma}$ contains the constant $g_{\sigma}$ in its upper
constant segment. $M_{\sigma^{\prime}}^{|C}$ is the restriction of
$M_{\sigma^{\prime}}$ to the subalgebra spawn by the terms and constants over
$C$, and it is a semilattice model that can be atomized by taking the atoms of
$M_{\sigma^{\prime}}$ and intersecting their upper constant segments with $C$;
we get
$M_{\sigma^{\prime}}^{|C}=M_{\sigma}^{|C}\cup\\{\phi^{|C}_{\sigma}\\}\cup(\phi_{\sigma}\bigtriangledown{\bf{dis}}_{M}(a,b))^{|C}=M_{\sigma}\cup{\bf{dis}}_{M}(a,b)$.
Substituting $M_{\sigma}$ we obtain
$M_{\sigma^{\prime}}^{|C}=(M-{\bf{dis}}_{M}(a,b))\,\cup\,({\bf{L}}^{a}_{M}(b)\bigtriangledown{\bf{dis}}_{M}(a,b))\cup{\bf{dis}}_{M}(a,b)$
and, since ${\bf{dis}}_{M}(a,b)\subseteq M$ then
$M_{\sigma^{\prime}}^{|C}=M\,\cup\,({\bf{L}}^{a}_{M}(b)\bigtriangledown{\bf{dis}}_{M}(a,b))$.
The atoms of the discriminant are atoms of $M$ as well as the atoms of the
lower atomic segment ${\bf{L}}^{a}_{M}(b)\subseteq M$, so every atom in
${\bf{L}}^{a}_{M}(b)\bigtriangledown{\bf{dis}}_{M}(a,b)$ is redundant with $M$
and then it follows that $M_{\sigma^{\prime}}^{|C}$ can be atomized by the
same atoms than $M$, hence, they are isomorphic
$M_{\sigma^{\prime}}^{|C}\approx M$.
The model
$M_{\sigma^{\prime}}=M_{\sigma}\cup\\{\phi_{\sigma}\\}\cup(\phi_{\sigma}\bigtriangledown{\bf{dis}}_{M}(a,b))$
is atomized by the atoms in $M_{\sigma}$ and a bunch of other atoms that all
contain $g_{\sigma}$ in their upper constant segment. We argue that a non-
redundant atom $\phi$ of $M_{\sigma}$ is also non-redundant in
$M_{\sigma^{\prime}}$ because $\phi$ does not contain $g_{\sigma}$ in its
upper constant segment and therefore it cannot be written as a union of atoms
with some atom containing $g_{\sigma}$, so the extra atoms of
$M_{\sigma^{\prime}}$ cannot make $\phi$ redundant. Therefore, the non-
redundant atoms of $M_{\sigma}$ are non-redundant atoms of
$M_{\sigma^{\prime}}$ and we can write $M_{\sigma}\sqsubset
M_{\sigma^{\prime}}$.
We have proven that given a model $M$ of a semilattice with constants in $C$
and a duple $\sigma$ there is an extended model $M_{\sigma^{\prime}}$ with
constants in $C^{\prime}\supset C$ such that $M_{\sigma^{\prime}}^{|C}\approx
M$ and the set of non-redundant atoms of $M_{\sigma}\equiv
F_{C}(Th^{+}_{0}(M)\cup\\{\sigma\\})$ is a subset of the set of non-redundant
atoms of $M_{\sigma^{\prime}}$. We can represent this property with a
triangular cell:

${M_{\sigma}}$${M_{\sigma^{\prime}}}$${M}$$\sqsubset$$\scriptstyle{{}^{\vee}C}$$\scriptstyle{|C}$$\scriptstyle{\square_{\sigma}}$

where the vertical arrows represent a full crossing operation with $\sigma$,
written $\square_{\sigma}$. From $M^{{}^{\vee}C}_{\sigma}=M_{\sigma}$ and
$\\{\phi^{{}^{\vee}C}_{\sigma}\\}\cup(\phi_{\sigma}\bigtriangledown{\bf{dis}}_{M}(a,b))^{{}^{\vee}C}=\emptyset\,$
follows that $M_{\sigma^{\prime}}$ grounded to $C$ satisfies
$M^{{}^{\vee}C}_{\sigma^{\prime}}=M^{{}^{\vee}C}_{\sigma}\cup\\{\phi^{{}^{\vee}C}_{\sigma}\\}\cup(\phi_{\sigma}\bigtriangledown{\bf{dis}}_{M}(a,b))^{{}^{\vee}C}=M_{\sigma}$,
which is represented in the triangular cell.
If $R$ contains more than one duple, we can sort the duples in any order and
let the full diagram be:

${M_{\sigma_{1}\sigma_{2}...\sigma_{n}}}$${M_{\sigma^{\prime}_{1}\sigma_{2}...\sigma_{n}}}$${M_{\sigma^{\prime}_{1}\sigma^{\prime}_{2}...\sigma_{n}}}$${...}$${{M_{\sigma^{\prime}_{1}\sigma^{\prime}_{2},...,\sigma^{\prime}_{n}}}}$${M_{\sigma_{1}\sigma_{2}\sigma_{3}}}$${M_{\sigma^{\prime}_{1}\sigma_{2}\sigma_{3}}}$${M_{\sigma^{\prime}_{1}\sigma^{\prime}_{2}\sigma_{3}}}$${M_{\sigma^{\prime}_{1}\sigma^{\prime}_{2}\sigma^{\prime}_{3}}}$${M_{\sigma_{1}\sigma_{2}}}$${M_{\sigma^{\prime}_{1}\sigma_{2}}}$${M_{\sigma^{\prime}_{1}\sigma^{\prime}_{2}}}$${M_{\sigma_{1}}}$${M_{\sigma^{\prime}_{1}}}$${M}$$\sqsubset$$\sqsubset$$\sqsubset$$\sqsubset$$\sqsubset$$\sqsubset$$\sqsubset$$\scriptstyle{|C\,\cup\,\\{g_{\sigma_{2}}\\}}$$\sqsubset$$\scriptstyle{\square_{\sigma_{3}}}$$\sqsubset$$\scriptstyle{\square_{\sigma_{3}}}$$\scriptstyle{\square_{\sigma_{3}}}$$\scriptstyle{|C\,\cup\,\\{g_{\sigma_{1}}\\}}$$\sqsubset$$\scriptstyle{\square_{\sigma_{2}}}$$\scriptstyle{\square_{\sigma_{2}}}$$\scriptstyle{|C}$$\scriptstyle{\square_{\sigma_{1}}}$

Consider the square diagrams:

${M_{\sigma}}$${O_{\sigma}}$${M_{\sigma_{1}\sigma_{2}}}$${M_{\sigma_{1}^{\prime}\sigma_{2}}}$${M}$${O}$${M_{\sigma_{1}}}$${M_{\sigma_{1}^{\prime}}}$$\subset$$\sqsubset$$\scriptstyle{{}^{\vee}C}$$\scriptstyle{\square_{\sigma}}$$\subset$$\scriptstyle{\square_{\sigma}}$$\scriptstyle{\square_{\sigma_{2}}}$$\sqsubset$$\scriptstyle{\square_{\sigma_{2}}}$

The square cell on the left says that if $M$ is atomized by a subset of the
atoms of $O$ then the result of full crossing $\sigma$ over $M$ produces a
model $M_{\sigma}$ that can be atomized by a subset of the atoms of
$O_{\sigma}$, which is straightforward from the definition of full crossing.
For the triangular cells we have proven that the non-redundant atoms of
$M_{\sigma}$ are also non-redundant atoms of $M_{\sigma^{\prime}}$. For a
square cell this property does not hold in general, however it does for all
the square cells in the full diagram; on each square cell we have some
$O=M\,\cup\,X^{g}$ where $X^{g}$ is a set of atoms that contain each some
constant $g$ that is not in the upper segment of any atom of $M$. In addition,
the full crossing in the square cells occurs with some duple
$\sigma\equiv(a\leq b)$ with $a$ and $b$ terms over a set of constants that do
not contain $g$. It is easy to show that in this situation
$O_{\sigma}=M_{\sigma}\,\cup\,Y^{g}$ where $Y^{g}$ is again a set of atoms
that contain $g$ in their upper constant segments and, hence, cannot make any
atom of $M_{\sigma}$ redundant in $O_{\sigma}$ and we can write
$M_{\sigma}\sqsubset O_{\sigma}$. Also, the grounded model to $C$ of
$O_{\sigma}$ when $C$ contains the constants of $O_{\sigma}$ except $g$
produces
$O^{{}^{\vee}C}_{\sigma}=M^{{}^{\vee}C}_{\sigma}\,\cup\,(Y^{g})^{{}^{\vee}C}=M_{\sigma}$.
Finally, since
$F_{C}(Th^{+}_{0}(M_{\sigma_{1}})\cup\\{\sigma_{2}\\})=F_{C}(Th^{+}_{0}(M)\cup\\{\sigma_{1}\\}\cup\\{\sigma_{2}\\})$
we can identify
$M_{\sigma^{\prime}_{1}\sigma^{\prime}_{2},...,\sigma^{\prime}_{n}}$ with the
model $F_{C^{\prime}}(Th^{+}_{0}(M)\cup R)^{\prime}$ and this proves the
lemma. ∎

######  Theorem 22.

Let $R$ be an embedding set over the constants $C$ for a problem $P$ with
interpretation $(Q,{\bf{\varphi}},\Gamma)$ and a scope sentence $\Xi$ that is
a first order sentence without quantifiers and with atomic subclauses in the
separator set $\,\Gamma$. Create a new constant $g_{\sigma}$ for each atomic
sentence $\sigma\equiv(a\leq b)$ of $\Gamma$ and define
$\sigma^{\prime}\equiv(a\leq b\odot g_{\sigma})$ and the set
$\Gamma^{\prime}=\cup_{\sigma\in\Gamma}\\{\sigma^{\prime}\\}$:
i) The extended embedding set $R^{E}=R\cup\Gamma^{\prime}$ over the embedding
constants $C\,\cup_{\sigma\in\Gamma}\\{g_{\sigma}\\}$ is an embedding of $P$
with the same interpretation and scope sentence.
ii) The extended embedding $R\cup\Gamma^{\prime}$ is an explicit and also
tight embedding.
iii) For each solution $S$ the freest solution model of the extended embedding
restricted to $C$ is equal to the freest solution model of the original
embedding.
iv) The extended embedding is concise if and only if the embedding $R$ is
concise.
v) The extended embedding is complete if and only if the embedding $R$ is
complete.

###### Proof.

For a solution $S$ of $P$ consider the following diagram obtained applying
lemma 10.1:

${{F_{C_{S}}(R^{+}\cup(\Gamma\cap\overline{S})^{\prime}\,\cup\,S)}}$${{F_{C\,\cup_{\sigma\in\Gamma}\\{g_{\sigma}\\}}(R^{+}\cup\Gamma^{\prime})}}$${{F_{C}(R^{+}\cup(\Gamma\cap\overline{S}))}}$${{F_{C_{S}}(R^{+}\cup(\Gamma\cap\overline{S})^{\prime})}}$${F_{C}(R^{+})}$${F_{C}(\emptyset)}$$\sqsubset$$\scriptstyle{|C_{S}}$$\sqsubset$$\scriptstyle{|C}$$\scriptstyle{\square_{S}}$$\scriptstyle{\square_{\Gamma\cap\overline{S}}}$$\scriptstyle{\square_{R^{+}}}$

where $C_{S}\equiv C\,\cup\\{g_{\sigma}:\sigma\in\Gamma\cap\overline{S}\\}$.
(i) We argue that, just like $F_{S}\equiv F_{C}(R^{+}\cup S)$ is a model
solution of $S$ that satisfies $\,\Xi$ (see theorem 8), the model $N_{S}\equiv
F_{C\,\cup\\{g_{\sigma}:\sigma\in\Gamma\cap\overline{S}\\}}(R^{+}\cup(\Gamma\cap\overline{S})^{\prime}\,\cup\,S)$
is also a solution of $P$ that can be identified as $S$ (we use $\overline{S}$
for the complement of $S$ in $\Gamma$, i.e.
$\Gamma\cap\overline{S}=\Gamma-S$). Since a positive atomic sentence
$\sigma^{\prime}\in\Gamma^{\prime}$ has no consequences in the subalgebra of
$N_{S}$ spawned by terms over $C$, i.e. in the subalgebra $N_{S}^{|C}$, then
it follows that any positive or negative atomic sentence over the constants of
$C$ is true in $N_{S}$ if and only if it is true in $F_{C}(R^{+}\cup S)$; we
can write $N_{S}^{|C}\approx F_{S}\equiv F_{C}(R^{+}\cup S)$. From the diagram
above and lemma 10.1 we have that
$N_{S}=F_{C\,\cup_{\sigma\in\Gamma}\\{g_{\sigma}\\}}(R^{+}\cup\Gamma^{\prime})^{{}^{\vee}C_{S}}$
and also $N_{S}\sqsubset
F_{C\,\cup_{\sigma\in\Gamma}\\{g_{\sigma}\\}}(R^{+}\cup\Gamma^{\prime})$.
We have built an extended embedding with embedding set $R^{E}\equiv
R\,\cup\,\Gamma^{\prime}$ and embedding constants $C^{E}\equiv
C\,\cup\\{g_{\sigma}:\sigma\in\Gamma\\}$. Notice that every pair
$\sigma,\sigma^{\prime}$ satisfies $\sigma\Rightarrow\sigma^{\prime}$ and then
the freest solution model for $S$ in the extended embedding $F_{S}^{E}\equiv
F_{C^{E}}((R^{E})^{+}\cup S)=F_{C^{E}}(R^{+}\cup\Gamma^{\prime}\cup
S)=F_{C^{E}}(R^{+}\cup(\Gamma\cap\overline{S})^{\prime}\,\cup\,S)$ a model
that, we are about to show, differs from $N_{S}$ in a bunch of non-redundant
atoms. Since the constants in $\\{g_{\sigma}:\sigma\in S\\}$ are not mentioned
in $R^{+}\cup(\Gamma\cap\overline{S})^{\prime}\,\cup\,S$, a non-redundant atom
of $F_{C^{E}}(\emptyset)$ with an upper constant segment equal to a single
constant in $\\{g_{\sigma}:\sigma\in S\\}$ remains unaltered after the full
crossing of the duples in
$R^{+}\cup(\Gamma\cap\overline{S})^{\prime}\,\cup\,S$ as a non-redundant atom
of $F_{S}^{E}$. It follows that $F_{S}^{E}$ is the model spawned by the atoms
of $N_{S}$ plus a set of atoms $\Lambda$ each with a single constant in its
upper constant segment, a constant in the set $\\{g_{\sigma}:\sigma\in S\\}$,
so we can write $F_{S}^{E}=N_{S}+\Lambda$. Applying theorem 1,
$(F_{S}^{E})^{|(C\,\cup\\{g_{\sigma}:\sigma\in\Gamma\cap\overline{S}\\})}=N_{S}$
and also $(F_{S}^{E})^{|C}=N_{S}^{|C}\approx F_{S}$. This proves that if we
can use $\Gamma$ to build a model for each solution of $P$ using the embedding
set $R$ we can also use $\Gamma$ to build a model for each solution of $P$
using the embedding set $R^{E}$.
(ii) Since the constants $g_{\sigma}$ only appear in the right hand side of
the duples of $R^{E}$ then the atoms in the freest model
$F_{C^{E}}(\emptyset)$ with upper constant segments in the set
$\\{g_{\sigma}:\sigma\in\Gamma\\}$ remain all in $F_{C^{E}}(R^{E+})$ as they
survive every full crossing operation with a duple in $R^{E+}$. This implies
the atoms of $\Lambda$ are all atoms in $F_{C^{E}}(R^{E})$ and, since they
have a single constant in their upper constant segment then they are non-
redundant atoms, i.e. $\Lambda\sqsubset F_{C^{E}}(R^{E+})$. We showed above
that $N_{S}\sqsubset F_{C^{E}}(R^{E+})$. Since $F_{S}^{E}=N_{S}+\Lambda$ and
both $N_{S}$ and $\Lambda$ are tight subset models of $F_{C^{E}}(R^{E+})$ then
$F_{S}^{E}\sqsubset F_{C^{E}}(R^{E+})$. Therefore, for every solution $S$ of
$P$ the freest solution model $F_{S}^{E}$ is spawned by a subset of the non-
redundant atoms of $F_{C^{E}}(R^{E+})$ and this proves that the extended
embedding $R^{E}$ is tight.
Since $N_{S}$ a model over
$C\,\cup\\{g_{\sigma}:\sigma\in\Gamma\cap\overline{S}\\}$ and $\Lambda$ is a
set of atoms over $\\{g_{\sigma}:\sigma\in S\\}$ that spawn the freest model
$F_{\\{g_{\sigma}:\sigma\in S\\}}(\emptyset)$, we can write
$F_{S}^{E}=N_{S}+F_{\\{g_{\sigma}:\sigma\in S\\}}(\emptyset)$ and, since the
sets of constants of both models are disjoint $F_{S}^{E}=N_{S}\oplus
F_{\\{g_{\sigma}:\sigma\in S\\}}(\emptyset)$. It follows that the extended
embedding is explicit.
(iii) We showed above that $(F_{S}^{E})^{|C}=N_{S}^{|C}\approx F_{S}$.
(iv) Theorem 9 says that an embedding is concise if and only if for each
solution $S$ the freest solution model $F_{S}$ restricted to the
interpretation constants $Q$ is equal to $F_{Q}(S)$ for each solution $S$ of
$P$. Using (iii), from $(F_{S}^{E})^{|C}=F_{S}$ we get
$(F_{S}^{E})^{|Q}=((F_{S}^{E})^{|C})^{|Q}=F_{S}^{|Q}$ so the extended
embedding is concise if and only if the original embedding is concise.
(v) The diagram above shows that $F_{C^{E}}(R^{E+})^{|C}=F_{C}(R^{+})$, so for
every positive atomic sentence $r^{+}$ over the interpretation constants
$Q\subseteq C$ we have that $R\vdash r^{+}$ if and only if $R^{E}\vdash r^{+}$
and then the extended embedding is complete if and only if the original
embedding is complete. ∎

######  Theorem 23.

An irreducible model of a set $R$ of duples has at most $|R^{-}|+1$ atoms.

###### Proof.

It is a consequence of two facts: it is enough with one atom to discriminate
any negative duple and removing atoms from a model of $R^{+}$ always produces
a model of $R^{+}$. Atoms can be removed from a model as long as $R^{-}$ is
still satisfied and there is an atom in the lower atomic segment of every
constant. Since $\ominus_{C}$ is in every model, adding $\ominus_{C}$ to an
atomization suffices to ensure that the sixth axiom of atomized semilattices
is satisfied. Hence, it is always possible to remove some atom from an
atomized model that has more than $|R^{-}|$ atoms and still get a model of $R$
if we add $\ominus_{C}$ when needed. It follows that an irreducible model of
$R$ should always have fewer than $|R^{-}|+1$ atoms. ∎

######  Theorem 24.

Consider an algebraic embedding for a problem $P$ with embedding set $R$ and a
scope sentence $\Xi$ that can be written as a conjunction of disjunctions,
i.e. $\Xi=\wedge_{i}\xi_{i}$, with each $\xi_{i}$ a disjunction of positive
atomic sentences.
i) Every irreducible model of a solution $S$ is an irreducible model of $R$.
ii) For each solution $S$ of $P$ there is an irreducible model of $R$ that can
be identified with $S$.
iii) If $R$ is a tight embedding, for each solution $S$ of $P$ there is an
irreducible model of $R$ atomized with non-redundant atoms of $F_{C}(R^{+})$
that can be identified with $S$.

###### Proof.

A solution model is any model of $R\cup\\{\Xi\\}$. If
$\,\Xi=\wedge_{i}\xi_{i}$ is a conjunction of disjunctions of positive atomic
sentences in a set $\Lambda$, we can express $\Xi$ in disjunctive normal form
as a disjunction $\Xi=\vee_{k}\Xi_{k}$ of conjunctions $\Xi_{k}$ of positive
atomic sentences in the same set $\Lambda$. The index $k$ usually runs along a
much larger set of values than the original index $i$ and most values of $k$
correspond to clauses $\Xi_{k}$ satisfied by no solution of $P$. However,
every solution $S$ must satisfy at least one clause $\Xi_{k}$. If $S$
satisfies more than one $\Xi_{k}$ we can do the conjunction of these so,
without loss of generality, we can assume there is a single value of $k$, the
value $k(S)$, that maps to the solution $S$. Because $\Xi_{k(S)}$ contains
only positive atomic sentences $R^{+}\cup S\Rightarrow\Xi_{k(S)}$. It follows
that a model of a solution $S$ is any model of the set of atomic sentences
$R_{S}=R^{+}\cup R^{-}\cup S$.
(i) Suppose $M$ is an irreducible model of $R_{S}$, i.e. it is not possible to
remove a non-redundant atom of $M$ and still model $R_{S}$. It is clear that
$M$ is a model of $R=R^{+}\cup R^{-}$. We argue that $M$ is also an
irreducible model of $R$. The elimination of one or many atoms from a model
preserves the positive atomic sentences entailed by the model, i.e. any
elimination of atoms from $M$ still models $R^{+}\cup S$. Therefore, since $M$
is an irreducible model of $R_{S}$ after the elimination of an atom the model
spawned by the remaining atoms should not satisfy at least one negative atomic
sentence in $R^{-}$, which means that $M$ is an irreducible model of $R$.
(ii) We have assumed $R$ is an embedding set of $P$ so there are models of $R$
for each solution $S$. These solution models are the models of $R_{S}$. We can
find irreducible models for any set of atomic sentences, so $R_{S}$ should
have irreducible models and according to part (i) these models are also
irreducible for $R$. Therefore, we can find for each solution $S$ an
irreducible model of $R$ that models $S$.
(iii) If the embedding is tight the non-redundant atoms of the freest solution
model $F_{S}=F_{C}(R^{+}\cup S)$ are all non-redundant atoms of
$F_{C}(R^{+})$. It is clear that $F_{S}\models R_{S}$. We start with $F_{S}$
atomized with non-redundant atoms and select a subset $M$ of the atoms of
$F_{S}$ that suffice to satisfy $R^{-}$ and such that it cannot be made
smaller, i.e. an irreducible model of $R_{S}$. From part (i), $M$ is an
irreducible model of $R$ and is atomized by non-redundant atoms of
$F_{C}(R^{+})$. ∎

##  11 Context Constants

Context constants are useful to build explicit embeddings that can be used in
practice. In lemma 10.1 a different context constant $g_{\sigma}$ is used for
each duple $\sigma$. We will see in this section that we can reuse some of our
context constants and still obtain an explicit embedding.

Consider the following observation:

######  Lemma 11.1.

Lemma 10.1 holds if duples $\sigma^{\prime}$ are defined as
$\sigma^{\prime}\equiv(a\leq b\odot g)$ where the same constant $g$ is used
for every $\sigma$ (instead of a different constant $g_{\sigma}$).

###### Proof.

The restriction to $C$ of $M_{R^{\prime}}$ should be equal to $M$ as the
duples of the form $\sigma^{\prime}$ have no consequences in the space spawned
by the constants in $C$. With the new definition for $\sigma^{\prime}$ the
proof of lemma 10.1 still holds step by step. We get to a model
$M_{R^{\prime}}=M_{R}\cup\\{\phi_{g}\bigtriangledown X\\}$ where $X$ is some
set of atoms and $\phi_{g}$ is an atom with an upper constant segment equal to
$g$. From here it follows immediately that $M_{R}\sqsubset M_{R^{\prime}}$ and
$M_{R}=M^{{}^{\vee}C}_{R^{\prime}}$. ∎

Lemma 11.1 is simpler than lemma 10.1 as it uses a single “context constant”
but it is also weaker than lemma 10.1. In fact, we cannot prove theorem 22
from it. A stronger version of 10.1 is the following:

######  Lemma 11.2.

Let M be a semilattice model with constants $C$ and $R=\\{\sigma_{i}:i\in
I\\}$ a set of positive duples over $C$ indexed by a set $I$ and let
$M_{R}\equiv F_{C}(Th^{+}_{0}(M)\cup R)$. Extend the constants with an
additional set of (context) constants $G$ disjoint with $C$, to an extended
set $C^{\prime}=C\cup G$ and for every duple $\sigma_{i}\equiv(a_{i}\leq
b_{i})$ of $R$ define one or many duples $\sigma_{ij}^{\prime}\equiv(a_{i}\leq
b_{i}\odot g_{ij})$ where $g_{ij}\in G$. Let $R^{\prime}$ be the set of such
duples $\sigma_{ij}^{\prime}$ and let $M_{R^{\prime}}\equiv
F_{C^{\prime}}(Th^{+}_{0}(M)\cup R^{\prime})$; then $M_{R}\sqsubset
M_{R^{\prime}}$ and the restriction and grounding to $C$ satisfy
$M_{R^{\prime}}^{|C}=M$ and $M_{R^{\prime}}^{{}^{\vee}C}\approx M_{R}$
respectively.

Lemma 11.2 can be proven in the same way as lemma 10.1. This lemma says that
we can use the same context constant for all the duples or one context
constant for each duple or any choice of context constants in between. In
addition, a duple $\sigma$ of $R$ can have in $R^{\prime}$ one or many
$\sigma^{\prime}$ by using one or many constants in $G=C^{\prime}-C$.

Theorem 22 implies that we can find the freest solution model of every
solution $S$ by calculating the grounding
$N_{S}=F_{C^{\prime}}(R^{+}\cup\Gamma^{\prime})^{{}^{\vee}C_{S}}$ to some
subset $C_{S}\subseteq C^{\prime}$. We proved theorem 22 from lemma 10.1 and
we can also prove it from lemma 11.2 although not every choice of context
constants works in this case. We will need a set of context constants
sufficiently large to “separate” every solution $S$ of the problem $P$ as the
grounded model to some subset $C_{S}$:

######  Theorem 25.

Let $R$ be an embedding set over $C$ for a problem $P$ with interpretation
$(Q,{\bf{\varphi}},\Gamma)$ and a scope sentence $\Xi$ that is a first order
sentence without quantifiers and with atomic subclauses in the separator set
$\,\Gamma$. Assume $C$ is extended to $C^{\prime}=C\cup G$ with an additional
set of (context) constants $G$, disjoint with $C$ and such that for each
$\sigma_{i}\equiv(a_{i}\leq b_{i})$ in the separator set $\Gamma$ there is one
or many $\sigma_{ij}^{\prime}\equiv(a_{i}\leq b_{i}\odot g_{ij})$ in a set
$\Gamma^{\prime}$ where $g_{ij}\in G$.
The embedding $R\cup\Gamma^{\prime}$ over $C^{\prime}$ is explicit if and only
if for each solution $S\subseteq\Gamma$ there is at least one set
$G_{S}\subseteq G$ of context constants such that:
\- if $\sigma\in\Gamma$ appears as $\sigma^{\prime}\in\Gamma^{\prime}$ using a
context constant from $G_{S}$ then $\sigma\in S$, and
\- for every $\sigma\in S$ there is at least one
$\sigma^{\prime}\in\Gamma^{\prime}$ that uses a context constant in $G_{S}$.

###### Proof.

We can follow the steps of the proof of theorem 22. To build this proof we
relied on a diagram that requires the existence of a subset of constants
$C_{S}$. We can relax the requirement of having a different context constant
for each atomic sentence $\sigma$ in $\Gamma$ as long as there is still a
suitable subset $C_{S}$ of the extended set of constants $C^{\prime}$. We
claim that $C_{S}=C-G_{S}$ is such suitable subset.
In the proof of theorem 22 we had
$N_{S}=F_{C^{\prime}}(R^{+}\cup\Gamma^{\prime})^{{}^{\vee}C_{S}}$ where
$N_{S}$ is a freest solution model for $S$. For this equality to hold, a
$\sigma^{\prime}\in\Gamma^{\prime}$ that uses a context constant in the set
$C^{\prime}-C_{S}$ (i.e. in $G_{S}$) should correspond to a $\sigma\in S$,
otherwise the grounded model
$F_{C^{\prime}}(R^{+}\cup\Gamma^{\prime})^{{}^{\vee}C_{S}}$ would satisfy a
positive duple that is not satisfied by the freest solution model of $S$. We
also need for every $\sigma\in S$ at least one
$\sigma^{\prime}\in\Gamma^{\prime}$ that uses a context constant in
$C^{\prime}-C_{S}$ otherwise the grounded model
$F_{C^{\prime}}(R^{+}\cup\Gamma^{\prime})^{{}^{\vee}C_{S}}$ does not satisfy
$\sigma\in S$ and it cannot be a solution model of $S$. ∎

It may seem at first glance that in order to use theorem 25 we need to know
the solutions $S$ in advance, but this is not true. We use theorem 25 to
reduce the number of context constants in the vertical bar and the hamiltonian
graph embeddings without knowing the solutions.

##  12 Acknowledgments

We thank Nabil Abderrahaman Elena, Antonio Ricciardo, Emilio Suarez and David
Mendez for critical comments on the manuscript. We are grateful for the
support from Champalimaud Foundation (Lisbon, Portugal) provided through the
Algebraic Machine Learning project, from Portuguese national funds through FCT
in the context of the project UIDB/04443/2020, and from the European
Commission provided through projects H2020 ICT48 _Humane AI; Toward AI Systems
That Augment and Empower Humans by Understanding Us, our Society and the World
Around Us_ (grant $\\#820437$) and the H2020 ICT48 project _ALMA: Human
Centric Algebraic Machine Learning_ (grant $\\#952091$).

##  13 Notation

We use repetition of subscripts (Einstein notation) such as $\vee_{i}x_{i}$ to
mean $\vee^{b}_{i=a}x_{i}$ for some omitted limits $a$ and $b$ when $a$ and
$b$ are obvious. Sometimes we just omit one of the limits, for example we
write $\vee^{b}_{i}x_{i}$.

We use $Th^{+}_{0}(M)$ to refer to the set of all positive atomic sentences
satisfied by $M$ and $Th^{-}_{0}(M)$ to refer to the set of all positive
atomic sentences not satisfied by $M$. We read them as the positive or
negative theory of $M$ with 0 quantifiers.

We say that a model $M$ has an atom $\phi$ if either $\phi$ is a non-redundant
atom of $M$ or $\phi$ is redundant with $M$. If a model $M$ has an atom or not
is independent of its atomization. We sometimes write $\phi\in M$. If $M$ has
an atom $\phi$ then we say that it $\phi$ is in $M$ or is an atom of $M$.

If an atom $\phi$ is not in $M$ we say that it is out of $M$ or that is
external to $M$.

With respect to a model an atom can be in three possible situations: it can be
external to the model, it can be a non-redundant atom of the model or it can
be a redundant atom with the model.

We say that an atom is in $M$, written $\phi\in M$, if $\phi$ is a non-
redundant atom in $M$ or if it is redundant with $M$. An atom is universally
defined independent of the model. With respect to a model an atom can be in
three situations: it is either a non-redundant atom in the model OR redundant
with the model OR out of the model.

We often use the same letter for a model and its atomization. Since redundant
atoms can be discarded from an atomization and the remaining set of atoms
still spawns the same model there are many valid atomizations of a model. We
use the same letter for a model and for its atomization when the particular
atomization chosen is not relevant. Alternatively, we can consider that a set
of atoms that has the same name than the model they spawn contains all the
atoms of the model.

A model $M$ is a subset model of $N$, written $M\subset N$ if every atom that
is in model $M$ is in model $N$. A model $M$ is a tight subset model of $N$,
written $M\sqsubset N$ if the non-redundant atoms of $M$ are a subset of the
non-redundant atoms of $N$. We use $\square_{w}M$ to represent the result of
full-crossing $w$ on $M$. The crossing of a duple $w$ on a model $M$ produces
a strictly less free model. Any atom of $\square_{w}M$ is either a non-
redundant atom of $M$ or redundant with $M$, i.e. is in $M$ and we can write
$\square_{w}M\subset M$.

We say a sentence $\Xi$ has no negative subclauses if once is expressed in
disjunctive normal form it only has positive subclauses.

## References

  * [1] Fernando Martin-Maroto and Gonzalo G. Polavieja “Finite Atomized Semilattices” In _arXiv:2102.08050_ , 2021
  * [2] Stanley Burris and H.. Sankappanavar “A course in universal algebra” Springer-Verlag, 1981
  * [3] David Marker “Model Theorey: An Introduction” Springer-Verlag, 2000
  * [4] Fernando Martin-Maroto and Gonzalo G. Polavieja “Algebraic Machine Learning” In _arXiv:1803.05252_ , 2018