# Homomorphism Preservation Theorems for Many-valued Structures

James Carr  University of Queensland

###### Abstract.

A canonical result in model theory is the homomorphism preservation theorem
(h.p.t.) which states that a first-order formula is preserved under
homomorphisms on all structures if and only if it is equivalent to an
existential-positive formula, standardly proved via a compactness argument.
Rossman (2008) established that the h.p.t. remains valid when restricted to
finite structures. This is a significant result in the field of finite model
theory. It stands in contrast to the other preservation theorems proved via
compactness where the failure of the latter also results in the failure of the
former [1],[23]. Moreover, almost all results from traditional model theory
that do survive to the finite are those whose proofs work just as well when
considering finite structures. Rossman’s result is interesting as an example
of a result which remains true in the finite but whose proof uses entirely
different methods. It is also of importance to the field of constraint
satisfaction due to the equivalence of existential-positive formulas and
unions of conjunctive queries [7]. Adjacently, Dellunde and Vidal (2019)
established a version of the h.p.t. holds for a collection of first-order
many-valued logics, namely those whose structures (finite and infinite) are
defined over a fixed finite MTL-chain.

In this paper we unite these two strands. We show how one can extend Rossman’s
proof of a finite h.p.t. to a very wide collection of many-valued predicate
logics. In doing so, we establish a finite variant to Dellunde and Vidal’s
result, one which not only applies to structures defined over algebras more
general than MTL-chains but also where we allow for those algebra to vary
between models. We identify the fairly minimal critical features of classical
logic that enable Rossman’s proof from a model-theoretic point of view, and
demonstrate how any non-classical logic satisfying them will inherit an
appropriate finite h.p.t. This investigation provides a starting point in a
wider development of finite model theory for many-valued logics and, just as
the classical finite h.p.t. has implications for constraint satisfaction, the
many-valued finite h.p.t. has implications for valued constraint satisfaction
problems.

##  1\. Introduction

Preservation theorems are a group of results from model theory that describe
relationships between syntactic and semantic properties of first-order
formulas. Three fundamental preservation theorems dating from the 1950s are
the Łos–Tarski theorem [17, Theorem 5.4.4], Lyndon’s positivity theorem [19,
Corollary 5.3] and the homomorphism preservation theorem (h.p.t.) [22, Theorem
1.3]. Each states that a certain syntactic class of formulas contains (up to
logical equivalence) all first-order formulas preserved under a particular
kind of homomorphism, and each is standardly proved via compactness. Their
place in traditional classical model theory naturally motivated an interest in
their status in other model-theoretic contexts. Two in particular are finite
model theory and many-valued logics.

It was known for some time that many famous theorems about first-order logic
fail when restricted to finite structures, including the bedrock compactness
theorem[14, Chapter 0]. This failure suggested that theorems which utilised
compactness in their proofs might also fail; indeed both the Łos–Tarski [23]
and Lyndon positivity theorem [1, 15] fail in the finite. By contrast, Rossman
(2008) established that the h.p.t. remains valid when restricted to finite
structures. This result is an interesting example in the world of finite model
theory, frequently the results and techniques from traditional model theory
that do survive to the finite (such as Ehrenfeucht–Fraïssé games [14, Chapter
1]) are those whose proofs work just as well when considering only finite
structures. With Rossman’s result we have a theorem which remains true in the
finite but whose proof uses entirely different methods.111Notably, Rossman’s
proof strategy can be used retroactively in the infinite setting. That is, one
way to understand why the h.p.t. remains true in the finite is that whilst the
h.p.t. is usually proved via compactness there are compactness free proof
strategies which the finite setting brings to light. This is not simply a
curiosity, it has substantive consequences. The compactness-free strategy
provides a refinement of the standard h.p.t. to an ’equirank version’ which
Rossman also proves [22, Theorem 4.12]. We will pick this up again in section
7.

A separate stand is the status of preservation theorems in non-classical
logics - especially many-valued ones. Dellunde and Vidal (2019) established a
version of the h.p.t. that holds for structures defined over a fixed finite
MTL-chain. MTL-algebras provide the algebraic semantics for the monoidal
t-norm logic MTL, a basic propositional fuzzy logic that encompasses the most
well-studied fuzzy logics including Hájek’s basic logic BL, Gödel–Dummett
logic G and Łukasiewicz logic Ł [16, Chapter 1, Section 2]. MTL-chains are the
finitely subdirectly irreducible MTL-algebras [21] and so provide a natural
restricted class to work over that is better behaved [12]. Accordingly,
Dellunde and Vidal’s result applies to a significant collection of first-order
many-valued logics. The choice to work with a finite MTL-chain is far from
arbitrary, rather it reflects a common pattern in research into non-classical
logic:

  1. (1)

Identify a potential theorem about classical logic to be generalised to non-
classical settings, adjusting concepts involved if needed.

  2. (2)

Attempt a proof in a non-classical logic as weak as possible whilst being able
to formulate the theorem in question.

  3. (3)

Strengthen the logic you work with, bringing it closer to classical logic, in
accordance with problems arising in attempted proofs.

  4. (4)

Ideally, demonstrate that the aspects of classical logic adopted were
necessary through counterexamples.

Rather than a strict ordering these steps feed into each other. For example,
the setting of a proof will affect how classical concepts are appropriately
generalised or exactly which generalised concepts one decides to work with
affects what aspects of classical logic may be relevant. In a model-theoretic
concept this process plays out especially with regard to the algebra that
models are defined over. When it comes to Dellunde and Vidal’s work, the
essential components are a form of compactness theorem and a condition on
models called witnessing, and the importance of these are what motivates the
finite MTL-chain setting.

Our investigation picks up at the meeting point of these two strands. We will
demonstrate how one can extend Rossman’s proof of a finite h.p.t. to a very
wide collection of many-valued predicate logics. In doing so we establish a
finite variant to Dellunde and Vidal’s result, a variant which not only
applies to structures defined over more general algebras than MTL-chains, but
also where we allow for the algebra our structures are defined over to vary.
The paper proceeds as follows. In Section 3 we properly introduce our many-
valued models including both the class of algebras we define our models over
and the models themselves. We’ll also introduce the appropriate
generalisations of the essential model-theoretic concepts we are interested
in. In Section 4 we turn to an important piece of background theory -
back-&-forth systems. These have already been investigated in a many-valued
context [11] and we recall this work whilst making small adaptations fit for
our context. In Section 5 we introduce existential-positive sentences in the
many-valued context, noting that in their generalisation we see a splitting of
one syntactic class into a collection of interrelated classes. Accordingly, we
identify the appropriate generalisation of the h.p.t. in our many-valued
context by proving the straightforward direction of the theorem, before
turning to the proof of the main theorem in Section 6. We finally consider in
Section 7 some variants of the the main theorem and tie it directly to the
work of Dellunde and Vidal before concluding with some remarks about further
study.

##  2\. Related Work

Our work sits firmly within the wider project of developing finite model
theory for many-valued logics begun in recent years. In the same fixed and
finite MTL-chain setting as Dellunde and Vidal’s work there have been
investigations into the status of other preservation theorems. These have been
quite successful, including a proof of a generalised Łos–Tarski theorem and a
Chang–Łos–Suszko theorem which links $\forall_{2}$ formulas to preservation
under unions of chains [3].

Much of this work is built on the generalisation of fundamental concepts of
classical model theory to the non-classic setting. This includes understanding
the different types of maps one can define between many-valued models [10],
the method of diagrams [9], back-and-forth systems [11] and Löwenheim–Skolem
theorems [10]. Other themes explored in the literature include developing
appropriate 0-1 law equivalents in the many-valued setting [2, 4].

Directly adjacent to our main interest in homomorphism preservation theorems
in finite models is the field of constraint satisfaction problems . The
classical constraint satisfaction problem (CSP) is closely connected with
classical finite-model theory as finite databases are naturally represented by
classical finite models in relational signatures. Moreover, there is an
equivalence between existential-positive formulas and unions of conjunctive
queries [7] (the syntactic class and query class that the h.p.t. and CSP are
concerned with respectively). This means Rossman’s result is of direct
consequence for the CSP field [22]. Similarly, Dellunde and Vidal’s
investigation is further motivated by the application of models defined over
MTL-algebras to valued constraint satisfaction problems (VCSP). A
generalisation of classical CSP, in a valued constraint satisfaction problem
the constraints are assigned some form of weighting which is optimised in the
solution. This has been effectively modelled by taking the weights as elements
of an algebra and utilising the algebraic operations to interpret their
combination in a potential solution [6].

##  3\. Preliminaries

We start by introducing the structures we are concerned with. These will
consist of two components, a non-empty set equipped with interpretations of
non-logical symbols akin to the familiar classical model and an algebra that
is used to define truth. As we will see, the choice of algebras we define our
structures over is intimately tied with the resulting properties of the
structures. In practice different motivations lead one to be concerned with
more specific algebras than what we introduce here, however we choose a level
of generality that can be applied cleanly to a multitude of cases.

######  Definition 3.1.

An abelian l-monoid is an algebra $A$ in signature
$\mathcal{L}=\langle\land,\lor,\&,1\rangle$ such that:

  * •

$\langle A,\land,\lor\rangle$ is a distributive lattice;

  * •

$\langle A,\&,1\rangle$ is a commutative (abelian) monoid;

  * •

$\forall a,b,c\in A$ $a\leq b$ implies $a\ \&\ c\leq b\ \&\ c$.

Moreover, we say an abelian l-monoid is $1$-$\lor$-prime iff $a\lor b\geq 1$
implies $a\geq 1$ or $b\geq 1$. As short hand, from now on we will refer to
$1$-$\lor$-prime abelian l-monoids as interpreting algebras. We will refer to
$\&$ as residuated conjunction.222This is inherited from contexts where the
monoid is residuated with its residuum $\rightarrow$ acting as an
interpretation for implication. Our investigation is not concerned with the
implication connective which is why we do not require it in our algebra
definition.

######  Remarks 3.2.

The restriction to $1$-$\lor$-prime algebras may seem unmotivated, but we will
later see that it is an essential restriction (example 5.8).

This setting encompasses a number of the algebras that many-valued models have
been investigated over in the literature. From a logical perspective, it
covers UL-algebras. UL-algebras are the algebraic semantics of the uninorm
logic and are abliean l-monoids which are further bounded, residuated and
prelinear. These are discussed in the context of many-valued models in [11].
Subdirectly irreducible UL-algebras are linearly ordered, (and referred to as
UL-chains), and attention is often restricted to models defined over UL-chains
rather than all UL-algebras. The linear order implies that UL-chains are
$1$-$\lor$-prime, so our setting more accurately applies to models defined
over UL-chains.

As previously mentioned, MTL-algebras are the algebraic semantics for the
monoidal t-norm logic and a homomorphism preservation theorem for (possibly
infinite) models defined over a fixed and finite MTL-chain was established in
[12]. They are the integral restrictions of UL-algebras meaning that the unit
ofresiduated conjunction $\&$ is also the top element of the lattice. MTL-
algebras are one of the potential candidates for interpreting valued
constraint satisfaction problems, another class of algebras discussed in the
VCSP context are linearly-ordered integral abelian monoids [18]. These are
also covered by our $1$-$\lor$-prime interpreting algebras, in our setting we
drop the integral restriction and weaken linearity to the prime property. The
most general approach towards the study of VCSP complexity takes c-semirings
(semirings with a few additional constraints) as their evaluating algebras
[6]. These are also integral in the above sense, but are not interpreting
algebras. However, due to their integrality there is something we can say, and
we return to consider the integral setting in Section 7.

