# Local positive logic

Arturo Rodríguez Fanlo  and  Ori Segel  Einstein Institute of Mathematics,
Hebrew University of Jerusalem, 91904, Jerusalem, Israel.
<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract.

We develop the basic model theory of local positive logic, a new logic that
mixes positive logic (where negation is not allowed) and local logic (where
models omit types of infinite distant pairs). We study several basic model
theoretic notions such as compactness, positive closedness (existential
closedness), completeness (irreducibility), type spaces and retractors
(saturated models).

###### Key words and phrases:

Positive logic, local logic, retractors

###### 2010 Mathematics Subject Classification:

03C95, 03B60

Rodríguez Fanlo is supported by the Israel Academy of Sciences and Humanities
& Council for Higher Education Excellence Fellowship Program for International
Postdoctoral Researchers and partially supported by STRANO
PID2021-122752NB-I0.

## Introduction

It is common in mathematics to enrich basic objects with more and more
structure in the aim of generality. In model theory, well-known examples are
continuous logic [BYBHU08] and positive logic [PY18, BY03] as enrichments of
first-order logic. In this paper we introduce the basic framework of a new
logic.

Local positive logic was first introduced by Hrushovski in [Hru22a] and
applied in his study of approximate subgroups. Local positive logic is the
combination of positive logic and local logic. While positive logic is well-
known, local logic was also introduced for the first time in [Hru22a].

Local logic is a variation of first-order logic aiming to relax compactness.
Compactness is a fundamental tool in model theory, but its full power is
sometimes a hindrance. Local logic tries to replace the role of compactness in
first-order logic by “local compactness”. To do so, it restricts quantifiers
to local quantifiers, namely every quantifier imposes that the variable is
localised in some “ball”. Although local logic presents several
characteristics distinguishing it from first-order logic, at the same time
this extension is very slight in that, upon adding constants, local logic
could be reduced to many sorted first-order logic by adding a new sort for
each ball centred at the constants.

The aim of this paper is to develop the basic theory of local positive logic,
specially underlining the differences and similarities between local positive
logic and usual positive logic. In particular, this paper should be considered
a continuation on [Hru22a, Section 2]. For the remaining of the introduction,
we outline the structure of the paper and remark the main new results with
respect to Hrushovski’s work.

In Section 1, we define _local languages_ and _local structures_ in the many
sorted case and with arbitrary local signatures (Definitions 1.1 and 1.5), and
prove a compactness theorem for this logic (Theorem 1.9). In [Hru22a],
Hrushovski defines local positive logic in the one sort case. While in
standard positive logic the generalisation to many sorts is mostly
straightforward, in local positive logic a few technical subtleties appear.
For instance, the presence of several sorts brings to the surface the notion
of _pointed variables_ (Definition 1.3), which plays a significant role in
several places of the paper (e.g. to define semi-Hausdorffness).

In Section 2, we recall _local positive closedness_ (called existential
closedness in [Hru22a]) in Definition 2.2. We prove their existence in Theorem
2.7 — this result was already stated (with omitted proof) in [Hru22a, Section
2]. We also recall the definition of _denials of formulas_ (Definition 2.11)
and prove their existence in Lemma 2.12, which was stated without proof in
[Hru22a, Section 2] — it should be noted that the version stated in [Hru22a,
Section 2] is only true for pointed variables. We also show that positive
substructures of local positively closed models are local positively closed
models in Corollary 2.13, a fact that was implicitly assumed in [Hru22a]. We
end this section with Lemma 2.16, which is useful to find easy examples of
local positively closed models.

The study of completeness in local positive logic is the main topic of this
paper. We define several completeness properties (Definition 3.1) and discuss
their relations in Section 3. While in standard positive logic all the
completeness properties are equivalent, this is no longer true for local
positive logic (Theorems 3.11, 3.4 and 3.7). We conclude the section studying
weak completions and completions (Lemmas 3.12, 3.14, 3.16 and 3.17).

Types for local positive logic were not really discussed in [Hru22a]. Here, we
cover the study of types for local positive logic in Section 4. The right
notion of types for local positive logic seems to be _local positive types_
(Definition 4.1). For this notion we find in Lemma 4.9 the right version of
finite satisfiability. It is worth noting that for pointed variables (for
instance, in the one-sort case previously studied by Hrushovski) local
positive types can be replaced by positive types (Lemma 4.11). We also study
the topology of spaces of local positive types and adapt the definitions of
Hausdorffness and semi-Hausdorffness for local positive logic. We conclude
giving characterisations of some completeness properties in terms of local
positive types (Lemmas 4.32 and 4.33).

In his paper, Hrushovski mostly focuses on the study of _retractor spaces_ ,
being [Hru22a, Proposition 2.1] his main result on local positive logic. We
continue this study in Section 5. In Section 5.1, in Theorems 5.22 and 5.23,
we prove stronger versions of [Hru22a, Lemma 2.4]. In Section 5.2, we recall
the equivalence of the existence of retractors and local positive compactness
(called _primitive positive compactness_ , ppC, in [Hru22a]), and discus
consequences of this equivalence under different completeness properties. In
Section 5.3, we discus the relationship between local retractors and non-local
homomorphism universal models. We continue the study of the group of
automorphisms of retractors of [Hru22a, Subsection 2.5] in Section 5.4. In
particular, we adapt to local positive logic several results from [Hru22b]
that were not studied in [Hru22a].

We conclude the paper discussing when local positive logic reduces to standard
positive logic in Section 6, giving various equivalent formulations in Theorem
6.4.

We have some open questions in this paper (Questions 3.18, 4.34 and 5.41).
Beyond these specific questions, we also leaves as an open task to adapt more
elaborated model theoretic machinery (e.g. classification theory) to local
positive logic.

This is the first of a series of papers which aims to extend several results
of [Hru22a] to rough approximate subgroups. In a subsequent paper we will
study the definability patterns for local positive logic, extending the
results of [Hru22b, Seg22]. Later, we will apply the definability patterns to
study hyperdefinable approximate subgroups and rough approximate subgroups.

##  1\. Local languages and structures

######  Definition 1.1.

A _local (first-order) language_ is a first-order language ${\mathtt{L}}$ with
the following additional data:

  1. (i)

It is a relational language with constants, i.e. it has no function symbols
except for constant symbols.

  2. (ii)

It has a distinguished partial ordered monoid
$\mathtt{D}^{s}\coloneqq(\mathtt{D}^{s},{\mathrm{d}}^{0},\ast_{s},\prec_{s})$
of binary relation symbols for each single sort $s$. The binary relation
symbols in $\mathtt{D}^{s}$ are the _locality relation symbols_ on the sort
$s$. The identity ${\mathrm{d}}^{0}$ of $\mathtt{D}^{s}$ is the equality
symbol on sort $s$ and it is also the least element for $\prec_{s}$.

  3. (iii)

There is a function $\mathtt{B}$ assigning to any pair $c_{1}\,c_{2}$ of
constant symbols of the same sort a locality relation symbol
$\mathtt{B}_{c_{1},c_{2}}$ on that sort. We call $\mathtt{B}$ the _bound
function_ and $\mathtt{B}_{c_{1},c_{2}}$ the _bound_ for $c_{1}$ and $c_{2}$.

We call $(\mathtt{D},\mathtt{B})$ the _local signature_ of ${\mathtt{L}}$. A
_sort_ is a tuple of single sorts; its _arity_ is its length. We write
$\mathtt{S}$ for the set of single sorts. A _variable_ $x$ is a set of single
variables; its _arity_ is its size. The _sort_ of a variable $x$ is the sort
$s=(s_{x_{i}})_{x_{i}\in x}$ where $s_{x_{i}}$ is the sort of $x_{i}$.

######  Remark 1.2.

Let us make some remarks about Definition 1.1, highlighting possible
generalisations:

  1. (i)

We only study relational languages with constants. This significantly
simplifies the definition of the bound function $\mathtt{B}$. In many
situations, one could deal with function symbols by using relations defining
their graphs. This is common practice in positive logic, since those relations
are forced to define graphs of functions in positively closed models. We leave
as a task to develop local positive logic for languages with function symbols.
The key issue is to find a good definition of $\mathtt{B}$ for function
symbols that is not too restrictive.

  2. (ii)

We only consider locality relations between elements of the same sort. For
locality relations between different sorts, it might be more natural to merge
all these sorts in a new one and replace them by disjoint unary predicates.
For positively closed models, these predicates would give a partition of the
new sort.

  3. (iii)

Locality relations are binary. We leave as an open task the development of a
higher-arity local logic.

A _local reduct_ is a local language which is a reduct; a _local expansion_ is
a local language which is an expansion. As usual, we write ${\mathtt{L}}(C)$
for the expansion of ${\mathtt{L}}$ given by adding the symbols in $C$. Note
that, when adding constant symbols, the expansion should also extend the bound
function $\mathtt{B}$. Among all the local expansion, we denote by
${\mathtt{L}}_{\star}$ the expansion of ${\mathtt{L}}$ that consists on
“forgetting” the local signature, i.e. ${\mathtt{L}}_{\star}$ is the expansion
of ${\mathtt{L}}$ given by adding to each sort a maximal locality relation
symbol ${\mathrm{d}}_{\star}$ whose intended interpretation is trivial.

######  Definition 1.3.

We say that a local language ${\mathtt{L}}$ is _pointed_ if it has at least
one constant symbol for every sort. We say that a set of parameters (new
constants) $A$ is _pointed_ for ${\mathtt{L}}$ if the expansion
${\mathtt{L}}(A)$ is pointed. We say that a variable $x$ of sort $s$ is
_pointed_ in ${\mathtt{L}}$ if there is at least one constant symbol for every
sort that does not appear in $s$. We say that a sort $s$ is _pointed_ if there
is at least one constant symbol for every sort that does not appear in $s$.

For locality relation symbols ${\mathrm{d}}_{1},\ldots,{\mathrm{d}}_{n}$ of
respective single sorts $s_{1},\ldots,s_{n}$, we write
${\mathrm{d}}_{1}\times\cdots\times{\mathrm{d}}_{n}(x,y)\coloneqq\bigwedge_{1\leq
i\leq n}{\mathrm{d}}_{i}(x_{i},y_{i})$ for the _product_ of the locality
relation symbols. A _locality relation symbol_ of sort
$s=(s_{1},\ldots,s_{n})$ is a product of locality relation symbols of the
respective single sorts. We write $\mathtt{D}^{s}$ for the locality relation
symbols of sort $s$ and pointwise extend $\ast$ and $\prec$ to products.

Let ${\mathrm{For}}({\mathtt{L}})$ denote the set of first-order formulas of
${\mathtt{L}}$. Given a variable $x$, let ${\mathrm{For}}^{x}({\mathtt{L}})$
denote the subset of formulas whose free single variables are contained in $x$
— in particular, ${\mathrm{For}}^{0}({\mathtt{L}})$ is the set of sentences of
${\mathtt{L}}$.

A formula is _positive_ if it is built from atomic formulas by conjunctions,
disjunctions and existential quantifiers; let ${\mathrm{For}}_{+}$ denote the
set of positive formulas. A formula is _primitive positive_ if it is built
from atomic formulas by conjunctions and existential quantifiers; let
${\mathrm{For}}_{+_{0}}$ denote the set of primitive positive formulas. A
formula is _quantifier free positive_ if it is built from atomic formulas by
conjunctions and disjunctions; let ${\mathrm{For}}_{{\mathrm{qf}}_{+}}$ denote
the set of quantifier free positive formulas. A formula is _quantifier free
primitive positive_ if it is a conjunction of atomic formulas. A formula is
_negative_ if it is the negation of a positive formula; let
${\mathrm{For}}_{-}$ denote the set of negative formulas. A formula is
_primitive negative_ if it is the negation of a primitive positive formula. A
formula is _quantifier free negative_ if it is the negation of a quantifier
free positive formula.

Let $\varphi$ be a formula, $x$ a single variable, ${\mathrm{d}}$ a locality
relation on the sort of $x$ and $t$ a term of the same sort such that $x$ does
not appear in $t$ (i.e. a constant or a variable different to $x$). The _local
existential quantification of $\varphi$ on $x$ in ${\mathrm{d}}(t)$_ is the
formula $\exists x{\in}{\mathrm{d}}(t)\,\varphi\coloneqq\exists
x\,{\mathrm{d}}(x,t)\wedge\varphi$.

A formula is _local_ if it is built from atomic formulas using negations,
conjunctions and local existential quantification; let ${\mathrm{LFor}}$
denote the set of local formulas. A formula is _local positive_ if it is built
from atomic formulas using conjunctions, disjunctions and local existential
quantification; let ${\mathrm{LFor}}_{+}$ denote the set of local positive
formulas. A formula is _local negative_ if it is the negation of a local
positive formula.

Finally, we define $\Pi_{n}$-local formulas and $\Sigma_{n}$-local formulas
recursively on $n\in\mathbb{N}$. A formula is _$\Sigma_{0}$ -local_ if it is a
local formula. A formula is _$\Pi_{n}$ -local_ if it is the negation of a
$\Sigma_{n}$-local formula. A formula is _$\Sigma_{n+1}$ -local_ if it is of
the form $\exists x\,\varphi$ where $\varphi$ is a $\Pi_{n}$-local formula. We
write $\Pi_{n}$ for the set of $\Pi_{n}$-local formulas and $\Sigma_{n}$ for
the set of $\Sigma_{n}$-local formulas.

######  Remark 1.4.

We have the following normal forms:

  1. •

Every primitive positive formula is equivalent to $\exists x\,\phi$ for some
finite variable $x$ and some quantifier free primitive positive formula
$\phi$.

  2. •

Every positive formula is equivalent to a finite disjunction of primitive
positive formulas. Every positive formula is equivalent to $\exists x\,\phi$
for some finite variable $x$ and some quantifier free positive formula $\phi$.
In particular, every positive formula is existential and every negative
formula is universal.

  3. •

Every local formula is equivalent to
$Q_{1}x_{1}{\in}{\mathrm{d}}_{1}(t_{1})\ldots
Q_{n}x_{n}{\in}{\mathrm{d}}_{n}(t_{n})\,\phi$ for some quantifiers
$Q_{1},\ldots,Q_{n}$, some single variables $x_{1},\ldots,x_{n}$, some terms
$t_{1},\ldots,t_{n}$, some locality relation symbols
${\mathrm{d}}_{1},\ldots,{\mathrm{d}}_{n}$ and some quantifier free formula
$\phi$.

  4. •

Every local positive formula is equivalent to $\exists
x_{1}{\in}{\mathrm{d}}_{1}(t_{1})\ldots\exists
x_{n}{\in}{\mathrm{d}}_{n}(t_{n})\,\phi$ for some single variables
$x_{1},\ldots,x_{n}$, some terms $t_{1},\ldots,t_{n}$, some locality relation
symbols ${\mathrm{d}}_{1},\ldots,{\mathrm{d}}_{n}$ and some quantifier free
positive formula $\phi$.

From now on, unless otherwise stated, fix a local language ${\mathtt{L}}$.

######  Definition 1.5.

A _local ${\mathtt{L}}$-structure_ is an ${\mathtt{L}}$-structure $M$
satisfying the following locality axioms:

  1. (A1)

Every locality relation symbol is interpreted as a symmetric binary relation.

  2. (A2)

Any two locality relation symbols ${\mathrm{d}}_{1}$ and ${\mathrm{d}}_{2}$ on
the same sort with ${\mathrm{d}}_{1}\preceq{\mathrm{d}}_{2}$ satisfy
${\mathrm{d}}^{M}_{1}\subseteq{\mathrm{d}}^{M}_{2}$.

  3. (A3)

Any two locality relation symbols ${\mathrm{d}}_{1}$ and ${\mathrm{d}}_{2}$ on
the same sort satisfy
${\mathrm{d}}^{M}_{1}\circ{\mathrm{d}}^{M}_{2}\subseteq({\mathrm{d}}_{1}\ast{\mathrm{d}}_{2})^{M}$.

  4. (A4)

Any two constant symbols $c_{1}$ and $c_{2}$ of the same sort satisfy
$\mathtt{B}_{c_{1},c_{2}}(c_{1},c_{2})$.

  5. (A5)

Any two single elements $a$ and $b$ of the same sort satisfy
${\mathrm{d}}(a,b)$ for some locality relation ${\mathrm{d}}$ on that sort.

For any element $a$ and locality relation ${\mathrm{d}}$ on its sort, the
_${\mathrm{d}}$ -ball at $a$_ is the set
${\mathrm{d}}(a)\coloneqq\\{b:M\models{\mathrm{d}}(a,b)\\}$.

Expansions and reducts of local structures are defined in the usual way.

######  Remark 1.6.

The first four locality axioms could be easily expressed by first-order
universal axiom schemes. We write ${\mathtt{T}}_{\mathrm{loc}}({\mathtt{L}})$
for the universal first-order theory given by axioms A1, A2, A3 and A4 — we
omit ${\mathtt{L}}$ if it is clear from the context. On the other hand, A5 is
a second-order axiom. It says that some particular quantifier free binary
types are omitted.

Let ${\mathtt{L}}$ be a local language and $\Gamma$ a set of sentences of
${\mathtt{L}}$. An _${\mathtt{L}}$ -local model_ of $\Gamma$ is a local
${\mathtt{L}}$-structure satisfying it. We restrict satisfaction to local
structures: we write $M\models_{{\mathtt{L}}}\Gamma$ to say that $M$ is an
${\mathtt{L}}$-local model of $\Gamma$. We write
$\mathcal{M}(\Gamma/{\mathtt{L}})$ for the class of ${\mathtt{L}}$-local
models of $\Gamma$. We say that $\Gamma$ is _${\mathtt{L}}$ -locally
satisfiable_ if it has an ${\mathtt{L}}$-local model. We say that $\Gamma$ is
_finitely ${\mathtt{L}}$-locally satisfiable_ if every finite subset of
$\Gamma$ is ${\mathtt{L}}$-locally satisfiable. We typically omit
${\mathtt{L}}$ if it is clear from the context.

Given two subsets of sentences $\Gamma_{1}$ and $\Gamma_{2}$, we say that
$\Gamma_{1}$ _${\mathtt{L}}$ -locally implies_ $\Gamma_{2}$, written
$\Gamma_{1}\models_{{\mathtt{L}}}\Gamma_{2}$, if every ${\mathtt{L}}$-local
model of $\Gamma_{1}$ is an ${\mathtt{L}}$-local model of $\Gamma_{2}$. We say
that $\Gamma_{1}$ and $\Gamma_{2}$ are _${\mathtt{L}}$ -locally elementary
equivalent_ if they have the same local models. We typically omit
${\mathtt{L}}$ if it is clear from the context.

######  Notation.

We write $\mathrel{\mathord{\models}_{\star}}$ for satisfaction for arbitrary
structures and $\mathcal{M}_{\star}(\Gamma)$ for the class of arbitrary models
of $\Gamma$.

A _negative ${\mathtt{L}}$-local theory_ ${\mathtt{T}}$ is a set of negative
sentences closed under local implication. The _associated positive
counterpart_ ${\mathtt{T}}_{+}$ is the set of positive sentences whose
negations are not in ${\mathtt{T}}$. In other words, a positive formula
$\varphi$ is in ${\mathtt{T}}_{+}$ if and only if there is a local model
$M\models{\mathtt{T}}$ satisfying $\varphi$; we say in that case that $M$ is a
_witness of $\varphi\in{\mathtt{T}}_{+}$_. We write
${\mathtt{T}}_{\pm}\coloneqq{\mathtt{T}}\wedge{\mathtt{T}}_{+}$. We typically
omit ${\mathtt{L}}$ if it is clear from the context.

We say that ${\mathtt{T}}$ is _${\mathtt{L}}$ -locally axiomatisable_ by a
subset $\Gamma\subseteq{\mathtt{T}}$ if $\Gamma$ is ${\mathtt{L}}$-locally
elementary equivalent to ${\mathtt{T}}$. Abusing of the notation, we may use
$\Gamma$ to denote ${\mathtt{T}}$ or vice versa.

######  Remark 1.7.

The associated _primitive negative local theory_ is the subset of primitive
negative sentences of ${\mathtt{T}}$. Every sentence in ${\mathtt{T}}$ is
(elementary equivalent to) a finite conjunction of primitive negative
sentences, so the associated primitive negative local theory always (locally)
axiomatises ${\mathtt{T}}$. In sum, we could generally work only with
primitive negative sentences; this is very useful in practical examples and
was repeatedly used in [Hru22b, Seg22].

The first fundamental result in local logic is the following easy lemma
reducing local satisfiability to usual satisfiability.

######  Lemma 1.8.

Let $\Gamma$ be a set of $\Pi_{1}$-local sentences. Then, $\Gamma$ is locally
satisfiable if and only if $\Gamma\wedge{\mathtt{T}}_{\mathrm{loc}}$ is
satisfiable. Furthermore, suppose
$N\mathrel{\mathord{\models}_{\star}}\Gamma\wedge{\mathtt{T}}_{\mathrm{loc}}$
and pick $o\coloneqq(o_{s})_{s\in\mathtt{S}}$ with $o_{s}\in N^{s}$ for each
single sort $s$. If there are constants of sort $s$, assume that
${\mathrm{d}}(o_{s},c^{N})$ for some constant $c$ of sort $s$ and some
locality relation. Then, the _local component $\mathtt{D}(o)$ at $o$_, given
by
$\mathtt{D}(o)^{s}\coloneqq\bigcup_{{\mathrm{d}}\in\mathtt{D}^{s}}{\mathrm{d}}(o_{s})$
for each sort $s$, is a local model of
$\Gamma\wedge{\mathtt{T}}_{\mathrm{loc}}$.

###### Proof.

Obviously, any local model of $\Gamma$ is a model of
$\Gamma\wedge{\mathtt{T}}_{\mathrm{loc}}$. On the other hand, suppose that
$N\mathrel{\mathord{\models}_{\star}}\Gamma\wedge{\mathtt{T}}_{\mathrm{loc}}$,
$(o_{s})_{s\in\mathtt{S}}$ and $\mathtt{D}(o)$ as in the statement. By A4,
every constant symbol is interpreted in $\mathtt{D}(o)$, so it is the universe
of a substructure of $N$. As ${\mathtt{T}}_{\mathrm{loc}}$ is universal, it
follows that $M$ satisfies A1, A2, A3 and A4. Also, A5 trivially holds: for
any $a,b\in\mathtt{D}(o)^{s}$ there are locality relations ${\mathrm{d}}_{1}$
and ${\mathrm{d}}_{2}$ such that ${\mathrm{d}}_{1}(a,o_{s})$ and
${\mathrm{d}}_{2}(b,o_{s})$, so we have
${\mathrm{d}}_{1}\ast{\mathrm{d}}_{2}(a,b)$.

By a straightforward induction on the complexity, we have that, for any
$\varphi(x)\in{\mathrm{LFor}}^{x}({\mathtt{L}})$ and $a\in\mathtt{D}(o)^{x}$,
$\mathtt{D}(o)\models\varphi(a)$ if and only if
$N\mathrel{\mathord{\models}_{\star}}\varphi(a)$. Hence, take
$\varphi\in\Gamma$ and suppose $\varphi=\forall x\,\phi$ with $\phi$ a local
formula. As $N\mathrel{\mathord{\models}_{\star}}\varphi$, in particular,
$N\mathrel{\mathord{\models}_{\star}}\phi(a)$ for any $a\in\mathtt{D}(o)^{x}$,
concluding that $\mathtt{D}(o)\models\phi(a)$ for any $a\in\mathtt{D}(o)^{x}$.
So, $\mathtt{D}(o)\models\varphi$ and, as $\varphi$ was arbitrary,
$\mathtt{D}(o)\models\Gamma$. ∎

As an immediate corollary, we get the following compactness theorem for local
logic.

######  Theorem 1.9 (Compactness theorem).

Let $\Gamma$ be a set of $\Pi_{1}$-local sentences. Then, $\Gamma$ is locally
satisfiable if and only if it is finitely locally satisfiable.

Every substructure of a local structure is a local structure too, as
${\mathtt{T}}_{\mathrm{loc}}$ is universal. Therefore, we can freely apply the
downwards Löwenheim-Skolem Theorem in local logic. For the upward Löwenheim-
Skolem Theorem we have the following straightforward version.

######  Theorem 1.10 (Löwenheim-Skolem Theorem).

Let $\Gamma$ be a set of $\Pi_{1}$-local sentences and
$\kappa\geq|{\mathtt{L}}|$ a cardinal. Let $S$ be a subset of single sorts of
${\mathtt{L}}$. Suppose that, for each $s\in S$, $\Gamma$ has a local model
with some infinite ball on $s$. Then, $\Gamma$ has a local model $M$ such that
$|M^{s}|=\kappa$ for each $s\in S$.

###### Proof.

Take a (non-local) $\kappa$-saturated model
$N\mathrel{\mathord{\models}_{\star}}\Gamma\wedge{\mathtt{T}}_{\mathrm{loc}}$.
By hypothesis and saturation of $N$, there is $o=(o_{s})_{s\in\mathtt{S}}$
with $o_{s}\in N^{s}$ such that, if there is a constant $c$ of sort $s$,
${\mathrm{d}}(o_{s},c^{N})$ for some locality relation ${\mathrm{d}}$, and, if
$s\in\mathtt{S}$, $|{\mathrm{d}}(o_{s})|\geq\kappa$ for some locality relation
${\mathrm{d}}$. Thus, by Lemma 1.8, the local component $\mathtt{D}(o)$ of $N$
at $o$ realises $\Gamma$. Obviously, $|\mathtt{D}(o)^{s}|\geq\kappa$ for each
$s\in S$. Applying downwards Löwenheim-Skolem Theorem now, we can find
$M\prec\mathtt{D}(o)$ such that $|M^{s}|=\kappa$ for $s\in\mathtt{S}$. ∎

For a local structure $M$, we write ${\mathrm{Th}}_{-}(M)$ for its negative
theory, i.e. the set of negative sentences satisfied by $M$. For a subset $A$,
we write ${\mathrm{Th}}_{-}(M/A)$ for the theory of the expansion of $M$ given
by adding parameters for $A$. Note that ${\mathrm{Th}}_{-}(M)$ must be a local
theory when $M$ is local. We say that a negative local theory ${\mathtt{T}}$
is _( ${\mathtt{L}}$-locally) weakly complete_ if there is a local structure
$M$ such that ${\mathtt{T}}={\mathrm{Th}}_{-}(M)$ (see Definition 3.1 for more
details).

######  Remark 1.11.

Note that ${\mathtt{T}}={\mathrm{Th}}_{-}(M)$ if and only if
$M\models{\mathtt{T}}_{\pm}$. In particular, a negative local theory
${\mathtt{T}}$ is weakly complete if and only if ${\mathtt{T}}_{\pm}$ is
locally satisfiable.

######  Remark 1.12.

Every negative formula is universal, so it is in particular $\Pi_{1}$-local.
Hence, Lemma 1.8 could be used to show that a negative local theory is locally
satisfiable. However, in general, ${\mathtt{T}}_{\pm}$ is not $\Pi_{1}$-local,
so Lemma 1.8 cannot be used to show that ${\mathtt{T}}$ is weakly complete.

##  2\. Local positive closedness

From now on, unless otherwise stated, fix a local language ${\mathtt{L}}$ and
a locally satisfiable negative local theory ${\mathtt{T}}$.

A homomorphism $f\colon A\to B$ between two structures is a _positive
embedding_ if $B\mathrel{\mathord{\models}_{\star}}\varphi(f(a))$ implies
$A\mathrel{\mathord{\models}_{\star}}\varphi(a)$ for any positive formula
$\varphi(x)$ and $a\in A^{x}$; we write $A\precsim^{+}B$ if there is a
positive embedding from $A$ into $B$. A _positive substructure_ is a
substructure $A\leq B$ such that the inclusion ${\iota}\colon A\to B$ is a
positive embedding; we write $A\preceq^{+}B$ if $A$ is a positive substructure
of $B$. We say that a structure $A$ is _positively closed_ 111In positive
logic, _positive closedness_ is often simply called _existential closedness_
(for instance, in [Hru22b, Hru22a]). The reason is that, when classical first-
order logic is presented as a particular case of positive logic (via
Morleyization), the classical existential closedness becomes positive
closedness. However, in general, we consider this abuse of terminology
confusing. for a class of structures $\mathcal{K}$ if every homomorphism
$f\colon A\to B$ with $B\in\mathcal{K}$ is a positive embedding.

######  Remark 2.1.

The composition of positive embeddings is a positive embedding. Therefore,
structures with positive embeddings form a category. Similarly, $\preceq^{+}$
is a partial order and $\precsim^{+}$ is a preorder.

######  Definition 2.2.

Let $\Gamma$ be a set of sentences. We say that $M$ is a _local positively
closed_ model of $\Gamma$, written
$M\models^{\mathrm{pc}}_{{\mathtt{L}}}\Gamma$, if $M$ is a local model of
$\Gamma$ positively closed for the class $\mathcal{M}(\Gamma/{\mathtt{L}})$ of
local models of $\Gamma$; we write
$\mathcal{M}^{\mathrm{pc}}(\Gamma/{\mathtt{L}})$ for the class of local
positively closed models of $\Gamma$. We say that $M$ is _local positively
closed_ if it is a local positively closed model of ${\mathrm{Th}}_{-}(M)$. We
typically omit ${\mathtt{L}}$ if it is clear from the context.

Given two subsets $\Gamma_{1}$ and $\Gamma_{2}$ of first-order sentences, we
write $\Gamma_{1}\models^{\mathrm{pc}}\Gamma_{2}$ if $N\models\Gamma_{2}$ for
any $N\models^{\mathrm{pc}}\Gamma_{1}$.

######  Notation.

We say that $M$ is a _(non-local) positively closed model of $\Gamma$_,
written $M\mathrel{\mathord{\models}^{\mathrm{pc}}_{\star}}\Gamma$, if $M$ is
a model of $\Gamma$ and is positively closed for the class
$\mathcal{M}_{\star}(\Gamma)$. We say that
$\Gamma_{1}\mathrel{\mathord{\models}^{\mathrm{pc}}_{\star}}\Gamma_{2}$ if
$N\mathrel{\mathord{\models}_{\star}}\Gamma_{2}$ for any
$N\mathrel{\mathord{\models}^{\mathrm{pc}}_{\star}}\Gamma_{1}$

######  Remark 2.3.

Recall that homomorphisms preserve satisfaction of positive formulas, i.e. if
$f\colon A\to B$ is a homomorphism and
$A\mathrel{\mathord{\models}_{\star}}\varphi(a)$ with $\varphi(x)$ a positive
formula and $a\in A^{x}$, then
$B\mathrel{\mathord{\models}_{\star}}\varphi(f(a))$. Thus, when $f\colon A\to
B$ is a positive embedding, we have
$A\mathrel{\mathord{\models}_{\star}}\varphi(a)$ if and only if
$B\mathrel{\mathord{\models}_{\star}}\varphi(f(a))$. In particular, positive
embeddings are embeddings and every positive substructure of a local structure
is also a local structure.

######  Remark 2.4.

We recall the following easy fact from positive logic. Let $A$ be an
${\mathtt{L}}$-structure, $B_{A}$ an ${\mathtt{L}}(A)$-structure and $B$ its
${\mathtt{L}}$-reduct. Then, ${\mathrm{Th}}_{-}(B_{A})={\mathrm{Th}}_{-}(A/A)$
if and only if $f\colon A\to B$ given by $a\mapsto a^{B_{A}}$ is a positive
embedding.

Recall that a _direct system of (local) structures_ is a sequence
$(M_{i},f_{i,j})_{i,j\in I,i\succeq j}$ indexed by a direct set $(I,\prec)$
where each $M_{i}$ is a (local) structure, each $f_{i,j}\colon M_{j}\to M_{i}$
is a homomorphism for each $i,j\in I$ with $i\succeq j$ and $f_{i,j}\circ
f_{j,k}=f_{i,k}$ for any $i\succeq j\succeq k$. The _direct limit structure_
$\underrightarrow{\lim}\,M_{i}$ is the structure with universe
$\mathchoice{\raise 2.15277pt\hbox{$\displaystyle\bigsqcup
M^{s}_{i}$}\kern-1.00006pt/\kern-1.00006pt\lower
1.07639pt\hbox{$\displaystyle\sim$}}{\raise
2.15277pt\hbox{$\textstyle\bigsqcup
M^{s}_{i}$}\kern-1.00006pt/\kern-1.00006pt\lower
1.07639pt\hbox{$\textstyle\sim$}}{\raise 2.15277pt\hbox{$\scriptstyle\bigsqcup
M^{s}_{i}$}\kern-1.00006pt/\kern-1.00006pt\lower
1.07639pt\hbox{$\scriptstyle\sim$}}{\raise
2.15277pt\hbox{$\scriptscriptstyle\bigsqcup
M^{s}_{i}$}\kern-1.00006pt/\kern-1.00006pt\lower
1.07639pt\hbox{$\scriptscriptstyle\sim$}}$ for each sort and interpretation
$\mathchoice{\raise 2.15277pt\hbox{$\displaystyle\bigsqcup
R(M_{i})$}\kern-1.00006pt/\kern-1.00006pt\lower
1.07639pt\hbox{$\displaystyle\sim$}}{\raise
2.15277pt\hbox{$\textstyle\bigsqcup
R(M_{i})$}\kern-1.00006pt/\kern-1.00006pt\lower
1.07639pt\hbox{$\textstyle\sim$}}{\raise 2.15277pt\hbox{$\scriptstyle\bigsqcup
R(M_{i})$}\kern-1.00006pt/\kern-1.00006pt\lower
1.07639pt\hbox{$\scriptstyle\sim$}}{\raise
2.15277pt\hbox{$\scriptscriptstyle\bigsqcup
R(M_{i})$}\kern-1.00006pt/\kern-1.00006pt\lower
1.07639pt\hbox{$\scriptscriptstyle\sim$}}$ for each relation symbol; where
$a\sim b$ for $a\in M_{i}$ and $b\in M_{j}$ if there is some $k\succeq i,j$
such that $f_{k,i}(a)=f_{k,j}(b)$.

Let $N$ be a structure and $(g_{i})_{i\succeq i_{0}}$ a sequence of
homomorphisms $g_{i}\colon N\to M_{i}$ with $i_{0}\in I$ such that
$g_{i}=f_{i,j}\circ g_{j}$ for any $i\succeq j\succeq i_{0}$. The _direct
limit homomorphism_ $\underrightarrow{\lim}\,g_{i}\colon N\to M$ is the
homomorphism defined by $a\mapsto[g_{i}(a)]_{\sim}$ for some (any) $i\succeq
i_{0}$. In particular, we write $f_{i}=\underrightarrow{\lim}_{j\succeq
i}f_{j,i}$ for the canonical projection of $M_{i}$ to $M$, which is defined by
$f_{i}(a)=[a]_{\sim}$.

######  Lemma 2.5.

Let $(M_{i},f_{i,j})_{i,j\in I,i\succ j}$ be a direct system of
${\mathtt{L}}$-structures and $M$ the direct limit structure. Let $\varphi(x)$
be a formula and $a\in M^{x}$.

  1. (1)

If $\varphi$ is a positive formula, then
$M\mathrel{\mathord{\models}_{\star}}\varphi(a)$ if and only if there is $i\in
I$ such that $M_{i}\models\varphi(\widetilde{a})$ for $\widetilde{a}\in
M^{x}_{i}$ with $a=f_{i}(\widetilde{a})$.

  2. (2)

If $\varphi$ is an existential formula, then $M\models\varphi(a)$ implies that
there is $i\in I$ with $a=f_{i}(\widetilde{a})$ for some $\widetilde{a}\in
M^{x}_{i}$ such that $M_{i}\models\varphi(\widetilde{a})$.

In particular, $M$ is a model of $\bigcap{\mathrm{Th}}_{\forall}(M_{i})$.

###### Proof.

(1) and (2) follow by an easy induction on the complexity. By (2), we have
that $M$ is a model of $\bigcap{\mathrm{Th}}_{\forall}(M_{i})$. ∎

######  Lemma 2.6.

Let $(M_{i},f_{i,j})_{i,j\in I,i\succ j}$ be a direct system of local models
of ${\mathtt{T}}$. Then, the direct limit structure $M$ is a local model of
${\mathtt{T}}$. Furthermore, let $h\colon M\to A$ be a homomorphism to another
local ${\mathtt{L}}$-structure. Suppose $h_{i}\coloneqq h\circ f_{i}\colon
M_{i}\to A$ is a positively embedding for every $i$, where
$f_{i}\coloneqq\underrightarrow{\lim}_{j\succeq i}f_{j,i}$. Then, $h$ is a
positive embedding. In particular, if $M_{i}\models^{\mathrm{pc}}{\mathtt{T}}$
for each $i\in I$, then $M\models^{\mathrm{pc}}{\mathtt{T}}$.

###### Proof.

By Lemma 2.5, as ${\mathtt{T}}\wedge{\mathtt{T}}_{\mathrm{loc}}$ is a
universal set of sentences satisfied by $M_{i}$ for each $i$, we know that $M$
satisfies ${\mathtt{T}}$ and axioms A1, A2, A3 and A4. It remains to check
axiom A5. Let $a,b$ be elements in $M$ of the same sort. Suppose
$a=f_{i}(\widetilde{a}^{\prime})$ and $b=f_{j}(\widetilde{b}^{\prime})$ for
some $\widetilde{a}^{\prime}$ in $M_{i}$ and $\widetilde{b}^{\prime}$ in
$M_{j}$. Take $k\succeq i,j$, so $a=f_{k}(\widetilde{a})$ and
$b=f_{k}(\widetilde{b})$ with $\widetilde{a}=f_{k,i}(\widetilde{a}^{\prime})$
and $\widetilde{b}=f_{k,j}(\widetilde{b}^{\prime})$. As $M_{k}$ is a local
structure, there is a locality relations ${\mathrm{d}}$ such that
${\mathrm{d}}^{M_{k}}(\widetilde{a},\widetilde{b})$. Hence,
${\mathrm{d}}(a,b)$.

Now, suppose that, for every $i\in I$, $h_{i}$ is a positive embedding. Let
$\varphi(x)\in{\mathrm{For}}^{x}_{+}({\mathtt{L}})$ be a positive formula,
$a\in M^{x}$ and assume $A\models\varphi(h(a))$. Let $i\in I$ be such that
$a=f_{i}(\widetilde{a})$ for some $\widetilde{a}\in M^{x}_{i}$. As
$h_{i}\colon M_{i}\to A$ is a positive embedding and
$A\models\varphi(h_{i}(\widetilde{a}))$, we conclude that
$M_{i}\models\varphi(\widetilde{a})$. Then, by Lemma 2.5, we conclude that
$M\models\varphi(a)$. As $\varphi$ and $a$ are arbitrary, we conclude that $h$
is a positive embedding. In particular, if
$M_{i}\models^{\mathrm{pc}}{\mathtt{T}}$ for every $i\in I$, we conclude that
$M\models^{\mathrm{pc}}{\mathtt{T}}$. ∎

######  Theorem 2.7.

Let $N$ be a local model of ${\mathtt{T}}$. Then, there exists a homomorphism
$f\colon N\to M$ to $M\models^{\mathrm{pc}}{\mathtt{T}}$.

###### Proof.

We define by recursion a particular sequence
$(M_{i},f_{i,i^{\prime}})_{i^{\prime}<i\in\omega}$ of local models of
${\mathtt{T}}$ and homomorphisms $f_{i,i^{\prime}}\colon M_{i^{\prime}}\to
M_{i}$ with $M_{0}=N$. We take then $M$ and $f_{i}\colon M_{i}\to M$ to be the
resulting direct limits. Hence, by Lemma 2.6, we find that $M$ is a local
model of ${\mathtt{T}}$ and $f\coloneqq f_{0}$ is a homomorphism.

Given $M_{i}$ and $f_{i,i^{\prime}}$, we define $M_{i+1}$ and
$f_{i+1,i^{\prime}}$ as follows. Let
$\\{(\varphi_{j},a_{j})\\}_{j\in\lambda_{i}}$ be an enumeration of all pairs
where $\varphi_{j}\in{\mathrm{For}}_{+}({\mathtt{L}})$ is a positive formula
and $a_{j}$ is a tuple in $M_{i}$ on the free variables of $\varphi_{j}$. We
define by recursion a sequence $(M^{j}_{i},g^{j,k}_{i})_{k<j\in\lambda_{i}}$
of local models of ${\mathtt{T}}$ and homomorphisms $g^{j,k}_{i}\colon
M^{k}_{i}\to M^{j}_{i}$ such that $M^{0}_{i}=M_{i}$. We take $M_{i+1}$ and
$g^{k}_{i}$ to be the respective direct limits. By Lemma 2.6, we have that
$M_{i+1}$ is a local model of ${\mathtt{T}}$ and $g^{k}_{i}\colon M^{k}_{i}\to
M_{i+1}$ is a homomorphism. We take $f_{i+1,i}=g^{0}_{i}$ and
$f_{i+1,i^{\prime}}=f_{i+1,i}\circ f_{i,i^{\prime}}$.

For $\delta\in\lambda_{i}$ limit, we take $M^{\delta}_{i}$ and
$g^{\delta,k}_{i}$ as direct limit of
$(M^{j}_{i},g^{j,k}_{i})_{k<j\in\delta}$. In this case, we have that
$M^{\delta}_{i}$ is a local model of ${\mathtt{T}}$ and $g^{\delta,k}_{i}$ is
a homomorphism by Lemma 2.6.

Assume $M^{j}_{i}$ and $g^{j,k}_{i}$ are already defined. We check if there is
a local model $N\models{\mathtt{T}}$ and a morphism $g\colon M^{j}_{i}\to N$
such that $N\models\varphi_{j}(g(g^{j,0}_{i}(a_{j})))$. If $N$ and $g$ exist,
we take $M^{j+1}_{i}=N$ and $g^{j+1,k}_{i}=g\circ g^{j,k}_{i}$. Otherwise, we
take $M^{j+1}_{i}=M^{j}_{i}$ and $g^{j+1,k}_{i}=g^{j,k}_{i}$.

Now, it remains to show that, with this particular construction, the resulting
structure $M$ is local positively closed. Let $B$ be a local model of
${\mathtt{T}}$ and $h\colon M\to B$ a homomorphism. Suppose that there is a
positive formula $\varphi(x)$ and an element $a$ in $M$ such that
$B\models\varphi(h(a))$. By construction, there is some $i\in\mathbb{N}$ and
$\widetilde{a}$ in $M_{i}$ such that $a=f_{i}(\widetilde{a})$. Hence, there is
$j\in\lambda_{i}$ such that $\widetilde{a}=a_{j}$ and $\varphi=\varphi_{j}$.
As $h\colon M\to B$ is a homomorphism, we have that $g=h\circ f_{i+1}\circ
g^{j}_{i}\colon M^{j}_{i}\to B$ is a homomorphism to a local model of
${\mathtt{T}}$ such that $B\models\varphi_{j}(g(g^{j,0}_{i}(a_{j})))$.
Therefore, $M^{j+1}_{i}\models\varphi(g^{j+1,0}_{i}(\widetilde{a}))$,
concluding that $M_{i+1}\models\varphi(f_{i+1,i}(\widetilde{a}))$, so
$M\models\varphi(a)$. As $\varphi$, $a$, $B$ and $h$ are arbitrary, we
conclude that $M$ is local positively closed. ∎

######  Remark 2.8.