There is one piece of elementary behaviour of the lattice connectives of an
interpreting algebra that is essential for our investigation and worth
highlighting.

######  Lemma 3.3.

Let $A$ be an interpreting algebra. Then $\forall a,b\in A$:

$\displaystyle a\land b\geq 1$ $\displaystyle\text{ iff }a\geq 1\text{ and
}b\geq 1$ $\displaystyle a\lor b\geq 1$ $\displaystyle\text{ iff }a\geq
1\text{ or }b\geq 1.$

###### Proof.

The left to right direction in the second claim is simple
$1$-$\lor$-primeness. The rest are basic properties of lattices. ∎

We define our many-valued structures over interpreting algebras.

######  Definition 3.4.

A predicate language $\mathcal{P}$ is a pair $(P,F)$ where $R$ is a non-empty
set of predicate symbols and $F$ a set of function symbols (disjoint from $P$)
all of which comes with an asigned natural number that is its arity. The
predicate symbols of arity zero are called truth constants while the function
symbols with arity zero are called object constants.

We fix a propostional language $\mathcal{L}$ such that
$\\{\lor,\land,\&\\}\subseteq\mathcal{L}$ and a countable set of variable’s
$Var$. We then define the set of $\mathcal{P}$-terms and
$\mathcal{P}$-formulas inductively as in classical logic. That is the set of
$\mathcal{P}$-terms is the minimum set $X$ such that:

  * •

$Var\subseteq X$,

  * •

If $t_{1},...t_{n}\in X$ and $f$ is an $n$-ary function symbol of
$\mathcal{P}$ then $f(t_{1},...t_{n})\in X$.

The set of $\mathcal{P}$-formulas is the minimum set $X$ such that:

  * •

$X$ contains all expressions of the form $P(t_{1},...,t_{n})$ where $P$ is an
$n$-ary predicate symbol and $t_{1},...,t_{n}$ are $\mathcal{P}$-terms. These
are the atomic $\mathcal{P}$-formulas

  * •

$X$ is closed under the propositional connectives of $\mathcal{L}$ (in
particular it contains all the truth constants of $\mathcal{L}$). If
$\varphi\in X$ and $x\in Var$ then $\forall x\varphi$ and $\exists x\varphi\in
X$.

We define the notions of free occurrence of a variable, open formula,
substitutability and sentence as in classical model theory. We assume that the
equality symbol $=$ is in the language and will be interpreted in every
structure as the crisp identity.

######  Remarks 3.5.

We introduce the language complete with function symbols. Whilst some of our
preliminary work applies to arbitrary languages for the main theorem we will
restrict to relational languages and structures.

######  Definition 3.6.

Let $\mathcal{P}$ be a predicate language and $A$ an interpreting algebra. We
define a $\mathcal{P}$-structure $\mathcal{M}$ as a pair $(A,M)$ where $A$ is
an interpreting algebra and $M$ is a triple $(M,\langle
P^{M}\rangle_{P\in\mathcal{P}},\langle F^{M}\rangle_{F\in\mathcal{P}})$ where:

  * •

$M$ is a non-empty set,

  * •

$F^{M}:M^{n}\rightarrow M$ for each $n$-ary function $F\in\mathcal{P}$
$(F^{M}\in M$ when $n=0$),

  * •

$P^{M}:M^{n}\rightarrow A$ for each $P\in\mathcal{P}$ ($P^{M}\in A$ when
$n=0$).

The set $M$ is called the domain of $\mathcal{M}$ and the mappings $F^{M}$ and
$P^{M}$ are called the interpretations of function and predicate symbols in
$\mathcal{M}$.

######  Remarks 3.7.

In the definition of structure we see an important difference between a
propositional truth-constant $d\in\mathcal{L}$ and an interpreted nullary
predicate symbol for $P\in\mathcal{P}$. The former is interpreted by the same
truth value $d\in A$ for each structure $(A,M)$. The latter does not come with
a fixed interpretation on the algebra, each structure assigns it some truth
value $P^{M}\in M$.

######  Definition 3.8.

As in classical logic, we define an $\mathcal{M}$-valuation of the object
variables is a mapping $v$ from the set of object variables $Var$ into $M$.
Given an $M$-valuation $v$, an object variable $x$ and an element $m\in M$ we
denote by $v_{x=m}$ the $M$-valuation defined as:

$v_{x=m}:=\begin{cases}m&\text{if }y=x\\\ v(y)&\text{otherwise}\end{cases}$

Given a $\mathcal{P}$-structure $\mathcal{M}$ we extend an $M$-valuation $v$
to all $\mathcal{P}$-terms by setting for each $n$-ary $f\in\mathcal{P}$:

$v(f(t_{1},...,t_{n})).$

Let $\mathcal{M}$ be a $\mathcal{P}$-structure. We define the value of
$\mathcal{P}$-terms and truth values of the $\mathcal{P}$-formulas for a given
$M$-valuation $v$ recursively as follows:

$\displaystyle||x||^{M}_{v}=v(x),$
$\displaystyle||F(t_{1},...,t_{n})||^{M}_{v}=F^{M}(||t_{1}||^{M}_{v},...,||t_{n}||^{M}_{v}),\text{
for each }n\text{-ary }F\in\mathcal{P},$
$\displaystyle||P(t_{1},..,t_{n})||^{M}_{v}=P^{M}(||t_{1}||^{M}_{v},...,||t_{n}||^{M}_{v}),\text{
for each }n\text{-ary }P\in\mathcal{P},$
$\displaystyle||\circ(\varphi_{1},...,\varphi_{n})||^{M}_{v}=\circ^{A}(||\varphi_{1}||^{M}_{v},...,||\varphi_{n}||^{M}_{v}),\text{
for each }n\text{-ary }\circ\in\mathcal{L},$ $\displaystyle||\forall
x\varphi||^{M}_{v}=inf_{\leq}\\{||\varphi||^{M}_{v_{x=a}}:a\in M\\},$
$\displaystyle||\exists
x\varphi||^{M}_{v}=sup_{\leq}\\{||\varphi||^{M}_{v_{x=a}}:a\in M\\}.$

If the infimum or supremum does not exist we take the truth-value of such a
formula to be undefined. We say that a $\mathcal{P}$-structure is safe iff
$||\varphi||^{M}_{v}$ is defined for every formula and every valuation, and
reserve the term $\mathcal{P}$-model for safe $\mathcal{P}$-structures. We
will restrict attention to $\mathcal{P}$-models.

We denote by $||\varphi||^{M}=a$ for $a\in A$ that $||\varphi||^{M}_{v}=a$ for
all $M$-valuations $v$. Given a set of sentences $\Phi$ we say that
$\mathcal{M}$ is a model of $\Phi$, denoted $(A,M)\models\Phi$, iff for every
$\varphi\in\Phi$ $||\varphi||^{M}\geq 1$.

With the definition of validity in place many of the standard concepts from
model theory can be defined just as they are in classically, e.g. the theory
of a model is still just all the sentences that it models
$Th(\mathcal{M}):=\\{\varphi\in Fm:\mathcal{M}\models\varphi\\}$. Others
require adjustments and generalisations. Two straightforward concepts are
elementary equivalence and models of theories. In the case of elementary
equivalence we have the familiar notion and then a new stronger notion when
the interpreting algebra is the same.

######  Definition 3.9.

We say that two $\mathcal{P}$-models $\mathcal{M},\mathcal{N}$ are
elementarily equivalent, denoted $\mathcal{M}\equiv\mathcal{N}$ iff
$Th(\mathcal{M})=Th(\mathcal{N})$.

We say that two $\mathcal{P}$-models $M,N$ defined over the same interpreting
algebra $A$ are strongly elementarily equivalent, denoted $M\equiv^{s}N$ iff
for all $\varphi\in Fm$ $||\varphi||^{M}=||\varphi||^{N}$.

In full generality we can consider the models of theories defined over any
interpreting algebra. However, later we will want to make further restrictions
on the algebras we define models over to compare and contrast the resulting
model theoretic behaviour. It thus proves convenient to consider models
defined over specified classes of algebras.

######  Definition 3.10.

Let $\Phi$ be a $\mathcal{P}$ theory and $K$ a class of interpreting algebras.
We define the following sets of $\mathcal{P}$-models.

$\displaystyle Mod^{K}(\varphi)$ $\displaystyle:=\\{(A,M):A\in K,M\text{ a
safe structure over }A\text{ and }(A,M)\models\varphi\\}.$ $\displaystyle
Mod^{K}_{fin(\varphi)}$ $\displaystyle:=\\{(A,M):A\in K,M\text{ a safe finite
structure over }A\text{ and }(A,M)\models\varphi\\}.$

When $K=\\{A\\}$ we denote this $Mod^{A}(\varphi)$ and $Mod^{A}_{fin}(A)$.
When $K$ is the entire variety of interpreting algebras we omit reference to
it.

When we consider maps between structures we see a more radical departure from
the classical case with our previous single definition of morphism shattering
into a number of related notions. The landscape of maps between many-valued
models is discussed in both [10] and [11] along with some initial outlining of
the relationships between the different maps and motivates them. We highlight
three types of map (along with some additional properties they may have). Two
are pre-existing in the literature [10] whilst the third is new and motivated
by our current investigation.

######  Definition 3.11.

Let $(A,M),(B,N)$ be $\mathcal{P}$-models. A map $g\colon M\rightarrow N$ is a
protomorphism from $(A,M)$ to $(B,N)$ iff:

$\displaystyle\text{for every }F\in\mathcal{P}\text{ and }\bar{m}\in M\
g(F^{M}(\bar{m}))=F^{N}(g(\bar{m})).$ $\displaystyle\text{for every
}R\in\mathcal{P}\text{ and }\bar{m}\in M\ R^{M}(\bar{m})\geq 1\text{ implies
}R^{N}(g(\bar{m}))\geq 1.$

We say that a protomorphism is strict iff it satisfies the stronger condition:

$\text{for every }R\in\mathcal{P}\text{ and }\bar{m}\in M\;R^{M}(\bar{m})\geq
1\text{ iff }R^{N}(g(\bar{m}))\geq 1.$

We say that $g$ is an embedding iff it is strict and injective and an
isomorphism iff $g$ is a surjective embedding.

Let $f\colon A\rightarrow B$ and $g\colon M\rightarrow N$ be maps. We call the
pair $(f,g)\colon(A,M)\rightarrow(B,M)$ a homomorphism from $(A,M)$ to $(B,N)$
iff:

  * •

$f$ is a $\mathcal{L}$-homomorphism, i.e. it preserves the algebraic
connectives of interpreting algebras.

  * •

$g$ is a protomorphism from $(A,M)$ to $(B,N)$.

We say that a homomorphism $(f,g)$ is strict iff $g$ is strict, an embedding
iff $f$ is injective and $g$ is strict and injective and an isomorphism iff
$f$ and $g$ are surjective embedding.

Let $(f,g)\colon(A,M)\rightarrow(B,N)$ be a homomorphism. We say that $(f,g)$
is a strong homomorphism iff

$\text{for every }R\in\mathcal{P}\text{ and }\bar{m}\in
M\;f(R^{M}(\bar{m}))=R^{N}(g(\bar{m})).$

We define strong embeddings and strong isomorphisms as for homomorphisms.

######  Remarks 3.12.

In the classical case a number of these concepts collapse together. Working
over a fixed algebra means that any protomorphism is a homomorphsim when
paired with the identity map, and every strong homomorphism is strict. In
fact, because we only have two elements in the algebra strict and strong
homomorphisms coincide and the identity is the only available homomorphism of
algebras.

The notion of homomorphism can be thought of as the most direct attempt to
generalise the classical notion of homomorphism, in this case preserving the
relations that are true. Strong homomorphisms,first introduced in [13], come
from a categorical lens. They preserve the structure more rigidly demanding
equality of all relations rather than simply preserving truth.

Protomorphisms are a weakening of homomorphisms. They emerge from the
observation that there really is no interaction between the algebra and
structure map in the definition of homomorphism - we simply require the
algebra map to be present. This naturally suggests considering the weaker
notion where we do not require its presence, especially important when
considering models defined over algebras $A$ and $B$ when
$Hom(A,B)=\varnothing$.

######  Definition 3.13.

The existence of a given map between $\mathcal{P}$-models is a relation on the
class of $\mathcal{P}$-models and denoted as follows:

$\displaystyle(A,M)\rightarrow_{p}(B,N)$ $\displaystyle:\text{protomorphism}$
$\displaystyle(A,M)\rightarrow(B,N)$ $\displaystyle:\text{homomorphism}$
$\displaystyle(A,M)\rightarrow_{s}(B,N)$ $\displaystyle:\text{strong
homomorphism}$

##  4\. Back-and-forth systems

Before we begin our investigation into the finite homomorphism preservation
theorem for our many-valued models we first need to recover an important
model-theoretic tool - back-and-forth systems. Back-and-forth systems have
already been covered in a many-valued setting in [11] where a back-and-forth
system result for models defined over UL-algebras is established. An
effectively immediate generalisation of these proofs apply to models defined
over interpreting algebras. We include the details here for direct reference.

######  Definition 4.1.

Let $(A,M),(B,N)$ be $\mathcal{P}$-models. We say a partial mapping
$(p,r)\colon(A,M)\rightarrow(B,N)$ is a partial isomorphism from $(A,M)$ to
$(B,N)$ iff:

  1. (1)

$p$ and $r$ are embeddings.

  2. (2)

for every $\circ\in\mathcal{L}$ and $\bar{a}\in A:\bar{a}\in dom(p)$ and
$\circ(\bar{a})\in dom(p)$

$p(\circ^{A}(\bar{a}))=\circ^{B}(p(\bar{a})).$

  3. (3)

for every $F\in\mathcal{P}$ and $\bar{m}\in M:\bar{m},F^{M}(\bar{m})\in
dom(r)$

$r(F^{M}(\bar{m}))=F^{N}(r(\bar{m})).$

  4. (4)

for every $R\in\mathcal{P}$ and $\bar{m}\in M:\bar{m}\in dom(r)$

$p(R^{M}(\bar{m}))=R^{N}(r(\bar{m})).$

$(A,M)$ and $(B,N)$ are said to be finitely isomorphic, denoted
$(A,M)\cong_{f}(B,N)$ iff there is a sequence $\langle
I_{n}:n\in\omega\rangle$ with the following properties:

  1. (1)

Every $I_{n}$ is a non-empty set of partial isomorphisms from $(A,M)$ to
$(B,N)$ and $I_{n+1}\subseteq I_{n}$.

  2. (2)

Forth R: for every $(p,r)\in I_{n+1}$ and $m\in M$ $\exists(p,r^{\prime})\in
I_{n}:r\subseteq r^{\prime}$ and $m\in dom(r^{\prime})$.

  3. (3)