Applying downwards Löwenheim-Skolem in each step of the previous proof, we can
take $|M^{j+1}_{i}|\leq|{\mathtt{L}}|+|M^{j}_{i}|$ for each $i\in\omega$ and
$j\in\lambda_{i}$. As $\lambda_{i}\leq|{\mathtt{L}}|+|M_{i}|$, we can get
$|M_{i+1}|\leq|M_{i}|$. Therefore, we can add $|M|\leq|{\mathtt{L}}|+|N|$ to
Theorem 2.7.

The following lemma explains how local positively closed models are affected
by adding parameters.

######  Lemma 2.9.

Let $M\models^{\mathrm{pc}}{\mathtt{T}}$ and $A$ a subset. Let $f\colon M\to
N$ be a homomorphism to $N\models{\mathtt{T}}$. Consider the
${\mathtt{L}}(A)$-expansion $N_{A}$ given by $a^{N_{A}}=f(a)$ for $a$ in $A$.
Then, $N_{A}$ is a local model of ${\mathrm{Th}}_{-}(M/A)$. Furthermore,
$N_{A}\models^{\mathrm{pc}}{\mathrm{Th}}_{-}(M/A)$ if and only if
$N\models^{\mathrm{pc}}{\mathtt{T}}$.

###### Proof.

For any $\varphi(a)\in{\mathrm{Th}}_{-}(M/A)$, we have that
$M\not\models\neg\varphi(a)$. As $f$ is a positive embedding,
$N\not\models\neg\varphi(f(a))$. Being $\varphi$ arbitrary, we conclude that
$N_{A}\models{\mathrm{Th}}_{-}(M/A)$.

Suppose $g\colon N_{A}\to B_{A}$ is a homomorphism to a local model
$B_{A}\models{\mathrm{Th}}_{-}(M/A)$. Then, $g\colon N\to B$ is also a
homomorphism with $B\models{\mathtt{T}}$. Obviously, if $g\colon N\to B$ is a
positive embedding, then $g\colon N_{A}\to B_{A}$ is also a positive
embedding. Therefore, if $N\models^{\mathrm{pc}}{\mathtt{T}}$, we conclude
$N_{A}\models^{\mathrm{pc}}{\mathrm{Th}}_{-}(M/A)$.

Conversely, suppose $g\colon N\to B$ is a homomorphism to a local model
$B\models{\mathtt{T}}$. Then, $g\circ f\colon M\to B$ is a homomorphism, so,
taking the respective ${\mathtt{L}}(A)$-expansion,
$B_{A}\models{\mathrm{Th}}_{-}(M/A)$ and $g\circ f$ is an
${\mathtt{L}}(A)$-homomorphism. In particular, $g\colon N_{A}\to B_{A}$ is a
homomorphism. Obviously, if $g\colon N_{A}\to B_{A}$ is a positive embedding,
we conclude that $g\colon N\to B$ is a positive embedding too. Therefore, if
$N_{A}\models^{\mathrm{pc}}{\mathrm{Th}}_{-}(M/A)$, then
$N\models^{\mathrm{pc}}{\mathtt{T}}$. ∎

######  Remark 2.10.

Suppose $M\models^{\mathrm{pc}}{\mathtt{T}}$ and
$M\models{\mathtt{T}}^{\prime}$ with
${\mathtt{T}}\subseteq{\mathtt{T}}^{\prime}$. Then,
$M\models^{\mathrm{pc}}{\mathtt{T}}^{\prime}$. In particular, if
$M\models^{\mathrm{pc}}{\mathtt{T}}$ for some negative local theory
${\mathtt{T}}$, then $M$ is a local positively closed model of
${\mathrm{Th}}_{-}(M)$. Furthermore, for any subset of parameters $A$, $M_{A}$
is local positively closed for ${\mathrm{Th}}_{-}(M/A)$.

######  Definition 2.11.

Let $\varphi$ be a positive formula. A _denial_ of $\varphi$ is a positive
formula $\psi$ such that ${\mathtt{T}}\models\neg\exists x\,\varphi\wedge\psi$
— note that since ${\mathtt{T}}$ is closed under local implications and
$\neg\exists x\,\varphi\wedge\psi$ is negative, we get in fact that
$\neg\exists x\,\varphi\wedge\psi\in{\mathtt{T}}$. We write
${\mathtt{T}}\models\varphi\perp\psi$ or $\varphi\perp\psi$ if ${\mathtt{T}}$
is clear from the context.

So far, local positive logic has shown similar behaviour to usual positive
logic. The first difference appears in Lemma 2.12. In usual positive logic,
denials of positive formulas are positive formulas. In local positive logic,
on the other hand, denials of local positive formulas are still positive
formulas, but not necessarily local. This technical subtlety underlines many
of the singularities that local positive logic has.

######  Lemma 2.12.

Let $\varphi\in{\mathrm{LFor}}^{x}_{+}({\mathtt{L}})$,
$M\models^{\mathrm{pc}}{\mathtt{T}}$ and $a\in M^{x}$. Then,
$M\not\models\varphi(a)$ if and only if $M\models\psi(a)$ for some
$\psi\in{\mathrm{For}}^{x}_{+_{0}}({\mathtt{L}})$ with
${\mathtt{T}}\models\varphi\perp\psi$. Furthermore, we may take
$\psi\in{\mathrm{LFor}}^{x}_{+_{0}}({\mathtt{L}})$ when $x$ is pointed.

###### Proof.

Obviously, if $M\models\psi(a)$ with $\psi\perp\varphi$, then
$M\not\models\varphi(a)$. On the other hand, suppose that
$M\not\models\varphi(a)$. Up to elementary equivalence, we have that

$\varphi(x)=\exists y{\in}{\mathrm{d}}(t(x))\,\phi(x,y),$

where $\phi(x,y)\in{\mathrm{For}}_{{\mathrm{qf}}_{+}}({\mathtt{L}})$. Let
$\underline{y}=(\underline{y}_{1},\ldots,\underline{y}_{n})$ be new constant
symbols and consider the expansion ${\mathtt{L}}(M,\underline{y})$ of
${\mathtt{L}}(M)$ where $\mathtt{B}_{\underline{y},t^{M}(a)}={\mathrm{d}}$ —
and $\mathtt{B}$ given by $\prec$ for other constants. Consider the universal
set of ${\mathtt{L}}(M,\underline{y})$-sentences

$\Gamma\coloneqq{\mathtt{T}}\wedge{\mathrm{Diag}}_{{\mathrm{at}}}(M)\wedge\phi(a,\underline{y}).$

Note that $\Gamma$ is not locally satisfiable. Indeed, in order to reach a
contradiction, suppose that $N_{M,\underline{y}}\models\Gamma$. Then, we get a
homomorphism $h\colon M\to N$ to a local model $N\models{\mathtt{T}}$ such
that $N\models\varphi(h(a))$ witnessed by
$b=\underline{y}^{N_{\underline{y}}}$. However, as $M$ is local positively
closed for ${\mathtt{T}}$, we conclude that $M\models\varphi(a)$,
contradicting our initial hypothesis.

As $\Gamma$ is universal, by Lemma 1.8, we conclude that
$\Gamma\wedge{\mathtt{T}}_{\mathrm{loc}}({\mathtt{L}}(M,\underline{y}))$ is
not finitely satisfiable. Take
$\Lambda(a,c)\subseteq{\mathrm{Diag}}_{{\mathrm{at}}}(M)$ finite, where $c$
are some possible extra parameters, such that

${\mathtt{T}}\wedge{\mathtt{T}}_{\mathrm{loc}}\wedge{\mathrm{d}}(t(a),\underline{y})\wedge\Lambda(a,c)\wedge\phi(a,\underline{y})$

is not satisfiable. If $x$ is pointed, take the subtuple $a_{c}$ of $a$ on the
sort of $c$ and consider $\psi(x)=\exists
z{\in}\mathtt{B}_{a_{c},c}(a_{c})\,\bigwedge\Lambda(x,z)\in{\mathrm{LFor}}^{x}_{+_{0}}({\mathtt{L}})$.
Otherwise, take $\psi(x)=\exists z\,\bigwedge\Lambda(x,z)$. Note that
$M\models\psi(a)$ witnessed by $c$.

On the other hand, $\varphi\perp\psi$. Indeed, in order to reach a
contradiction, suppose otherwise, so there is $N\models{\mathtt{T}}$ and
$a^{\prime}\in N^{x}$ such that $N\models\psi(a^{\prime})$ and
$N\models\varphi(a^{\prime})$. Then, there are $b^{\prime}\in N^{y}$ and
$c^{\prime}\in N^{z}$ such that $N\models\Lambda(a^{\prime},c^{\prime})$ and
$N\models\phi(a^{\prime},b^{\prime})$, which contradicts that
${\mathtt{T}}\wedge{\mathtt{T}}_{\mathrm{loc}}\wedge\Lambda(a,c)\wedge{\mathrm{d}}(a,\underline{y})\wedge\phi(a,\underline{y})$
is not satisfiable. ∎

######  Corollary 2.13.

Every positive substructure of a local positively closed model of
${\mathtt{T}}$ is a local positively closed model of ${\mathtt{T}}$.

###### Proof.

Let $A\preceq^{+}M\models^{\mathrm{pc}}{\mathtt{T}}$ and $f\colon A\to B$
homomorphism to $B\models{\mathtt{T}}$. Take
$\varphi\in{\mathrm{For}}^{x}_{+}({\mathtt{L}})$ and $a\in A^{x}$ arbitrary
and suppose $B\models\varphi(f(a))$. Without loss of generality,
$\varphi(x)=\exists y\,\phi(x,y)$ where
$\phi\in{\mathrm{For}}^{xy}_{{\mathrm{qf}}_{+}}({\mathtt{L}})$. Hence, there
is $b\in B^{y}$ such that $B\models\phi(f(a),b)$. Take $c\in A^{y}$ arbitrary.
By the locality axioms, we have ${\mathrm{d}}^{B}(b,f(c))$ for some locality
relation ${\mathrm{d}}$ on the sort of $b$. Hence,
$B\models\varphi^{\prime}(f(a),f(c))$ with $\varphi^{\prime}(x,z)=\exists
y{\in}{\mathrm{d}}(z)\,\phi(x,y)\in{\mathrm{LFor}}^{xz}_{+}({\mathtt{L}})$.

Now, for any $\psi\perp\varphi^{\prime}$, we have that
$B\not\models\psi(f(a),f(c))$. Therefore, by Remark 2.3,
$A\not\models\psi(a,c)$. As $A\preceq^{+}M$, that means that
$M\not\models\psi(a,c)$. As $\psi$ is arbitrary, by Lemma 2.12, we conclude
that $M\models\varphi^{\prime}(a,c)$. Since $A\preceq^{+}M$, we conclude that
$A\models\varphi^{\prime}(a,c)$. In particular, $A\models\varphi(a)$. As
$\varphi$ and $a$ are arbitrary, we conclude that $f$ is a positive embedding.
As $f$ and $B$ are also arbitrary, we conclude that
$A\models^{\mathrm{pc}}{\mathtt{T}}$. ∎

Let ${\mathtt{L}}$ be a local language and ${\mathtt{T}}$ be a negative local
theory. Let $\varphi(x)$ and $\psi(x)$ be local positive formulas of
${\mathtt{L}}$. We say that $\psi$ is an _approximation_ to $\varphi$ if every
denial of $\psi$ is a denial of $\varphi$; we write
${\mathtt{T}}\models\varphi\leq\psi$ or $\varphi\leq\psi$ if ${\mathtt{T}}$ is
clear from the context. We say that $\psi$ and $\varphi$ are _complementary_
if $\varphi$ approximates every denial of $\psi$; we write
${\mathtt{T}}\models\varphi\mathrel{\top}\psi$ or $\varphi\mathrel{\top}\psi$
if ${\mathtt{T}}$ is clear from the context.

######  Lemma 2.14.

Let $\varphi(x)$ and $\psi(x)$ be positive formulas of ${\mathtt{L}}$.

  1. (1)

Suppose $\psi$ is a local positive formula. Then,
${\mathtt{T}}\models\varphi\leq\psi$ if and only if
${\mathtt{T}}\models^{\mathrm{pc}}\forall x\,\varphi(x)\rightarrow\psi(x)$.
Furthermore, in this case,
${\mathtt{T}}\mathrel{\mathord{\models}^{\mathrm{pc}}_{\star}}\forall
x\,\varphi(x)\rightarrow\psi(x)$.

  2. (2)

Suppose $\varphi$ and $\psi$ are local positive formulas. Then,
${\mathtt{T}}\models\varphi\mathrel{\top}\psi$ if and only if
${\mathtt{T}}\models^{\mathrm{pc}}\forall x\,\varphi(x)\vee\psi(x)$.
Furthermore, in this case,
${\mathtt{T}}\mathrel{\mathord{\models}^{\mathrm{pc}}_{\star}}\forall
x\,\varphi(x)\vee\psi(x)$.

###### Proof.

  1. (1)

Suppose $\varphi\leq\psi$. Take $M\models^{\mathrm{pc}}{\mathtt{T}}$ and
$a\in\varphi(M)$ arbitrary. For any $\phi\perp\psi$, as $\phi\perp\varphi$, we
have $M\not\models\phi(a)$. By Lemma 2.12, we conclude then that
$M\models\psi(a)$, so $a\in\psi(M)$. As $a$ is arbitrary, we conclude that
$M\models\forall x\,\varphi\rightarrow\psi$. As $M$ is arbitrary, we conclude
${\mathtt{T}}\models^{\mathrm{pc}}\forall x\,\varphi\rightarrow\psi$.

Suppose $\varphi\not\leq\psi$. There is then $\phi\perp\psi$ such that
$\phi\not\perp\varphi$. As $\phi\not\perp\varphi$, there is
$M\models{\mathtt{T}}$ such that $M\models\exists x\,\phi\wedge\varphi$. By
Theorem 2.7, there is a homomorphism $f\colon M\to N$ to
$N\models^{\mathrm{pc}}{\mathtt{T}}$. By Remark 2.3, $N\models\exists
x\,\phi\wedge\varphi$. Hence, $\phi(N)\cap\varphi(N)\neq\emptyset$. As
$\phi\perp\psi$, we have $\phi(N)\cap\psi(N)=\emptyset$. Therefore, we
conclude that $\varphi(N)\not\subseteq\psi(N)$. In other words,
$N\not\models\forall x\,\varphi\rightarrow\psi$, so
${\mathtt{T}}\not\models^{\mathrm{pc}}\forall x\,\varphi\rightarrow\psi$.

Suppose now $\varphi\leq\psi$ and
$M\mathrel{\mathord{\models}^{\mathrm{pc}}_{\star}}{\mathtt{T}}$. Let
$a\in\varphi(M)$ arbitrary, and assume towards a contradiction that
$a\notin\psi(M)$. By [Hru22b, Lemma 2.3(1)], there is some positive $\phi(x)$
such that $a\in\phi(M)$ and
${\mathtt{T}}\mathrel{\mathord{\models}_{\star}}\neg\exists
x\,\psi\wedge\phi$. In particular, ${\mathtt{T}}\models\neg\exists
x\,\psi\wedge\phi$ and thus $\phi\perp_{\mathtt{T}}\psi$ which implies
$\phi\perp_{\mathtt{T}}\varphi$, that is $\neg\exists
x\,\varphi\wedge\phi\in{\mathtt{T}}$. Since $a\in\varphi(M)\cap\phi(M)$, this
contradicts $M\mathrel{\mathord{\models}_{\star}}{\mathtt{T}}$. Therefore we
get that $a\in\psi(M)$ and thus since $M,a$ were arbitrary that
${\mathtt{T}}\mathrel{\mathord{\models}^{\mathrm{pc}}_{\star}}\forall
x\,\varphi(x)\rightarrow\psi(x)$.

  2. (2)

Suppose $\varphi\mathrel{\top}\psi$. Take $M\models^{\mathrm{pc}}{\mathtt{T}}$
and $a\notin\psi(M)$ arbitrary. By Lemma 2.12, we have $a\in\phi(M)$ for some
$\phi\perp\psi$. As $\phi\leq\varphi$, by (1), we get $a\in\varphi(M)$. As $a$
is arbitrary, we conclude that $M\models\forall x\,\varphi\vee\psi$. As $M$ is
arbitrary, we conclude that ${\mathtt{T}}\models^{\mathrm{pc}}\forall
x\,\varphi\vee\psi$.

Suppose $\varphi\not\mathrel{\top}\psi$. There is then $\phi\perp\psi$ such
that $\phi\not\leq\varphi$. By (1), there is then
$M\models^{\mathrm{pc}}{\mathtt{T}}$ such that
$\phi(M)\not\subseteq\varphi(M)$. Hence, there is $a\in\phi(M)$ such that
$a\notin\varphi(M)$. As $\phi\perp\psi$, we also have $a\notin\psi(M)$, so
$M\not\models\forall x\,\varphi\vee\psi$. In particular,
${\mathtt{T}}\not\models^{\mathrm{pc}}\forall x\,\varphi\vee\psi$.

Suppose now $\varphi\mathrel{\top}\psi$ and
$M\mathrel{\mathord{\models}^{\mathrm{pc}}_{\star}}{\mathtt{T}}$. Let
$a\notin\varphi(M)$ arbitrary. Then again by [Hru22b, Lemma 2.3(1)], there is
some positive $\phi(x)$ such that $a\in\phi(M)$ and
${\mathtt{T}}\mathrel{\mathord{\models}_{\star}}\neg\exists
x\,\varphi\wedge\phi$, which implies $\varphi\perp_{\mathtt{T}}\phi$. By
assumption, this means $\phi\leq_{\mathtt{T}}\psi$, thus $M\models\forall
x\,\varphi(x)\vee\psi(x)$ by (1). Therefore we get $a\in\psi(M)$ and thus
since $M,a$ were arbitrary that
${\mathtt{T}}\mathrel{\mathord{\models}^{\mathrm{pc}}_{\star}}\forall
x\,\varphi(x)\vee\psi(x)$. ∎

######  Remark 2.15.

In the case of weakly complete theories, it is easy to identify approximations
and complements. If $M\models\forall x\,\varphi(x)\rightarrow\psi(x)$, then
${\mathrm{Th}}_{-}(M)\models\varphi(x)\leq\psi(x)$. Indeed, if
${\mathrm{Th}}_{-}(M)\models\phi\perp\psi$, then $M\models\neg\exists
x\,\phi(x)\wedge\psi(x)$, so $M\models\neg\exists x\,\phi(x)\wedge\varphi(x)$,
concluding that ${\mathrm{Th}}_{-}(M)\models\phi\perp\varphi$.

Similarly, if $M\models\forall x\,\varphi(x)\vee\psi(x)$, then
${\mathrm{Th}}_{-}(M)\models\varphi\mathrel{\top}\psi$. Indeed, if
${\mathrm{Th}}_{-}(M)\models\phi\perp\psi$, then $M\models\neg\exists
x\,\phi(x)\wedge\psi(x)$, so $M\models\forall
x\,\phi(x)\rightarrow\varphi(x)$, concluding
${\mathtt{T}}\models\phi\leq\varphi$.

######  Lemma 2.16.

Let $M$ be an ${\mathtt{L}}$-structure. Suppose that every ball in $M$ is
finite and $M$ is positive atomic, i.e. for every element $a$ in $M$ there is
a positive formula $\phi_{a}$ such that $a$ is the unique element realising
it. Then, $M$ is local positively closed.

###### Proof.

By Theorem 2.7, find $f\colon M\to N$ homomorphism to
$N\models^{\mathrm{pc}}{\mathtt{T}}$. We show that $f$ is an isomorphism.

Let $b$ be an arbitrary element in $N$. Pick $a_{0}$ in $M$ of the same sort
as $b$. Since $N$ is local, we have $N\models{\mathrm{d}}(f(a_{0}),b)$ for
some ${\mathrm{d}}$. By assumption, we have that

$M\models\forall x\,\left(\exists
y\,{\mathrm{d}}(y,x)\wedge\phi_{a_{0}}(y)\right)\leftrightarrow\bigvee_{a\in{\mathrm{d}}(a_{0})}\phi_{a}(x).$

Therefore, by Remark 2.15 and Lemma 2.14(1), $N\models\forall x\,\left(\exists
y\,{\mathrm{d}}(y,x)\wedge\phi_{a_{0}}(y)\right)\leftrightarrow\bigvee_{a\in{\mathrm{d}}(a_{0})}\phi_{a}(x)$.
Now, by Remark 2.3, $N\models\phi_{a_{0}}(f(a_{0}))$, so $N\models\phi_{a}(b)$
for some $a\in{\mathrm{d}}(a_{0})$.

Also, $M\models\forall x,y\,\phi_{a}(x)\wedge\phi_{a}(y)\rightarrow x=y$, so
$N\models\forall x,y\,\phi_{a}(x)\wedge\phi_{a}(y)\rightarrow x=y$ by Remark
2.15 and Lemma 2.14(1). Now, by Remark 2.3, $N\models\phi_{a}(f(a))$, so
$f(a)=b$, concluding that $f$ is surjective.

Suppose $M\models\neg\psi(a)$ with $\psi$ positive. Then, $M\models\neg\exists
x\,\psi(x)\wedge\phi_{a}(x)$, so ${\mathtt{T}}\models\phi_{a}\perp\psi$,
concluding that $N\models\neg\psi(b)$. Therefore, $f$ preserves negative
formulas, concluding that it is a positive embedding. ∎

######  Definition 2.17.

Let $\varphi\in{\mathrm{LFor}}^{x}_{+}({\mathtt{L}})$. A _full system of
denials_ of $\varphi$ in ${\mathtt{T}}$ is a family $\Psi$ of denials of
$\varphi$ such that, for any $M\models^{\mathrm{pc}}{\mathtt{T}}$ and any
$a\in M^{x}$, either $M\models\varphi(a)$ or $M\models\psi(a)$ for some
$\psi\in\Psi$. A _full system of approximations_ of $\varphi$ in
${\mathtt{T}}$ is a family $\Psi$ of approximations of $\varphi$ such that,
for any $M\models^{\mathrm{pc}}{\mathtt{T}}$ and any $a\in M^{x}$, if
$M\models\psi(a)$ for all $\psi\in\Psi$, then $M\models\varphi(a)$.