Back R: for every $(p,r)\in I_{n+1}$ and $n\in N$ $\exists(p,r^{\prime}\in
I_{n}:r\subseteq r^{\prime}$ and $n\in im(r^{\prime})$.

  4. (4)

Forth L: for every $(p,r)\in I_{n+1}$ and $a\in A$ $\exists(p^{\prime},r)\in
I_{n}:p\subseteq p^{\prime}$ and $a\in dom(p^{\prime})$.

  5. (5)

Back L: for every $(p,r)\in I_{n+1}$ and $b\in B$ $\exists(p^{\prime},r)\in
I_{n}:p\subseteq p;$ and $b\in im(p^{\prime})$.

We say $(A,M)$ and $(B,N)$ are $n$-finitely isomorphic, denoted
$(A,M)\cong_{n}(B,N)$ iff there is a sequence $\langle I_{m}:m\leq n\rangle$
with the preceding properties.

Alongside this generalised notion of partial isomorphism and b&f-system we
need a measure to compare with elementary equivalence. In classical logic this
is quantifier depth but here we need something finer grained.

######  Definition 4.2.

Let $\mathcal{P}$ be a predicate language. Given a $\mathcal{P}$-formula
$\varphi$ we define by induction the nested rank of $\varphi$, denoted
$nr(\varphi)$ as follows:

  * •

If $\varphi$ is atomic $nr(\varphi)=0$.

  * •

For every $\circ\in\mathcal{L}$ and $\varphi_{1},...,\varphi_{k}$
$nr(\circ(\varphi_{1},...,\varphi_{k}))=1+\sum\limits_{i=1}^{k}nr(\varphi_{i})$

  * •

For any $\mathcal{P}$-formula $\varphi(x)$ $nr(\forall x\varphi)=nr(\exists
x\varphi)=nr(\varphi)+3$.

We say two $\mathcal{P}$-models $(A,M)$ and $(B,N)$ are $n$-elementarily
equivalent, denoted $(A,M)\equiv_{n}(B,N)$ iff they are models of the same
$\mathcal{P}$-sentences up to nested rank $n$.

Now the proof of [11, Theorem 24] yields the corresponding theorem.

######  Theorem 4.3.

Let $\mathcal{P}$ be a finite relational language and $(A,M)$, $(B,N)$ be
$\mathcal{P}$-models and $n\in\omega$. Suppose $(A,M)\cong_{n}(B,N)$. Then
$(A,M)\equiv_{n}(B,N)$.

We get the infinite variant as a corollary:

######  Corollary 4.4.

Let $\mathcal{P}$ be a finite relational language and $(A,M)$ $(B,N)$ be
$\mathcal{P}$-models. Suppose $(A,M)\cong_{f}(B,N)$. Then $(A,M)\equiv(B,N)$.

In the fixed algebra case we may restrict out attention to partial isomorphism
where the left component is the identity. This can be convenient as it brings
us closer to the classical setting, allowing us to drop back from nested rank
to quantifier depth. This motivates the following definitions.333May is the
operative word here. One may still apply the general case and construct
partial isomorphisms where the algebra component is not the identity. This
does require working with nested rank again. We fix an interpreting algebra
$A$ and we use $M$ to denote the $\mathcal{P}$-model $(A,M)$.

######  Definition 4.5.

Let $M,N$ be $\mathcal{P}$-models. We say a partial mapping $r:M\rightarrow N$
is a simple partial isomorphism from $M$ to $N$ iff:

  1. (1)

$r$ is an embedding

  2. (2)

for every function symbol $F\in\mathcal{P}$ and $\bar{m}\in
M:\bar{m},F^{M}(\bar{m})\in dom(r)$

$\displaystyle r(F^{M}(\bar{m}))=F^{N}(r(\bar{m})).$

  3. (3)

for every predicate symbol $R\in\mathcal{P}$ and $\bar{m}\in M:\bar{m}\in
dom(r)$

$\displaystyle R^{M}(\bar{m})=R^{N}(r(\bar{m})).$

$M$ and $N$ are said to be simply finitely isomorphic, denoted $M\cong_{f}N$
iff there is a sequence $\langle I_{n}:n\in\omega\rangle$ with the following
properties:

  1. (1)

Every $I_{n}$ is a non-empty set of partial isomorphisms from $M$ to $N$ and
$I_{n+1}\subseteq I_{n}$

  2. (2)

Forth: For every $r\in I_{n+1}$ and $m\in M$ $\exists r^{\prime}\in
I_{n}:r\subseteq r^{\prime}$ and $m\in dom(r^{\prime})$.

  3. (3)

Back: For every $r\in I_{n+1}$ and $n\in N$ $\exists r^{\prime}\in
I_{n}:r\subseteq r^{\prime}$ and $n\in im(r^{\prime})$.

We say $M$ and $N$ are $n$-finitely isomorphic, denoted $M\cong_{n}N$ iff
there is a sequence $\langle I_{m}:m\leq n\rangle$ with the preceding
properties.

We then define $n$-elementary equivalence between for models $M$ and $N$
relative to $\mathcal{P}$-formulas with quantifier-depth at most $n$ rather
than nested rank at most $n$ (quantifier depth defined in the usual way for
classical logic). Following exactly the same proof as [11, Theorem 22] yields
the corresponding theorem and infinite corollary:

######  Theorem 4.6.

Let $\mathcal{P}$ be a finite relational language, $M$, $N$ be
$\mathcal{P}$-models and $n\in\omega$. Suppose $M\cong_{n}N$. Then
$M\equiv^{s}_{n}N$.

######  Corollary 4.7.

Let $\mathcal{P}$ be a finite relational language and $M$, $N$ be
$\mathcal{P}$-models. Suppose $M\cong_{f}N$. Then $M\equiv^{s}N$.

##  5\. Existential-Positive Sentences

Now we turn to the actual work of proving finite homomorphism preservation. We
note that from here on we restrict out attention to relational languages, that
is languages which only contain relation symbols (including those of 0-arity).
First we must make more precise the question we are asking. The syntactic
class of formulas we are interested in are the existential positive formulas.
In the classical setting these are defined as formulas build from only the
existential quantifier, disjunction and conjunction ($\exists$, $\lor$,
$\land$) and characterised as disjunctions of so called primitive positive
sentences, formulas built from only $\exists$ and $\land$ with a normal form:

$\exists\bar{x}\bigwedge\limits_{i=1}^{n}R_{i}(\bar{x_{i}}).$

where $\bar{x_{i}}$ denotes the subset of the free variables $\bar{x}$ that
$R$ takes as argument. In our context we have an additional notion of
residuated conjunction $\&$ to consider and its presence causes the classical
notion of existential-positive formulas to separate into three notions.

######  Definition 5.1.

Let $\mathcal{P}$ be a predicate language. We say a $\mathcal{P}$-sentence
$\varphi$ is a:

  1. (1)

$\land$-primitive formula iff
$\varphi=\exists\bar{x}\bigwedge\limits_{i=1}^{n}R_{i}(\bar{x_{i}})$.

  2. (2)

$\&$-primitive formula iff
$\varphi=\exists\bar{x}\bigodot\limits_{i=1}^{n}R_{i}(\bar{x_{i}})$.

  3. (3)

$\land$-$\&$-primitive formula (or primitive-positive) iff
$\varphi=\exists\bar{x}\bigwedge\limits_{i=1}^{n}\bigodot\limits_{j=1}^{m}R_{i,j}(\bar{x}_{i,j})$.

We extend these definitions and say $\varphi$ is:

  1. (1)

existential-$\land$-positive iff $\varphi=\bigvee\limits_{i=1}^{m}\psi_{i}$
where each $\psi_{i}$ is a $\land$.p-sentence.

  2. (2)

existential-$\&$-positive iff $\varphi=\bigvee\limits_{i=1}^{m}\psi_{i}$ where
each $\psi_{i}$ is a $\&$.p-sentence.

  3. (3)

existential-positive iff $\varphi=\bigvee\limits_{i=1}^{m}\psi_{i}$ where each
$\psi_{i}$ is a p.p-sentence.

We use $\bigodot\limits_{j=1}^{m}\varphi_{j}$ to denote $\varphi_{1}\ \&\ ...\
\&\ \varphi_{m}$.

######  Remarks 5.2.

In the classical case we usually define these as the formulas built from the
relevant connectives and show them to have such to have a canonical normal
form. Over certain weak algebras we may not have such an equivalence and so we
define them directly in the normal form. That said, in the context of finite
models over interpreting algebras we do have the required behaviour, namely
the various distribution laws regarding $\land$, $\lor$ and $\exists$.
Distributivity of $\land$ with $\lor$ and vice versa is built into the
definition of interpreting algebras, when it comes to the quantifier it
follows because we may essentially view $\forall$ and $\exists$ as conjunction
and disjunction respectively.

$||\forall x\varphi||^{M}_{v}=\bigwedge\\{||\varphi||^{M}_{v[x\mapsto m]}:m\in
M\\}\;\;||\exists x\varphi||^{M}_{v}=\bigvee\\{||\varphi||^{M}_{v[x\mapsto
m]}:m\in M\\}.$

Using this and regular distributivity between $\land$ and $\lor$ it is
straightforward (if tedious) to check that we have the desired distribution
laws for $\exists$ with $\land$ and $\lor$.

$\displaystyle||\exists x\exists y(\varphi(x)\land\psi(y))||$
$\displaystyle=||\exists x\varphi(x)\land\exists y\psi(y)||$
$\displaystyle||\exists x\exists y(\varphi(x)\lor\psi(y))||$
$\displaystyle=||\exists x\varphi(x)\lor\exists y\psi(y)||$

This outlines the syntax we are interested in, and the concepts necessary to
state our many-valued version of the finite homomorphism preservation. Given
that we’ve introduced a number of different maps between models alongside
classes of sentences that could act as generalisations of the two classical
notions, the question becomes which pairings are viable candidates. We
introduce two main homomorphism preservation theorems, one for the mixed
algebra case and another for the fixed algebra case.

######  Theorem 5.3 (Finite Protomorphism Preservation Theorem).

Let $\mathcal{P}$ be a predicate language and $\varphi$ a consistent
$\mathcal{P}$-sentence in the finite (i.e.
$Mod_{fin}(\varphi)\not=\varnothing)$. Then $\varphi$ is equivalent in the
finite to an e.$\land$.p-sentence $\psi$ iff $\varphi$ is preserved under
protomorphisms. That is there exists an e.$\land$.p-sentence
$\psi:Mod_{fin}(\varphi)=Mod_{fin}(\psi)$ iff $Mod_{fin}(\varphi)$ is closed
under $\rightarrow_{p}$.

######  Theorem 5.4 (Fixed Finite Homomorphism Preservation Theorem).

Let $\mathcal{P}$ be a predicate language, $A$ an interpreting algebra and
$\varphi$ a consistent $\mathcal{P}$ sentence over $A$ in the finite (i.e.
$Mod^{A}_{fin}(\varphi)\not=\varnothing$). The following are equivalent:

  1. i.

$\varphi$ is equivalent over $A$ in the finite to an e.$\land$.p sentence
$\psi$, i.e. there is an e.$\land$.p-sentence
$\psi:Mod^{A}_{fin}(\varphi)=Mod^{A}_{fin}(\psi)$.

  2. ii.

$\varphi$ is preserved under protomorphisms on $A$, i.e.
$Mod^{A}_{fin}(\varphi)$ is closed under $\rightarrow_{p}$.

  3. iii.

$\varphi$ is preserved under homomorphisms on $A$, i.e.
$Mod^{A}_{fin}(\varphi)$ is closed under $\rightarrow$.

In the most general setting we are currently working in these are the only two
viable candidates. Viable here simply means that the ‘easy’ direction of the
theorem holds, that formulas of the type in question are actually preserved by
the map in question. Proving that the e.$\land$.p and protomorphism pairing is
viable is a straightforward induction driven by the semantic properties of
$\exists,\land$ and $\lor$ we have already encountered. Whilst straightforward
it is worth belabouring the point a little to make clear exactly what
behaviour of interpreting algebras is driving this. For $\land$ and $\lor$
this is lemma 3.3. In the case of $\exists$ the critical property is the
finiteness of the model reducing $\exists$ to a large disjunction across all
elements of the domain combined with $1$-$\lor$-primeness. Together this means
that in the finite model setting the truth value of an e.$\land$.p-sentence in
a model is entirely determined at the atomic level and independent of the
given interpreting algebra.

######  Lemma 5.5.

Let $(A,M)$ be a finite $\mathcal{P}$-model and
$\psi=\bigvee\limits_{i=1}^{n}\theta_{i}$ an e.$\land$.p-sentence. Then
$(A,M)\models\psi$ iff $\exists 1\leq i\leq n:\exists\bar{m}\in M:$ for all
atomic subformula $R_{j}(\bar{x_{j}})\subseteq\theta_{i}$
$R^{M}_{j}(\bar{m_{j}})\geq 1_{A}$, where $\bar{m_{j}}$ denotes the
subsequence of $\bar{m}$ corresponding to the subsequence $\bar{x_{j}}$ of
$\bar{x}$.

###### Proof.

$\displaystyle(A,M)\models\psi\text{ iff }||\psi||^{M}\geq 1_{A}\text{ iff
}||\bigvee\limits_{i=1}^{n}\theta_{i}||^{M}\geq 1_{A}$ $\displaystyle\text{
iff }\exists 1\leq i\leq n:||\theta_{i}||^{M}\geq 1$ (lemma 3.3)
$\displaystyle\text{ iff }\exists 1\leq i\leq n:\bigvee\limits_{\bar{m}\in
M}||\bigwedge\limits_{j=1}^{M}R_{j}(\bar{x_{j}})||^{M}_{v[\bar{x}\mapsto\bar{m}]}||\geq
1_{A}$ finiteness of model $\displaystyle\text{ iff }\exists 1\leq i\leq
n:\exists\bar{m}\in
M:\bigwedge\limits_{j=1}^{m}||R_{j}(\bar{x_{j}})||^{M}_{v[\bar{x}\mapsto\bar{m}]}\geq
1_{A}$ $\displaystyle 1\text{-}\lor\text{-}\text{prime}$ $\displaystyle\text{
iff }\exists 1\leq i\leq n:\exists\bar{m}\in M:\text{ for all atomic
subformula }R_{j}\subseteq\theta_{i}||R_{j}(\bar{m_{j}})||\geq 1_{A}$
$\displaystyle\text{ (lemma \ref{lattruthfunctional})}.$

∎

With this we can quickly prove the easy direction of the f.p.p.t.

######  Lemma 5.6.

Let $\mathcal{P}$ be a predicate language and $\psi$ an e.$\land$.p-sentence.
$Mod_{fin}(\psi)$ is closed under $\rightarrow_{p}$.

###### Proof.

Suppose $(A,M)\models\psi$ and $(A,M)\rightarrow_{p}(B,N)$, i.e. $\exists
g\colon(A,M)\rightarrow(B,N)$ where $g$ is a protomorphism. By the previous
lemma $\exists 1\leq i\leq n:\exists\bar{m}\in M$ such that for all atomic
$R_{j}\subseteq\theta_{i}$ $R_{j}^{M}(\bar{m})\geq 1_{A}$. Therefore for all
atomic $R_{j}\subseteq\theta_{i}$ $R_{j}^{N}(g(\bar{m_{j}}))\geq 1_{B}$ and by
the previous lemma again $(B,N)\models\psi$. ∎

This of course immediately implies that $e$.$\land$.p-sentences are preserved
under homomorphisms. In the fixed algebra case any protomorphism is also a
homomorphism when paired with the identity map and so the converse is also
true, that is any formula is preserved under protomorphisms iff it is
preserved under homomorphisms. In the mixed algebra case the relationship
between protomorphisms and homomorphisms proper is more complicated and a
topic we’ll return to later.

The remaining sentence types both include the residuated conjunction $\&$.
When it comes to homomorphisms (and by extension protomorphisms) viability
fails.

######  Example 5.7.

Let $A$ be the standard UL-chain on $[0,1]$, that is we take $\land=min$,
$\lor=max$ and $\&=\ast\colon[0,1]^{2}\rightarrow[0,1]$ by

$x\ast y\begin{cases}min(x,y)&\text{if }y\leq 1-x\\\
max(x,y)&\text{o.w}.\end{cases}$

The unit of $\ast$ is $\frac{1}{2}$.

We consider $\mathcal{P}=\\{R,P\\}$ where both $R$ and $P$ are unary relation
symbols and define two models $M_{1}$ and $M_{2}$ over $A$ both with domain
$\\{m\\}$ and

$\displaystyle R^{M_{1}}(m)=\frac{5}{6}$ $\displaystyle
P^{M_{1}}(m)=\frac{4}{6}$ $\displaystyle R^{M_{2}}(m)=\frac{1}{3}$
$\displaystyle P^{M_{2}}(m)=\frac{1}{6}$

Then $M_{1}\rightarrow M_{2}$ via the double identity map, but we can make the
following calculations to show that the $e.p$-sentence $\exists x\exists
yR(x)\ \&\ P(y)$ is not preserved.

$\displaystyle||\exists x\exists yR(x)\ \&\
P(y)||^{M_{1}}=||R(m)||^{M_{1}}\ast||P(m)||^{M_{1}}=\frac{5}{6}$
$\displaystyle\ast\frac{1}{3}=\frac{5}{6}\geq\frac{1}{2}$
$\displaystyle||\exists x\exists yR(x)\ \&\
yP(y)||^{M_{2}}=||R(m)||^{M_{2}}\ast||P(m)||^{M_{2}}=\frac{4}{6}$
$\displaystyle\ast\frac{1}{6}=\frac{1}{6}<\frac{1}{2}.$

Again the status of sentences $e.\&.p$-sentences and $e.p$-sentences is a
question we’ll return to in Section 7.

The viability of the theorem also demonstrates the necessity in restricting to
$1$-$\lor$-prime algebras. Whilst the other claims concerning how $\land$ and
$\lor$ are truth functional with respect to $1$ made in lemma 3.3 can be seen
as inherent to these connective being a conjunction/disjunction, the
$1$-$\lor$-prime condition forms a more substantive restriction and one may
wonder if it can be dropped. It necessity can be easily demonstrated; without
it we lose viability.

######  Example 5.8.

Let $A$ be the $4$ element Boolean algebra considered as an interpreting
algebra where $1=\top$ and $\&=\land$ which we label as follows:

$\cdot$$\bot$$\cdot$$a$$\cdot$$b$$\cdot$$\top$

Taking $\mathcal{P}=\\{R\\}$ we define two $\mathcal{P}$-models over $A$
$\mathcal{M}_{1}$ and $\mathcal{M}_{2}$ with the same domain $M=\\{x,y\\}$ and

$\displaystyle R^{M_{1}}:\begin{cases}x\mapsto a\\\ y\mapsto b\end{cases}$
$\displaystyle R^{M_{2}}:\begin{cases}x\mapsto a\\\ y\mapsto\bot\end{cases}$

Then $\mathcal{M}_{1}\rightarrow_{p}\mathcal{M}_{2}$ via the identity but if
we consider the e.$\land$.p-sentence $\exists zR(z)$ we can easily check that:

$\displaystyle\mathcal{M}_{1}\models\exists zR(z)$
$\displaystyle\mathcal{M}_{2}\not\models\exists zR(z).$

##  6\. Finite Homomorphism Preservation

Let us turn to our core discussion - proving the harder direction of our
preservation theorems. The heart of our proof strategy is a recognition that
Rossman’s classical proof is fundamentally about the behaviour of models with
minimal interaction with the underlying logic. Similarly, as we demonstrated
in the previous section, protomorphisms and e.$\land$.p-sentences are
fundamentally concerned with whether certain atomic formula are true (mapped
to above $1$) or not. The specifics of the associated algebra do not matter.
This allows us to translate between $\mathcal{P}$-models over interpreting
algebras and a classical counterpart in such a way that the behaviour with
regards to protomorphisms and e.$\land$.p-sentences is preserved and then
apply Rossman’s result to the classical translations before pulling back to
the our own setting.

This translation can be introduced in a few different ways. Here it is
convenient to present it as a $\mathcal{P}$-model over the 2 element Boolean
algebra $\\{\top,\bot\\}$ which by inspection is an interpreting algebra
(where we take $\&=\land$).

######  Definition 6.1.

Let $(A,M)$ be a $\mathcal{P}$-model over an interpreting algebra $A$. We
define the $\mathcal{P}$-model $(\\{\top,\bot\\},M^{\top})$, also denoted
simply as $M^{\top}$ as follows:

$R^{M^{\top}}(\bar{m})=\begin{cases}\top&\text{ if }R^{M}(\bar{m})\geq
1_{A}\\\ \bot&\text{ if }R^{M}(\bar{m})<1_{A}.\end{cases}$

######  Remarks 6.2.

In the case where $R$ is a 0-ary relation symbol then it takes no argument
$\bar{m}$ from the model and accordingly $R^{M^{\top}}=\top$ iff $R^{M}\geq
1_{A}$ and $R^{M^{\top}}=\bot$ iff $R^{M}<1_{A}$.

The critical feature of the model just defined is that it is both a many-
valued $\mathcal{P}$-model taking values in the interpreting algebra
$\\{\top,\bot\\}$ and also simply a classical $\mathcal{P}$-model (utilising
characteristic functions). This allows us to apply results from classical
finite model theory such as Rossman’s. Of course, these results have a
specific meaning for $M^{\top}$ so we do need to understand how they apply to
our context. We make two observations. Firstly, if we consider two
$\mathcal{P}$-models $(A,M)$ and $(B,N)$ any back-and-forth system between
$M^{\top}$ and $N^{\top}$ as defined in definition 4.5 is also a classical
back-and-forth system between them viewed as classical models. We will
continue to use the notation $\cong^{n}_{f}$ and $\cong_{f}$ to state the
existence of such a back-&-forth system viewed in either sense. Secondly, a
straightforward induction establishes that for any
$\mathcal{L},\mathcal{P}$-sentences $\varphi$ such that $\varphi$ is a
$\mathcal{L}\cap\mathcal{L}(CL),\mathcal{P}$-sentence444That is $\varphi$ is a
sentence both in the language $\mathcal{L}$ and also the language of classical
logic. we have

$M^{\top}\models\varphi\text{ iff }M^{\top}\models_{cl}\varphi.$

The first basic relationship between a $\mathcal{P}$-model and its classical
counterpart is the precise version of the aforementioned mirroring for both
protomorphisms and e.$\land$.p-sentences.

######  Lemma 6.3.

Let $(A,M)$ be a $\mathcal{P}$-model. Then $(A,M)\leftrightarrows_{p}M^{\top}$
and for any e.$\land$.p-sentence $\psi$ $(A,M)\models\psi$ iff
$M^{\top}\models\psi$.

###### Proof.

We consider the map $id_{M}\colon M\leftrightarrows M$ and check it is a
protomorphism. Indeed for any $R\in\mathcal{P}$ and $\bar{m}\in M$
$R^{M}(\bar{m})\geq 1_{A}$ iff $R^{M{\top}}(\bar{m})=\top$ iff
$R^{M^{\top}}(\bar{m}))\geq\top$.