######  Corollary 2.18.

Let $x$ be a variable and $\varphi\in{\mathrm{LFor}}^{x}_{+}({\mathtt{L}})$.
Then, there is a full system of denials of $\varphi$. Furthermore, if $x$ is
pointed, we can take it to be local positive.

##  3\. Completeness

Recall that, unless otherwise stated, we have fixed a local language
${\mathtt{L}}$ and a locally satisfiable negative local theory ${\mathtt{T}}$.

######  Definition 3.1.

  1. (I)

${\mathtt{T}}$ is _irreducible_ if, for any two positive formulas $\varphi(x)$
and $\psi(y)$ with $x$ and $y$ disjoint finite variables of the same sort, we
have

$\exists x\,\varphi(x)\in{\mathtt{T}}_{+}\mathrm{\ and\ }\exists
y\,\psi(y)\in{\mathtt{T}}_{+}\Rightarrow\exists x,y\
\varphi(x)\wedge\psi(y)\in{\mathtt{T}}_{+}.$

  2. (UI)

Let ${\mathrm{d}}=({\mathrm{d}}_{s})_{s\in\mathtt{S}}$ be a choice of a
locality relation symbols for each single sort. ${\mathtt{T}}$ is
_${\mathrm{d}}$ -irreducible_ if, for any two positive formulas $\varphi(x)$
and $\psi(y)$ with $x$ and $y$ disjoint finite variables of the same sort $s$,

$\exists x\,\varphi(x)\in{\mathtt{T}}_{+}\mathrm{\ and\ }\exists
y\,\psi(y)\in{\mathtt{T}}_{+}\Rightarrow\exists
x,y\,{\mathrm{d}}_{s}(x,y)\wedge\varphi(x)\wedge\psi(y)\in{\mathtt{T}}_{+}.$

We say that ${\mathtt{T}}$ is _uniformly irreducible_ if it is
${\mathrm{d}}$-irreducible for some ${\mathrm{d}}$.

  3. (LJP)

${\mathtt{T}}$ has the _local joint (homomorphism) property_ if for any two
local models $A,B\models{\mathtt{T}}$ there are homomorphisms $f\colon A\to M$
and $g\colon B\to M$ to a common local model $M\models{\mathtt{T}}$.

  4. (wC)

${\mathtt{T}}$ is _weakly complete_ if ${\mathtt{T}}={\mathrm{Th}}_{-}(M)$ for
some $M\models^{\mathrm{pc}}{\mathtt{T}}$.

  5. (C)

${\mathtt{T}}$ is _complete_ if ${\mathtt{T}}={\mathrm{Th}}_{-}(M)$ for every
$M\models^{\mathrm{pc}}{\mathtt{T}}$.

######  Remark 3.2.

Note that, by Remarks 2.3 and 2.7, our definition of weakly complete here
coincides with the previously one studied.

######  Lemma 3.3.

A negative theory ${\mathtt{T}}$ is complete if and only if
${\mathrm{Th}}_{-}(M)={\mathrm{Th}}_{-}(N)$ for every
$M,N\models^{\mathrm{pc}}{\mathtt{T}}$.

###### Proof.

One implication is obvious. On the other hand, take
$M\models^{\mathrm{pc}}{\mathtt{T}}$ and $\varphi\in{\mathtt{T}}_{+}$
arbitrary. Then, there is $A\models{\mathtt{T}}$ witnessing
$\varphi\in{\mathtt{T}}_{+}$. By Theorem 2.7, there is a homomorphism $f\colon
A\to N$ to $N\models^{\mathrm{pc}}{\mathtt{T}}$. By Remark 2.3,
$N\models\varphi$, so $N\not\models\neg\varphi$. By hypothesis,
${\mathrm{Th}}_{-}(N)={\mathrm{Th}}_{-}(M)$, so $M\not\models\neg\varphi$,
concluding $M\models\varphi$. As $\varphi$ is arbitrary, we conclude that
$M\models{\mathtt{T}}_{\pm}$, so ${\mathtt{T}}$ is complete. ∎

######  Theorem 3.4.

The following implications are true:

$\mathrm{(UI)}\Rightarrow\mathrm{(LJP)}\Rightarrow\mathrm{(C)}\Rightarrow\mathrm{(wC)}\Rightarrow\mathrm{(I)}.$

###### Proof.

  1. (wC)$\Rightarrow$(I)

Suppose ${\mathtt{T}}$ is weakly complete. Say $\exists
x\,\varphi(x)\in{\mathtt{T}}_{+}$ and $\exists y\,\psi(y)\in{\mathtt{T}}_{+}$
with $x$ and $y$ on the same sort. Let $M$ be a local structure with
${\mathtt{T}}={\mathrm{Th}}_{-}(M)$. Then, $M\models{\mathtt{T}}_{\pm}$, so
there are $a$ and $b$ in $M$ such that $M\models\varphi(a)$ and
$M\models\psi(b)$. Thus, $M\models\exists x,y\,\varphi(x)\wedge\psi(y)$, so
$\exists x,y\,\varphi(x)\wedge\psi(y)\in{\mathtt{T}}_{+}$. As $\varphi$ and
$\psi$ are arbitrary, we conclude that ${\mathtt{T}}$ is irreducible.

  2. (C)$\Rightarrow$(wC)

Trivial.

  3. (LJP)$\Rightarrow$(C)

Let $A,B\models^{\mathrm{pc}}{\mathtt{T}}$. By the joint property, there are
homomorphisms $f\colon A\to M$ and $g\colon B\to M$ to a common local model
$M\models{\mathtt{T}}$. As they are local positively closed, $f$ and $g$ are
positive embeddings. By Remark 2.3, we conclude
${\mathrm{Th}}_{-}(A)={\mathrm{Th}}_{-}(M)={\mathrm{Th}}_{-}(B)$. By Lemma
3.3, we conclude.

  4. (UI)$\Rightarrow$(LJP)

Let ${\mathrm{d}}=({\mathrm{d}}_{s})_{s\in\mathtt{S}}$ be a choice of locality
relation symbols such that ${\mathtt{T}}$ is ${\mathrm{d}}$-irreducible. Let
$A,B\models{\mathtt{T}}$. Consider the expansion ${\mathtt{L}}(A,B)$ of
${\mathtt{L}}$: we extend $\mathtt{B}$ to pairs of elements of $A$ or pairs of
elements of $B$ in the natural way and, for $a\in A^{s}$ and $b\in B^{s}$, we
take $\mathtt{B}_{a,b}={\mathrm{d}}_{s}$. Consider

$\Gamma={\mathtt{T}}\wedge{\mathrm{Diag}}_{{\mathrm{at}}}(A)\wedge{\mathrm{Diag}}_{{\mathrm{at}}}(B).$

We prove that $\Gamma\wedge{\mathtt{T}}_{\mathrm{loc}}({\mathtt{L}}(A,B))$ is
finitely satisfiable. Take a finite subset
$\Lambda\subseteq\Gamma\wedge{\mathtt{T}}_{\mathrm{loc}}({\mathtt{L}}(A,B))$.
Then, there are finite subsets of atomic formulas $\Phi(x)$ and $\Psi(y)$,
with $x$ and $y$ of the same sort $s$, and tuples $a\in A^{s}$ and $b\in
B^{s}$, with $A\models\Phi(a)$ and $B\models\Psi(b)$, such that
$\Lambda\subseteq{\mathtt{T}}\wedge{\mathtt{T}}_{\mathrm{loc}}\wedge\Phi(a)\wedge\Psi(b)\wedge{\mathrm{d}}_{s}(a,b)$.
Write $\phi=\bigwedge\Phi$ and $\psi=\bigwedge\Psi$. As $A\models\phi(a)$ and
$B\models\psi(b)$ with $A,B\models{\mathtt{T}}$, it follows that $\exists
x\,\phi(x),\exists y\,\psi(y)\in{\mathtt{T}}_{+}$. By
${\mathrm{d}}$-irreducibility, we have $\exists
x,y\,{\mathrm{d}}_{s}(x,y)\wedge\phi(x)\wedge\psi(y)\in{\mathtt{T}}_{+}$, so
there is a local model $M\models{\mathtt{T}}$ such that $M\models\exists
x,y\,{\mathrm{d}}_{s}(x,y)\wedge\phi(x)\wedge\psi(y)$. Thus, $\Lambda$ is
satisfiable. As $\Lambda$ is arbitrary, we conclude that
$\Gamma\wedge{\mathtt{T}}_{\mathrm{loc}}({\mathtt{L}}(A,B))$ is finitely
satisfiable. By compactness and Lemma 1.8, we conclude that $\Gamma$ is
locally satisfiable.

Let $M_{A,B}$ be a local model of $\Gamma$ and $M$ its ${\mathtt{L}}$-reduct,
so $M$ is a local model of ${\mathtt{T}}$. Let $f\colon A\to M$ and $g\colon
B\to M$ be given by $f(a)=a^{M_{A,B}}$ and $g(b)=b^{M_{A,B}}$. As
$M_{A,B}\models{\mathrm{Diag}}_{{\mathrm{at}}}(A)\wedge{\mathrm{Diag}}_{{\mathrm{at}}}(B)$,
we conclude that $f$ and $g$ are homomorphisms. Thus, ${\mathtt{T}}$ has the
local joint property.∎

######  Theorem 3.5.

The following equivalences are true in pointed local languages:

$\mathrm{(LJP)}\Leftrightarrow\mathrm{(C)}\Leftrightarrow\mathrm{(wC)}\Leftrightarrow\mathrm{(I)}.$

###### Proof.

By Theorem 3.4, we only need to prove the implication (I)$\Rightarrow$(LJP).
Let $A,B\models{\mathtt{T}}$. Consider the expansion ${\mathtt{L}}(A,B)$ of
${\mathtt{L}}$: we extend $\mathtt{B}$ to pairs of elements of $A$ or pairs of
elements of $B$ in the natural way and, for $a\in A^{s}$ and $b\in B^{s}$, we
take $\mathtt{B}_{a,b}$ given by $\prec$ from $\mathtt{B}_{a,c}$ and
$\mathtt{B}_{b,c}$ with $c$ (tuple of) constants of the sort of $a$ and $b$.
Consider

$\Gamma={\mathtt{T}}\wedge{\mathrm{Diag}}_{{\mathrm{at}}}(A)\wedge{\mathrm{Diag}}_{{\mathrm{at}}}(B).$

We prove that $\Gamma\wedge{\mathtt{T}}_{\mathrm{loc}}({\mathtt{L}}(A,B))$ is
finitely satisfiable with an argument similar to the one used in Theorem 3.4
for (UI)$\Rightarrow$(LJP). By compactness and Lemma 1.8, we conclude that
$\Gamma$ is locally satisfiable.

Let $M_{A,B}$ be a local model of $\Gamma$ and $M$ its ${\mathtt{L}}$-reduct,
so $M$ is a local model of ${\mathtt{T}}$. Let $f\colon A\to M$ and $g\colon
B\to M$ be given by $f(a)=a^{M_{A,B}}$ and $g(b)=b^{M_{A,B}}$. As
$M_{A,B}\models{\mathrm{Diag}}_{{\mathrm{at}}}(A)\wedge{\mathrm{Diag}}_{{\mathrm{at}}}(B)$,
we conclude that $f$ and $g$ are homomorphisms. Thus, ${\mathtt{T}}$ has the
local joint property. ∎

######  Lemma 3.6.

A negative theory ${\mathtt{T}}$ is uniformly irreducible if and only if it is
weakly complete and all its local positively closed models are balls, i.e. for
any $M\models^{\mathrm{pc}}{\mathtt{T}}$ and sort $s$ there are $o\in M^{s}$
and a locality relation ${\mathrm{d}}$ on sort $s$ such that
$M^{s}={\mathrm{d}}(o)$.

###### Proof.

Let ${\mathrm{d}}=({\mathrm{d}}_{s})_{s\in\mathtt{S}}$ be a choice of locality
relations such that ${\mathtt{T}}$ is ${\mathrm{d}}$-irreducible. By Theorem
3.4, we have that ${\mathtt{T}}$ is weakly complete. On the other hand, let
$M\models^{\mathrm{pc}}{\mathtt{T}}$. We claim that
$M\models{\mathrm{d}}_{s}\ast{\mathrm{d}}_{s}(a,b)$ for all $a,b\in M^{s}$.
Otherwise, by Lemma 2.12, there is a positive formula $\psi(x,y)$ with
$M\models\psi(a,b)$ and
${\mathtt{T}}\models\psi\perp{\mathrm{d}}_{s}\ast{\mathrm{d}}_{s}$. Hence,
$\exists x,y\,\psi(x,y)\in{\mathtt{T}}_{+}$. At the same time, $\exists
z,w\,z=w\in{\mathtt{T}}_{+}$ for $z,w$ of the same sort as $x,y$, so $\exists
x,y,z,w\,\psi(x,y)\wedge{\mathrm{d}}_{s}(x,z)\wedge{\mathrm{d}}_{s}(y,w)\wedge
z=w\in{\mathtt{T}}_{+}$ by ${\mathrm{d}}$-irreducibility, concluding $\exists
x,y\,\psi(x,y)\wedge{\mathrm{d}}_{s}\ast{\mathrm{d}}_{s}(x,y)\in{\mathtt{T}}_{+}$
by A1 and A3, which contradicts
$\psi\perp{\mathrm{d}}_{s}\ast{\mathrm{d}}_{s}$.

Conversely, suppose ${\mathtt{T}}$ is weakly complete and every local
positively closed model of ${\mathtt{T}}$ is a ball. Pick
$M\models^{\mathrm{pc}}{\mathtt{T}}$ with ${\mathtt{T}}={\mathrm{Th}}_{-}(M)$.
Let $o=(o_{s})_{s\in\mathtt{S}}$ be a choice of elements for each sort of $M$
and ${\mathrm{d}}=({\mathrm{d}}_{s})_{s\in\mathtt{S}}$ a choice of locality
relations such that $M^{s}={\mathrm{d}}_{s}(o_{s})$ for each $s\in\mathtt{S}$.
Say $\exists x\,\varphi(x)\in{\mathtt{T}}_{+}$ and $\exists
y\,\psi(y)\in{\mathtt{T}}_{+}$ with $\varphi,\psi$ positive formulas and $x$
and $y$ disjoint finite variables on the same sort. Then, $M\models\varphi(a)$
and $M\models\psi(b)$ for some $a,b\in M^{s}$. By A1 and A3, we get
$M\models\varphi(a)\wedge\psi(b)\wedge{\mathrm{d}}_{s}\ast{\mathrm{d}}_{s}(a,b)$,
so $\exists
x,y\,\varphi(x)\wedge\psi(y)\wedge{\mathrm{d}}_{s}\ast{\mathrm{d}}_{s}(x,y)\in{\mathtt{T}}_{+}$.
In conclusion, ${\mathtt{T}}$ is ${\mathrm{d}}\ast{\mathrm{d}}$-irreducible,
where
${\mathrm{d}}\ast{\mathrm{d}}=({\mathrm{d}}_{s}\ast{\mathrm{d}}_{s})_{s\in\mathtt{S}}$.
∎

######  Example 3.7.

The three first implications of Theorem 3.4 are strict:

  1. (1)

(wC)$\not\Rightarrow$(C) Consider the one-sorted local language ${\mathtt{L}}$
with locality predicates $\mathtt{D}=\\{{\mathrm{d}}_{n}\\}_{n\in\mathbb{N}}$
(with the usual ordered monoid structure induced by the natural numbers) and
unary predicates $\\{P_{n},Q_{n}\\}_{n\in\mathbb{N}}$. Consider the
${\mathtt{L}}$-structure $Z$ with universe $\mathbb{Z}$ given by
$Z\models{\mathrm{d}}_{n}(x,y)\Leftrightarrow|x-y|\leq n$, $Z\models
P_{n}(x)\Leftrightarrow x\geq n$ and $Z\models Q_{n}(x)\Leftrightarrow
x\leq-n$ for each $n\in\mathbb{N}$. Let ${\mathtt{T}}$ be its negative theory,
which is obviously a local theory as $Z$ is a local structure.

Now, let $\widetilde{Z}$ be a non-local $\aleph_{1}$-saturated elementary
extension of $Z$. Obviously,
$\widetilde{Z}\mathrel{\mathord{\models}_{\star}}{\mathtt{T}}$ and, as
${\mathtt{T}}$ is universal, any substructure of $\widetilde{Z}$ satisfies
${\mathtt{T}}$ too. Pick $\infty$ and $-\infty$ in $\widetilde{Z}$ such that
$\infty\in P_{n}(\widetilde{Z})$ and $-\infty\in Q_{n}(\widetilde{Z})$ for
every $n\in\mathbb{N}$. Let $I$ be the substructure whose universe only
contains $\infty$ and $J$ be the substructure whose universe only contains
$-\infty$; both are local models of ${\mathtt{T}}$.

We claim that $Z$, $I$ and $J$ are all the local positively closed models of
${\mathtt{T}}$ up to isomorphism. Indeed, say
$M\models^{\mathrm{pc}}{\mathtt{T}}$. Then, there are three cases: either
$M\models\neg\exists x\,Q_{0}(x)$, or $M\models\neg\exists x\,P_{0}(x)$, or
$M\models\left(\exists x\,P_{0}(x)\right)\wedge\left(\exists
x\,Q_{0}(x)\right)$. Since $Z\models\forall x\,P_{0}(x)\vee Q_{0}(x)$, we have
${\mathtt{T}}\models P_{0}\mathrel{\top}Q_{0}$ by Remark 2.15, so the three
cases are exclusive.

Consider first the case $M\models\left(\exists
x\,P_{0}(x)\right)\wedge\left(\exists x\,Q_{0}(x)\right)$. Since
$Z\models\forall x\,P_{0}(x)\vee Q_{1}(x)$, we have ${\mathtt{T}}\models
P_{0}\mathrel{\top}Q_{1}$ by Remark 2.15. Also, ${\mathtt{T}}\models
P_{0}\perp Q_{1}$. Thus, $M\models\forall x\,P_{0}(x)\leftrightarrow\neg
Q_{1}(x)$ by Lemma 2.14(2). Consequently, we have the well-defined map
$h\colon M\to Z$ given by

$h(a)=\begin{cases}\phantom{-}\min\\{k:M\models\exists
y\,{\mathrm{d}}_{k}(a,y)\wedge Q_{0}(y)\\}&\mathrm{if\ }M\models P_{0}(a),\\\
-\min\\{k:M\models\exists y\,{\mathrm{d}}_{k}(a,y)\wedge
P_{0}(y)\\}&\mathrm{if\ }M\models Q_{1}(a).\end{cases}$

We claim that $h$ is a homomorphism.

Indeed, $Z\models\neg\exists x,y\,P_{n}(x)\wedge{\mathrm{d}}_{k}(x,y)\wedge
Q_{0}(y)$ for $k<n$, so ${\mathtt{T}}\models P_{n}\perp\exists
y\,{\mathrm{d}}_{k}(x,y)\wedge Q_{0}(y)$. Thus, if $M\models P_{n}(a)$, then
$h(a)\geq n$, so $Z\models P_{n}(h(a))$. Similarly, if $M\models Q_{n}(a)$,
then $h(a)\leq-n$, so $Z\models Q_{n}(h(a))$. Suppose
$M\models{\mathrm{d}}_{n}(a,b)$, $|h(a)|=m$ and $|h(b)|=k$. Consider first the
case $M\models P_{0}(a)\wedge P_{0}(b)$. Since $M\models{\mathrm{d}}_{n}(a,b)$
and $M\models{\mathrm{d}}_{k}(b,c)$ for some $c$ with $M\models Q_{0}(c)$, we
get $N\models{\mathrm{d}}_{n+k}(a,c)$, so $m\leq n+k$. Similarly, $k\leq n+m$,
so $|m-k|\leq n$. In particular, if $M\models P_{1}(a)\wedge P_{1}(b)$, we
conclude that $Z\models{\mathrm{d}}_{n}(h(a),h(b))$. Similarly, if $M\models
Q_{1}(a)\wedge Q_{1}(b)$, we get $Z\models{\mathrm{d}}_{n}(h(a),h(b))$. On the
other hand, note that

$Z\models\neg\exists x,y\,P_{0}(x)\wedge
Q_{1}(y)\wedge{\mathrm{d}}_{n}(x,y)\wedge\left(\exists
z\,{\mathrm{d}}_{m}(x,z)\wedge Q_{0}(z)\right)\wedge\left(\exists
z\,{\mathrm{d}}_{k}(y,z)\wedge P_{0}(z)\right)$

for $n<m+k$. Therefore, if $M\models P_{0}(a)\wedge Q_{1}(b)$, we get $n\geq
m+k=|h(a)-h(b)|$. Thus, $Z\models{\mathrm{d}}_{n}(h(a),h(b))$. In conclusion,
$h$ is a homomorphism.

As $M$ is local positively closed, we conclude that $h$ is a positive
embedding. Now, $Z\models\exists x\,\left(P_{k}(x)\vee
Q_{k}(x)\right)\wedge\exists y\,{\mathrm{d}}_{k}(x,y)\wedge P_{0}(y)\wedge
Q_{0}(y)$ for all $k\in\mathbb{Z}$, so there is $a\in M$ such that
$M\models(P_{k}(a)\vee Q_{k}(a))\wedge\exists y\,{\mathrm{d}}_{k}(a,y)\wedge
P_{0}(y)\wedge Q_{0}(y)$. Thus, $Z\models(P_{k}(h(a))\vee
Q_{k}(h(a)))\wedge\exists y\,{\mathrm{d}}_{k}(h(a),y)\wedge P_{0}(y)\wedge
Q_{0}(y)$ by Remark 2.3. However, $k$ is the unique element in $Z$ realising
that formula, so $h(a)=k$. In conclusion, $h$ is surjective, so an
isomorphism.

Note that this implies $Z\models^{\mathrm{pc}}{\mathtt{T}}$. Indeed, let
$f\colon Z\to M$ be a homomorphism to $M\models^{\mathrm{pc}}{\mathtt{T}}$,
which exists by Theorem 2.7. Since $M\models\left(\exists
x\,P_{0}(x)\right)\wedge\left(\exists x\,Q_{0}(x)\right)$, we have that
$M\models\left(\exists x\,P_{0}(x)\right)\wedge\left(\exists
x\,Q_{0}(x)\right)$ by Remark 2.3. Thus, we have the isomorphism $h\colon M\to
Z$ defined as above. In fact, as $M\models P_{k}(f(k))\wedge\exists
y\,{\mathrm{d}}_{k}(f(k),y)$, we get that $h\circ f={\mathrm{id}}$, so $h$ is
a retraction of $f$ and $Z$ is a retractor of ${\mathtt{T}}$ as defined in
Definition 5.8.

Consider now the case $M\models\neg\exists x\,Q_{0}(x)$. Since
$Z\models\forall x\,Q_{n}(x)\rightarrow Q_{0}(x)$, we get ${\mathtt{T}}\models
Q_{n}\leq Q_{0}$ by Remark 2.15, so $M\models\neg\exists x\,Q_{n}(x)$ for all
$n\in\mathbb{N}$ by Lemma 2.14(1). Hence, the map $h\colon x\mapsto\infty$
from $M$ to $I$ is a homomorphism. As $M\models^{\mathrm{pc}}{\mathtt{T}}$, we
get that it is a positive embedding, so an isomorphism as it is surjective.

Note that this implies that $I\models^{\mathrm{pc}}{\mathtt{T}}$. Indeed, let
$f\colon I\to M$ be a homomorphism to $M\models^{\mathrm{pc}}{\mathtt{T}}$,
which exists by Theorem 2.7. We obviously have that
${\mathtt{T}}\models\neg\exists x,y\,{\mathrm{d}}_{n}(x,y)\wedge
P_{n+1}(x)\wedge Q_{0}(y)$ for every $n\in\mathbb{N}$. Therefore, as $M\models
P_{n}(f(\infty))$ for every $n\in\mathbb{N}$, we have that
$M\models\neg\exists y\,Q_{0}(y)$. Thus, we have the isomorphism $h\colon M\to
I$ defined as above. In fact, as $|I|=1$, $h\circ f={\mathrm{id}}$, so $h$ is
a retraction of $f$ and $I$ is a retractor of ${\mathtt{T}}$ as defined in
Definition 5.8.

Similarly, we conclude that $M\cong J$ for
$M\models^{\mathrm{pc}}{\mathtt{T}}$ with $M\models\neg\exists x\,P_{0}(x)$.
In particular, $J\models^{\mathrm{pc}}{\mathtt{T}}$. In fact, as above, we get
that $J$ is a retractor of ${\mathtt{T}}$ as defined in Definition 5.8.

In sum, ${\mathrm{Th}}_{-}(Z)$, ${\mathrm{Th}}_{-}(I)$ and
${\mathrm{Th}}_{-}(J)$ are different, so ${\mathtt{T}}$ is weakly complete but
no complete.

  2. (2)

(LJP)$\not\Rightarrow$(UI) Let ${\mathtt{L}}$ and $Z$ be as in the previous
example. Consider the expansion given by adding a constant for $0$ and
${\mathtt{T}}={\mathrm{Th}}_{-}(Z/0)$ the negative theory of $Z$ with a
constant for $0$. By Theorem 3.5, we know that ${\mathtt{T}}$ satisfies the
local joint property. On the other hand, for any locality relation
${\mathrm{d}}_{n}$, we have that ${\mathtt{T}}\models\neg\exists
x,y\,{\mathrm{d}}_{n}(x,y)\wedge P_{n}(x)\wedge Q_{n}(y)$. Therefore,
${\mathtt{T}}$ is not uniformly irreducible.

  3. (3)

(C)$\not\Rightarrow$(LJP) Consider the same one-sorted local language
${\mathtt{L}}$ and the ${\mathtt{L}}$-structure $M$ with universe $2^{\omega}$
and interpretations
$M\models{\mathrm{d}}_{n}(\eta,\zeta)\Leftrightarrow|\\{i:\eta(i)\neq\zeta(i)\\}|\leq
n$, $M\models P_{n}(\eta)\Leftrightarrow\eta(n)=1$ and $M\models
Q_{n}(\eta)\Leftrightarrow\eta(n)=0$ for each $n\in\mathbb{N}$. Let
${\mathtt{T}}={\mathrm{Th}}_{-}(M)$ be the negative theory of $M$. Since
$M\models{\mathtt{T}}_{\mathrm{loc}}$, ${\mathtt{T}}$ is locally satisfiable
by Theorem 1.9. For $\eta\in M$, write $M_{\eta}\coloneqq\mathtt{D}(\eta)$.

Now, we look at $M$ as no-local structure, i.e. as
${\mathtt{L}}_{\star}$-structure. Note that the positive logic topology in $M$
is coarser than the Tychonoff topology, so $M$ is compact with the positive
logic topology. Thus, by [Seg22, Lemma 2.24], we get that $M$ is homomorphism
universal for $\mathcal{M}_{\star}({\mathtt{T}})$. In particular, there is a
homomorphism $f\colon N\to M$ for every local positively closed model $N$ of
${\mathtt{T}}$.

Let $N\models^{\mathrm{pc}}{\mathtt{T}}$ be arbitrary and take $f\colon N\to
M$ homomorphism. Pick $a\in N$ arbitrary and set $\eta=f(a)$. Consider
$M_{\eta}$. By Lemma 1.8, $M_{\eta}\models{\mathtt{T}}$. Since $N$ is local,
$f\colon N\to M_{\eta}$. Since $N$ is local positively closed, we conclude
that $f$ is a positive embedding. Take $\zeta\in M_{\eta}$ arbitrary and take
$n=|\\{m:\zeta(m)\neq\eta(m)\\}|$, $I_{0}=\\{m:\zeta(m)=0,\ \eta(m)=1\\}$ and
$I_{1}=\\{m:\zeta(m)=1,\ \eta(m)=0\\}$. Note that, then,
$M_{\eta}\models\psi(\zeta,\eta)$ where
$\psi(\zeta,\eta)={\mathrm{d}}_{n}(\zeta,\eta)\wedge\bigwedge_{m\in
I_{0}}P_{m}(\zeta)\wedge\bigwedge_{m\in I_{1}}Q_{m}(\zeta)$. Hence, as $f$ is
a positive embedding, there is $b\in N$ such that $N\models\psi(b,a)$. Now, by
Remark 2.3, then $M_{\eta}\models\psi(f(b),\eta)$. However, by the pigeonhole
principle, $\zeta$ is the unique element realising $\psi(x,\eta)$ in
$M_{\eta}$, so we conclude that $f(b)=\zeta$. Since $\zeta$ is arbitrary, we
conclude that $f$ is surjective, so it is an isomorphism. Since $N$ is
arbitrary, we conclude that every local positively closed model of
${\mathtt{T}}$ is isomorphic to $M_{\eta}$ for some $\eta\in M$.

Let $\eta\in M$ and suppose $M\models\varphi$ with $\varphi$ a positive
formula in ${\mathtt{L}}$. For $n\in\mathbb{N}$, let ${\mathtt{L}}_{n}$ be the
reduct of ${\mathtt{L}}$ consisting of
$\\{{\mathrm{d}}_{k},P_{k},Q_{k}\\}_{k\leq n}$ and take $n$ such that
$\varphi$ is a formula in ${\mathtt{L}}_{n}$. Consider the map $f\colon M\to
M_{\eta}$ given by $f(\xi)(k)=\xi(k)$ for $k\leq n$ and $f(\xi)(k)=\eta(k)$
for $k>n$. Obviously, $P_{k}(\xi)$ implies $P_{k}(f(\xi))$ and $Q_{k}(\xi)$
implies $Q_{k}(f(\xi))$ for any $k\leq n$. On the other hand,
$|\\{m:f(\xi)(m)\neq f(\zeta)(m)\\}|\leq|\\{m:\xi(m)\neq\zeta(m)\\}|$, so
${\mathrm{d}}_{k}(\xi,\zeta)$ implies ${\mathrm{d}}_{k}(f(\xi),f(\zeta))$ for
any $k$. Thus, $f$ is an ${\mathtt{L}}_{n}$-homomorphism. By Remark 2.3, we
conclude that $M_{\eta}\models\varphi$. As $\varphi$ is arbitrary, we conclude
that ${\mathrm{Th}}_{-}(M_{\eta})={\mathtt{T}}$ for any $\eta\in M$. Hence,
${\mathtt{T}}$ is a complete local theory.

Finally, note that ${\mathtt{T}}$ does not have the local joint property. Take
$\eta,\zeta\in M$ with $\\{m:\zeta(m)\neq\eta(m)\\}$ infinite. In order to
reach a contradiction, suppose that there are homomorphisms $f\colon
M_{\zeta}\to N$ and $g\colon M_{\zeta}\to N$ with $N\models{\mathtt{T}}$.
Then, $\bigwedge_{m\in I}R_{m}(f(\eta),g(\zeta))$ where
$R_{m}(x,y)=(P_{m}(x)\wedge Q_{m}(y))\vee(Q_{m}(x)\wedge P_{m}(y))$ and
$I=\\{m:\zeta(m)\neq\eta(m)\\}$. On the other hand, for any finite subset
$J\subseteq\mathbb{N}$, ${\mathtt{T}}\models\neg\exists x,y\,\bigwedge_{m\in
J}R_{m}(x,y)\wedge{\mathrm{d}}_{|J|-1}(x,y)$. Thus, we get
$N\not\models{\mathrm{d}}_{n}(f(\eta),g(\zeta))$ for every $n\in\mathbb{N}$,
contradicting that $N$ is a local structure.

  4. (4)

(I)$\not\Rightarrow$(wC) Consider the one-sorted local language ${\mathtt{L}}$
with locality relations $\mathtt{D}=\\{{\mathrm{d}}_{n}\\}_{n\in\mathbb{N}}$
(with the usual ordered monoid structure induced by the natural numbers) and
unary predicates $\\{P_{\alpha}\\}_{\alpha<\omega_{1}}$. Let $\mathcal{C}$ be
the class of all ${\mathtt{L}}$-structures $M$ with universe $\mathbb{Z}$ such
that $M\models{\mathrm{d}}_{n}(a,b)\Leftrightarrow|a-b|\leq n$ and such that
$P_{\alpha}(M)\cap P_{\beta}(M)=\emptyset$ for all $\alpha<\beta<\omega_{1}$.
Let ${\mathtt{T}}\coloneqq\bigcap_{M\in\mathcal{C}}{\mathrm{Th}}_{-}(M)$ be
the negative theory of $\mathcal{C}$.

Note that ${\mathtt{T}}$ is a local negative theory; if
${\mathtt{T}}\models\varphi$ for $\varphi$ a negative sentence, then, in
particular, $M\models\varphi$ for any $M\in\mathcal{C}$ (since $M$ is local
and ${\mathtt{T}}\subseteq{\mathrm{Th}}_{-}(M)$), so $\varphi\in{\mathtt{T}}$.

Pick $\exists x\,\varphi(x)\in{\mathtt{T}}_{+}$ and
$\exists\,y\psi(y)\in{\mathtt{T}}_{+}$ arbitrary. There are
$M_{1},M_{2}\in\mathcal{C}$ such that $M_{1}\models\exists x\,\varphi(x)$ and
$M_{2}\models\exists y\,\psi(y)$ by definition of ${\mathtt{T}}$. Let $a\in
M_{1}^{x}$ and $b\in M_{2}^{y}$ be tuples such that $M_{1}\models\varphi(a)$,
$M_{2}\models\psi(b)$. Let $M$ be the ${\mathtt{L}}$-structure with universe
$\mathbb{Z}$, $M\models{\mathrm{d}}_{n}(x,y)\Leftrightarrow|x-y|\leq n$ and

$M\models P_{\alpha}(c)\Leftrightarrow\begin{cases}M_{1}\models
P_{\alpha}(c+\max(a))&\mathrm{if\ }c\leq 0,\\\ M_{2}\models
P_{\alpha}(c-\min(b)-1)&\mathrm{if\ }c>0.\end{cases}$

Then, the substructure $(-\infty,\max(a)]\subseteq M_{1}$ is isomorphic to the
substructure $(-\infty,0]\subseteq M$. Similarly, the substructure
$[min(b),\infty)\subseteq M_{2}$ is isomorphic to the substructure
$[1,\infty)\subseteq M$. Therefore, $M\models\exists
x,y\,\varphi(x)\wedge\psi(y)$. Furthermore, the subsets
$\\{P_{\alpha}(M)\\}_{\alpha<\omega_{1}}$ are disjoint (since every negative
element is contained in at most one by $M_{1}\in\mathcal{C}$ and likewise for
positive). Thus, $M\in\mathcal{C}$, concluding $\exists
x,y\,\varphi(x)\wedge\psi(y)\in{\mathtt{T}}_{+}$ witnessed by
$M\models{\mathtt{T}}$. As $\varphi$ and $\psi$ are arbitrary, we conclude
that ${\mathtt{T}}$ is irreducible.

On the other hand, take $M\models{\mathtt{T}}$ arbitrary and choose a single
element $a\in M$. Then, for any $n\in\mathbb{N}$, the set
$C_{n}=\\{\alpha<\omega_{1}:P_{\alpha}(M)\cap{\mathrm{d}}_{n}(a)\neq\emptyset\\}$
is of cardinality at most $2n+1$. Indeed, for any distinct
$\alpha_{0},\ldots,\alpha_{2n+1}$, we have that $\varphi=\neg\exists
x,y_{0},\ldots,y_{2n+1}\,\bigwedge_{i\leq
2n+1}P_{\alpha_{i}}(y_{i})\wedge{\mathrm{d}}_{n}(x,y_{i})$ holds in every
structure in $\mathcal{C}$, so $\varphi\in{\mathtt{T}}$. Therefore,
$\bigcup_{n\in\mathbb{N}}C_{n}$ is at most countable, and so there is some
$\alpha\in\omega_{1}\setminus\bigcup_{n\in\mathbb{N}}C_{n}$. For such
$\alpha$, we get

$\emptyset=\bigcup_{n\in\mathbb{N}}(P_{\alpha}(M)\cap{\mathrm{d}}_{n}(a))=P_{\alpha}(M)\cap\bigcup_{n\in\mathbb{N}}{\mathrm{d}}_{n}(a)=P_{\alpha}(M).$

In sum, $M\models\neg\exists x\,P_{\alpha}(x)$, while clearly $\neg\exists
x\,P_{\alpha}(x)\notin{\mathtt{T}}$. Thus,
${\mathtt{T}}\neq{\mathrm{Th}}_{-}(M)$. As $M\models{\mathtt{T}}$ is
arbitrary, it follows that ${\mathtt{T}}$ is not weakly complete.

On the other hand, for countable languages the implication
$\mathrm{(wC)}\Rightarrow\mathrm{(I)}$ of Theorem 3.4 is in fact an
equivalence, as Theorem 3.11 shows.

######  Definition 3.8.

Let $x=\\{x_{i}\\}_{i\in N}$ be a variable. Let $I$ be the subset of indexes
$i\in N$ such that there is a constant symbol on the sort of $x_{i}$ and $J$
the set of pairs of indexes $(i,j)\in N\times N$ such that $x_{i}$ and $x_{j}$
are on the same sort. A _bound_ of $x$ in ${\mathtt{T}}$ is a partial
quantifier free type of the form

$\mathrm{B}(x)\coloneqq\bigwedge_{i\in
I}{\mathrm{d}}_{i}(x_{i},c_{i})\wedge\bigwedge_{(i,j)\in
J}{\mathrm{d}}_{i,j}(x_{i},x_{j})$

where $c_{i}$ is some constant on the sort of $x_{i}$ for $i\in I$,
${\mathrm{d}}_{i}$ is a locality relation on the sort of $x_{i}$ for $i\in I$
and ${\mathrm{d}}_{i,j}$ is a locality relation on the common sort of $x_{i}$
and $x_{j}$ for $(i,j)\in J$.

######  Remark 3.9.

When $x$ is a finite variable, the bounds of $x$ are quantifier free positive
formulas on $x$ constructed using only locality predicates and constants.

######  Lemma 3.10.

Let $\varphi(x)$ be a positive formula such that $\exists
x\,\varphi(x)\in{\mathtt{T}}_{+}$. Then, there is a bound $\mathrm{B}(x)$ of
$x$ such that $\exists x\,\mathrm{B}(x)\wedge\varphi(x)\in{\mathtt{T}}_{+}$.

###### Proof.

Suppose $\exists x\,\varphi(x)\in{\mathtt{T}}_{+}$. Take $M$ witnessing it and
$a\in M^{x}$ such that $M\models\varphi(a)$. As $M$ is local, there is a bound
$\mathrm{B}(x)$ such that $M\models\mathrm{B}(a)$. Therefore, $M\models\exists
x\,\mathrm{B}(x)\wedge\varphi(x)$, concluding $\exists
x\,\mathrm{B}(x)\wedge\varphi(x)\in{\mathtt{T}}_{+}$. ∎

######  Theorem 3.11.

Assume ${\mathtt{L}}$ is countable. Then, ${\mathtt{T}}$ is weakly complete if
and only if it is irreducible.

###### Proof.

Let $I$ be the family of quantifier free primitive positive formulas $\varphi$
(up to renaming variables) such that $\exists
x\,\varphi(x)\in{\mathtt{T}}_{+}$. Without loss of generality, we pick
disjoint variables $x_{\varphi}$ for each $\varphi\in I$. Since ${\mathtt{L}}$
is countable, fix an enumeration $\\{\varphi_{i}(x_{i})\\}_{i\in\mathbb{N}}$
of $I$.

By irreducibility, recursively define bounds $\mathrm{B}_{i}$ of $x_{0}\ldots
x_{i}$ for each $i\in\mathbb{N}$ such that $\exists x_{0}\ldots
x_{i}\,\psi_{i}\in{\mathtt{T}}_{+}$ where $\psi_{i}\coloneqq\bigwedge_{j\leq
i}\varphi_{j}(x_{j})\wedge\mathrm{B}_{j}(x_{0}\ldots x_{j})$. Indeed, by Lemma
3.10, we can find $\mathrm{B}_{0}$. Now, given
$\mathrm{B}_{0},\ldots,\mathrm{B}_{i}$, as $\exists x_{0}\ldots
x_{i}\,\psi_{i}\in{\mathtt{T}}_{+}$ and $\exists
x_{i+1}\,\varphi_{i+1}(x_{i+1})\in{\mathtt{T}}_{+}$, by irreducibility and
Lemma 3.10, there is a bound $\mathrm{B}_{i+1}(x_{0}\ldots x_{i+1})$ such that
$\exists x_{0}\ldots x_{i+1}\,\psi_{i+1}=\exists x_{0}\ldots
x_{i+1}\,\psi_{i}\wedge\varphi_{i+1}\wedge\mathrm{B}_{i+1}\in{\mathtt{T}}_{+}$.

Consider the partial type
$\Sigma(x_{i})_{i\in\mathbb{N}}=\\{\psi_{i}(x_{0},\ldots,x_{i})\\}_{i\in\mathbb{N}}$.
Then, it is finitely satisfiable with
${\mathtt{T}}\cup{\mathtt{T}}_{\mathrm{loc}}$ by construction, so there is
some structure
$M^{\prime}\mathrel{\mathord{\models}_{\star}}{\mathtt{T}}\cup{\mathtt{T}}_{\mathrm{loc}}$
and $a\coloneqq(a_{i})_{i\in\mathbb{N}}$ in $M^{\prime}$ realising $\Sigma$.
Pick a subtuple $b$ of $a$ containing one element for each sort and consider
$M=\mathtt{D}(b)$, which is certainly an ${\mathtt{L}}$-structure and contains
$a$. By Lemma 1.8, $M\models{\mathtt{T}}$ and $M\models\Sigma(a)$. Thus,
${\mathrm{Th}}_{-}(M^{\prime})={\mathtt{T}}$ as required. ∎

A _(local) weak completion_ of ${\mathtt{T}}$ is a negative local theory that
is minimal among the weakly complete negative local theories containing
${\mathtt{T}}$. A _(local) completion_ of ${\mathtt{T}}$ is a negative local
theory that is minimal among the complete negative local theories containing
${\mathtt{T}}$.

######  Lemma 3.12.

Let $\widetilde{{\mathtt{T}}}$ be a weak completion of ${\mathtt{T}}$. Then,
$\widetilde{{\mathtt{T}}}={\mathrm{Th}}_{-}(M)$ for some
$M\models^{\mathrm{pc}}{\mathtt{T}}$.

###### Proof.

Take a local model $N\models\widetilde{{\mathtt{T}}}$ with
${\mathrm{Th}}_{-}(N)=\widetilde{{\mathtt{T}}}$. Obviously,
$N\models{\mathtt{T}}$. By Theorem 2.7, there is a homomorphism $f\colon N\to
M$ to $M\models^{\mathrm{pc}}{\mathtt{T}}$. By Remark 1.11, $N$ is a local
model of $\widetilde{{\mathtt{T}}}_{\pm}$. As $f$ is a homomorphism, by Remark
2.3, we have that $M\models\varphi$ for any
$\varphi\in\widetilde{{\mathtt{T}}}_{+}$. Hence,
$\widetilde{{\mathtt{T}}}_{+}\subseteq{\mathrm{Th}}_{+}(M)$, concluding that
${\mathtt{T}}\subseteq{\mathrm{Th}}_{-}(M)\subseteq\widetilde{{\mathtt{T}}}$.
By minimality of $\widetilde{{\mathtt{T}}}$, it follows that
$\widetilde{{\mathtt{T}}}={\mathrm{Th}}_{-}(M)$. ∎