The second claim that follows immediately by lemma 5.6. ∎

The second relationship revolves around a concept central to Rossman’s proof,
the idea of $n$-homomorphisms themselvesdefined using the Gaifman graph of a
structure [22, Section 2&3].

######  Definition 6.4.

Let $(A,M)$ be a $\mathcal{P}$-model. We define its Gaifman graph, denoted
$G(A,M)$ as the graph with vertex set $M$ and $(m,n)\in E$ iff $\exists
R\in\mathcal{P}:\exists\bar{x}\in M:m,n\in\bar{x}$ and $R^{M}(\bar{x})\geq
1_{A}$.

We define the tree-depth of $(A,M)$, denoted $td(A,M)$ to be the tree-depth of
$G(A,M)$.

######  Remarks 6.5.

It is immediately clear that $G(A,M)=G(M^{\top})$, with the latter also being
the Gaifman graph of $M^{\top}$ when viewed as a classical structure.

We use this to define a form of protomorphism relative to tree-depth. Note
that we could do this for all the different kinds of maps we’ve introduced.

######  Definition 6.6.

Let $(A,M),(B,N)$ be $\mathcal{P}$-models. We say $(A,M)$ $n$-protomorphically
maps to $(B,N)$, denoted $(A,M)\rightarrow^{n}_{p}(B,N)$ iff for all
$\mathcal{P}$-models $(C,S)$ with $td(C,S)\leq n$ $(C,S)\rightarrow_{p}(A,M)$
implies $(C,S)\rightarrow_{p}(B,N)$.

We could equivalently define $\rightarrow^{n}_{p}$ via the translated
structures directly.

######  Lemma 6.7.

Let $(A,M),(B,N)$ be $\mathcal{P}$-models. $(A,M)\rightarrow^{n}_{p}(B,N)$ iff
$M^{\top}\rightarrow^{n}_{cl}N^{\top}$, that is iff for all classical models
$C:td(C)\leq n$ $C\rightarrow M^{\top}$ implies $C\rightarrow N^{\top}$.

###### Proof.

For the only if direction; let $(A,M)\rightarrow^{n}_{p}(B,N)$ and let $S$ be
a classical $\mathcal{P}$-model with tree-depth $\leq n$ such that
$S\rightarrow M^{\top}$. We can consider $S$ as a $\mathcal{P}$-model
$(\\{\top,\bot\\},S)$ over the 2 element Boolean algebra and the map
$S\rightarrow M^{\top}$ also witnesses
$(\\{\top,\bot\\}S)\rightarrow_{p}(A,M)$. $td(\\{\top,\bot\\},S)=td(S)\leq n$
therefore by assumption $(\\{\top,\bot\\},S)\rightarrow_{p}(B,N)$ and this
also witnesses that $S\rightarrow N^{\top}$ as required.

For the if direction; letting $M^{\top}\rightarrow^{n}_{cl}N^{\top}$ and
$(C,S)\rightarrow_{p}(A,M)$ with $td(C,S)\leq n$ then $S^{\top}\rightarrow
M^{\top}$ and $td(S^{\top})\leq n$ so $S^{\top}\rightarrow N^{\top}$ and this
also witnesses $(C,S)\rightarrow_{p}(B,N)$. ∎

With the two comparisons in place we can immediately prove a many-valued
version of Rossman’s main combinatorial result - the finite extendability
theorem.

######  Theorem 6.8 (Finite Proto Extendability Theorem).

Let $(A,M),(B,N)$ be $\mathcal{P}$-models such that
$(A,M)\leftrightarrows^{p(n)}_{p}(B,N)$555The function p(n) is defined
explicitly by Rossman [22, Remark 5.3], although it can be taken as any
’sufficiently increasing’ function. Then there exists two $\mathcal{P}$-models
$(\\{\top,\bot\\},\tilde{M})$ and $(\\{\top,\bot\\},\tilde{N})$ such that:

$(A,M)\leftrightarrows_{p}(\\{\top,\bot\\},\tilde{M})\equiv_{n}(\\{\top,\bot\\},\tilde{N})\leftrightarrows_{p}(B,N).$

###### Proof.

By lemmas 6.3 & 6.7 we have $(A,M)\leftrightarrows_{p}M^{\top}$,
$(B,N)\leftrightarrows_{p}N^{\top}$ and
$M^{\top}\leftrightarrows^{p(n)}N^{\top}$. Applying Rossman’s finite
extendability theorem [22, Corollary 5.14] for classical structures
$\exists\tilde{M},\tilde{N}$ such that $\tilde{M}\cong^{n}_{f}\tilde{N}$,
$M^{\top}\leftrightarrows\tilde{M}$ and $N^{\top}\leftrightarrows\tilde{N}$
(as classical structures). Taking composition of the following gives us the
first and last equivalence we need:

$(A,M)\leftrightarrows_{p}M^{\top}\leftrightarrows_{p}(\\{\top,\bot\\},\tilde{M})\;\;(\\{\top,\bot\\},\tilde{N})\leftrightarrows_{p}N^{\top}\leftrightarrows_{p}(B,N).$

For the last equivalence, viewing $\tilde{M}$ and $\tilde{N}$ as
$\mathcal{P}$-models $(\\{\top,\bot\\},\tilde{M})$ and
$(\\{\top,\bot),\tilde{N})$ we have
$(\\{\top,\bot\\},\tilde{M})\cong^{n}_{f}(\\{\top,\bot\\}),\tilde{N})$. Then
by theorem 4.6
$(\\{\top,\bot\\},\tilde{M})\equiv_{n}(\\{\top,\bot\\},\tilde{N})$. ∎

To prove our initial versions of the finite h.p.t. we need to get a little
deeper into the proof of Rossman’s result itself. First we quote the well-
known association with finite structures and $\land$-primitive formulas,
namely that for any classical finite structure $M$ there is a
$\land$-primitive sentence $\theta_{M}$ such that $qd(\theta_{M})=td(M)$ and
for any classical structure $N$ $M\rightarrow N$ iff $N\models\theta_{M}$ [22,
Lemma 2.14]. Secondly, we utilise the concept of an $n$-core of a classical
structure [22, Definition 3.10, Lemma 3.11]. Rossman develops a fair amount of
theory around $n$-cores, but for our purposes we just need that for any
classical structure $M$ and its $n$-core $Core^{n}(M)$ the following
properties hold:

$\displaystyle M\leftrightarrows^{n}Core^{n}(M)\>\>\>$ $\displaystyle
td(Core^{n}(M))=\leq n,$ $\displaystyle M\rightarrow^{n}N\text{ iff
}Core^{n}(M)\rightarrow N$ $\displaystyle\text{ for any classical structure
}N.$

We use our translated models to prove new versions of the two main components
to Rossman’s result. The first is a variant of [22, Lemma 3.16].

######  Lemma 6.9.

Let $P$ and $Q$ be classes of $\mathcal{P}$-models over interpreting algebras
such that for any pair of $\mathcal{P}$-models over interpreting algebras
$(A,M),(B,N)$, $(A,M)\in P$ and $(A,M)\rightarrow^{n}_{p}(B,N)$ implies
$(B,N)\in Q$. Then there is an e.$\land$.p-sentence of quantifier depth $n$
$\psi$ such that $P\subseteq Mod_{fin}(\psi)\subseteq Q$.

###### Proof.

We consider the set $P^{\top}=\\{M^{\top}:M\in P\\}$ and let $\mathbb{P}$ be
the set of $n$-cores of structures in $\mathcal{P}^{\top}$. This is finite so
let $\\{C_{n}\\}_{i=1}^{m}$ be its members and consider the $\land$-primitive
formula sentences $\theta_{i}$ corresponding to each $C_{n}$. We note that
each $\theta_{i}$ has quantifier depth $n$ and for any classical structure $D$
$C_{i}\rightarrow D$ iff $D\models_{cl}\theta_{i}$. We let
$\psi:=\bigvee\limits_{i=1}^{m}\theta_{i}$.

Now consider $(A,M)\in P$. $M^{\top}\in P^{\top}$ and
$Core^{n}(M^{\top})\in\mathbb{P}$, i.e. $Core^{n}(M^{\top})=C_{i}$ for some
$i\leq m$. A basic property of $n$-cores is that
$Core^{n}(M^{\top})\rightarrow M^{\top}$ [22, Definition 3.10] and so
$M^{\top}\models_{cl}\theta_{i}$ and consequently $M^{\top}\models\theta_{i}$
and moreover $M^{\top}\models\psi$. Then by lemma 6.3 $(A,M)\models\psi$ and
we have $P\subseteq Mod_{fin}(\psi)$

Let $(B,N)$ be a $\mathcal{P}$-model such that $(B,N)\models\psi$. By lemma
6.3 again $N^{\top}\models\psi$ so $N^{\top}\models\theta_{i}$ for some $i\leq
m$. Therefore, $N^{\top}\models_{cl}\theta_{i}$ and $C_{i}\rightarrow
N^{\top}$. Then $C_{i}\in\mathbb{P}$ so $C_{i}=Core^{n}(M^{\top})$ for some
$M^{\top}\in P^{\top}$ with $(A,M)\in P$. From [22, Definition 3.10] we have
$Core^{n}(M^{\top})\rightarrow N^{\top}$ implies
$M^{\top}\rightarrow^{n}N^{\top}$ and so by lemma 6.7
$(A,M)\rightarrow^{n}_{p}(B,N)$. Therefore, by our initial assumption
$(B,N)\in Q$ and $Mod_{fin}(\psi)\subseteq Q$ as required. ∎

The second main component to Rossman’s proof is using finite extendability to
check the sufficiency condition just established [22, Theorem 5.15]

######  Lemma 6.10.

Let $P$ and $Q$ be classes of $\mathcal{P}$-models over interpreting algebras
and $\varphi$ a $\mathcal{P}$-sentence with quantifier depth at most $n$ such
that for any $\mathcal{P}$-models $(A,M),(B,N)$ we have:

  * •

$(A,M)\in P$, $(A,M)\rightarrow_{p}(B,N)$ implies $(B,N)\models\varphi$.

  * •

$(A,M)\models\varphi$, $(A,M)\rightarrow_{p}(B,N)$ implies $(B,N)\in Q$.

Then $(A,M)\in P$ and $(A,M)\rightarrow^{p(n)}(B,N)$ implies $(B,N)\in Q$.

###### Proof.

Let $(A,M)\in P$ and $(A,M)\rightarrow^{p(n)}_{p}(B,N)$. By lemmas 6.3 and 6.7
$(A,M)\leftrightarrows_{p}M^{\top}\rightarrow^{p(n)}_{cl}N^{\top}\leftrightarrows_{p}(B,N)$.
We consider $Core^{p(n)}(M^{\top})$, for which
$M^{\top}\leftrightarrows^{p(n)}Core^{p(n)}(M^{\top})$ and
$Core^{p(n)}(M^{\top})\rightarrow N^{\top}$. Applying finite extendability to
$M^{\top}$ and $Core^{p(n)}(M^{\top})$ we obtain $\tilde{M^{\top}}$ and
$\tilde{Core^{p(n)}(M^{\top})}$ such that
$\tilde{M^{\top}}\equiv_{n}\tilde{Core^{p(n)}(M^{\top})}$. Putting this
together gives the following diagram:

${\tilde{\mathcal{M}^{\top}}}$${\equiv_{n}}$${\tilde{Core^{p(n)}(\mathcal{M}^{\top})}}$${\uparrow\downarrow}$${\uparrow\downarrow}$${{(\mathcal{A},\mathcal{M})}}$${\leftrightarrows_{p}}$${\mathcal{M}^{\top}}$${\leftrightarrows^{p(n)}_{cl}}$${Core^{p(n)}(\mathcal{M}^{\top})}$${\rightarrow_{p}}$${\mathcal{N}^{\top}}$${\leftrightarrows_{p}}$${{(\mathcal{B},\mathcal{N})}}$

Tracing through our diagram we obtain that $(B,N)\in Q$:

$\displaystyle(A,M)\in P\text{ and }(A,M)\rightarrow_{p}\tilde{M^{\top}}\text{
implies }\tilde{M^{\top}}\models\varphi.$
$\displaystyle\tilde{M^{\top}}\models\varphi,qd(\varphi)\leq n\text{ and
}\tilde{M^{\top}}\equiv_{n}\tilde{Core^{p(n)}(M^{\top})}\text{ implies
}\tilde{Core^{p(n)}(M^{\top})}\models\varphi.$
$\displaystyle\tilde{Core^{p(n)}(M^{\top})}\models\varphi\text{ and
}\tilde{Core^{p(n)}(M^{\top})}\rightarrow_{p}(B,N)\text{ implies }(B,N)\in Q.$

∎

We can now give the proofs of our first two preservation theorem; the fixed
case as a corollary.

###### Proof of Finite Protomorphism Preservation Theorem.

Our if direction is lemma 5.6, so let $\varphi$ be a $\mathcal{P}$-sentence
preserved under protomorphisms. Taking $P=Mod_{fin}(\varphi)=Q$ we immediately
have for any $\mathcal{P}$-models $(A,M)$ and $(B,N)$ $(A,M)\in P$ and
$(A,M)\rightarrow_{p}(B,N)$ implies $(B,N)\models\varphi$ and
$(A,M)\models\varphi$ and $(A,M)\rightarrow_{p}(B,N)$ implies $(B,N)\in Q$ so
by lemma 6.10 for any two $\mathcal{P}$-models $(A,M)\in P$ and
$(A,M)\rightarrow^{p(n)}(B,N)$ implies $(B,N)\in Q$. Therefore, by lemma 6.9
there is an e.$\land$.p-sentence $\psi$ with quantifier depth $p(n)$ such that
$Mod_{fin}(\varphi)=P\subseteq Mod_{fin}(\psi)\subseteq Q=Mod_{fin}(\varphi)$,
i.e. $Mod_{fin}(\varphi)=Mod_{fin}(\psi)$ as required. ∎

###### Proof of Fixed Finite Homomorphism Preservation Theorem.

By fixing an interpreting algebra $A$ and only considering models over $A$ all
protomorphism are homomorphism when paired with the identity map $id_{A}$.
Then lemma 5.6 gives $i.\Rightarrow iii.$, $iii.\Rightarrow ii.$ is immediate
from the above comment and $ii.\Rightarrow i.$ is the previous theorem
restricted to models over $A$. ∎

##  7\. Residuated Conjunction and Integrality

Before closing we want to apply our results to the previous work concerning
homomorphism preservation theorems for many-valued models by Dellunde and
Vidal. Recall that in [12] they give a compactness based proof of a
homomorphism preservation theorem for structures interpreted over a fixed
finite MTL-chain. Following our proof strategy for the finite case one can
give a homomorphism preservation theorem for infinite structures that is
compactness free. This is possible because alongside proving classical finite
homomorphism preservation Rossman also proved an ’equi-rank’ version of the
standard classical homomorphism preservation theorem [22, Theorem 4.12] and
accordingly we can utilise this in exactly the same way we did the finite
version. An important difference is that if we take our models over arbitrary
interpreting as we did in the finite case we lose that $\exists$ is witnessed.
To recover this we insist that we only consider models over finite
interpreting algebras; our ability to work with possibly infinite structures
comes at the cost of reducing the class of algebras we work over666This
restriction and the reasoning for it is also recognised by Dellunde and Vidal
in their work [12, pg 5]. The avoidance of compactness is not just an
interesting methodological feature, it means that we obtain a theorem that
still holds for our quite generalised interpreting algebras even in the
absence of a compactness theorem for these structures. Accordingly, we get the
following two theorems.

######  Theorem 7.1 (Protomorphism Preservation Theorem).

Let $K$ be the class of finite interpreting algebras. Let $\mathcal{P}$ be a
predicate language and $\varphi$ a consistent $\mathcal{P}$-sentence over $K$,
i.e $Mod^{K}(\varphi)\not=\varnothing$.

Then $\varphi$ is equivalent in the finite to an e.$\land$.p-sentence $\psi$
with the same nested rank iff $\varphi$ is preserved under protomorphisms.
That is there exists an e.$\land$.p-sentence $\psi:nr(\varphi)=nr(\psi)$ and
$Mod^{K}(\varphi)=Mod^{K}(\psi)$ iff $Mod^{K}(\varphi)$ is closed under
$\rightarrow_{p}$.

######  Theorem 7.2 (Fixed Homomorphism Preservation Theorem).

Let $\mathcal{P}$ be a predicate language, $A$ a finite interpreting algebra
and $\varphi$ a consistent $\mathcal{P}$-sentence over $A$ (i.e.
$Mod^{A}(\varphi)\not=\varnothing)$. The following are equivalent:

  1. i.

$\varphi$ is equivalent over $A$ to an e.$\land$.p-sentence $\psi$ with the
same quantifier depth. i.e. there is an e.$\land$.p-sentence
$\psi:qd(\varphi)=qd(\psi)$ and $Mod^{A}(\varphi)=Mod^{A}(\psi)$.

  2. ii.

$\varphi$ is preserved under protomorphisms on $A$, i.e. $Mod^{A}(\varphi)$ is
closed under $\rightarrow_{p}$.

  3. iii.

$\varphi$ is preserved under homomorphisms on $A$, i.e. $Mod^{K}(\varphi)$ is
closed under $\rightarrow$.