######  Remark 3.13.

By Lemma 3.12, in particular, the weak completions of ${\mathtt{T}}$ are
exactly the minimal elements of
$\\{{\mathrm{Th}}_{-}(M):M\models^{\mathrm{pc}}{\mathtt{T}}\\}$.

######  Lemma 3.14.

Assume ${\mathtt{L}}$ is countable. Every negative local theory has a weak
completion.

###### Proof.

By Zorn’s Lemma, it is sufficient to show that if $\mathcal{T}$ is a (non-
empty) family of weakly complete negative local theories linearly ordered
under inclusion, then ${\mathtt{T}}=\bigcap\mathcal{T}$ is also a weakly
complete negative local theory. Certainly, ${\mathtt{T}}$ is locally
satisfiable, since any local model of any
${\mathtt{T}}^{\prime}\in\mathcal{T}$ is also a local model of ${\mathtt{T}}$.
It is also obviously closed under local implication. Indeed, if
${\mathtt{T}}\models\varphi$ for some negative sentence $\varphi$, then
${\mathtt{T}}^{\prime}\models\varphi$ for any
${\mathtt{T}}^{\prime}\in\mathcal{T}$, so $\varphi\in{\mathtt{T}}^{\prime}$
for all ${\mathtt{T}}^{\prime}\in\mathcal{T}$, concluding
$\varphi\in{\mathtt{T}}$.

Finally, by Theorem 3.11, it is enough to show that ${\mathtt{T}}$ is
irreducible. Suppose $\exists x\,\varphi(x)$ and $\exists y\,\psi(y)$ are in
${\mathtt{T}}_{+}$, with $\varphi(x)$ and $\psi(y)$ positive formulas and $x$
and $y$ disjoint variables on the same sort. Then, there are
${\mathtt{T}}^{\prime},{\mathtt{T}}^{\prime\prime}\in\mathcal{T}$ such that
$\exists x\,\varphi(x)\in{\mathtt{T}}^{\prime}_{+}$ and $\exists
y\,\psi(y)\in{\mathtt{T}}^{\prime\prime}_{+}$. Since $\mathcal{T}$ is linearly
ordered, we may assume ${\mathtt{T}}^{\prime}={\mathtt{T}}^{\prime\prime}$.
Since ${\mathtt{T}}^{\prime}$ is irreducible by Theorem 3.11, we conclude
$\exists x,y\,\varphi(x)\wedge\psi(y)\in{\mathtt{T}}^{\prime}_{+}$. Therefore,
since ${\mathtt{T}}\subseteq{\mathtt{T}}^{\prime}$, we get
${\mathtt{T}}^{\prime}_{+}\subseteq{\mathtt{T}}_{+}$, so $\exists
x,y\,\varphi(x)\wedge\psi(y)\in{\mathtt{T}}_{+}$ as required. ∎

######  Remark 3.15.

In uncountable languages, weak completions may not exist. In fact, consider
${\mathtt{T}}$ from Example 3.7(4) and consider for any $\alpha<\omega_{1}$
the theory ${\mathtt{T}}_{\alpha}$ defined the same way as ${\mathtt{T}}$ but
only allowing $P_{\beta}$ for $\beta<\alpha$. Then each
${\mathtt{T}}_{\alpha}$ is irreducible, and since it is effectively a theory
of a countable language it is weakly complete by Theorem 3.11.

Every weakly complete theory ${\mathtt{T}}^{\prime}$ containing ${\mathtt{T}}$
is by definition the theory of a model $M$ of ${\mathtt{T}}$, thus
$\\{\beta<\omega_{1}:\ \neg\exists
xP_{\beta}(x)\notin{\mathtt{T}}^{\prime}\\}$ is countable, thus has some bound
$\alpha<\omega_{1}$. We conclude that
${\mathtt{T}}_{\alpha+2}\subsetneq{\mathtt{T}}^{\prime}$ (since
$M\models{\mathtt{T}}_{\alpha+2}$) and thus a weak completion does not exist.

######  Lemma 3.16.

Let $N\models^{\mathrm{pc}}{\mathtt{T}}$ with ${\mathrm{Th}}_{-}(N)$ complete.
Then, ${\mathrm{Th}}_{-}(N)$ is a completion of ${\mathtt{T}}$ and maximal in
$\\{{\mathrm{Th}}_{-}(M):M\models^{\mathrm{pc}}{\mathtt{T}}\\}$.

###### Proof.

Let
${\mathtt{T}}\subseteq\widetilde{{\mathtt{T}}}\subseteq{\mathrm{Th}}_{-}(N)$
with $\widetilde{{\mathtt{T}}}$ a complete negative local theory. Then, as
$N\models\widetilde{{\mathtt{T}}}$ and $N\models^{\mathrm{pc}}{\mathtt{T}}$
with ${\mathtt{T}}\subseteq\widetilde{{\mathtt{T}}}$, it follows that
$N\models^{\mathrm{pc}}\widetilde{{\mathtt{T}}}$. Thus,
${\mathrm{Th}}_{-}(N)=\widetilde{{\mathtt{T}}}$ by completeness of
$\widetilde{{\mathtt{T}}}$.

Let $M\models^{\mathrm{pc}}{\mathtt{T}}$ with
${\mathrm{Th}}_{-}(N)\subseteq{\mathrm{Th}}_{-}(M)$. Then, as
$M\models{\mathrm{Th}}_{-}(N)$ and $M\models^{\mathrm{pc}}{\mathtt{T}}$ with
${\mathtt{T}}\subseteq{\mathrm{Th}}_{-}(N)$, it follows that
$M\models^{\mathrm{pc}}{\mathrm{Th}}_{-}(N)$, so
${\mathrm{Th}}_{-}(N)={\mathrm{Th}}_{-}(M)$ by completeness of
${\mathrm{Th}}_{-}(N)$. ∎

On the other hand, note that not every maximal element of
$\\{{\mathrm{Th}}_{-}(M):M\models^{\mathrm{pc}}{\mathtt{T}}\\}$ is necessarily
complete, as the following example shows.

######  Example 3.17.

Let ${\mathtt{L}}$ be the one-sorted language with unary relations
$\\{S\\}\cup\\{P_{n},Q_{n}\\}_{n\in\mathbb{N}}$ and locality relations
$\mathtt{D}=\\{d_{n}\\}_{n\in\mathbb{N}}$ (with the usual ordered monoid
structure induced by the natural numbers). Let $G=(V,E)$ be the graph with
vertices $V=\\{(v_{1},v_{2})\in\mathbb{N}\times\mathbb{Z}:|v_{1}|\leq
v_{2}\\}$ and edges $v\mathrel{E}w$ if and only if
$v_{2}=w_{2}\wedge|v_{1}-w_{1}|=1$ or $|v_{2}-w_{2}|=1\wedge v_{1}=w_{1}=0$.
In other words, $G$ is the tree made of paths $C_{m}=\\{v:v_{2}=m\\}$ of
length $2m+1$ and one path $\Gamma=\\{v:v_{1}=0\\}$ connecting all the paths
$C_{m}$ at the centre.

Construct from $G$ a structure $M$ with universe $V$ and interpretations

$P_{n}(v)\Leftrightarrow v_{1}\geq n,\ Q_{n}(v)\Leftrightarrow v_{2}\leq-n,\
S(v)\Leftrightarrow|v_{1}|=v_{2}$

and $M\models{\mathrm{d}}_{n}(v,w)\Leftrightarrow{\mathrm{d}}_{G}(v,w)\leq n$,
where ${\mathrm{d}}_{G}$ is the graph distance of $G$. Since $G$ is connected,
$M$ is a local structure, thus ${\mathtt{T}}={\mathrm{Th}}_{-}(M)$ is a weakly
complete local theory.

Let $Z$ be the structure with universe $\mathbb{Z}$ described in Example
3.7(1) considered as an ${\mathtt{L}}$-structure, i.e. $Z\models
P_{k}(n)\Leftrightarrow n\geq k$, $Z\models Q_{k}(n)\Leftrightarrow n\leq-k$,
$Z\models{\mathrm{d}}_{k}(n,m)\Leftrightarrow|n-m|\leq k$ and
$S(Z)=\emptyset$. Then, $Z\models{\mathtt{T}}$, since every finite
substructure of $Z$ is also a substructure of $M$ (contained in any long
enough $C_{n}$).

Let $I_{S}$ be the structure with a single element $\infty$ satisfying all
$P_{n}$ as well as $S$ and no $Q_{n}$. Let $J_{S}$ be the structure with a
single element $-\infty$ satisfying all $Q_{n}$ as well as $S$ and no $P_{n}$.
Both are local models of ${\mathtt{T}}$ since the types
$\\{S(x)\\}\cup\\{P_{n}(x)\\}_{n\in\mathbb{N}}$ and
$\\{S(x)\\}\cup\\{Q_{n}(x)\\}_{n\in\mathbb{N}}$ are finitely satisfiable in
$M$.

We claim that $M$, $Z$, $I_{S}$ and $J_{S}$ are all the local positively
closed models of ${\mathtt{T}}$. Indeed, say
$N\models^{\mathrm{pc}}{\mathtt{T}}$. Then, there are four cases: either
$N\models\neg\exists x\,Q_{0}(x)$, $N\models\neg\exists x\,P_{0}(x)$,
$N\models(\exists x\,P_{0}(x))\wedge(\exists x\,Q_{0}(x))\wedge(\neg\exists
x\,S(x))$ or $N\models(\exists x\,P_{0}(x))\wedge(\exists
x\,Q_{0}(x))\wedge(\exists x\,S(x))$. Since $M\models\forall x\,P_{0}(x)\vee
Q_{0}(x)$, we have ${\mathtt{T}}\models P_{0}\mathrel{\top}Q_{0}$ by Remark
2.15, so the four cases are exclusive.

Consider the case $N\models\neg\exists x\,Q_{0}(x)$. Since $M\models\forall
x\,Q_{n}(x)\rightarrow Q_{0}(x)$, we get ${\mathtt{T}}\models Q_{n}\leq Q_{0}$
by Remark 2.15, so $N\models\neg\exists x\,Q_{n}(x)$ for all $n\in\mathbb{N}$
by Lemma 2.14(1). Hence, the map $h\colon x\mapsto\infty$ from $N$ to $I_{S}$
is a homomorphism. As $N\models^{\mathrm{pc}}{\mathtt{T}}$, we get that it is
a positive embedding, so an isomorphism as it is surjective.

Note that this implies that $I_{S}\models^{\mathrm{pc}}{\mathtt{T}}$. Indeed,
let $f\colon I_{S}\to N$ be a homomorphism to
$N\models^{\mathrm{pc}}{\mathtt{T}}$, which exists by Theorem 2.7. We
obviously have that ${\mathtt{T}}\models\neg\exists
x,y\,{\mathrm{d}}_{n}(x,y)\wedge P_{n+1}(x)\wedge Q_{0}(y)$ for every
$n\in\mathbb{N}$. Therefore, as $N\models P_{n}(f(\infty))$ for every
$n\in\mathbb{N}$, we have that $N\models\neg\exists y\,Q_{0}(y)$. Thus, we
have the isomorphism $h\colon N\to I_{S}$ defined above. In fact, as
$|I_{S}|=1$, $h\circ f={\mathrm{id}}$, so $h$ is a retraction of $f$ and
$I_{S}$ is a retractor of ${\mathtt{T}}$ as defined in Definition 5.8.

Similarly, we conclude that $N\cong J_{S}$ for
$N\models^{\mathrm{pc}}{\mathtt{T}}$ with $N\models\neg\exists x\,P_{0}(x)$.
In particular, $J_{S}\models^{\mathrm{pc}}{\mathtt{T}}$. In fact, as above, we
get that $J_{S}$ is a retractor of ${\mathtt{T}}$ as defined in Definition
5.8.

Consider now the case $N\models\left(\exists
x\,P_{0}(x)\right)\wedge\left(\exists
x\,Q_{0}(x)\right)\wedge\left(\neg\exists x\,S(x)\right)$. By Remark 2.15,
${\mathtt{T}}\models P_{0}\mathrel{\top}Q_{1}$ and ${\mathtt{T}}\models
P_{0}\perp Q_{1}$, so we get $N\models\forall x\,P_{0}(x)\leftrightarrow\neg
Q_{1}(x)$ by Lemma 2.14(2). Consequently, we have the well-defined map
$h\colon N\to Z$ given by

$h(a)=\begin{cases}\phantom{-}\min\\{k:N\models\exists
y\,{\mathrm{d}}_{k}(a,y)\wedge Q_{0}(y)\\}&\mathrm{if\ }N\models P_{0}(a),\\\
-\min\\{k:N\models\exists y\,{\mathrm{d}}_{k}(a,y)\wedge
P_{0}(y)\\}&\mathrm{if\ }N\models Q_{1}(a).\end{cases}$

We claim that $h$ is an isomorphism. Indeed, this follows by essentially the
same argument as in Example 3.7(1).

Note that this implies that $Z\models^{\mathrm{pc}}{\mathtt{T}}$. Indeed, let
$f\colon Z\to N$ be a homomorphism to $N\models^{\mathrm{pc}}$, which exists
by Theorem 2.7. Since $Z\models\left(\exists
x\,P_{0}(x)\right)\wedge\left(\exists x\,Q_{0}(x)\right)$, we have that
$N\models\left(\exists x\,P_{0}(x)\right)\wedge\left(\exists
x\,Q_{0}(x)\right)$. It remains to show that $N\models\neg\exists x\,S(x)$.
Assume towards a contradiction that $N\models S(a)$ for some $a$ and pick $k$
such that $N\models{\mathrm{d}}_{k}(a,f(0))$.

First of all, note that $f(0)$ does not satisfy $S$, so $k\neq 0$. Indeed,
${\mathtt{T}}\models S(x)\perp P_{0}(x)\wedge Q_{0}(x)\wedge\exists
y\,P_{1}(y)\wedge{\mathrm{d}}_{1}(x,y)$ as the only element in $M$ satisfying
$S$, $P_{0}$ and $Q_{0}$ is $(0,0)$, whose ${\mathrm{d}}_{1}$-ball contains no
realisation of $P_{1}$ — it only contains $(0,0)$ and $(1,0)$. Now, $Z\models
P_{0}(0)\wedge Q_{0}(0)\wedge P_{1}(1)\wedge{\mathrm{d}}_{1}(0,1)$, so $f(0)$
must not satisfy $S$.

Now, for $k>0$,

${\mathtt{T}}\models S(x)\wedge\exists y\,{\mathrm{d}}_{k}(x,y)\wedge
P_{0}(y)\wedge Q_{0}(y)\perp\exists y\,P_{2k}(y)\wedge{\mathrm{d}}_{3k}(x,y).$

Indeed, in $M$, $M\models\exists y\,{\mathrm{d}}_{k}(v,y)\wedge P_{0}(y)\wedge
Q_{0}(y)\Leftrightarrow{\mathrm{d}}_{G}(v,\Gamma)=|v_{1}|\leq k$. Hence, we
have that $M\models S(v)\wedge\exists y\,{\mathrm{d}}_{k}(v,y)\wedge
P_{0}(y)\wedge Q_{0}(y)\Leftrightarrow v_{2}=|v_{1}|\leq k$. On the other
hand, if $w\in M$ satisfies $P_{2k}$, then $w_{2}\geq w_{1}\geq 2k$. Since
$v_{2}\leq k<2k\leq w_{2}$, we have that
${\mathrm{d}}_{G}(v,u)=|v_{1}|+|w_{2}-v_{2}|+|w_{1}|=v_{2}+w_{2}-v_{2}+w_{1}=w_{1}+w_{2}\geq
4k$, so $M\models\neg\exists x,y\,\phi_{k}(x)\wedge
P_{2k}(y)\wedge{\mathrm{d}}_{3k}(x,y)$. Now, $N\models
S(a)\wedge{\mathrm{d}}_{k}(a,f(0))\wedge{\mathrm{d}}_{3k}(a,f(2k))\wedge
P_{2k}(f(2k))$, contradicting $N\models{\mathtt{T}}$.

Hence, as $N\models\neg\exists x\,S(x)$, we have the isomorphism $h\colon N\to
Z$ described above. In fact, as $N\models P_{k}(f(k))\wedge\exists
y\,{\mathrm{d}}_{k}(f(k),y)\wedge Q_{0}(y)$, we get that $h\circ
f={\mathrm{id}}$, so $h$ is a retraction of $f$ and $Z$ is a retractor of
${\mathtt{T}}$ as defined in Definition 5.8.

Finally, consider the case $N\models\left(\exists
x\,P_{0}(x)\right)\wedge\left(\exists x\,Q_{0}(x)\right)\wedge\left(\exists
x\,S(x)\right)$. Since ${\mathtt{T}}\models P_{0}\mathrel{\top}Q_{1}$ and
${\mathtt{T}}\models P_{0}\perp Q_{1}$, we have that $N\models\forall
x\,P_{0}(x)\leftrightarrow\neg Q_{1}(x)$ by Lemma 2.14(1). Consequently, we
have the well-defined map $h=(h_{1},h_{2})\colon N\to M$ given by

$h_{1}(a)=\begin{cases}\phantom{-}\min\\{k:N\models\exists
y\,{\mathrm{d}}_{k}(a,y)\wedge Q_{0}(y)\\}&\mathrm{if\ }N\models P_{0}(a),\\\
-\min\\{k:N\models\exists y\,{\mathrm{d}}_{k}(a,y)\wedge
P_{0}(y)\\}&\mathrm{if\ }N\models Q_{1}(a);\end{cases}$

and

$h_{2}(a)=|h_{1}(a)|+\min\\{k:N\models\exists y\,{\mathrm{d}}_{k}(a,y)\wedge
S(y)\\}.$

We claim that $h$ is an isomorphism.

Indeed, recall ${\mathtt{T}}\models P_{n}\perp\exists
y\,{\mathrm{d}}_{k}(x,y)\wedge Q_{0}(y)$ for $k<n$. Thus, if $N\models
P_{n}(a)$, then $h_{1}(a)\geq n$, so $M\models P_{n}(h(a))$. Similarly, if
$N\models Q_{n}(a)$, then $h(a)\leq-n$, so $M\models Q_{n}(h(a))$. If
$N\models S(a)$, then $h_{2}(a)=|h_{1}(a)|$, so $M\models S(h(a))$.

Suppose $N\models{\mathrm{d}}_{n}(a,b)$ with $h(a)=v=(v_{1},v_{2})$ and
$h(b)=w=(w_{1},w_{2})$. Now, for $0\leq n\leq m$, consider the positive
formulas

$\phi_{n,m}(x)\coloneqq P_{n}(x)\wedge\left(\exists
y\,{\mathrm{d}}_{n}(x,y)\wedge Q_{0}(y)\right)\wedge\left(\exists
y\,{\mathrm{d}}_{m-n}(x,y)\wedge S(y)\wedge P_{m}(y)\right),$

and

$\phi_{-n,m}(x)\coloneqq Q_{n}(x)\wedge\left(\exists
y\,{\mathrm{d}}_{n}(x,y)\wedge P_{0}(y)\right)\wedge\left(\exists
y\,{\mathrm{d}}_{m-n}(x,y)\wedge S(y)\wedge Q_{m}(y)\right).$

Note that, in $M$, for $v\in M$, the unique element satisfying $\phi_{v}$ is
precisely $v$. Also, for $0\leq n\leq m$, consider the formulas

$\psi_{n,m}(v)\coloneqq P_{0}(v)\wedge\left(\exists
y\,{\mathrm{d}}_{n}(v,y)\wedge Q_{0}(y)\right)\wedge\left(\exists
y\,{\mathrm{d}}_{m-n}(v,y)\wedge S(y)\right)$

and

$\psi_{-n,m}(v)\coloneqq Q_{1}(v)\wedge\left(\exists
y\,{\mathrm{d}}_{n}(v,y)\wedge P_{0}(y)\right)\wedge\left(\exists
y\,{\mathrm{d}}_{m-n}(v,y)\wedge S(y)\right)$

Note that

$M\models\psi_{n,m}(v)\vee\psi_{-n,m}(v)\Leftrightarrow-n\leq v_{1}\leq n,\
v_{2}\leq m.$

Therefore,

$M\models\forall
x\,\psi_{n,m}(x)\vee\psi_{-n,m}(x)\leftrightarrow\bigvee_{\begin{subarray}{c}-n\leq
i\leq n\\\ \phantom{-}0\leq j\leq m\end{subarray}}\phi_{i,j}(x).$

Thus, by Remark 2.15,
${\mathtt{T}}\models\psi_{n,m}\vee\psi_{-n,m}\leq\bigvee\phi_{i,j}$ and
${\mathtt{T}}\models\bigvee\phi_{i,j}\leq\psi_{n,m}\vee\psi_{-n,m}$. Since
$h(a)=v=(v_{1},v_{2})$, we get that $N\models\psi_{v}(a)$ and
$N\not\models\psi_{n,m}(a)$ for $|n|\leq|v_{1}|$ or $m\leq v_{2}$. Hence, by
Lemma 2.14(1), $N\models\phi_{v}(a)$. Similarly, $N\models\phi_{w}(b)$. Now,
$M\models\neg\exists
x,y\,\phi_{v}(x)\wedge\phi_{w}(y)\wedge{\mathrm{d}}_{n}(x,y)$ for
$n<{\mathrm{d}}_{G}(v,w)$, so
${\mathtt{T}}\models\phi_{v}(x)\wedge\phi_{w}(y)\perp{\mathrm{d}}_{n}(x,y)$
for $n<{\mathrm{d}}_{G}(v,w)$, concluding that
$n\geq{\mathrm{d}}_{G}(h(a),h(b))$, so $M\models{\mathrm{d}}_{n}(h(a),h(b))$,
concluding that $h$ is a homomorphism.

As $N$ is local positively closed, we conclude that $h$ is a positive
embedding. Now, $M\models\exists x\,\phi_{v}(x)$ for all $v\in M$, so there is
$a\in N$ such that $N\models\phi_{v}(a)$. Thus, $M\models\phi_{v}(h(a))$ by
Remark 2.3. However, $v$ is the unique element in $M$ realising that formula,
so $h(a)=v$. In conclusion, $h$ is surjective, so an isomorphism.

Note that this implies $M\models^{\mathrm{pc}}{\mathtt{T}}$. Indeed, let
$f\colon M\to N$ be a homomorphism to $N\models^{\mathrm{pc}}{\mathtt{T}}$,
which exists by Theorem 2.7. Since $M\models\left(\exists
x\,P_{0}(x)\right)\wedge\left(\exists x\,Q_{0}(x)\right)\wedge\left(\exists
x\,S(x)\right)$, we have that $N\models\left(\exists
x\,P_{0}(x)\right)\wedge\left(\exists x\,Q_{0}(x)\right)\wedge\left(\exists
x\,S(x)\right)$ by Remark 2.3. Thus, we have the isomorphism $h\colon N\to M$
defined above. In fact, as $N\models\phi_{v}(f(v))$, we get that $h\circ
f={\mathrm{id}}$, so $h$ is a retraction of $f$ and $M$ is a retractor of
${\mathtt{T}}$ as defined in Definition 5.8.

Hence, we have that ${\mathrm{Th}}_{-}(Z)$ is maximal among the negative
theories of $\mathcal{M}^{\mathrm{pc}}({\mathtt{T}})$. However, as showed in
Example 3.7(1), ${\mathrm{Th}}_{-}(Z)$ is not complete. For instance,
${\mathrm{Th}}_{-}(Z)$ has three different local positively closed models,
which are $Z$, $I=\\{\infty\\}$ and $J=\\{-\infty\\}$, with $I\models
P_{k}(\infty)\wedge\neg Q_{k}(\infty)$ and $J\models Q_{k}(-\infty)\wedge\neg
P_{k}(-\infty)$ for all $k\in\mathbb{N}$, and $I\models\neg S(\infty)$ and
$J\models\neg S(-\infty)$.

######  Question 3.18.

Are there always completions? Is every completion of the form
${\mathrm{Th}}_{-}(M)$ for some $M\models^{\mathrm{pc}}{\mathtt{T}}$? Are
there always maximal elements in
$\\{{\mathrm{Th}}_{-}(M):M\models^{\mathrm{pc}}{\mathtt{T}}\\}$?

Trying to replicate the proof of Lemma 3.14 applying some variation of Zorn’s
Lemma to answer Question 3.18 is unlikely to work. The key issue is that, as
the following example shows, there are negative local theories ${\mathtt{T}}$
and chains of complete negative local theories containing ${\mathtt{T}}$
without a complete lower bound (containing ${\mathtt{T}})$.

######  Example 3.19.

Consider Example 3.7(1). Recall that
${\mathtt{L}}\coloneqq\\{P_{n},Q_{n},{\mathrm{d}}_{n}\\}_{n\in\mathbb{N}}$ and
${\mathtt{T}}\coloneqq{\mathrm{Th}}_{-}(Z)$ where $Z$ is the
${\mathtt{L}}$-structure with universe $\mathbb{Z}$ and interpretations
$Z\models P_{n}(x)\Leftrightarrow x>n$, $Z\models N_{n}(x)\Leftrightarrow
x<-n$ and $Z\models{\mathrm{d}}_{n}(x,y)\Leftrightarrow|x-y|\leq n$. For each
$n\in\mathbb{N}$, consider the substructure $C_{n}=[-n,n]\subseteq Z$ and the
negative local theory ${\mathtt{T}}_{n}\coloneqq{\mathrm{Th}}_{-}(C_{n})$.
Obviously, for each $n\in\mathbb{N}$, ${\mathtt{T}}_{n}$ is
${\mathrm{d}}_{2n}$-irreducible, so complete by Theorem 3.4. Since $C_{n}$
embeds into $C_{n+1}$ for each $n\in\mathbb{N}$, we get by Remark 2.3 that
${\mathtt{T}}_{n+1}\subseteq{\mathtt{T}}_{n}$. Since $Z$ is isomorphic to the
direct limit of all $C_{n}$ (with the natural inclusions), we get that
${\mathtt{T}}=\bigcap_{n\in\mathbb{N}}{\mathtt{T}}_{n}$ by Lemma 2.5. Thus,
there is no complete theory containing ${\mathtt{T}}$ and contained in
${\mathtt{T}}_{n}$ for all $n\in\mathbb{N}$.

##  4\. Local positive types

Recall that, unless otherwise stated, we have fixed a local language
${\mathtt{L}}$ and a locally satisfiable negative local theory ${\mathtt{T}}$.

######  Definition 4.1.

Let $x$ be a variable. A _partial local positive type on $x$ of
${\mathtt{T}}$_ is a subset
$\Gamma\subseteq{\mathrm{LFor}}^{x}_{+}({\mathtt{L}})$ such that $\Gamma$ is
_locally satisfiable_ in ${\mathtt{T}}$, i.e. there is a local model
$M\models{\mathtt{T}}$ and an element $a\in M^{x}$ such that
$M\models\Gamma(a)$. A _local positive type_ of ${\mathtt{T}}$ is a maximal
partial local positive type of ${\mathtt{T}}$. As usual, we omit $x$ if it is
clear from the context.

Let $M$ be a local ${\mathtt{L}}$-structure, $A$ a subset and $a\in M^{x}$.
The _partial local positive type_ of $a$ in $M$ over $A$ is the set

${\mathrm{ltp}}^{M}_{+}(a/A)\coloneqq\\{\varphi\in{\mathrm{LFor}}^{x}_{+}({\mathtt{L}}(A)):M\models\varphi(a)\\}.$

We omit $M$ if it is clear from the context, and we omit $A$ if $A=\emptyset$.

######  Remark 4.2.

It is a well known fact in positive logic that, in general,
${\mathrm{ltp}}^{M}_{+}(a)$ is not maximal. Indeed, suppose that there is a
homomorphism $h\colon M\to N$ such that $N\models\varphi(h(a))$ with
$\varphi\in{\mathrm{LFor}}_{+}({\mathtt{L}})$ while $M\not\models\varphi(a)$.
Then, ${\mathrm{ltp}}^{M}_{+}(a)\subsetneq{\mathrm{ltp}}^{N}_{+}(h(a))$.

######  Lemma 4.3.

Let $\Gamma\subseteq{\mathrm{LFor}}^{x}_{+}({\mathtt{L}})$ be a subset of
local positive formulas. Then, $\Gamma$ is a partial local positive type of
${\mathtt{T}}$ if and only if there are $M\models^{\mathrm{pc}}{\mathtt{T}}$
and $a\in M^{x}$ such that $M\models\Gamma(a)$.

###### Proof.

Suppose $\Gamma$ is a partial local positive type. By definition, $\Gamma$ is
locally satisfiable. Then, there is $N\models{\mathtt{T}}$ and $b\in N^{x}$
such that $N\models\Gamma(b)$. By Theorem 2.7, there is a homomorphism
$f\colon N\to M$ to $M\models^{\mathrm{pc}}{\mathtt{T}}$. Thus, by Remark 2.3,
we conclude that $M\models\Gamma(a)$ for $a=f(b)$, so $\Gamma$ is realised in
a local positively closed model of ${\mathtt{T}}$. ∎

######  Remark 4.4.

Using downwards Löwenheim-Skolem, we can take $|M|\leq|{\mathtt{L}}|+|x|$ in
Lemma 4.3.

######  Lemma 4.5.

Let $M\models{\mathtt{T}}$. Then, $M$ is a local positively closed model of
${\mathtt{T}}$ if and only if ${\mathrm{ltp}}^{M}_{+}(a)$ is a local positive
type of ${\mathtt{T}}$ for every pointed tuple $a$ in $M$.

###### Proof.

Suppose that ${\mathrm{ltp}}^{M}_{+}(c)$ is a local positive type of
${\mathtt{T}}$ for every pointed $c$ in $M$. Let $h\colon M\to N$ be a
homomorphism to a local model $N\models{\mathtt{T}}$. Suppose
$N\models\varphi(h(a))$ for some
$\varphi\in{\mathrm{For}}^{x}_{+}({\mathtt{L}})$ and $a\in M^{x}$. We want to
show that $M\models\varphi(a)$.

Without loss of generality, $\varphi(x)=\exists y\,\phi(x,y)$ where
$\phi(x,y)\in{\mathrm{For}}_{{\mathrm{qf}}_{+}}({\mathtt{L}})$. Then,
$N\models\phi(a,c)$ for some $c\in N^{y}$. Take $b\in M^{y}$ arbitrary and
extend $ab$ to a pointed $a^{\prime}$ arbitrarily. As $N$ is a local model, we
have that $N\models{\mathrm{d}}(c,h(b))$ for some locality relation symbol
${\mathrm{d}}$. Consider $\varphi^{\prime}(x,y)=\exists
z{\in}{\mathrm{d}}(y)\,\phi(x,z)\in{\mathrm{LFor}}^{x,y}_{+}({\mathtt{L}})$
where $z$ is of the same sort as $y$. Then, we have that
$N\models\varphi^{\prime}(h(a,b))$, so
$\varphi^{\prime}(x,y)\in{\mathrm{ltp}}^{N}_{+}(h(a^{\prime}))$.

By Remark 2.3,
${\mathrm{ltp}}^{M}_{+}(a^{\prime})\subseteq{\mathrm{ltp}}^{N}_{+}(h(a^{\prime}))$.
As ${\mathrm{ltp}}^{M}_{+}(a^{\prime})$ is maximal among partial local
positive types of ${\mathtt{T}}$, it follows that
${\mathrm{ltp}}^{M}_{+}(a,b)={\mathrm{ltp}}^{N}_{+}(h(a,b))$, so we get
$M\models\varphi^{\prime}(a,b)$. In particular, $M\models\phi(a,c^{\prime})$
for some $c^{\prime}$ in $M$, so $M\models\varphi(a)$. Since $a$, $h$, $N$ and
$\varphi$ are arbitrary, we conclude that $M$ is a local positively closed
model of ${\mathtt{T}}$.

On the other hand, suppose $M$ is a local positively closed model and $a\in
M^{x}$ pointed. Take $\varphi\in{\mathrm{LFor}}^{x}_{+}({\mathtt{L}})$ such
that $M\not\models\varphi(a)$. By Lemma 2.12, we have $M\models\psi(a)$ for
some $\psi\in{\mathrm{LFor}}^{x}_{+}({\mathtt{L}})$ such that
${\mathtt{T}}\models\psi\perp\varphi$. Thus, there is
$\psi\in{\mathrm{ltp}}^{M}_{+}(a)$ such that $\\{\varphi,\psi\\}$ is not
locally satisfiable in ${\mathtt{T}}$. In other words,
${\mathrm{ltp}}^{M}_{+}(a)\wedge\varphi$ is not locally satisfiable in
${\mathtt{T}}$. As $\varphi$ is arbitrary, we conclude that
${\mathrm{ltp}}^{M}_{+}(a)$ is a local positive type of ${\mathtt{T}}$. ∎

######  Corollary 4.6.

Let $x$ be a pointed variable and
$\Gamma\subseteq{\mathrm{LFor}}^{x}_{+}({\mathtt{L}})$ a subset of local
positive formulas. Then, $\Gamma$ is a local positive type of ${\mathtt{T}}$
if and only if $\Gamma={\mathrm{ltp}}^{M}_{+}(a)$ for some
$M\models^{\mathrm{pc}}{\mathtt{T}}$ and $a\in M^{x}$.

As an immediate consequence of Theorems 2.7 and 4.6, we can show that every
partial local positive type on a pointed variable extends to a local positive
type. Naturally, the same is still true for arbitrary variables, but we
require an alternative argument relying on the notion of _bounded
satisfiability_. As Lemma 4.9 shows, this notion is the right replacement of
finite satisfiability in local logic. In particular, boundedness is the
necessary condition to apply compactness in local logic.

######  Definition 4.7.

A subset of formulas $\Gamma(x)\subseteq{\mathrm{For}}^{x}({\mathtt{L}})$ is
_boundedly satisfiable_ in ${\mathtt{T}}$ if there is a bound $\mathrm{B}(x)$
(recall Definition 3.8) such that $\Gamma(x)\wedge\mathrm{B}(x)$ is finitely
locally satisfiable in ${\mathtt{T}}$. In that case, we say that $\mathrm{B}$
is a _feasible bound_ for $\Gamma$.

######  Remark 4.8.

If $\Gamma\models\mathrm{B}$ for some bound $\mathrm{B}$. Then, $\Gamma$ is
boundedly satisfiable if and only if it is finitely locally satisfiable.

######  Lemma 4.9.

Let $\Gamma$ be a subset of $\Pi_{1}$-local formulas of ${\mathtt{L}}$. Then,
$\Gamma$ is locally satisfiable in ${\mathtt{T}}$ if and only if it is
boundedly satisfiable in ${\mathtt{T}}$.

###### Proof.

Obviously, if $\Gamma$ is locally satisfiable, then it is boundedly
satisfiable as any $a$ realising $\Gamma$ gives us a feasible bound for
$\Gamma$. On the other hand, suppose that $\Gamma(x)$ is boundedly
satisfiable. Pick a feasible bound $\mathrm{B}(x)$ for $\Gamma(x)$. Let
${\mathtt{L}}(\underline{x})$ be the expansion of ${\mathtt{L}}$ given by
adding new constant symbols for each variable in $x$: we take
$\mathtt{B}_{\underline{x}_{i},c_{i}}$ and
$\mathtt{B}_{\,\underline{x}_{i},\underline{x}_{j}}$ according to $\mathrm{B}$
— for any other constant $c^{\prime}$ in ${\mathtt{L}}(\underline{x})$, we
define $\mathtt{B}_{\underline{x}_{i},c^{\prime}}$ via $\preceq$. Now,
consider $\widetilde{{\mathtt{T}}}={\mathtt{T}}\wedge\Gamma(\underline{x})$.
By hypothesis, $\widetilde{{\mathtt{T}}}$ is finitely locally satisfiable.
Thus, by Theorem 1.9, there is a local ${\mathtt{L}}(\underline{x})$-structure
$M_{\underline{x}}$ satisfying $\widetilde{{\mathtt{T}}}$. Hence, the
respective ${\mathtt{L}}$-reduct $M$ is a local model of ${\mathtt{T}}$
realising $\Gamma$. ∎

######  Corollary 4.10.

Let $\Gamma\subseteq{\mathrm{LFor}}^{x}_{+}({\mathtt{L}})$ be a partial local
positive type of ${\mathtt{T}}$. Then, there is a local positive type
extending $\Gamma$.

###### Proof.

As $\Gamma$ is boundedly satisfiable, pick any feasible bound $\mathrm{B}(x)$.
Take $\Gamma^{\prime}(x)=\Gamma(x)\wedge\mathrm{B}(x)$. Now, consider
$\mathcal{K}=\\{\Sigma\subseteq{\mathrm{LFor}}^{x}_{+}({\mathtt{L}}):\Gamma^{\prime}\subseteq\Sigma$
finitely locally satisfiable in ${\mathtt{T}}\\}$, which is partially ordered
by $\subseteq$. For any $\Omega\subseteq\mathcal{K}$ chain, $\bigcup\Omega$ is
a bound in $\mathcal{K}$. Indeed, for any $\Lambda\subseteq\bigcup\Omega$
finite, there is $\Sigma\in\Omega$ such that $\Lambda\subseteq\Sigma$, so
$\bigcup\Omega$ is finitely locally satisfiable, so
$\bigcup\Omega\in\mathcal{K}$. By Zorn’s Lemma, there is a maximal element
$p\in\mathcal{K}$. We know that $\Gamma\subseteq p$ and $p$ is boundedly
satisfiable. On the other hand, if $p\subseteq\Sigma$ with $\Sigma$ boundedly
satisfiable, then $\Sigma\in\mathcal{K}$ and, by maximality of $p$,
$\Sigma=p$. Hence, $p$ is a local positive type extending $\Gamma$. ∎

In general, we consider only partial local positive types, as local
compactness only applies to this kind of formulas (Theorem 1.9). However, when
we consider pointed variables, we can instead deal with partial positive
types.

######  Lemma 4.11.

Let $M$ be a local ${\mathtt{L}}$-structure. Let $x$ be a pointed variable and
$a,b\in M^{x}$. Then,
${\mathrm{ltp}}^{M}_{+}(a)\subseteq{\mathrm{ltp}}^{M}_{+}(b)$ if and only if
${\mathrm{tp}}^{M}_{+}(a)\subseteq{\mathrm{tp}}^{M}_{+}(b)$.

###### Proof.

Obviously, ${\mathrm{tp}}_{+}(a)\subseteq{\mathrm{tp}}_{+}(b)$ implies
${\mathrm{ltp}}_{+}(a)\subseteq{\mathrm{ltp}}_{+}(b)$. Conversely, assume
${\mathrm{ltp}}_{+}(a)\subseteq{\mathrm{ltp}}_{+}(b)$. Take
$\varphi(x)\in{\mathrm{For}}^{x}_{+}({\mathtt{L}})$. Without loss of
generality, $\varphi(x)=\exists y\,\phi(x,y)$ with $\phi$ quantifier-free
positive. Suppose $M\models\varphi(a)$. Then, there is $c$ such that
$M\models\phi(a,c)$. As $a$ is pointed, we can find a term $t(a)$ on the sort
of $c$. As $M$ is a local structure, there is a locality relation
${\mathrm{d}}$ with ${\mathrm{d}}(t(a),c)$. Thus,
$M\models\varphi^{\prime}(a)$ where $\varphi^{\prime}(x)=\exists
y{\in}{\mathrm{d}}(t(x))\,\phi(x,y)\in{\mathrm{LFor}}^{x}_{+}({\mathtt{L}})$.
As ${\mathrm{ltp}}_{+}(a)\subseteq{\mathrm{ltp}}_{+}(b)$, we conclude that
$\models\varphi^{\prime}(b)$ too. Since $\varphi$ is arbitrary, we conclude
that ${\mathrm{tp}}_{+}(a)\subseteq{\mathrm{tp}}_{+}(b)$.∎

######  Definition 4.12.

Let $M$ be a local ${\mathtt{L}}$-structure and $A$ a subset. A _(partial)
local positive type of $M$ over $A$_ is a (partial) local positive type of
${\mathrm{Th}}_{-}(M/A)$.

######  Lemma 4.13.

Let $M$ be a local ${\mathtt{L}}$-structure and $A$ a subset. Let
$\Gamma\subseteq{\mathrm{LFor}}^{x}_{+}({\mathtt{L}}(A))$ be a subset of local
positive formulas with parameters in $A$. Assume $M$ has the local joint
property over $A$. Then, $\Gamma$ is a partial local positive type of $M$ over
$A$ if and only if there is an ${\mathtt{L}}(A)$-homomorphism $f\colon
M_{A}\to N_{A}$ to $N_{A}\models^{\mathrm{pc}}{\mathrm{Th}}_{-}(M/A)$
realising $\Gamma$. Furthermore, suppose $x$ is pointed over
${\mathtt{L}}(A)$. Then, $\Gamma(x)$ is a local positive type of $M$ over $A$
if and only if there is an ${\mathtt{L}}(A)$-homomorphism $f\colon M_{A}\to
N_{A}$ to some $N_{A}\models^{\mathrm{pc}}{\mathrm{Th}}_{-}(M/A)$ such that
$\Gamma={\mathrm{ltp}}^{N_{A}}_{+}(a/A)$ for some $a\in N^{x}$.

###### Proof.

If there is an ${\mathtt{L}}(A)$-homomorphism to a local positively closed
model of ${\mathrm{Th}}_{-}(M/A)$ realising $\Gamma$, then $\Gamma$ is
obviously a partial local positive type over $A$. On the other hand, suppose
$\Gamma$ is a partial local positive type over $A$. By Lemma 4.3, there are
$N^{\prime}_{A}\models^{\mathrm{pc}}{\mathrm{Th}}_{-}(M/A)$ and
$b\in{N^{\prime}}^{x}_{A}$ such that $N^{\prime}_{A}\models\Gamma(b)$. By
assumption, ${\mathrm{Th}}_{-}(M/A)$ satisfies the local joint property, so
there are ${\mathtt{L}}(A)$-homomorphisms $h_{0}\colon N^{\prime}_{A}\to
N^{\prime\prime}_{A}$ and $h_{1}\colon M_{A}\to N^{\prime\prime}_{A}$ to a
common local model $N^{\prime\prime}_{A}\models{\mathrm{Th}}_{-}(M/A)$. By
Theorem 2.7, there is an ${\mathtt{L}}(A)$-homomorphism $f^{\prime}\colon
N^{\prime\prime}_{A}\to N_{A}$ to
$N_{A}\models^{\mathrm{pc}}{\mathrm{Th}}_{-}(M/A)$, so $f=f^{\prime}\circ
h_{1}\colon M_{A}\to N_{A}$ is an ${\mathtt{L}}(A)$-homomorphism with
$N_{A}\models^{\mathrm{pc}}{\mathrm{Th}}_{-}(M/A)$. By Remark 2.3, we have
that $N_{A}\models\Gamma(a)$ with $a=f^{\prime}\circ h_{0}(b)$, so it realises
$\Gamma$.

Finally, if $\Gamma$ is a local positive type of $M$ over $A$, then
$\Gamma={\mathrm{ltp}}^{N}_{+}(a/A)$ by maximality. On the other hand, by
Lemma 4.5, ${\mathrm{ltp}}^{N}_{+}(a/A)$ is a local positive type of
${\mathrm{Th}}_{-}(M/A)$ for any
$N_{A}\models^{\mathrm{pc}}{\mathrm{Th}}_{-}(M/A)$ and $a\in N^{x}_{A}$
whenever $x$ is pointed. ∎