These theorems are not strictly a generalisation of the one presented by
Dellunde and Vidal [12, Theorem 11.3] because theirs incorporates the other
forms of existential-positive sentences, namely including the residuated
conjunction $\&$. As it stands, our result seems to mostly say that the
’classical part’ of many-valued structures behave as we would expect, which
whilst interesting is perhaps less compelling than an understanding of the
residuated connectives. In the general setting we’ve worked in so far we have
already seen why we must exclude residuated conjunction, however we can
recover its good behaviour with respect to morphisms (of either type) by
including an additional restriction on our interpreting algebras -
integrality. An interpreting algebra is integral iff $1$ is the top element in
the lattice, i.e. $\forall a\in A$ $a\leq 1$. Consequently, the set of ’true’
elements becomes just $\\{1\\}$.

As a corollary to our two initial preservation theorems we have their versions
for integral interpreting algebras. We can also recover that
e.$\&$.p-sentences and consequently e.p-sentences are preserved under
$\rightarrow_{p}$.

######  Lemma 7.3.

Let $A$ be an integral interpreting algebra. $\forall a,b\in A$ $a\ \&\ b=1$
iff $a=1$ and $b=1$.

###### Proof.

Follows easily by monotonicty of $\&$. $a\leq 1$ implies $a\ \&\ b\leq 1\ \&\
b=b$ and symmetrically $a\ \&\ b\leq a$. Then, $1=a\ \&\ b\leq a$ implies
$a=1$ and similarly $b=1$. The reverse is trivial. ∎

######  Lemma 7.4.

Let $\mathcal{P}$-predicate language and $(A,M)$ be a $\mathcal{P}$-model over
an integral interpreting algebra $A$ and
$\psi=\bigvee\limits_{i=1}^{n}\theta_{i}$ an e.p-sentence. $(A,M)\models\psi$
iff $\exists 1\leq i\leq n:\exists\bar{m}\in M:$ for all atomic subformula
$R_{j,k}\subseteq\theta_{i}$ $R^{M}_{j,k}(\bar{m_{j,k}})=1$ where
$\bar{m_{j,k}}$ is the subsequence of $\bar{m}$ corresponding to the
subsequence $\bar{x_{j,k}}$ of $\bar{x}$.

Moreover, $Mod_{fin}(\psi)$ is closed under $\rightarrow_{p}$.

###### Proof.

Following the proof of lemma 5.5 we obtain that $(A,M)\models\psi$ iff
$\exists 1\leq i\leq n:\exists\bar{m}\in M:\forall 1\leq j\leq n_{1}$
$||\bigodot\limits_{k=1}^{n_{2}}R_{j,k}(\bar{x_{j,k}})||_{v[\bar{x}\mapsto\bar{m}]}=1$.
Then by the previous lemma, the latter holds iff $\exists 1\leq i\leq
n:\exists\bar{m}\in M:$ for all atomic subformula $R_{j,k}\subseteq\theta_{i}$
$||R_{j,k}(\bar{x_{j,k}})||_{v[\bar{x}\mapsto\bar{x}]}=1$ iff $\exists 1\leq
i\leq n:\exists\bar{m}\in M:$ for all atomic subformula
$R_{j,k}\subseteq\theta_{i}$ $R^{M}_{j,k}(\bar{m_{j,k}})=1$.

For the moreover, letting $(A,M)\models\psi$ and $(A,M)\rightarrow_{p}(B,N)$
where $A,B$ are integral interpreting algebra. We have that $\exists 1\leq
i\leq n:\exists\bar{m}\in M:$ for all atomic subformula
$R_{j,k}\subseteq\theta_{i}$ $R^{M}_{j,k}(\bar{m_{j,k}})=1$. Letting
$g\colon(A,M)\rightarrow(B,N)$ be a protomorphism from $(A,M)$ to $(B,N)$, by
the definition of protomorphisms $R^{N}_{j,k}(g(\bar{m_{j,k}}))$, so taking
$g(\bar{m})$ and $i$ as witness we have by our previous part that
$(B,N)\models\psi$. ∎

With this recovered we can easily prove preservation theorem extended to cover
e.p-sentences.

######  Theorem 7.5 (Finite Integral Protomorphism Preservation Theorem).

Let $K$ be the class of integral interpreting algebras. Let $\mathcal{P}$ be a
predicate language and $\varphi$ a consistent $\mathcal{P}$-sentence in the
finite (i.e. $Mod^{K}_{fin}(\varphi)\not=\varnothing)$. Then $\varphi$ is
equivalent over $K$ in the finite to an e.p-sentence $\psi$ iff $\varphi$ is
preserved under protomorphisms over $K$. That is there exists an e.p-sentence
$\psi:Mod^{K}_{fin}(\varphi)=Mod_{fin}(\psi)$ iff $Mod^{K}_{fin}(\varphi)$ is
closed under $\rightarrow_{p}$.

Moreover, if $A$ is an integral interpreting algebra and $\varphi$ a
consistent $\mathcal{P}$-sentence over $A$ (i.e.
$Mod^{A}_{fin}(\varphi)\not=\varnothing$) then the following are equivalent:

  1. i.

$\varphi$ is equivalent over $A$ in the finite to an e.p-sentence $\psi$.

  2. ii.

$\varphi$ is preserved under protomorphisms on $A$, i.e.
$Mod^{A}_{fin}(\varphi)$ is closed under $\rightarrow_{p}$.

  3. iii.

$\varphi$ is preserved under homomorphisms on $A$, i.e.
$Mod^{A}_{fin}(\varphi)$ is closed under $\rightarrow$.

###### Proof.

The only if direction is just the last claim of our previous lemma. For the if
direction by the finite p.p.t. theorem $\varphi$ is equivalent to an
e.$\land$.p-sentence $\psi$ which is of course also an e.p-sentence. The
moreover follows similarly from the fixed finite h.p.t. theorem and the
previous lemma upon noting as usual that any protomorphism between models
defined over $A$ is automatically a homomorphism when paired with the identity
map. ∎

This additional restriction also gives the direct comparison to the work done
by Dellunde and Vidal. MTL-algebras (and moreover MTL-chains) are integral so
the preceding theorem specialises to give a direct answer to the status of
finite preservation they asked. Additionally, we can combine the integral
restriction with our prior ’equi-rank’ protomorphism preservation theorem to
obtain an equivalent theorem for (possibly infinite) models defined over a
finite integral interpreting algebra.

The residuated and a lattice conjunction being logically interchangeable in
integral contexts also has consequences for an alternative treatment of our
problem inspired by the framework for VCSP by Bistarelli, Montanari and Rossi
in [6]. Their work provides the most general treatment of VCSPs and takes what
are known as c-semirings as their valuation structure.

######  Definition 7.6.

A c-semiring is tuple algebra $A=\langle A,+,\times,0,1\rangle$ such that

  * •

$+\colon\mathcal{P}(A)\rightarrow A$ is defined over (possibly infinite) sets
of elements of $A$ where

    * –

$+(\\{a\\})=a$,

    * –

$+(\varnothing)=0$ $+(A)=1$,

    * –

$+(\bigcup_{i\in S}A_{i})=+(\bigcup\limits_{i\in S}+(A_{i}))$

  * •

$\times$ is a binary operation that is associative and commutative with unit
element $1$ and absorption element $0$.

  * •

$\times$ distributives over $+$, that is for any $a\in A$ and $B\subseteq A$
$a\times+(B)=+(\\{a\times b\in A:b\in B\\})$.

Importantly, c-semirings are bounded complete lattices where we take $+$ as
the generalised infinite disjunction with $1$ and $0$ acting as the top and
bottom element of the lattice. Moreover $\times$ is monotone with respect to
the resulting lattice order. Consequently, c-semirings are subsumed by the
(potentially) non-distributive integral abelian l-monoids. Therefore with a
few small but significant adjustments, we can apply our previous work to the
finite models defined over c-semirings. First, we have to restrict to
$1$-$+$-prime c-semirings. In a theoretical treatment this is a substantive
restriction, but in practice all the major VCSP formalisms also make this
restriction777For example, all three of the more specific contexts consider in
[6, Section 6] are $1$-$+$-prime. Second, we have to account for the loss of
distributivity between the various connectives. This does not pose a massive
problem, if we review our proof we will see that the only use of
distributivity was in the equivalence of our normal form based definition
$e$.$\land$.p sentences (et. al.) with the more usual definition of formulas
built from the relevant connectives. Finally, in this context the interest is
very firmly on the $\&$-primitive and existential-$\&$-positive sentences
rather than the $\land$-primitive and $e$.$\land$.p sentences we have been
primarily treating. The adjustment is simply to note that because $\times$ is
intensive in c-semirings (i.e. $a\times b\leq a$ and $a\times b\leq b$ for all
$a,b\in A$) that together with integrality means we have an equivalent to
lemma 7.3 for c-semirings, $a\times b=1$ iff $a=1$ and $b=1$. Thus, one can
simply rerun our entire proof but replacing $\land$ with $\&$, inducing a
syntactic translation from the c-semiring syntax into the classical syntax.
Putting all this together will yield:

######  Theorem 7.7 (Finite c-semiring Protomorphism Theorem).

Let $K$ the class of $1$-$+$-prime c-semirings. Let $\mathcal{P}$ be a
predicate language and $\varphi$ a consistent $\mathcal{P}$-sentence in the
finite over $K$ (i.e. $Mod^{K}_{fin}(\varphi)\not=\varnothing)$. Then
$\varphi$ is equivalent over $K$ in the finite to an e.$\&$.p-sentence $\psi$
iff $\varphi$ is preserved under protomorphisms over $K$. That is there exists
an e.$\&$.p-sentence $\psi:Mod^{K}_{fin}(\varphi)=Mod^{K}_{fin}(\psi)$ iff
$Mod^{K}_{fin}(\varphi)$ is closed under $\rightarrow_{p}$.

Moreover, if $A$ is a $1$-$+$-prime c-semiring and $\varphi$ a consistent
$\mathcal{P}$-sentence over $A$ (i.e.
$Mod^{A}_{fin}(\varphi)\not=\varnothing$) then the following are equivalent:

  1. i.

$\varphi$ is equivalent over $A$ in the finite to an e.$\&$.p-sentence $\psi$.

  2. ii.

$\varphi$ is preserved under protomorphisms on $A$, i.e.
$Mod^{A}_{fin}(\varphi)$ is closed under $\rightarrow_{p}$.

  3. iii.

$\varphi$ is preserved under homomorphisms on $A$, i.e.
$Mod^{A}_{fin}(\varphi)$ is closed under $\rightarrow$.

##  8\. Conclusions and Further Study

In this paper we have begun the investigation on preservation theorems for
finite many-valued models. Inspired by the successful generalisation of the
homomorphism preservation theorem into first-order MTL by Dellunde and Vidal
and Rossman’s recovery of the same theorem in classical finite models, we
utilised the latter’s result to identify and prove the appropriate version of
the theorem in the many-valued setting - our finite protomorphism preservation
theorem. There remains a lot of work to be done on the topic of many-valued
preservation theorems. In the infinite setting, the Łos–Tarski theorem
(linking universal sentences with strong embeddings) and Chang–Łoś–Suszko
theorem (linking $\forall_{2}$-formulas with unions of chains) have been
recovered for models defined over a fixed finite MTL-algebra [3]. This was the
same setting as the (infinite) homomorphism preservation theorem by Dellunde
and Vidal [12] and given our expansion of that theorem to models defined over
interpreting algebras it prompts whether something similar is possible for the
other preservation theorems. In the finite setting less is known, the
Łos–Tarski theorem and Lyndon positivity [22, Theorem 1.4,1.5] fail for
classical finite models which would suggest they also fail in the many-valued
setting but this requires conformation.