######  Remark 4.14.

Applying downwards Löwenheim-Skolem repeatedly we can take
$|N|\leq|{\mathtt{L}}|+|M|+|x|$ in Lemma 4.13.

It should be noted that, contrary to what happens in usual positive logic,
local positive types might not be preserved under adding parameters.
Explicitly, a partial local positive type of $M$ over $A$ is not necessarily a
partial local positive type of $M$ over $B$ for $A\subseteq B$. The key issue
is that a bound over $A$ is not generally a bound over $B$. For instance,
consider Example 3.7(1). Recall that
${\mathtt{L}}\coloneqq\\{P_{n},Q_{n},{\mathrm{d}}_{n}\\}_{n\in\mathbb{N}}$ and
${\mathtt{T}}\coloneqq{\mathrm{Th}}_{-}(\mathbb{Z})$ where $\mathbb{Z}\models
P_{n}(x)\Leftrightarrow x>n$, $\mathbb{Z}\models Q_{n}(x)\Leftrightarrow x<-n$
and $\mathbb{Z}\models{\mathrm{d}}_{n}(x,y)\Leftrightarrow|x-y|\leq n$. Then,
$\bigwedge_{n\in\mathbb{N}}P_{n}(x)$ is a partial local positive type over
$\emptyset$ but it is not a partial local positive type over $0$. Of course,
such a counterexample cannot be given when $A$ is pointed:

######  Lemma 4.15.

Let $M$ be a local ${\mathtt{L}}$-structure and $A$ a pointed subset. Let
$A\subseteq B$. Then, every partial local positive type of $M$ over $A$ is a
partial local positive type of $M$ over $B$.

###### Proof.

Let $\Gamma(x)$ be a partial local positive type of $M$ over $A$. By Lemma
4.9, $\Gamma(x)$ is boundedly satisfiable over $A$. Pick a feasible bound
$\mathrm{B}(x)$ of $x$ over $A$ for $\Gamma$. Since $A$ is pointed,
$\mathrm{B}(x)$ is also a bound over $B$. Hence, $\Gamma(x)$ is boundedly
satisfiable over $B$ with feasible bound $\mathrm{B}$, so a partial local
positive type over $B$ by Lemma 4.9. ∎

It is natural to wonder if we can relax the pointedness hypothesis in the
previous lemma. The following example shows that assuming the local joint
property is not enough:

######  Example 4.16.

Consider the language ${\mathtt{L}}$ with two sorts $\mathtt{S}=\\{1,2\\}$,
locality relations
$\mathtt{D}^{s}=\\{{\mathrm{d}}^{s}_{q}:q\in\mathbb{Q}_{\geq 0}\\}$ for each
$s\in\mathtt{S}$ (and the usual ordered monoid structure induced by the
positive rationals), and one binary relation $P$ of sort $(1,2)$. Let $R$ be
the local ${\mathtt{L}}$-structure with universes two copies of the positive
reals, $\mathbb{R}_{\geq 0}^{1},\mathbb{R}_{\geq 0}^{2}$, and interpretations
$R\models{\mathrm{d}}^{s}_{q}(x,y)\Leftrightarrow|x-y|\leq q$ and $R\models
P(x,y)\Leftrightarrow x\neq 0\wedge y>\nicefrac{{1}}{{x}}$. Consider the sets
of parameters $A=\\{0^{1}\\}$ and $B=\\{0^{1},0^{2}\\}$ and the partial local
positive type $p(x,y)=\bigwedge_{q>0}{\mathrm{d}}^{1}_{q}(x,0^{1})\wedge
P(x,y)$, where $0^{s}$ is the zero of sort $s$. We claim that $R$ has the
local joint property over $A$ and $p$ is a partial local positive type over
$A$, but it is not a partial local positive type over $B$.

Now, let $\widetilde{R}$ be an $\aleph_{1}$-saturated elementary extension of
$R$. Since $p(x,y)$ is finitely satisfiable, we find $\varepsilon^{1}$ of sort
$1$ and $\infty^{2}$ of sort $2$ in $\widetilde{R}$ realising $p$. Consider
the substructure $I$ of $\widetilde{R}$ with universe
$I^{1}=\\{\varepsilon^{1},0^{1}\\}$ and $I^{2}=\\{\infty^{2}\\}$. We get that
$I\models{\mathrm{Th}}_{-}(R/A)$. Now, for any
$M\models{\mathrm{Th}}_{-}(R/A)$, consider $f\colon M\rightarrow I$ given by
$f\colon 0^{1}\to 0^{1}$, $f\colon a\mapsto\varepsilon^{1}$ for all $a\in
M^{1}$ with $a\neq 0^{1}$, and $f\colon a\mapsto\infty^{2}$ for all $a\in
M^{2}$. Trivially, $f$ is a homomorphism. Therefore, ${\mathrm{Th}}_{-}(R/A)$
has the local joint property. Also, we just show that $p(x,y)$ is locally
satisfiable over $A$.

Now, $R\models\neg\exists x\,{\mathrm{d}}_{\nicefrac{{1}}{{n}}}(x,0^{1})\wedge
P(x,y)\wedge{\mathrm{d}}_{n}(y,0^{2})$ for all $n\in\mathbb{N}$. Therefore,
${\mathrm{Th}}_{-}(R/B)\models{\mathrm{d}}_{\nicefrac{{1}}{{n}}}(x,0^{1})\wedge
P(x,y)\perp{\mathrm{d}}_{n}(y,0^{2})$. Hence, $p(x,y)$ is not boundedly
satisfiable over $B$, so it is not a partial local positive type over $B$.

######  Definition 4.17.

The _space of local positive types_
${\mathbf{S}}^{x}_{{\mathrm{loc}}+}({\mathtt{T}}/{\mathtt{L}})$ of
${\mathtt{T}}$ on $x$ over ${\mathtt{L}}$ is the set of local positive types
of ${\mathtt{T}}$ on $x$ over ${\mathtt{L}}$; the _space of local positive
types_ ${\mathbf{S}}_{{\mathrm{loc}}+}({\mathtt{T}}/{\mathtt{L}})$ is the
respective sorted set. We omit ${\mathtt{L}}$ if it is clear from the context.

Let $\Gamma\subseteq{\mathrm{LFor}}^{x}_{+}({\mathtt{L}})$ be a subset of
local positive formulas. The _interpretation_ of $\Gamma$ in
${\mathbf{S}}^{x}_{{\mathrm{loc}}+}({\mathtt{T}}/{\mathtt{L}})$ is the set

$\langle\Gamma(x)\rangle_{{\mathbf{S}}_{{\mathrm{loc}}+}({\mathtt{T}}/{\mathtt{L}})}\coloneqq\\{p\in{\mathbf{S}}^{x}_{{\mathrm{loc}}+}({\mathtt{T}}/{\mathtt{L}}):\Gamma\subseteq
p\\}$

As usual, we omit ${\mathtt{L}}$ and $x$ if they are clear from the context.

The _local positive logic topology_ of
${\mathbf{S}}^{x}_{{\mathrm{loc}}+}({\mathtt{T}})$ is the topology defined by
taking $\langle\Gamma\rangle$ as closed for every
$\Gamma\subseteq{\mathrm{LFor}}^{x}_{+}({\mathtt{L}})$ — we may need to add
$\emptyset$ as closed.

######  Lemma 4.18.

Let $x$ be a variable. The local positive logic topology of
${\mathbf{S}}^{x}_{{\mathrm{loc}}+}({\mathtt{T}})$ is a well-defined topology.

###### Proof.

By Corollary 4.10, there is a local positive type extending $x=x$, so
${\mathbf{S}}^{x}_{{\mathrm{loc}}+}({\mathtt{T}})\neq\emptyset$. Obviously,
$\langle x=x\rangle={\mathbf{S}}^{x}_{{\mathrm{loc}}+}({\mathtt{T}})$, so it
is closed. By hypothesis, $\emptyset$ is closed.

Let $\\{\Gamma_{i}\\}_{i\in I}$ be a family of local positive formulas. Then,
$\bigcap\langle\Gamma_{i}\rangle=\langle\bigwedge\Gamma_{i}\rangle$, so
arbitrary intersection of closed subsets are closed.

Let $\Gamma_{1},\Gamma_{2}\subseteq{\mathrm{LFor}}^{x}_{+}({\mathtt{L}})$ and
write
$\Gamma_{1}\vee\Gamma_{2}\coloneqq\\{\varphi_{1}\vee\varphi_{2}:\varphi_{1}\in\Gamma_{1},\
\varphi_{2}\in\Gamma_{2}\\}$. Then,
$\langle\Gamma_{1}\vee\Gamma_{2}\rangle=\langle\Gamma_{1}\rangle\cup\langle\Gamma_{2}\rangle$.
Indeed, trivially
$\langle\Gamma_{1}\rangle\cup\langle\Gamma_{2}\rangle\subseteq\langle\Gamma_{1}\vee\Gamma_{2}\rangle$.
On the other hand, suppose
$p\notin\langle\Gamma_{1}\rangle\cup\langle\Gamma_{2}\rangle$. Then, there are
$\varphi_{1}\in\Gamma_{1}$ and $\varphi_{2}\in\Gamma_{2}$ such that
$\varphi_{1}\notin p$ and $\varphi_{2}\notin p$. By Lemma 4.3, take
$M\models^{\mathrm{pc}}{\mathtt{T}}$ an $a\in M^{x}$ such that
${\mathrm{ltp}}^{M}_{+}(a)=p$. As $M\not\models\varphi_{1}(a)$ and
$M\not\models\varphi_{2}(a)$, we conclude that
$\varphi_{1}\vee\varphi_{2}\notin p$, so
$p\notin\langle\Gamma_{1}\vee\Gamma_{2}\rangle$. ∎

######  Remark 4.19.

Note that the local positive logic topology is tautologically a
$\mathrm{T}_{1}$ topology (i.e. Fréchet). Indeed, for every local positive
type $p$, we have that $\langle p\rangle$ is closed and only contains $p$.

As we have already noted, compactness is not true in general for local logic.
In particular, ${\mathbf{S}}_{{\mathrm{loc}}+}({\mathtt{T}})$ is not
necessarily compact. However, compactness is true under boundedness.

######  Lemma 4.20.

Every bound of $x$ is a compact subset of
${\mathbf{S}}^{x}_{{\mathrm{loc}}+}({\mathtt{T}})$.

###### Proof.

Let $\mathrm{B}(x)$ be a bound of $x$ in ${\mathtt{T}}$. We claim that
$\langle\mathrm{B}(x)\rangle$ is a compact subset of
${\mathbf{S}}^{x}_{{\mathrm{loc}}+}({\mathtt{T}})$. Let
$\\{\Gamma_{i}(x)\\}_{i\in I}$ be any family of partial local positive types
of ${\mathtt{T}}$ and suppose that $\bigcap_{i\in
I_{0}}\langle\Gamma_{i}(x)\rangle\cap\langle\mathrm{B}(x)\rangle$ is not empty
for every $I_{0}\subseteq I$ finite. Consider
$\Gamma(x)=\bigwedge\Gamma_{i}(x)\wedge\mathrm{B}(x)$. Then, $\Gamma$ is
finitely locally satisfiable in ${\mathtt{T}}$ and $\Gamma\models\mathrm{B}$.
Therefore, by Lemma 4.9, $\Gamma$ is locally satisfiable in ${\mathtt{T}}$. By
Corollary 4.10, we conclude that there is
$p\in\langle\Gamma\rangle=\bigcap\langle\Gamma_{i}\rangle\cap\langle\mathrm{B}\rangle$.
As $\\{\Gamma_{i}\\}_{i\in I}$ is arbitrary, we conclude that
$\langle\mathrm{B}\rangle$ is compact. ∎

######  Definition 4.21.

We say that ${\mathtt{T}}$ is _Hausdorff_ if
${\mathbf{S}}_{{\mathrm{loc}}+}({\mathtt{T}})$ is Hausdorff with the local
positive logic topology.

######  Lemma 4.22.

${\mathtt{T}}$ is Hausdorff if and only if, for any two different local
positive types $p(x)$ and $q(x)$ on the same variable, there are local
positive formulas $\varphi(x)$ and $\psi(x)$ with $\varphi\notin p$,
$\psi\notin q$ and $\varphi\mathrel{\top}\psi$.

###### Proof.

Suppose ${\mathtt{T}}$ is Hausdorff and let $p(x)$ and $q(x)$ be two different
local positive types on the same variable. Thus, as
${\mathbf{S}}^{x}_{{\mathrm{loc}}+}({\mathtt{T}})$ is Hausdorff, there are
$\Gamma_{1},\Gamma_{2}\subseteq{\mathrm{LFor}}^{x}_{+}({\mathtt{L}})$ such
that
$\langle\Gamma_{1}\vee\Gamma_{2}\rangle=\langle\Gamma_{1}\rangle\cup\langle\Gamma_{2}\rangle={\mathbf{S}}^{x}_{{\mathrm{loc}}+}({\mathtt{T}})$
and $p\notin\langle\Gamma_{1}\rangle$ and $q\notin\langle\Gamma_{2}\rangle$.
Thus, there are $\varphi\in\Gamma_{1}$ and $\psi\in\Gamma_{2}$ such that
$\varphi\notin p$ and $\psi\notin q$. As
$\langle\Gamma_{1}\vee\Gamma_{2}\rangle={\mathbf{S}}^{x}_{{\mathrm{loc}}+}({\mathtt{T}})$,
we have that
$\langle\varphi\vee\psi\rangle={\mathbf{S}}^{x}_{{\mathrm{loc}}+}({\mathtt{T}})$.
Thus, for any $M\models^{\mathrm{pc}}{\mathtt{T}}$ and any $a\in M^{x}$, we
have that $\varphi\vee\psi\in{\mathrm{ltp}}_{+}(a)$. In other words,
${\mathtt{T}}\models^{\mathrm{pc}}\forall x\,\varphi\vee\psi$, i.e.
$\varphi\mathrel{\top}\psi$.

On the other hand, suppose that for any two different local positive types
$p(x)$ and $q(x)$ on the same variable there are
$\varphi,\psi\in{\mathrm{LFor}}^{x}_{+}({\mathtt{L}})$ such that
$\varphi\notin p$, $\psi\notin q$ and $\varphi\mathrel{\top}\psi$. Then,
$\langle\varphi\rangle\cup\langle\psi\rangle=\langle\varphi\vee\psi\rangle={\mathbf{S}}^{x}_{{\mathrm{loc}}+}({\mathtt{T}})$,
so $\langle\varphi\rangle^{c}$ and $\langle\psi\rangle^{c}$ are open disjoint
subsets of ${\mathbf{S}}^{x}_{{\mathrm{loc}}+}({\mathtt{T}})$ separating $p$
and $q$. ∎

Let $x$ and $y$ be two variables. Recall that a _substitution_ of $x$ by $y$
is a function $\zeta\colon x\to y$ such that $x_{i}$ and $\zeta(x_{i})$ have
the same sort for any $x_{i}\in x$. Given a formula $\varphi$, we write
$\zeta_{*}(\varphi)$ for the formula recursively defined by replacing in
$\varphi$ every free instance of $x_{i}$ by a free instance of $\zeta(x_{i})$
for each $x_{i}\in x$ at the same time.

In positive logic, a key notion alternative to Hausdorffness is semi-
Hausdorffness. The definition of semi-Hausdorffness depends on the fact that
pull-backs by substitutions of variables are well-defined continuous maps
between the spaces of types. Unfortunately, in local positive logic, for non
pointed variables, the pull-back of a local positive type by a substitution of
variables is not necessarily maximal, i.e. it may be only a partial local
positive type. Therefore, for non pointed variables, pull-backs by
substitutions of variables are not necessarily well-defined maps between
spaces of types. In particular, the definition of semi-Hausdorffness only
makes sense for pointed variables.

######  Lemma 4.23.

Let $x$ and $y$ be pointed variables and $\zeta$ a substitution of $x$ by $y$.
Then:

  1. (1)

$\zeta^{*}\coloneqq{\mathrm{Im}}^{-1}\zeta_{*}\colon{\mathbf{S}}^{y}_{{\mathrm{loc}}+}({\mathtt{T}})\to{\mathbf{S}}^{x}_{{\mathrm{loc}}+}({\mathtt{T}})$
is a well-defined function. Furthermore, for any $M\models{\mathtt{T}}$ and
$a\in M^{y}$, we have
$\zeta^{*}{\mathrm{ltp}}_{+}(a)={\mathrm{ltp}}_{+}(\zeta^{*}a)$.

  2. (2)

${\mathrm{Im}}^{-1}\zeta^{*}(\langle\Gamma\rangle)=\langle{\mathrm{Im}}\,\zeta_{*}(\Gamma)\rangle$
for any $\Gamma\subseteq{\mathrm{LFor}}^{x}_{+}({\mathtt{L}})$.

###### Proof.

  1. First of all, recall that $\mathrel{\mathord{\models}_{\star}}\zeta_{*}\varphi(a)$ if and only if $\mathrel{\mathord{\models}_{\star}}\varphi(\zeta^{*}a)$. Thus, $\zeta_{*}\varphi\in{\mathrm{ltp}}_{+}(a)$ if and only if $\varphi\in{\mathrm{ltp}}_{+}(\zeta^{*}a)$ for any $\varphi\in{\mathrm{LFor}}^{x}_{+}({\mathtt{L}})$, $M\models{\mathtt{T}}$ and $a\in M^{y}$. In other words, $\zeta^{*}{\mathrm{ltp}}_{+}(a)={\mathrm{ltp}}_{+}(\zeta^{*}a)$. In particular, by Corollary 4.6, $\zeta^{*}\colon{\mathbf{S}}^{y}_{{\mathrm{loc}}+}({\mathtt{T}})\to{\mathbf{S}}^{x}_{{\mathrm{loc}}+}({\mathtt{T}})$ is a well-defined function.

  2. (2)

${\mathrm{Im}}^{-1}\zeta^{*}(\langle\Gamma\rangle)=\\{q\in{\mathbf{S}}^{y}_{{\mathrm{loc}}+}({\mathtt{T}}):\zeta^{*}(q)\in\langle\Gamma\rangle\\}=\\{q\in{\mathbf{S}}^{y}_{{\mathrm{loc}}+}({\mathtt{T}}):\Gamma\subseteq{\mathrm{Im}}^{-1}\zeta_{*}(q)\\}=\\{q\in{\mathbf{S}}^{y}_{{\mathrm{loc}}+}({\mathtt{T}}):{\mathrm{Im}}\,\zeta_{*}(\Gamma)\subseteq
q\\}=\langle{\mathrm{Im}}\,\zeta_{*}(\Gamma)\rangle.$ ∎

######  Corollary 4.24.

Let $x$ and $y$ be pointed variables and $\zeta$ a substitution of $x$ by $y$.
Then,
$\zeta^{*}\colon{\mathbf{S}}^{y}_{{\mathrm{loc}}+}({\mathtt{T}})\to{\mathbf{S}}^{x}_{{\mathrm{loc}}+}({\mathtt{T}})$
is a continuous map for the logic topologies.

Let $x_{1},\ldots,x_{n}$ be pointed variables and write
$\overline{x}=(x_{1},\ldots,x_{n})$. Take $y=x_{1}\sqcup\cdots\sqcup x_{n}$,
i.e. $y$ is a variable together with some injective substitutions
$\iota_{i}\colon x_{i}\to y$ such that $\\{\iota_{i}(x_{i})\\}_{i}$ is a
partition of $y$. Then,

$\begin{array}[]{lccc}\iota^{*}:&{\mathbf{S}}^{y}_{{\mathrm{loc}}+}({\mathtt{T}})&\to&{\mathbf{S}}^{\bar{x}}_{{\mathrm{loc}}+}({\mathtt{T}})\coloneqq\prod_{i}{\mathbf{S}}^{x_{i}}_{{\mathrm{loc}}+}({\mathtt{T}})\\\
&p&\mapsto&(\iota^{*}_{1}(p),\ldots,\iota^{*}_{n}(p))\end{array}$

is a continuous map.

Let $\Gamma\subseteq{\mathrm{LFor}}^{y}_{+}({\mathtt{L}})$ be a subset of
local positive formulas. The _interpretation_ of $\Gamma$ in
${\mathbf{S}}^{\bar{x}}_{{\mathrm{loc}}+}({\mathtt{T}})=\prod{\mathbf{S}}^{x_{i}}_{{\mathrm{loc}}+}({\mathtt{T}})$
is the subset
$\Gamma({\mathbf{S}}^{\overline{x}}_{{\mathrm{loc}}+}({\mathtt{T}}))\coloneqq{\mathrm{Im}}\,\iota^{*}(\langle\Gamma\rangle)$.
We say that a subset $V$ of
${\mathbf{S}}^{\overline{x}}_{{\mathrm{loc}}+}({\mathtt{T}})$ is _local
positive $\bigwedge$-definable_ if there is
$\Gamma\subseteq{\mathrm{LFor}}^{y}_{+}({\mathtt{L}})$ such that
$V=\Gamma({\mathbf{S}}^{\bar{x}}_{{\mathrm{loc}}+}({\mathtt{T}}))$. We say
that $\Gamma$ _defines_ $V$ if
$V=\Gamma({\mathbf{S}}^{\bar{x}}_{{\mathrm{loc}}+}({\mathtt{T}}))$. For
$(p_{1},\ldots,p_{n})\in{\mathbf{S}}^{\bar{x}}_{{\mathrm{loc}}+}({\mathtt{T}})$,
we write ${\mathtt{T}}\models\Gamma(p_{1},\ldots,p_{n})$ if
$(p_{1},\ldots,p_{n})\in\Gamma({\mathbf{S}}^{\bar{x}}_{{\mathrm{loc}}+}({\mathtt{T}}))$.

######  Remark 4.25.