As referenced throughout, there is a general interest in the application of
many-valued model theory to questions of computational complexity, a first
approach can be found in [18], and classically the finite homomorphism
preservation theorem is linked to the constraint satisfaction problem (CSP)
[22]. Our main theorem and the ancillary discussion in section 7 cover many of
the algebraic structures that VCSP problems consider, and we can naturally ask
what the impact the finite protomorphism preservation theorem may have. The
failure of residuated conjunction preservation in non-integral settings could
be of particular interest for the feasibility of VCSP investigations in those
contexts.

To close we comment on two more areas of future study in a little more detail.
First is the status of the residuated conjunction in non-integral settings.
We’ve already seen the residuated conjunction is not preserved by
homomorphisms without integrality. However, there is a natural class of maps
between structures that do preserve residuated conjunction even in non-
integral settings - monomorphisms.

######  Definition 8.1.

Let $(A,M),(B,N)$ be $\mathcal{P}$-models defined over interpreting algebras.
A homomorphism $(f,g)\colon(A,M)\rightarrow(B,N)$ is a monomorphism iff

$\text{for every }R\in\mathcal{P}\ \bar{m}\in M\ f(R^{M}(\bar{m}))\leq
R^{N}(g(\bar{m})).$

At present, we are only able to show the viability of preservation of
$e.p$-sentences by monomorphisms for $\exists$-witnessed models, that is
models where for any $\mathcal{P}$-formula $\varphi(\bar{x}):=\exists
x\psi(x,\bar{x})$ and any $\bar{m}\in M$ there is some $m\in M$ such that
$||\exists x\psi(x,\bar{m})||^{M}=||\psi(m,\bar{m})||$.

######  Lemma 8.2.

Let $\mathcal{P}$ be a predicate language and $\psi$ and $e.p$-sentence. Then
models the of $\psi$ (defined over interpreting algebras) are closed under
monomorphisms.

###### Proof.

Suppose $(A,M)\models\psi$ and $(f,g)\colon(A,M)\rightarrow(B,N)$ a
monomorphism. We claim that $f(||\psi||^{M})\leq||\psi||^{N}$, in that case
$(A,M)\models\psi$ implies $1_{A}\leq||\psi||^{M}$ and so $1_{B}\leq
f(||\psi||^{M})\leq||\psi||^{N}$ and $(B,N)\models\psi$ as required. For the
claim we prove by induction that for any $e.p$-formula $\varphi(\bar{x})$ and
$\bar{m}\in M$ $f(||\varphi(\bar{m})||^{M})\leq||\varphi(g(\bar{m}))||^{N}$.

The base case where $\varphi$ is atomic is simply the definition of
monomorphism. The inductive step for $\lor$,$\land$ and $\&$ all follow by
their monotonicity in the algebra, e.g. with $\&$ we have by monotonicity that
$\forall a,b,c,d\in A$ that $a\leq b$ and $c\leq d$ imply $a\&c\leq b\&c\leq
b\&d$ and so assuming that
$f(||\psi(\bar{m})||^{M}\leq||\psi(g(\bar{m}))||^{N}$
$f(||\lambda(\bar{m})||^{M}\leq||\psi(g(\bar{m})||^{N}$ we obtain
$f(||\psi(\bar{m})\&||\lambda(\bar{m})||^{M})$ =
$f(||\psi(\bar{m})||^{M})\&f(||\lambda(\bar{m})||^{M})\leq||\psi(g(\bar{m}))||^{N}\&||\psi(g(\bar{m})||^{N}=||\psi\&\lambda(g(\bar{m}))||^{N}$.
This just leaves the case for $\exists$. Considering $\exists
x\psi(x,\bar{x})$ we letting $\bar{m}$ be arbitrary and apply
$\exists$-witnessed to find $m\in M$ such that $||\exists
x\psi(x,\bar{m})||^{M}=||\psi(m,\bar{m})||^{M}$. Then applying $f$ and the
inductive hypothesis we obtain:

$f(||\exists
x\psi(x,\bar{m})||^{M})=f(||\psi(m,\bar{m})||^{M})\leq||\psi(g(m),g(\bar{m})||^{N}\leq||\exists
x\psi(x,g(\bar{m})||^{N}.$

∎

Unfortunately, when it comes to attempting a proof of the full monomorphism
preservation theorem (infinite or finite) our easy strategy of applying
Rossman’s result no longer works, because there is no way to define a
classical counterpart to a structure on the two element Boolean algebra that
has mutual monomorphism available with the original structure. We believe that
the most viable strategy would require a full recovery of Rossman’s original
classical proof with appropriate generalisations to the many-valued context of
the concepts contained within.

Another relationship we want to understand better is that between the
existence of a protomorphism and homomorphism between two given structures and
whether there are significant consequences for when one is only able to define
a protomorphism between structures. Recall that any protomorphism
$g\colon(A,M)\rightarrow(B,N)$ is a homomorphism when paired with any
$\mathcal{L}$-algebra homomorphism $f\colon A\rightarrow B$ and accordingly
the only difference between the $\rightarrow_{p}$ and $\rightarrow$ relations
is the existence of some homomorphism $f\colon A\rightarrow B$. Any
information of the map $f$ seems to have no direct consequence on the
structures themselves, its action is irrelevant to the comparison in atomic
formulas the map $g$ enables making its presence seem unnecessary. At the same
time, our proof for preservation between structures defined over a class of
algebras really does only go through for protomorphisms. This prompts the
question of whether there really is some genuine difference (at the logical
level) between the two relations or whether at the weakest level of
homomorphism we are essentially free to ignore our algebra component and
solely work with protomorphisms.

We can say a small amount about the most straightforward case. We could
bluntly require that for our class of algebras $K$ that for any (non-trivial)
$A,B\in K$ there exists a homomorphishm $f\colon A\rightarrow B$. In this case
the two notions collapse. This situation has had some prior attention, namely
for quasivarieties of finite type with at least one finite non-trivial member
the condition is equivalent to a property called passive structural
completeness (PSC) [20, Theorem 7.6]. The restriction to quasivarieties of
finite type is not major, all the classes of algebras we are interested in are
subclasses of a given variety or quasivariety. In such a situation we can
obtain the following corollary to our main theorem.

######  Corollary 8.3.

Let $K$ be a class of interpreting algebras contained within a PSC
quasivariety containing a finite non-trivial member. Then the relations of
$\rightarrow_{p}$ and $\rightarrow$ for models over $K$ coincide and in
particular any $\mathcal{P}$-sentence $\varphi$ is is preserved under
$\rightarrow_{p}$ over $K$ iff $\varphi$ is preserved under $\rightarrow$ over
$K$.

The class of FSI Heyting algebras provide an example of this type. The variety
of Heyting algebras is PSC [20, Example 7.9] and Heyting algebras are abelian
l-monoids where we take $\&=\land$ and $1=\top$. Restricting to FSI Heyting
algebras makes them interpreting algebras and fall within the scope of our
work.

## Acknowledgments

We were partially supported by the Australian Research Council grant
DE220100544.

## References

  * [1] M. Ajtai, Y. Gurevich.  Monotone versus positive.  J. ACM 34:1004–1015, 1987.
  * [2] G. Badia, X. Caicedo, C. Noguera.  Asymptotic truth-value laws in many-valued logics.  arXiv:2306.13904 2023\.
  * [3] G. Badia, V. Costa, P. Dellunde, C. Noguera.  Syntactic characterisations of classes of first-order structures in mathematical fuzzy logic.  Soft Computing 23:2177–2186, 2019.
  * [4] G. Badia, C. Noguera.  A 0-1 Law in Mathematical Fuzzy Logic  IEEE Transactions on Fuzzy Systems 30(9):3833–3840 2022.
  * [5] G. Bezhanishvili, N. Bezhanishvili.  Profinite Heyting Algebras.  Order 25(3):211–227, 2008.
  * [6] S. Bistareli, U. Montanari, F. Rossi.  Semiring-based constraint satisfaction and optimization.  Journal of the ACM 44(2):201-236, 1997.
  * [7] A. Chandra, P. Merlin.  Optimal implementation of conjunctive queries in relational databases.  Proceedings of the ninth annual ACM symposium on Theory of Computing 77–90, 1977.
  * [8] P. Cintula, C. Noguera.  Logic and Implication Springer, 2021.
  * [9] M.P. Dellunde.  Preserving mappings in fuzzy predicate logics.  Journal of Logic and Computation 22(6):1367–1389, 2012.
  * [10] M.P. Dellunde, À, García-Cerdaña, C. Noguera.  Löwenheim–Skolem theorems for non-classical first-order algebraizable logics.  Logic Journal of IGPL, 24(3):321–345, 2016.
  * [11] M.P. Dellunde, À. García-Cerdaña, C. Noguera.  Back-and-forth systems for fuzzy first-order models.  Fuzzy Sets and Systems, 345, 2018.
  * [12] M.P. Dellunde, A. Vidal.  Truth-preservation under fuzzy pp-formulas.  International Journal of Uncertainty, Fuzziness and Knowledge-Based Systems. 27:89–105, 2019.
  * [13] A. Di Nola, G. Gerla.  Fuzzy models of first-order languages.  Zeitshrift für Mathematische Logik und Grundlagen der Mathematik 32(19-24) 331–340, 1986.
  * [14] H.D. Ebbinghaus, J. Flum.  Finite Model Theory Springer, 1995.
  * [15] Yuri Gurevich. Toward logic tailored for computational complexity In _Computation and Proof Theory_ (Ed. M. Richter et al.) Springer Lecture Notes in Mathematics 1104 175-216, 1984.
  * [16] P. Cintula, P. Hájek, C. Noguera (eds.).  Handbook of Mathematical Fuzzy Logic Vol 1 College Publications, 2011.
  * [17] W. Hodges.  A shorter model theory Cambridge University Press, 1997.
  * [18] R. Horc̆ík, T. Moraschini, A. Vidal.  An Algebraic Apporach to Valued Constraint Satisifaction.  26th EACSL Annual Conference on Computer Science Logic 82, 2017.
  * [19] R. Lyndon.  Properties preserved under homomorphism  Pacific J. Math 9:129–142, 1959.
  * [20] T. Moraschini, J. Raftery, J.J. Wannenburg.  Single generated quasivarieties and residuated structures.  Mathematical Logic Quarterly 66:150–172, 2020.
  * [21] C. Noguera.  Algebraic study of axiomatic extensions of triangular norm based fuzzy logics.  Monographs of the Artificial Intelligence Research Institute vol. 27, Barcelona, 2007.
  * [22] B. Rossman.  Homomorphism preservation theorems.  Journal of the ACM 55(3), 2008.
  * [23] W. Tait.  A counterexample to a conjecture of Scott and Suppes  J. Symbolic Logic 24:15-16 1959.