# Continuous logic in a classical setting

Claudio Agostini  ,  Stefano Baratella  ,  Silvia Barbina  ,  Luca Motto Ros
and  Domenico Zambella  Institut für Diskrete Mathematik und Geometrie, TU
Wien  Dipartimento di Matematica, Università di Trento  Sezione di Matematica,
Università di Camerino  Dipartimento di Matematica, Università di Torino

###### Abstract.

Let ${\mathcal{L}}$ be a first-order two-sorted language and consider a class
of $\mathcal{L}$-structures of the form $\langle M,X\rangle$ where $M$ varies
among structures of the first sort, while $X$ is fixed in the second sort, and
it is assumed to be a compact Hausdorff space. When $X$ is a compact subset of
the real line, one way to treat classes of this kind model-theoretically is
via continuous-valued logic, as in [BYBHU]. Prior to that, Henson and Iovino
proposed an approach based on the notion of positive formulas [HI]. Their work
is tailored to the model theory of Banach spaces. Here we show that a similar
approach is possible for a more general class of models. We introduce suitable
versions of elementarity, compactness, saturation, quantifier elimination and
other basic tools, and we develop basic model theory.

###### Key words and phrases:

Continuous model theory, continuous logic, positive logic

###### 2020 Mathematics Subject Classification:

03C66

Claudio Agostini was partially supported by the FWF grant P 35655. Silvia
Barbina and Luca Motto Ros were partially supported by PRIN2022 Models, sets
and classifications, prot. 2022TECZJA. Domenico Zambella was partially
supported by PRIN2022 Logical methods in combinatorics, prot. 2022BXH4R5

##  1\. Introduction

As a motivating example for our work, consider a first-order structure $M$
equipped with a bounded distance $d:M^{2}\rightarrow[0,1]$, where $[0,1]$ is
the real unit interval. We regard $d$ as a function in a two-sorted structure
$\langle M,[0,1]\rangle$. We introduce a suitable two-sorted language
$\mathcal{L}$ and we require that the formulas in this language should remain
classically (i.e. two-) valued, as opposed to what happens in continuous
logic, where the set of truth values is the real unit interval $[0,1]$ — see
[BYBHU] for an introduction to continuous logic and [K] for a generalisation
to structures without a metric.

More generally, we deal with structures of the form $\langle M,X\rangle$,
where $M$ is some first-order structure and $X$ is a fixed compact Hausdorff
space, also treated as a first-order structure, in a way that we detail in
Section 2. In this regard, we point out again that — differently from [CK],
where formulas take values in an arbitrary compact Hausdorff space — in our
setting formulas are classically valued.

Our goal is to be able to apply basic model-theoretic results, such as
compactness and the existence of elementary and saturated extensions, to
structures like $\langle M,X\rangle$, while requiring that $X$ should stay
fixed. Ours is an attempt to reconcile these two conflicting requirements to a
certain extent. For example, with reference to our motivating example, when
considering a saturated extension of $\langle M,[0,1]\rangle$, we would like
the metric to still take values in $[0,1]$, rather than in an elementary
extension that would possibly contain nonstandard elements.

We treat the class of structures described above with an approach similar to
[HI]. As in [HI], we isolate a suitable subclass of formulas
$\mathcal{F}\subseteq\mathcal{L}$ with respect to which we prove a compactness
theorem and we formulate appropriate versions of notions such as elementary
extension and saturation. We point out a difference from [HI]. In the class of
formulas $\mathcal{F}$ we explicitly allow quantification over elements of the
topological space $X$. Though we show that these quantifiers can be
eliminated, their presence simplifies the comparison with real-valued
logic–see Example 4. A second difference is discussed after Remark 3.

We also borrow tools from nonstandard analysis, more precisely from
nonstandard topology, to define what we call the _standard part_ of a
structure. The latter plays a crucial role in the proof of our compactness
theorem. See [D] for a concrete introduction to nonstandard analysis.

We give a brief outline of the paper. In Section 2, we describe our two-sorted
language $\mathcal{L}$, and the subclass of $\mathcal{L}$-structures in which
we are interested, namely those of the form $\langle M,X\rangle$, where $M$ is
any structure and $X$ is a given nonempty compact Hausdorff space.

The language $\mathcal{L}$ contains, but is not limited to, symbols for
continuous function from $X^{n}$ (equipped with the product topology) to $X$
for $n\geq 0$ – the case $n=0$ gives a constant for each element of $X$ – and
predicate symbols for the closed (equivalently: compact) subsets of $X^{n}$ ,
for all $0<n$.

We also describe the subset $\mathcal{F}$ of $\mathcal{L}$-formulas with
respect to which we later define our versions of elementarity and saturation:
the set $\mathcal{F}$ restricts negations in such a way that the structure $X$
stays the same in elementary extensions of $\langle M,X\rangle$. Section 3
introduces the notions of an _approximation_ of a formula in $\mathcal{F}$,
and of _approximate satisfiability_ , used in Section 4 to define
$\mathcal{F}$-elementary maps. In order to partly recover the connective
negation, in Section 3 we also introduce the notion of _strong negation_ of an
$\mathcal{F}$-formula.

In Section 5, we use tools from nonstandard analysis to define the _standard
part_ $\langle N,X\rangle$ of an elementary extension $\langle
N,\,^{*}X\rangle$ of a structure $\langle M,X\rangle$, thus providing the
basis for the compactness theorem proved in Section 6 and the existence of
saturated structures. In Section 6 we also prove that approximate
satisfiability is the same as satisfiability in models that are
$\omega$-saturated with respect to the class of $\mathcal{F}$-formulas.

These results allow us, in Section 7, to work in a monster model and to
formulate the analogue in our context of classical quantifier elimination.
More precisely, we show that each $\mathcal{F}$-formula formula $\varphi$ and
each approximation $\varphi^{\prime}$ of $\varphi$ admit an interpolant
$\mathcal{F}$-formula that does not contain quantifiers of the sort which is
associated to the elements of $X$.

In Section 7 we formulate analogues of the Tarski-Vaught Test and the
Löwenheim-Skolem Theorem. We also introduce some technical notions that allow
us to obtain, among other results, a form of the Perturbation Lemma proved in
[HI] in the monster model. We conclude this section by applying these notions
to bounded metric spaces.

##  2\. A class of two-sorted structures

We adopt standard model-theoretic notation and conventions. In particular,
when there is no ambiguity, we identify a language with the set of its
formulas and a structure with its domain.

We fix a nonempty, compact Hausdorff space $X$. Recall that $X$ is a normal
space. We always assume that $X^{n}$ is endowed with the product topology, for
every $n>1$.

We associate to $X$ a first-order language $\mathcal{L}_{\sf S}$. The
subscript $\sf S$ denotes the sort of this language, which we call the _space
sort_. The non-logical symbols of $\mathcal{L}_{\sf S}$ are:

  * •

a set of $n$-ary predicate symbols $C$, one for each $n\geq 1$ and each closed
subset $C$ of $X^{n}$: for each such symbol, we write $(x_{1},\dotsc,x_{n})\in
C$ instead of $C(x_{1},\dotsc,x_{n})$;

  * •

a set of function symbols $f$, one for every $n\geq 0$ and every (uniformly)
continuous $f\colon X^{n}\to X$.

We also use $X$ to denote the structure with domain $X$ which interprets
$\mathcal{L}_{\sf S}$-symbols as expected; depending on the context, $C,f$ and
$r$ denote either $\mathcal{L}_{\sf S}$-symbols or their interpretations in
the structure $X$. An example of a structure $X$ as above is the real unit
interval $[0,1]$, equipped with all closed sets $C\subseteq[0,1]^{n}$, all
continuous functions $f\colon[0,1]^{n}\to[0,1]$, and all constants
$r\in[0,1]$. We always assume that $[0,1]$ is equipped with its standard
topology.

Next we fix an arbitrary first-order language $\mathcal{L}_{\sf H}$, which we
call the language of the _home sort_ $\sf H$. Finally, we let ${\mathcal{L}}$
be a full two-sorted language that expands both $\mathcal{L}_{\sf H}$ and
$\mathcal{L}_{\sf S}$, where the only new symbols are function symbols of sort
${\sf H}^{n}\to{\sf S}$, for some $n\geq 1$.

######  Definition 1.

A _standard structure_ is a two-sorted ${\mathcal{L}}$-structure of the form
$\langle M,X\rangle$, where $M$ is some $\mathcal{L}_{\sf H}$-structure and
$X$ is the structure fixed above.

Since $X$ is fixed, we often write $M$ instead of $\langle M,X\rangle$. From
now on, the capital letters $M$ and $N$ always denote standard structures.
Unless otherwise specified, we use the letters $a$, $b$, …to denote elements
of $M$, and the Greek letters $\alpha$, $\beta$, …to denote elements of $X$.

The notion of standard structure is inspired by that of normed space structure
introduced in [HI]. In what follows, when comparing our setting with that of
[HI] we always refer to the case of two-sorted structures therein, with our
space sort $\sf S$ playing the role of the real unit interval $[0,1]$.
However, the component of sort H of a standard structure is an arbitrary
first-order structure.

Since we are working in a _classical_ model-theoretic setting, saturated
${\mathcal{L}}$-structures exist but, when $X$ is infinite, they are not
standard structures in the sense of Definition 1. For this reason, we
introduce a set ${\mathcal{F}}$ of formulas such that $\mathcal{L}_{\sf
H}\subseteq{\mathcal{F}}\subseteq{\mathcal{L}}$ and every standard structure
has an ${\mathcal{F}}$-elementary, ${\mathcal{F}}$-saturated extension which
is itself a standard structure.

######  Definition 2.

The set ${\mathcal{F}}$ is the least subset of $\mathcal{L}$ such that:

  1. (i)

all formulas of $\mathcal{L}_{\sf H}$ belong to $\mathcal{F}$;

  2. (ii)

all formulas of the form $t(x\,;\eta)\in C$ belong to $\mathcal{F}$, where $C$
is a closed subset of $X^{n}$, for some $n\geq 1$, and $t(x\,;\eta)$ is an
$n$-tuple of terms, each of sort ${\sf H}^{|x|}\times{\sf S}^{|\eta|}\to{\sf
S}$;

  3. (iii)

$\mathcal{F}$ is closed under the Boolean connectives $\wedge$ and $\vee$;

  4. (iv)

$\mathcal{F}$ is closed under the quantifiers
$\forall\raisebox{4.73611pt}{\scaleto{\sf H}{.8ex}\kern-0.86108pt}$,
$\exists\raisebox{4.73611pt}{\scaleto{\sf H}{.8ex}\kern-0.86108pt}$ of sort
${\sf H}$ and the quantifiers $\forall\raisebox{4.73611pt}{\scaleto{\sf
S}{.8ex}\kern-0.86108pt}$, $\exists\raisebox{4.73611pt}{\scaleto{\sf
S}{.8ex}\kern-0.86108pt}$ of sort ${\sf S}$.

We denote by ${\mathcal{H}}$ the subset of ${\mathcal{F}}$ formed by the
formulas that do not contain quantifiers of sort ${\sf S}$.

We adopt the convention that, in a term or in a formula, Latin letters
$x,y,z,\dots$ denote tuples of variables of sort ${\sf H}$ and Greek letters
$\eta,\varepsilon,\dots$ denote tuples of variables of sort ${\sf S}$. Hence
we can safely drop the superscript from a quantifier. Formulas of type (i) and
(ii) in Definition 2 are called $\mathcal{F}$-atomic.

######  Remark 3.

In general, the negation of an $\mathcal{F}$-formula $\varphi$ is not
logically equivalent to an $\mathcal{F}$-formula, unless all its
$\mathcal{F}$-atomic subformulas of the form $t\in C$ are such that $C$ is
clopen. Nevertheless, the negation of an $\mathcal{F}$-formula is a well-
formed $\mathcal{L}$-formula and can be evaluated in any (standard) structure.

Formally, the set $\mathcal{F}$ does not contain equalities of sort ${\sf S}$.
However, if $\alpha$ and $\beta$ are in $X$, the equality $\alpha=\beta$ can
be expressed as $(\alpha,\beta)\in\Delta$, where $\Delta$ is the diagonal in
$X\times X$.

To simplify the exposition we assume that $\mathcal{L}_{\sf H}$ contains a
relation symbol $r_{\varphi}(x)$ for every formula $\varphi(x)$, and that all
$\mathcal{L}_{\sf H}$-structures below model
$r_{\varphi}(x)\leftrightarrow\varphi(x)$. In other words, we assume the
Morleyzation of $\mathcal{L}_{\sf H}$. The notion of $\mathcal{F}$-atomic
formula in Definition 2 is consistent with this assumption, and we implicitly
assume that all $\mathcal{L}_{\sf H}$-formulas are atomic. Moreover, we
identify $\neg r_{\varphi}$ with $r_{\neg\varphi}$ etc.

The ${\mathcal{H}}$-formulas extend the so-called positive bounded formulas
introduced in [HI]. Indeed, the former are more expressive than the latter and
contain all the $\mathcal{L}_{\sf H}$-formulas. This is a double-edged sword:
the expressiveness of $\mathcal{L}_{\sf H}$, even when $\mathcal{L}_{\sf H}$
is empty (i.e., it only includes equality), simplifies the proof of
compactness and ensures many properties of standard structures. On the other
hand, it excludes interesting examples such as the classical function spaces.
This issue is discussed in [Z].

In Section 6 we will prove the Compactness Theorem for the larger class of all
${\mathcal{F}}$-formulas. The greater expressive power of $\mathcal{F}$ is
useful. For instance, it is easy to show that the $\sup$-quantifier of real-
valued logic can be recovered by means of an $\mathcal{F}$-formula. Somewhat
surprisingly, we will also prove (Propositions 32 and 33) that
${\mathcal{F}}$-formulas can be approximated, in a sense to be made precise,
by ${\mathcal{H}}$-formulas.

######  Example 4.

Let $X=[0,1]$ be the real unit interval. Let $\dotminus$ and $\dotplus$
denote, respectively, the cut difference and the cut sum on $X$. Let $t(x)$ be
a term of sort ${\sf H}\to{\sf S}$. Then there is an ${\mathcal{F}}$-formula
expressing the equality $\sup_{x}t(x)=\tau$. For instance, consider the
formula

$\forall x\
\big{(}t(x)\dotminus\tau\in\\{0\\}\big{)}\,{\wedge}\,\forall\varepsilon\Big{(}\varepsilon\in\\{0\\}\
\vee\ \exists x\
\big{(}\tau\dotminus(t(x)\dotplus\varepsilon)\in\\{0\\}\big{)}\Big{)}.$

##  3\. Approximations and strong negations

In this section we generalize the notion of _approximation of a positive
bounded formula_ introduced in [HI]. We also define the concept of _strong
negation_ of a formula. These two notions are crucial throughout the paper.

If $\varphi,\psi$ are $\mathcal{L}$-formulas, we write $\varphi\to\psi$ to say
that the implication is valid in the class of all standard structures. We also
write $\varphi\to\psi\to\eta$ as an abbreviation for
$(\varphi\to\psi)\land(\psi\to\eta).$

Let $A\subseteq M$ be a subset of an $\mathcal{L}_{\sf H}$-structure. We let
${\mathcal{L}}(A)$ be the set of formulas in the expansion of $\mathcal{L}$
containing a name for each element of $A$. The set of formulas
$\mathcal{F}(A)$ and $\mathcal{H}(A)$ are defined accordingly, following
Definition 2.

######  Definition 5.

Let $M$ be a standard structure, and let $\varphi,\varphi^{\prime}$ be
${\mathcal{F}}(M)$-formulas. We say that $\varphi^{\prime}$ is an
_approximation_ of $\varphi$, and we write $\varphi^{\prime}>\varphi$, if
$\varphi^{\prime}$ is obtained by replacing each $\mathcal{F}$-atomic formula
of the form $t\in C$ occurring in $\varphi$ by $t\in C^{\prime}$, for some
closed neighborhood $C^{\prime}$ of $C$. When no such atomic formula occurs in
$\varphi$, we stipulate that $\varphi>\varphi$.

Clearly, $\varphi>\varphi$ also when all $\mathcal{F}$-atomic formulas of the
form $t\in C$ occurring in $\varphi$ are such that $C$ is clopen. Moreover, an
easy induction on the complexity of $\varphi$ shows that
$\varphi\to\varphi^{\prime}$ for each approximation $\varphi^{\prime}$ of
$\varphi$.

Note also that $>$ is a dense relation on ${\mathcal{F}}(M)$, in the sense
that if $\psi_{1}>\psi_{2}$ then there exists $\varphi$ such that
$\psi_{1}>\varphi>\psi_{2}$. Indeed, if $C^{\prime}$ is a closed neighborhood
of a compact set $C$, then the interior of $C^{\prime}$ is an open
neighborhood $W$ of $C$ such that $W\subseteq C^{\prime}$. By normality of
$X$, there is a closed neighborhood $C^{\prime\prime}$ of $C$ such that
$C\subseteq C^{\prime\prime}\subseteq W\subseteq C^{\prime}$, so that
$C^{\prime}$ is a closed neighborhood of $C^{\prime\prime}$. The density of
$>$ follows.

######  Definition 6.

Let $M$ be a standard structure, and let $\varphi$ be an
${\mathcal{F}}(M)$-formula. A _strong negation_ of $\varphi$ is an
$\mathcal{F}(M)$-formula $\tilde{\varphi}$ which is obtained from $\varphi$ in
the following way:

  * •

each $\mathcal{F}$-atomic formula of the form $t\in C$ occurring in $\varphi$
is replaced by an $\mathcal{F}$-atomic formula of the form $t\in\tilde{C}$,
where $\tilde{C}$ is some closed set disjoint from $C$;

  * •

each $\mathcal{F}$-atomic formula in $\mathcal{L}_{\sf H}$ occurring in
$\varphi$ is replaced by its negation (see Remark 3);

  * •

each connective, each quantifier of sort $\sf S$, and each quantifier of sort
$\sf H$ are replaced by their duals, that is, $\vee$ and $\wedge$ are replaced
by $\wedge$ and $\vee$, respectively, while existential (respectively,
universal) quantifiers are replaced by universal (respectively, existential)
quantifiers.

We write $\tilde{\varphi}\perp\varphi$ to say that $\tilde{\varphi}$ is a
strong negation of $\varphi$. By induction one can check that
$\tilde{\varphi}\to\neg\varphi$, which justifies our terminology.

######  Lemma 7.

For all $\varphi\in{\mathcal{F}}(M)$

  1. (1)

for every $\varphi^{\prime}>\varphi$, there are strong negations
$\tilde{\varphi}_{0}<\tilde{\varphi}_{1}$ of $\varphi$ such that

$\varphi\to\neg\tilde{\varphi}_{1}\to\neg\tilde{\varphi}_{0}\to\varphi^{\prime};$

  2. (2)

for every $\tilde{\varphi}\perp\varphi$, there is a formula
$\varphi^{\prime}>\varphi$ such that
$\varphi\rightarrow\varphi^{\prime}\rightarrow\neg\tilde{\varphi}$.

######  Proof 1.

We prove (1) and (2) by simultaneous induction on formulas. The case
$\varphi\in\mathcal{L}_{\sf H}$ is straightforward, so we consider the case
where $\varphi$ is of the form $t\in C$.

Let $\varphi^{\prime}>\varphi$ be $t\in C^{\prime}$ for some closed
neighborhood $C^{\prime}$ of $C$. Let $U_{0}$ be an open set such that
$C\subseteq U_{0}\subseteq C^{\prime}$. By normality of $X$, pick a closed
neighborhood $C^{\prime\prime}$ of $C$ satisfying $C^{\prime\prime}\subseteq
U_{0}$, and then let $U_{1}$ be any open set such that $C\subseteq
U_{1}\subseteq C^{\prime\prime}$. Then the formulas $\tilde{\varphi}_{i}$
given by $t\in X\smallsetminus U_{i}$ are as required in (1).

Suppose now that $\tilde{\varphi}\perp\varphi$ is of the form $t\in\tilde{C}$
for some closed set $\tilde{C}$ disjoint from $C$. By normality of $X$, there
is a closed neighborhood $C^{\prime}$ of $C$ which is disjoint from
$\tilde{C}$. Then the $\mathcal{F}$-formula $\varphi^{\prime}>\varphi$ given
by $t\in C^{\prime}$ is such that $\varphi^{\prime}\perp\tilde{\varphi}$ and
is as required in (2).

The inductive cases are straightforward.

For every type $p(x\,;\eta)\subseteq{\mathcal{F}}(M)$, we let

$p^{\prime}(x\,;\eta)=\big{\\{}\varphi^{\prime}(x\,;\eta)\mathbin{:}\varphi^{\prime}>\varphi\text{
for some }\varphi(x\,;\eta)\in p(x\,;\eta)\big{\\}}.$

In particular,
$\\{\varphi(x\,;\eta)\\}^{\prime}=\big{\\{}\varphi^{\prime}(x\,;\eta)\mathbin{:}\varphi^{\prime}>\varphi\big{\\}}$.

We say that a formula $\varphi(x\,;\eta)$ is _approximately satisfiable_ in a
standard structure $M$ if the set $\\{\varphi(x\,;\eta)\\}^{\prime}$ of its
approximations is satisfiable in $M$. By adapting the example in [HI, Chapter
5] to the current setting, one can show that, in general, approximate
satisfiability does not imply satisfiability.

##  4\. Morphisms

In this section we introduce the notion of elementary map with respect to both
the classes of $\mathcal{H}$\- and $\mathcal{F}$-formulas, as well as their
approximate versions, and we establish some basic facts about them.

######  Definition 8.

Let $M$ and $N$ be standard structures. We say that a partial map $f\colon
M\to N$ is _${\mathcal{F}}$ -elementary_ if for all
$\varphi(x)\in{\mathcal{F}}$ and all $a\in({\rm dom}f)^{|x|}$

($\dagger$) $M\models\varphi(a)\quad\Rightarrow\quad N\models\varphi(fa).$

An _${\mathcal{F}}$ -elementary embedding_ is a total
${\mathcal{F}}$-elementary map. If $M\subseteq N$ and the identity map ${\rm
id}_{M}\colon M\to N$ is an ${\mathcal{F}}$-elementary embedding we write
$M\preccurlyeq^{\mathcal{F}}N$ and we say that $M$ is an _${\mathcal{F}}$
-elementary substructure_ of $N$, or that $N$ is an _$\mathcal{F}$ -elementary
extension_ of $M$.

The definitions of _${\mathcal{H}}$ -elementary_ map or _$\mathcal{H}$
-elementary embedding_ are obtained by replacing ${\mathcal{F}}$ with
${\mathcal{H}}$ throughout.

Recall that the language $\mathcal{L}_{\sf S}$ has a name for each element of
$X$. Hence, if $f$ is ${\mathcal{F}}$-elementary the implication ($\dagger$ ‣
8) actually holds for all $\varphi(x\,;\eta)\in{\mathcal{F}}$ in the following
form: for all $a\in({\rm dom}f)^{|x|}$ and all $\alpha\in X^{|\eta|}$

$M\models\varphi(a\,;\alpha)\quad\Rightarrow\quad
N\models\varphi(fa\,;\alpha).$

The same remark applies to the classes of morphisms that we define next.

As ${\mathcal{F}}$\- and ${\mathcal{H}}$-elementary maps are in particular
$\mathcal{L}_{\sf H}$-elementary, they are injective; however, the inverse of
an ${\mathcal{F}}$-elementary map may not be ${\mathcal{F}}$-elementary. This
is because the class of $\mathcal{F}$-formulas is not closed under negation,
hence from the validity of ($\dagger$ ‣ 8) for all ${\mathcal{F}}$-formulas we
cannot derive the converse implication for a specific $\mathcal{F}$-formula
$\varphi$, unless $C$ is clopen in all $\mathcal{F}$-atomic subformulas of
$\varphi$ of the form $t\in C$.

This notion of elementary map is dictated by our framework, in particular by
our choice of working with the classical notion of satisfaction. This differs
from the approach in [HI], where _approximate satisfaction_ plays a crucial
role.

The approximate ${\mathcal{F}}$-morphisms that we define next preserve the
approximate satisfiability in [HI]. They are invertible in the class of
approximate ${\mathcal{F}}$-morphisms, as discussed in Proposition 10 below.

######  Definition 9.

We say that a partial map $f\colon M\to N$ is _approximate
${\mathcal{F}}$-elementary_ if for every formula $\varphi(x)\in{\mathcal{F}}$,
and every $a\in({\rm dom}f)^{|x|}$

($\ddagger$) $M\models\varphi(a)\quad\Rightarrow\quad
N\models\big{\\{}\varphi(fa)\big{\\}}^{\prime}.$

We define _approximate ${\mathcal{H}}$-elementary_ maps in the same manner.

Clearly, ${\mathcal{F}}$-elementarity implies its approximate version, and
similarly for ${\mathcal{H}}$-elementarity.

Later we will show that, under a weak saturation assumption, the converse
implication to ($\ddagger$ ‣ 9) holds as well (Proposition 25). Furthermore,
under full saturation, approximate elementary morphisms become
${\mathcal{L}}$-elementary maps (Corollary 31).

The following result holds without any saturation assumption.

######  Proposition 10.

If $f\colon M\to N$ is an approximate $\mathcal{F}$-elementary map, then for
every $\varphi(x)\in{\mathcal{F}}$ and every $a\in({\rm dom}f)^{|x|}$,

$M\models\big{\\{}\varphi(a)\big{\\}}^{\prime}\quad\Leftrightarrow\quad
N\models\big{\\{}\varphi(fa)\big{\\}}^{\prime}.$

The same holds for approximate ${\mathcal{H}}$-elementary maps and
$\mathcal{H}$-formulas $\varphi(x)$.

######  Proof 2.

For the left-to-right implication, assume
$M\models\big{\\{}\varphi(a)\big{\\}}^{\prime}$. Given an arbitrary
$\varphi^{\prime}>\varphi$, use density of $>$ and pick any
$\varphi^{\prime}>\varphi^{\prime\prime}>\varphi$. Then
$M\models\varphi^{\prime\prime}(a)$ by assumption, hence
$N\models\varphi^{\prime}(fa)$ by ($\ddagger$ ‣ 9) applied to
$\varphi^{\prime\prime}$. Since $\varphi^{\prime}$ was chosen arbitrarily, the
conclusion follows.

For the converse implication, assume
$N\models\big{\\{}\varphi(fa)\big{\\}}^{\prime}$ and let
$\varphi^{\prime}>\varphi^{\prime\prime}>\varphi$. By Lemma 7 there are
$\tilde{\varphi}_{0},\tilde{\varphi}_{1}\perp\varphi^{\prime\prime}$ with
$\tilde{\varphi}_{1}>\tilde{\varphi}_{0}$ such that
$\varphi^{\prime\prime}\to\neg\tilde{\varphi}_{1}$ and
$\neg\tilde{\varphi}_{0}\rightarrow\varphi^{\prime}$. Since
$N\models\varphi^{\prime\prime}(fa)$ by assumption, we get
$N\models\neg\tilde{\varphi}_{1}(fa)$, and thus
$M\models\neg\tilde{\varphi}_{0}(a)$ by ($\ddagger$ ‣ 9) applied to
$\tilde{\varphi}_{0}$. Hence $M\models\varphi^{\prime}(a)$, and since
$\varphi^{\prime}$ was an arbitrary approximation of $\varphi$ we are done.

Finally, we define the analogues of classical partial embeddings.

######  Definition 11.

A map $f\colon M\to N$ is a _partial ${\mathcal{F}}$-embedding_ if ($\dagger$
‣ 8) above holds for all ${\mathcal{F}}$-atomic formulas; equivalently,
($\dagger$ ‣ 8) holds for all $\mathcal{F}$-formulas $\varphi(x)$ without
quantifiers of sort $\sf H$.

######  Remark 12.

Let $f\colon M\to N$ be a partial ${\mathcal{F}}$-embedding. Then, for every
$a\in({\rm dom}f)^{|x|}$ and every ${\mathcal{F}}$-formula $\varphi(x)$
without quantifiers of sort ${\sf H}$,

$M\models\varphi(a)\quad\Leftrightarrow\quad N\models\varphi(fa).$

The forward implication is by definition of a partial $\mathcal{F}$-embedding,
so we only need to check the backward implication. This is trivial for
${\mathcal{F}}$-atomic formulas $\varphi\in\mathcal{L}_{\sf H}$, as they are
closed under negations. For an $\mathcal{F}$-atomic formula of the form
$t(x)\in C$, assume $M\not\models t(a)\in C$. Since $M\models t(a)\in\\{c\\}$
with $c=t^{M}(a)\notin C$, then $N\models t(fa)\in\\{c\\}$, and hence
$N\not\models t(fa)\in C$. The inductive cases are straightforward. (In order
to deal with quantifiers of sort $\sf S$, recall that the language
$\mathcal{L}_{\sf S}$ has a name for each element of $X$.)

##  5\. The standard part of a structure

Our goal is to prove the Compactness Theorem for the class of
${\mathcal{F}}$-formulas. We accomplish this in Section 6. We anticipate that
we do not resort to an ultraproduct construction. We rather build on the
Compactness Theorem for classical logic and make use of two basic notions in
nonstandard topology, those of monad of a point and of near-standard point. In
this section we prove the preliminary Lemma 19 that we later use in the proof
of Theorem 22.

Fix an $\mathcal{L}_{\sf S}$-elementary extension ${}^{*}\\!X$ of $X$. Here
and below, we denote by ${}^{*}\\!D$ the interpretation of the predicate
symbol $D$ in ${}^{*}\\!X$. Let $\eta$ be an $n$-tuple of variables of sort
${\sf S}$, for some $n\geq 1$. For each $\beta\in X^{n}$, we define the
$\mathcal{L}_{\sf S}$-type

${\rm m}_{\beta}(\eta)=\\{\eta\in D\mathbin{:}D\text{ is a closed neighborhood
of }\beta\\}.$

Then the set $X_{\beta}$ of realizations of ${\rm m}_{\beta}(\eta)$ in
${}^{*}\\!X$ is

$X_{\beta}=\bigcap\\{{}^{*}\\!D\mathbin{:}D\text{ is a closed neighborhood of
}\beta\\}.$

Thus, if we regard ${}^{*}\\!X$ as a nonstandard extension of the topological
space $X$ and recall that the closed neighborhoods of $\beta$ form a basis for
its neighborhood system, we have that $X_{\beta}$ is just what, in nonstandard
language, is called the _monad_ of $\beta$.

######  Remark 13.

For every $\alpha\in({}^{*}\\!X)^{n}$ there is a unique $\beta\in X^{n}$ such
that ${}^{*}\\!X\models{\rm m}_{\beta}(\alpha)$. This is straightforward if
one uses the nonstandard characterization of compactness (see, for instance,
[D]) and the Hausdorff assumption on $X$. However, for the benefit of the
reader who is not familiar with this argument, we provide a self-contained
model-theoretic argument. The uniqueness of $\beta$ follows from the Hausdorff
property of $X^{n}$, so we just prove existence. For a contradiction, let
$\alpha\in({}^{*}\\!X)^{n}$ be such that for each $\beta\in X^{n}$ there
exists a closed neighborhood $D_{\beta}$ of $\beta$ with
${}^{*}\\!X\not\models\alpha\in D_{\beta}$. By compactness of $X^{n}$, there
is some finite subset $Y$ of $X^{n}$ such that $X^{n}=\bigcup_{\beta\in
Y}D_{\beta}.$ From $X\preccurlyeq{}^{*}\\!X$ we get
$({}^{*}\\!X)^{n}\subseteq\bigcup_{\beta\in Y}{}^{*}D_{\beta}$, contradicting
the fact that $\alpha\notin{}^{*}D_{\beta}$ for all $\beta\in X^{n}$ .

We refer to Remark 13 by saying that every point in $({}^{*}\\!X)^{n}$ is
near-standard. We call $\beta$ the _standard part_ of $\alpha$, and we denote
it by ${\rm st}(\alpha)$. By definition of ${\rm st}(\alpha)$, if
$\alpha\in({}^{*}\\!X)^{n}$ and $C\subseteq X^{n}$ is a closed neighborhood of
${\rm st}(\alpha)$, then ${}^{*}\\!X\models\alpha\in C$. The following
proposition provides a converse to this, and it implies that if $\alpha\in
X^{n}$ then ${\rm st}(\alpha)=\alpha$. (Take $C=\\{\alpha\\}$ and use the fact
that $X\preccurlyeq{}^{*}\\!X$.)

######  Proposition 14.

Let $\alpha\in({}^{*}\\!X)^{n}$ and let $C\subseteq X^{n}$ be a closed set.
Then

${}^{*}\\!X\models\alpha\in C\ \to\ {\rm st}(\alpha)\in C.$

######  Proof 3.

By contraposition. Assume ${\rm st}(\alpha)\notin{}^{*}\\!C$. From
$X\preccurlyeq{}^{*}\\!X$ we get that ${\rm st}(\alpha)\notin C.$ By normality
of $X^{n}$ there is a closed neighborhood $D$ of ${\rm st}(\alpha)$ which is
disjoint from $C$. Hence ${}^{*}\\!C\cap{}^{*}\\!D=\emptyset$ by
$X\preccurlyeq{}^{*}\\!X$ again. On the other hand, by definition of ${\rm
st}(\alpha)$ we have $\alpha\in{}^{*}\\!D$. Thus $\alpha\notin{}^{*}\\!C$.

######  Remark 15.

Let $\alpha=\langle\alpha_{1},\dots,\alpha_{n}\rangle\in({}^{*}\\!X)^{n}$.
Then

${\rm st}(\alpha)=\langle{\rm st}(\alpha_{1}),\dots,{\rm
st}(\alpha_{n})\rangle.$

Indeed, fix an arbitrary closed neighborhood $D$ of $\langle{\rm
st}(\alpha_{1}),\dots,{\rm st}(\alpha_{n})\rangle$. Then there are closed
neighborhoods $D_{i}$ of ${\rm st}(\alpha_{i})$ such that
$D_{1}\times\ldots\times D_{n}\subseteq D$. By definition of ${\rm
st}(\alpha_{i})$, we have $\alpha_{i}\in{}^{*}\\!D_{i}$ for all $1\leq i\leq
n$. Moreover,
${}^{*}\\!D_{1}\times\ldots\times{}^{*}\\!D_{n}\subseteq{}^{*}\\!D$ by
$X\preccurlyeq{}^{*}\\!X$, hence $\alpha\in{}^{*}\\!D$.

If we regard ${}^{*}\\!X$ as a nonstandard extension of the topological space
$X$, the statement ($\circ$ ‣ 16) in the next proposition is a straightforward
consequence of the nonstandard characterization of continuity in terms of
monads (see [D]). For the reader’s convenience, below we provide a self-
contained argument.

######  Proposition 16.

For all $\alpha\in({}^{*}\\!X)^{|\alpha|}$ and function symbols
$f\in\mathcal{L}_{\sf S}$ of sort ${\sf S}^{|\alpha|}\to{\sf S}$,

($\circ$) ${}^{*}\\!X\models{\rm st}\big{(}f(\alpha)\big{)}=f\big{(}{\rm
st}(\alpha)\big{)}.$

######  Proof 4.

By definition of standard part, it suffices to prove that ${}^{*}\\!X\models
f(\alpha)\in D$ for every closed neighborhood $D$ of $f\big{(}{\rm
st}(\alpha)\big{)}$. Fix one such $D$. By continuity of $f$, the set
$C=f^{-1}[D]$ is a closed neighborhood of ${\rm st}(\alpha)$. By definition of
${\rm st}(\alpha)$, ${}^{*}\\!X\models\alpha\in C$. Finally,
$X\preccurlyeq{}^{*}\\!X$ yields that ${}^{*}\\!X\models\forall\eta\,(\eta\in
C\leftrightarrow f(\eta)\in D)$), hence ${}^{*}\\!X\models f(\alpha)\in D$.

An elementary extension of a standard structure $\langle M,X\rangle$ is a
nonstandard $\mathcal{L}$-structure of the form $\langle N,{}^{*}\\!X\rangle$
for some $X\preccurlyeq{}^{*}\\!X$. We now define a procedure to extract from
any $\mathcal{L}$-structure of the form $\langle N,{}^{*}\\!X\rangle$ a
standard structure $\langle N,X\rangle$ so that truth in $\langle
N,{}^{*}\\!X\rangle$ is closely related to truth in $\langle N,X\rangle$ (see
Lemma 19).

######  Definition 17.

Let $\langle N,{}^{*}\\!X\rangle$ be an $\mathcal{L}$-structure with
$X\preccurlyeq{}^{*}\\!X$. The _standard part_ of $\langle
N,{}^{*}\\!X\rangle$ is the standard structure $\langle N,X\rangle$ where

  * •

each symbol in $\mathcal{L}_{\sf S}$ is interpreted in $X$ as usual;

  * •

each symbol in $\mathcal{L}_{\sf H}$ is interpreted as in $N$ (so these
symbols have the same interpretation in both $\langle N,{}^{*}\\!X\rangle$ and
$\langle N,X\rangle$);

  * •

each function symbol $f$ of sort ${\sf H}^{n}\to{\sf S}$ is canonically
interpreted as the function $f^{\langle N,X\rangle}\colon N^{n}\to X$ such
that for all $a\in N^{n}$

$f^{\langle N,X\rangle}(a)={\rm st}\big{(}f^{\langle
N,{}^{*}\\!X\rangle}(a)\big{)}.$

To simplify notation, for each function symbol $f\in\mathcal{L}$ we denote by
${}^{*}\\!f$ its interpretation $f^{\langle N,{}^{*}\\!X\rangle}$ in $\langle
N,{}^{*}\\!X\rangle$, and by $f^{N}$ its interpretation in the standard
structure $\langle N,X\rangle$ (which, as usual, will simply be denoted by $N$
when there is no danger of confusion). Similar notation will be adopted for
$\mathcal{L}$-terms.

######  Proposition 18.

With the above assumptions and notation, let $t(x\,;\eta)$ be an
$\mathcal{L}$-term of sort ${\sf H}^{|x|}\times{\sf S}^{|\eta|}\to{\sf S}$.
Then, for all $a\in N^{|x|}$ and all $\alpha\in({}^{*}\\!X)^{|\eta|}$

($\$$) $t^{N}\big{(}a\,;{\rm st}(\alpha)\big{)}={\rm
st}\big{(}{}^{*}t(a\,;\alpha)\big{)}.$

######  Proof 5.

The case when $t$ is a constant symbol or a variable of sort $\sf S$ is
trivial.

If $t$ is $f(t_{1},\dots,t_{n})$ with $f$ of sort ${\sf H}^{n}\to{\sf S}$,
then each $t_{i}$ is an $\mathcal{L}_{\sf H}$-term and no variable of sort
${\sf S}$ occurs in it. Thus
${}^{*}t_{i}(a\,;\alpha)={}^{*}t_{i}(a)=t_{i}^{N}(a)=t_{i}^{N}(a\,;{\rm
st}(\alpha))$ for all $1\leq i\leq n$ by definition of $\langle N,X\rangle$,
and thus ($\$$ ‣ 18) holds by definition of $f^{N}$.

If $t$ is $f(t_{1},\dotsc,t_{n})$, for some function symbol $f$ of sort ${\sf
S}^{n}\to{\sf S}$, inductively assume that

$t_{i}^{N}\big{(}a\,;{\rm st}(\alpha)\big{)}={\rm
st}\big{(}{}^{*}t_{i}(a\,;\alpha)\big{)}$

holds for each term $t_{i}(x\,;\eta)$. Then the required equality follows from
Proposition 16, Remark 15, and $X\preccurlyeq{}^{*}\\!X$.

######  Lemma 19.

With the above assumptions and notation, for every ${\mathcal{F}}$-formula
$\varphi(x\,;\eta)$, for all $a\in N^{|x|}$ and all
$\alpha\in({}^{*}\\!X)^{|\eta|}$

($+$) $\langle
N,{}^{*}\\!X\rangle\models\varphi(a\,;\alpha)\quad\Rightarrow\quad\langle
N,X\rangle\models\varphi\big{(}a\,;{\rm st}(\alpha)\big{)}.$

######  Proof 6.

By induction on the complexity of $\mathcal{F}$-formulas. Suppose first that
$\varphi(x\,;\eta)$ is $\mathcal{F}$-atomic. If $\varphi(x\,;\eta)$ is an
$\mathcal{L}_{\sf H}$-formula, the validity of $(+)$ is straightforward.
Otherwise, $\varphi(x\,;\eta)$ has the form $t(x\,;\eta)\in C$ for some closed
set $C\subseteq X^{n}$ and $t(x\,;\eta)$ a sequence of $n$ terms
$t_{i}(x\,;\eta)$ of sort ${\sf H}^{|x|}\times{\sf S}^{|\eta|}\to{\sf S}$.
Assuming that $\langle N,{}^{*}\\!X\rangle\models t(a\,;\alpha)\in C$ gives
$\langle N,{}^{*}\\!X\rangle\models{\rm
st}\big{(}{}^{*}t(a\,;\alpha)\big{)}\in C$ by Proposition 14, and hence ${\rm
st}\big{(}{}^{*}t(a\,;\alpha)\big{)}\in C$ by $X\preccurlyeq{}^{*}\\!X$.
Therefore $t^{N}\big{(}a\,;{\rm st}(\alpha)\big{)}\in C$ by Remark 15 and
Proposition 18 applied to each term $t_{i}\,$. The inductive cases are
straightforward.

There is a partial converse to Lemma 19 using approximations.

######  Lemma 20.

With the above assumptions and notations, for every $\mathcal{F}$-formula
$\varphi(x\,;\eta)$, for all $a\in N^{|x|}$ and all
$\alpha\in{({}^{*}\\!X)}^{|\eta|}$

($\times$) $\langle N,X\rangle\models\varphi(a\,;{\rm
st}(\alpha))\quad\Rightarrow\quad\langle
N,{}^{*}\\!X\rangle\models\big{\\{}\varphi(a\,;\alpha)\big{\\}}^{\prime}.$

######  Proof 7.

The proof is similar to that of Lemma 19, the only nontrivial case being that
of an $\mathcal{F}$-atomic formula $\varphi$ of the form $t(x\,;\eta)\in C$.
Let $\varphi^{\prime}>\varphi$ be $t(x\,;\eta)\in C^{\prime}$, for some closed
neighborhood $C^{\prime}$ of $C$. If $t^{N}(a\,;{\rm st}(\alpha))\in C$, then
by Proposition 18 and Remark 15 the set $C^{\prime}$ is a closed neighborhood
of ${\rm st}\big{(}{}^{*}t(a\,;\alpha)\big{)}$. By definition of standard
part, this means that
${}^{*}t(a\,;\alpha)\in{}^{*}\\!\big{(}C^{\prime}\big{)}$, i.e. $\langle
N,{}^{*}\\!X\rangle\models\varphi^{\prime}(a\,;\alpha)$.

######  Corollary 21.

With the above assumptions and notations, for every $\mathcal{F}$-formula
$\varphi(x\,;\eta)$, for all $a\in N^{|x|}$ and all
$\alpha\in{({}^{*}\\!X)}^{|\eta|}$

$\langle
N,{}^{*}\\!X\rangle\models\big{\\{}\varphi(a\,;\alpha)\big{\\}}^{\prime}\quad\Leftrightarrow\quad\langle
N,X\rangle\models\big{\\{}\varphi(a\,;{\rm st}(\alpha))\big{\\}}^{\prime}.$

######  Proof 8.

The forward implication follows from Lemma 19. For the backward implication,
fix any $\varphi^{\prime}>\varphi$ and by density of $>$ pick any
$\varphi^{\prime\prime}$ such that
$\varphi^{\prime}>\varphi^{\prime\prime}>\varphi$. Then apply Lemma 20 to
$\varphi^{\prime\prime}$.

##  6\. Compactness

We distinguish between consistency with respect to standard structures and
consistency with respect to arbitrary ${\mathcal{L}}$-structures. We say that
an ${\mathcal{L}}$-theory $T$ is _${\mathcal{L}}$ -consistent_ if there is
some ${\mathcal{L}}$-structure $\langle M,J\rangle$ which satisfies $T.$ We
say that $T$ is _consistent_ if $M\models T$ for some standard structure $M$.
For simplicity we consider only the class of formulas $\mathcal{F}$, but all
definitions and results can easily be adapted to the subclass $\mathcal{H}$.

######  Theorem 22 ($\mathcal{F}$-Compactness Theorem).

Let $T\subseteq{\mathcal{F}}$ be finitely ${\mathcal{L}}$-consistent. Then $T$
is consistent.

######  Proof 9.

Suppose that $T$ is finitely consistent. By the Compactness Theorem for
classical logic, there is some ${\mathcal{L}}$-structure $\langle
M,{}^{*}\\!X\rangle$, with $X\preccurlyeq{}^{*}\\!X$, such that $\langle
M,{}^{*}\\!X\rangle\models T$. Let $\langle M,X\rangle$ be its standard part
as in Definition 17. Then $\langle M,X\rangle\models T$ by Lemma 19.

It is an open problem111An answer has been recently provided by [Z]. whether
it is possible to extend Theorem 22 to a larger class of formulas, in
particular when we allow in ${\mathcal{L}}$ function symbols of sort ${\sf
H}^{n}\times{\sf S}^{m}\to{\sf S}$, with both $n$ and $m$ positive. Functions
of this sort have a natural interpretation, for instance in the case of a
group acting on a compact Hausdorff space.

######  Definition 23.

A standard structure $N$ is _$\lambda$ -${\mathcal{F}}$-saturated_ if it
realizes all types $p(x\,;\eta)\subseteq{\mathcal{F}}(N)$ that are finitely
realized in $N$ and that have fewer than $\lambda$ parameters from $N$. When
$\lambda=|N|$ we simply say that $N$ is _${\mathcal{F}}$ -saturated._

Under suitable set-theoretic assumptions, the existence of
${\mathcal{F}}$-saturated standard structures can be proved as in the
classical case.

######  Theorem 24.

Assume $\lambda$ is such that $\lambda^{<\lambda}=\lambda>|\mathcal{L}|$. Then
every standard structure $M$ of cardinality $\lambda$ has an
${\mathcal{F}}$-elementary extension to an $\mathcal{F}$-saturated standard
structure of cardinality $\lambda$.

######  Proof 10.

We need the following easy consequence of the $\mathcal{F}$-compactness
theorem.

  * ($\star$)

For $\lambda$ and $M$ as in the assumptions, there is a model $M^{\prime}$ of
cardinality $\lambda$ that, for every $A\subseteq M$ with $|A|<\lambda$,
realises every type $p(x,\eta)\subseteq\mathcal{F}(A)$ that is finitely
consistent in some $M^{\prime\prime}\succeq^{\mathcal{F}}M$.

Note that finite consistency of $p(x,\eta)$ in some $\mathcal{F}$-elementary
extension of $M$ is a weaker requirement than finite consistency in $M$. The
proof of ($\star$) is entirely similar to the standard proof of the classical
version.

The construction of the desired $\mathcal{F}$-saturated standard structure is
the usual one: we build an $\mathcal{F}$-elementary chain $\langle
M_{i}:i<\lambda\rangle$ of models of cardinality $\lambda$, where

  * •

$M_{0}=M$

  * •

we take unions at limit stages

  * •

at stage $i+1$ we use $(\star)$ to get $M_{i+1}$.

Let $N$ be the union of the chain. Then $|N|=\lambda$ and, by an analogue of
the classical elementary chain lemma, $N\succeq^{\mathcal{F}}M_{i}$ for all
$i$. Let $p(x,\eta)\subseteq\mathcal{F}(A)$ be a type that is finitely
consistent in $N$, where $|A|<\lambda$. Since $\lambda$ is regular, there is
$i<\lambda$ such that $A\subseteq M_{i}$. By construction, $M_{i+1}$ realizes
$p(x)$, and therefore, by $\mathcal{F}$-elementarity, so does $N$.

With reference to the notion of approximate satisfiability that we introduced
at the end of Section 3, we show that $\omega$-${\mathcal{F}}$-saturation
implies that approximate satisfiability is equivalent to satisfiability.

######  Proposition 25.

Let $N$ be an $\omega$-${\mathcal{F}}$-saturated standard structure. Then for
every formula $\varphi(x;\eta)\in{\mathcal{F}}(N)$, for all $a\in N^{|x|}$ and
$\alpha\in X^{|\eta|}$

$N\models\big{\\{}\varphi(a\,;\alpha)\big{\\}}^{\prime}\quad\Leftrightarrow\quad
N\models\varphi(a\,;\alpha).$

Therefore, in $N$ each $\mathcal{F}$-type $p(x\,;\eta)$ is equivalent to its
approximation $p^{\prime}(x\,;\eta)$.

######  Proof 11.

The right-to-left implication is trivial because $\varphi\to\varphi^{\prime}$
for every $\varphi^{\prime}>\varphi$.

The converse implication trivially holds for $\mathcal{F}$-atomic formulas in
$\mathcal{L}_{\sf H}$, as in this case
$\big{\\{}\varphi(a\,;\alpha)\big{\\}}^{\prime}=\\{\varphi(a\,;\alpha)\\}$.
Suppose now that $\varphi$ is an $\mathcal{F}$-atomic formula of the form
$t\in C$, where $C$ is a closed subset of $X^{n}$. Since $X^{n}$ is compact
Hausdorff, and hence regular, if $t^{N}(a\,;\alpha)\notin C$ then there is
some closed neighborhood $C^{\prime}$ of $C$ such that
$t^{N}(a\,;\alpha)\notin C^{\prime}$, which means that
$N\not\models\varphi^{\prime}(a\,;\alpha)$ where $\varphi^{\prime}>\varphi$ is
$t\in C^{\prime}$.

The inductive steps for conjunction, disjunction, and for the universal
quantifiers of sort $\sf H$ and $\sf S$ are straightforward.

We now treat the case of the existential quantifier of sort ${\sf H}$.
Consider the formula $\exists y\,\varphi(x,y\,;\eta)$, and fix $a\in N^{|x|}$
and $\alpha\in X^{|\eta|}$. By inductive hypothesis, for all $b\in N$

($\sim$)
$N\models\big{\\{}\varphi(a,b;\alpha)\big{\\}}^{\prime}\quad\Rightarrow\quad
N\models\varphi(a,b;\alpha).$

Assume that $N\models\\{\exists y\,\varphi(a,y\,;\alpha)\\}^{\prime}$: we
prove that the $\mathcal{F}$-type
$p(z)=\\{\varphi^{\prime}(a,z\,;\alpha)\mathbin{:}\varphi^{\prime}>\varphi\\}$
is realized in $N$ by some $b\in N$, so that $N\models\varphi(a,b\,;\alpha)$
by ($\sim$ ‣ 11), and thus $N\models\exists y\,\varphi(a,y\,;\alpha)$. The
$\mathcal{F}$-type $p$ uses only finitely many parameters from $N$ because so
does $\varphi$, hence by $\omega$-$\mathcal{F}$-saturation of $N$ it is enough
to show that $p$ is finitely realizable in $N$. For notational simplicity, we
show that if $\varphi^{\prime}_{1},\varphi^{\prime}_{2}>\varphi$, then
$(\varphi_{1}\land\varphi_{2})(a,z\,;\alpha)$ is realized in $N$. First we
claim that there is some $\varphi^{\prime}>\varphi$ such that
$\varphi^{\prime}\rightarrow\varphi^{\prime}_{1}\wedge\varphi^{\prime}_{2}$.
In order to obtain one such $\varphi^{\prime}$, it suffices to replace each
$\mathcal{F}$-atomic subformula of $\varphi$ of the form $t\in C$ with $t\in
C_{1}\cap C_{2},$, where $t\in C_{1}$ and $t\in C_{2}$ are the
$\mathcal{F}$-atomic subformulas that occur in $\varphi^{\prime}_{1}$ and
$\varphi^{\prime}_{2}$ in place of $t\in C$. By assumption, $N\models\exists
y\,\varphi^{\prime}(a,y\,;\alpha)$, hence
$N\models(\varphi_{1}\wedge\varphi_{2})(a,b\,;\alpha)$, for some $b\in N$, as
desired.

The case of an existential quantifier of sort ${\sf S}$ is similar.

A consequence of Proposition 25 is that approximate $\mathcal{F}$-elementary
maps (see Definition 9) between $\omega$-${\mathcal{F}}$-saturated standard
structures coincide with their unapproximated version. In particular,
Proposition 10 gives the following corollary.

######  Corollary 26.

Let $M$ be an $\omega$-${\mathcal{F}}$-saturated standard structure and
$f\colon M\to N$ be an ${\mathcal{F}}$-elementary map. Then

$M\models\varphi(a)\quad\Leftrightarrow\quad N\models\varphi(fa)$

for every ${\mathcal{F}}$-formula $\varphi(x)$ and every $a\in({\rm
dom}f)^{|x|}$. If moreover $N$ is $\omega$-$\mathcal{F}$-saturated as well,
then the same is true for every approximate $\mathcal{F}$-elementary map
$f\colon M\to N$.

##  7\. The monster model

Throughout this section we fix a sufficiently large ${\mathcal{F}}$-saturated
standard structure $\langle\mathcal{U},X\rangle$, which exists by Theorem 24,
and as usual identify it with its first component $\mathcal{U}$. (Recall that
the structure $X$ is fixed). We call $\mathcal{U}$ the _monster model_. The
truth value of a formula is evaluated in $\mathcal{U}$, unless otherwise
specified. An ${\mathcal{F}}$-elementary substructure of $\mathcal{U}$ is
called a _model_. From now on, we assume that all standard structures under
consideration are models.

######  Remark 27.

For all models $M,N$ and all $a\in M^{|a|}\cap N^{|a|}$, the identity map on
the elements of the tuple $a$ is an approximate $\mathcal{F}$-elementary map
from $M$ to $N$. Indeed, let $\varphi$ be an $\mathcal{F}$-formula such that
$M\models\varphi(a)$, so that $\mathcal{U}\models\varphi(a)$ because $M$ is a
model, and assume towards a contradiction that
$N\not\models\varphi^{\prime}(a)$ for some $\varphi^{\prime}>\varphi$. Let
$\varphi^{\prime\prime}$ be such that
$\varphi^{\prime}>\varphi^{\prime\prime}>\varphi$, so that
$N\not\models\varphi^{\prime\prime}(a)$. By Lemma 7(1) there exists
$\tilde{\varphi}\perp\varphi$ such that
$\varphi\rightarrow\neg\tilde{\varphi}\rightarrow\varphi^{\prime\prime}$.
Since $N\not\models\varphi^{\prime\prime}(a)$ then
$N\models\tilde{\varphi}(a)$. Thus $\mathcal{U}\models\tilde{\varphi}(a)$
because $N$ is a model, a contradiction.

By definition of $\mathcal{F}$-elementary embedding, the truth of an
${\mathcal{F}}(M)$-formula is preserved from a model $M$ to the monster model;
if the converse implication also holds we say that $M$ is a _strong model_. By
Corollary 26, any $\omega$-$\mathcal{F}$-saturated model is strong. Notice
also that any (not necessarily $\omega$-$\mathcal{F}$-saturated) strong model
$M$ satisfies the conclusion of Proposition 25. Furthermore, by Remark 27
every model that satisfies the conclusion of Proposition 25 is a strong model.
Hence the strong models are precisely the models for which the equivalence in
Proposition 25 holds.

For the rest of this section, we fix a small subset $A$ of $\mathcal{U}$. For
all $n\geq 1$ we denote by $\tau_{n}(A)$ the topology on $\mathcal{U}^{n}$ for
which the closed sets are those defined by the $n$-types
$p(x)\subseteq{\mathcal{F}}(A)$. By $\mathcal{F}$-saturation the topology
$\tau_{n}(A)$ is compact.

In what follows, if $p(x)\subseteq\mathcal{F}(A)$ and $\psi(x)$ is an
$\mathcal{F}(A)$-formula, we write $p(x)\rightarrow\psi(x)$ when
$p(\mathcal{U})\subseteq\psi(\mathcal{U})$. When working in the monster model
$\mathcal{U}$, we freely use infinitary connectives in similar expressions
involving types — the meaning should be clear from the context.

Next we prove two consequences of ${\mathcal{F}}$-compactness that hold in our
setting. Note the differences with the classical setting.

######  Proposition 28.

Let $p(x)\subseteq{\mathcal{F}}(A)$ and $\varphi(x)\in{\mathcal{F}}({A})$.

  1. (1)

If $p(x)\rightarrow\neg\varphi(x)$, then $\psi(x)\rightarrow\neg\varphi(x)$
for some finite conjunction $\psi(x)$ of formulas in $p(x)$.

  2. (2)

If $p(x)\rightarrow\varphi(x)$ and $\varphi^{\prime}>\varphi$, then
$\psi(x)\rightarrow\varphi^{\prime}(x)$ for some finite conjunction $\psi(x)$
of formulas in $p(x)$.

######  Proof 12.

Part (1) is a straightforward consequence of $\mathcal{F}$-compactness
(Theorem 22). Part (2) follows from Lemma 7(1) and part (1).

For a tuple $x$ of variables, ${{\mathcal{F}}_{x}}(A)$ denotes the set of
$\mathcal{F}$-formulas whose free variables are in $x$. We use similar
notation for ${\mathcal{H}}$-formulas and $\mathcal{L}$-formulas.

Let $a$ be an $n$-tuple of elements from $\mathcal{U}$. We let

$\mathcal{F}\mbox{-tp}(a/A)=\big{\\{}\varphi(x)\in{\mathcal{F}}(A)\mathbin{:}\mathcal{U}\models\varphi(a)\big{\\}},\qquad
S_{\mathcal{F},n}(A)=\big{\\{}\mathcal{F}\mbox{-tp}(a/A)\mathbin{:}a\in\mathcal{U}^{n}\big{\\}},$

and $S_{\mathcal{F}}(A)=\bigcup_{n\in\omega}S_{\mathcal{F},n}(A)$. If $x$ is a
tuple of variables, $S_{\mathcal{F},x}(A)$ denotes the subset of
$S_{\mathcal{F}}(A)$ consisting of those types whose free variables range in
$x$.

######  Proposition 29.

Each type $p(x)\in S_{\mathcal{F},x}(A)$ is a maximal consistent subset of
${\mathcal{F}}_{x}(A)$ in the following sense: for every
$\varphi(x)\in{\mathcal{F}}_{x}(A)$, either $\varphi(x)\in p(x)$ or222The
asymmetric definition of maximality is due to the fact that $\mathcal{F}$ is
not closed under negations, so we cannot require $\neg\varphi(x)\in p(x)$.
$p(x)\rightarrow\neg\varphi(x)$.

The same holds for the types in $S_{\mathcal{H},x}(A)$ (in which case
maximality refers to $\mathcal{H}_{x}(A)$).

######  Proof 13.

Let $p(x)={\mathcal{F}}\mbox{-tp}(a/A)$, and pick any
$\varphi(x)\in\mathcal{F}(A)$. If $\varphi(x)\notin p(x)$ (i.e.
$\neg\varphi(a)$), then there is $\varphi^{\prime}>\varphi$ such that
$\neg\varphi^{\prime}(a)$ by Proposition 25. By Lemma 7(1) there is
$\tilde{\varphi}\perp\varphi$ such that
$\varphi\to\neg\tilde{\varphi}\to\varphi^{\prime}$. Thus $\tilde{\varphi}(a)$,
and so $p(x)\to\tilde{\varphi}(x)$ because $\tilde{\varphi}(x)\in p(x)$. Since
$\tilde{\varphi}\to\neg\varphi$, it follows that $p(x)\to\neg\varphi(x)$, as
desired.

###  7.1. Approximate elimination of quantifiers of sort S

In this subsection we show that the quantifiers of sort $S$ can be eliminated
at the cost of allowing approximations. In a classical setting, proving that
every complete type over a theory $T$ is equivalent to its quantifier-free
part amounts to proving quantifier elimination for $T$. Here we prove that, in
our setting, every complete ${\mathcal{F}}$-type is equivalent to its
restriction to ${\mathcal{H}}$. However, this equivalence does not imply that
every ${\mathcal{F}}$-formula is equivalent to an ${\mathcal{H}}$-formula:
given $\varphi\in\mathcal{F}$ and $\varphi^{\prime}>\varphi$, we can find
$\psi\in\mathcal{H}$ such that $\varphi\rightarrow\psi$, but we can only
obtain $\psi\to\varphi^{\prime}$ as a converse implication.

We say that a standard structure $M$ is _${\mathcal{H}}$ -homogeneous_ if
every ${\mathcal{H}}$-elementary map $f\colon M\to M$ of cardinality $<|M|$
extends to an automorphism of $M$. Notice that if $M$ is
$\omega$-$\mathcal{F}$-saturated, then one can equivalently consider
_approximate_ $\mathcal{H}$-elementary maps in the above definition. One could
also define a notion of $\mathcal{F}$-homogeneity: however, since
$\mathcal{H}\subseteq\mathcal{F}$ the latter would be a weaker notion. The
following result is thus the strongest we can expect.

######  Proposition 30.

The monster model (indeed, any $\mathcal{F}$-saturated standard structure) is
${\mathcal{H}}$-homogeneous.

######  Proof 14.

Let $f$ be a partial ${\mathcal{H}}$-elementary map such that
$|f|<|\mathcal{U}|$. We use a standard back-and-forth construction to extend
$f$ while maintaining $\mathcal{H}$-elementarity, until we get a total
surjective map, i.e. an automorphism of $M$.

We first show how to add a new element $b\in\mathcal{U}$ to the domain of $f$.
Let $B={\rm dom}f$ and let $p(x/B)={\mathcal{H}}\mbox{-tp}(b/B)$. By
$\mathcal{H}$-elementarity, the conjugate $\mathcal{H}$-type $p(x/f(B))$ is
finitely satisfiable in $\mathcal{U}$, hence it has a realisation $c$ by
saturation of $\mathcal{U}$. Then $f\cup\\{\langle b,c\rangle\\}$ is an
${\mathcal{H}}$-elementary extension of $f$.

To add an element to the range of $f$, we apply the same argument to $f^{-1}$.
This is possible because, as observed in Section 4, the map $f$ is injective,
hence invertible, and its inverse $f^{-1}$ is $\mathcal{H}$-elementary by
saturation and Propositions 10 and 25.

We now strengthen Proposition 29 by showing that consistent
$\mathcal{H}$-types are already complete with respect to the class of all
$\mathcal{L}_{x}(A)$-formulas. Recall that, throughout this section,
$A\subseteq\mathcal{U}$ is a fixed set with $|A|<|\mathcal{U}|$.

######  Corollary 31.

Let $p(x)\in S_{\mathcal{H},x}(A)$. Then $p(x)$ is complete for the formulas
in ${\mathcal{L}}_{x}(A)$. Namely, for every
$\varphi(x)\in{\mathcal{L}}_{x}(A)$, either $p(x)\rightarrow\varphi(x)$ or
$p(x)\rightarrow\neg\varphi(x)$.

Furthermore, $p^{\prime}(x)$ is also complete for the formulas in
${\mathcal{L}}_{x}(A)$.

######  Proof 15.

If $b\in\mathcal{U}$ is an arbitrary realization of
${\mathcal{H}}\mbox{-tp}(a/A)$, then the map $f$ which is the identity on $A$
and sends $a$ to $b$ is $\mathcal{H}$-elementary. By Proposition 30, such $f$
exends to an automorphism of $\mathcal{U}$. Since every automorphism is
${\mathcal{L}}$-elementary, the conclusion follows.

The last part of the statement follows from Proposition 25.

Let $a,b\in\mathcal{U}^{n}$. We write $a\equiv_{A}b$ if $a$ and $b$ satisfy
the same ${\mathcal{L}}(A)$-formulas in $n$ free variables. By Corollary 31,
formulas in ${\mathcal{H}}(A)$ or ${\mathcal{F}}(A)$, or their approximations,
suffice to test $\equiv_{A}$.

The next proposition shows that formulas in ${\mathcal{F}}(A)$ can be
approximated by formulas in ${\mathcal{H}}(A)$.

######  Proposition 32.

Let $\varphi(x)\in{\mathcal{F}}(A)$. For every $\varphi^{\prime}>\varphi$
there is some formula $\psi(x)\in{\mathcal{H}}(A)$ such that
$\varphi(x)\rightarrow\psi(x)\rightarrow\varphi^{\prime}(x)$.

######  Proof 16.

By Corollary 31

$\neg\varphi(x)\rightarrow\bigvee\big{\\{}p(x)\mathbin{:}p(x)\in
S_{\mathcal{H},x}(A)\text{ and }p(x)\rightarrow\neg\varphi(x)\Big{\\}},$

that is, for all $a\in\mathcal{U}^{|x|}$, if $\neg\varphi(a)$ then $p(a)$ for
some $p(x)\in S_{\mathcal{H},x}(A)$ with $p(x)\to\neg\varphi(x)$.

For each $p(x)\in S_{\mathcal{H},x}(A)$ such that $p(x)\to\neg\varphi(x)$ we
also have $p^{\prime}(x)\to\neg\varphi(x)$ by Proposition 25, hence by
Proposition 28(1) applied to $p^{\prime}(x)$ there is an approximation
$\chi^{\prime}_{p}(x)$ of some formula $\chi_{p}\in p(x)$ such that
$\chi^{\prime}_{p}(x)\rightarrow\neg\varphi(x)$. (Here we use the fact that
$p(x)$, and hence also $p^{\prime}(x)$, is closed under finite conjunctions.)

By applying Lemma 7(1) to $\chi_{p}<\chi_{p}^{\prime}$ we get a formula
$\psi_{p}$ such that $\psi_{p}\perp\chi_{p}$ and
$\chi_{p}\rightarrow\neg\psi_{p}\rightarrow\chi^{\prime}_{p}$. Note that
$\psi_{p}\perp\chi_{p}$ implies that $\psi_{p}$ is an $\mathcal{H}(A)$-formula
because so is $\chi_{p}$.

Hence

$\neg\varphi(x)\rightarrow\bigvee\big{\\{}\neg\psi(x)\mathbin{:}\psi(x)\in\mathcal{H}(A)\text{
and }\neg{\psi}(x)\rightarrow\neg\varphi(x)\\}$

or, equivalently, $q(x)\to\varphi(x)$, where
$q(x)\subseteq\mathcal{H}(A)\subseteq\mathcal{F}(A)$ is the type

$q(x)=\big{\\{}\psi(x)\mathbin{:}\psi(x)\in\mathcal{H}(A)\text{ and
}{\varphi(x)}\rightarrow{\psi}(x)\\}.$

By applying Proposition 28(2) to $q(x)$, we get that for every
$\varphi^{\prime}>\varphi$ there are finitely many
${\psi}_{1}(x),\dotsc,\psi_{n}(x)\in q(x)$ such that $\bigwedge_{1\leq i\leq
n}{\psi}_{i}(x)\to\varphi^{\prime}(x)$. But since $\psi_{i}(x)\in q(x)$ we
also have $\varphi(x)\to\psi_{i}(x)$ for every $1\leq i\leq n$, thus

$\varphi(x)\to\bigwedge_{1\leq i\leq n}{\psi}_{i}(x)\to\varphi^{\prime}(x)$

and the middle conjunction is the required $\mathcal{H}(A)$-formula $\psi(x)$.

We also prove an approximation result for the negation of formulas in
${\mathcal{F}}(A)$.

######  Proposition 33.

Let $\varphi(x)\in{\mathcal{F}}(A)$ be such that $\neg\varphi(x)$ is
consistent. Then there is a consistent formula $\psi(x)\in{\mathcal{H}}(A)$
such that $\psi^{\prime}(x)\rightarrow\neg\varphi(x)$ for some
$\psi^{\prime}>\psi$.

######  Proof 17.

Let $a\in\mathcal{U}^{|x|}$ be such that $\neg\varphi(a)$, and let
$p(x)={\mathcal{H}}\mbox{-tp}(a/A)$. By Corollary 31,
$p^{\prime}(x)\rightarrow\neg\varphi(x)$. By Proposition 28(1) applied to
$p^{\prime}(x)$, there is some $\psi^{\prime}(x)\in p(x)$ such that
$\psi^{\prime}(x)\rightarrow\neg\varphi(x)$. (Here we use again that
$p^{\prime}(x)$ is closed under finite conjunctions.) By definition of
$p^{\prime}(x)$, $\psi^{\prime}>\psi$ for some $\psi(x)\in
p(x)\subseteq\mathcal{H}(A)$, and $\psi(x)$ is consistent because it is
realized by $a$.

###  7.2. The Tarski-Vaught Test and the Löwenheim-Skolem Theorem

The following proposition can be regarded as an analogue of the Tarski-Vaught
Test when the larger structure is the monster model.

######  Proposition 34.

The following are equivalent for a subset $M$ of $\mathcal{U}$.

  1. (1)

$M$ is the domain of a model, i.e. $M$ is an $\mathcal{F}$-elementary standard
substructure of $\mathcal{U}$ when equipped with the restriction of the
interpretations in $\mathcal{U}$ of the symbols of $\mathcal{L}$;

  2. (2)

for every formula $\varphi(x)\in{\mathcal{H}}(M)$ without free variables of
sort $\sf S$,

$\exists x\,\varphi(x)\quad\Rightarrow\quad\text{ for every
}\varphi^{\prime}>\varphi\text{ there is }a\in M\text{ such that
}\varphi^{\prime}(a);$

  3. (3)

for every formula $\varphi(x)\in{\mathcal{F}}(M)$ without free variables of
sort $\sf S$,

$\exists x\,\neg\varphi(x)\quad\Rightarrow\quad\text{ there is }a\in M\text{
such that }\neg\varphi(a).$

######  Proof 18.

(1) $\Rightarrow$ (2). Assume that $\exists x\,\varphi(x)$, and let
$\varphi^{\prime}>\varphi$. By Lemma 7(1) there is some
$\tilde{\varphi}\perp\varphi$ such that
$\varphi(x)\rightarrow\neg\tilde{\varphi}(x)\rightarrow\varphi^{\prime}(x)$.
Then $\neg\forall x\,\tilde{\varphi}(x)$ and so, by part (1),
$M\models\neg\forall x\,\tilde{\varphi}(x)$. Then
$M\models\neg\tilde{\varphi}(a)$ for some $a\in M$. Hence
$M\models\varphi^{\prime}(a)$, and $\varphi^{\prime}(a)$ follows by (1) again.

(2) $\Rightarrow$ (3). Assume that $\exists x\,\neg\varphi(x)$. By Proposition
33, there are a consistent formula $\psi(x)\in{\mathcal{H}}(M)$ and an
approximation $\psi^{\prime}$ of $\psi$ such that
$\psi^{\prime}(x)\rightarrow\neg\varphi(x)$. Since $\exists x\,\psi(x)$, by
(2) there is $a\in M$ such that $\psi^{\prime}(a)$, hence $\neg\varphi(a)$ and
(3) is verified.

(3) $\Rightarrow$ (1). Recall that $\mathcal{L}_{\sf
H}(M)\subseteq{\mathcal{H}}(M)$. Then by (3) it is easy to see that $M$ is
closed under the interpretations of the constant and the function symbols in
$\mathcal{L}_{\sf H}(M)$. Hence $M$ is the domain of an ${\mathcal{L}_{\sf
H}}$-substructure of $\mathcal{U}$. By (3) and the classical Tarski-Vaught
test, $M\preceq^{\mathcal{L}_{\sf H}}\mathcal{U}$. This also implies that
$\langle M,X\rangle$ is an $\mathcal{L}$-substructure of
$\langle\mathcal{U},X\rangle$, which means that $t^{M}(a)=t(a)$ for all
$\mathcal{L}$-terms $t(x)$ and $a\in M^{|x|}$. Therefore, for every
${\mathcal{F}}$-atomic formula $\varphi(x)$ and every $a\in M^{|x|}$

$M\models\varphi(a)\quad\Leftrightarrow\quad\varphi(a).$

For the inductive step, consider the ${\mathcal{F}}$-formula $\forall
y\,\varphi(x,y)$. The inductive assumption is that, for all $a\in M^{|x|}$ and
all $b\in M^{|y|}$, if ${M\models\varphi(a,b)}$ then ${\varphi(a,b)}$. We
prove by contraposition that if $M\models\forall y\,\varphi(a,y)$ then
$\forall y\,\varphi(a,y)$. Indeed, using (3) in the second step gives

$\displaystyle\neg\forall y\,\varphi(a,y)\quad$
$\displaystyle\Rightarrow\quad\exists y\,\neg\varphi(a,y)$
$\displaystyle\Rightarrow\quad\neg\varphi(a,b)$ $\displaystyle\text{for some
}b\in M^{|y|}$ $\displaystyle\Rightarrow\quad M\not\models\varphi(a,b)$
$\displaystyle\text{for some }b\in M^{|y|}$ $\displaystyle\Rightarrow\quad
M\not\models\forall y\,\varphi(a,y).$

The inductive steps for the connectives $\vee$, $\wedge$ and the quantifiers
$\exists\raisebox{4.73611pt}{\scaleto{\sf H}{.8ex}\kern-0.86108pt}$,
$\exists\raisebox{4.73611pt}{\scaleto{\sf S}{.8ex}\kern-0.86108pt}$, and
$\forall\raisebox{4.73611pt}{\scaleto{\sf S}{.8ex}\kern-0.86108pt}$ are
straightforward.

In the classical setting, an important application of the Tarski-Vaught Test
is in the proof of the Downward Löwenheim-Skolem Theorem. In our setting, the
latter holds for arbitrary ${\mathcal{L}}$-structures; in particular, every
subset $A$ of ${\mathcal{U}}$ is contained in a model of cardinality at most
$|{\mathcal{L}}(A)|$. However, in the latter form the Löwenheim-Skolem Theorem
is not very informative because of the potentially large cardinality of
$\mathcal{L}_{\sf S}$. To prove a more meaningful result, we introduce the
notion of _separable_ language.

######  Definition 35.

A language ${\mathcal{L}}$ is _separable_ if there is a countable subset
$\mathcal{F}_{0}$ of ${\mathcal{F}}$ such that for all $\varphi\in\mathcal{F}$
and all $\varphi^{\prime}>\varphi$ there exists
$\varphi_{0}\in\mathcal{F}_{0}$ such that
$\varphi\rightarrow\varphi_{0}\rightarrow\varphi^{\prime}$.

######  Proposition 36.

Assume that ${\mathcal{L}}$ is a separable language. Let
$A\subseteq{\mathcal{U}}$ be countable. Then there is a countable model $M$
containing $A$.

######  Proof 19.

As in the classical proof of the Löwenheim-Skolem Theorem, construct a
countable subset $M$ of ${\mathcal{U}}$ that contains $A$ and a realization of
every consistent formula in ${\mathcal{F}}_{0}(M)$, where $\mathcal{F}_{0}$
witnesses the separability of $\mathcal{L}$. By the equivalence (1)$\iff$(2)
in Proposition 34, $M$ is a model.

The following result provides a sufficient condition for the separability of
${\mathcal{L}}$.

######  Proposition 37.

Let $X$ be second-countable. If ${\mathcal{L}}\setminus{\mathcal{L}}_{\sf S}$
is countable, then ${\mathcal{L}}$ is separable.

######  Proof 20.

For each $n\geq 1$ fix a countable basis ${\mathcal{B}}_{n}$ for $X^{n}$, and
let ${\mathcal{D}}_{n}$ be the collection of those sets which are the closure
of a finite union of elements of ${\mathcal{B}}_{n}$. Set also
${\mathcal{D}}=\bigcup_{n\geq 1}{\mathcal{D}}_{n}$. For every closed
$C\subseteq X^{n}$ and every open set $U\supseteq C$ there is a closed
neighborhood $D\in{\mathcal{D}}_{n}$ of $C$ such that $D\subseteq U$. Indeed,
by normality of $X$ there is a closed neighborhood $E$ of $C$ such that
$E\subseteq U$. By compactness of $C$, there is a finite subfamily of
${\mathcal{B}}_{n}$ whose union $V$ satisfies $C\subseteq V\subseteq E$. The
closure $D$ of $V$ is as desired.

Since $X$ is Hausdorff, second-countable and regular, it is metrizable by the
Urysohn Metrization Theorem, and hence completely metrizable because of
compactness. Thus for $k\geq 1$ the space $C(X^{k},X)$ of (uniformly)
continuous functions $f\colon X^{k}\to X$ is a completely metrizable separable
(i.e. Polish) space when equipped with the topology generated by the
neighborhoods of $f\in C(X^{k},X)$ given by

$\\{g\in C(X^{k},X)\mid\forall x\in X^{k}\,d(f(x),g(x))<\varepsilon\\},$

where $\varepsilon$ varies over positive reals and $d$ is any fixed (complete)
metric on $X$ compatible with its topology. (See e.g. [Kec, Theorem 4.19].)
Let ${\mathcal{G}}_{k}=\\{f^{(k)}_{n}\mid n\in\omega\\}$ be dense in
$C(X^{k},X)$ and let ${\mathcal{G}}=\bigcup_{k\geq 1}{\mathcal{G}}_{k}$.

Let ${\mathcal{F}}_{0}\subseteq{\mathcal{H}}$ be the set of
${\mathcal{F}}$-formulas $\varphi$ such that:

  1. (1)

if $t$ is a term occurring in $\varphi$, then all functions of sort ${\sf
S}^{k}\to{\sf S}$ appearing in $t$ belong to ${\mathcal{G}}$;

  2. (2)

if an atomic formula $t\in D$ occurs in $\varphi$, then $D\in{\mathcal{D}}$.

We claim that ${\mathcal{F}}_{0}$ witnesses that ${\mathcal{L}}$ is separable.
Clearly, ${\mathcal{F}}_{0}$ is countable because so are ${\mathcal{G}}$,
${\mathcal{D}}$, and ${\mathcal{L}}\setminus{\mathcal{L}}_{\sf S}$.

######  Claim 37.1.

For every term $t(x\,;\eta)$ of sort ${\sf H}^{|x|}\times{\sf
S}^{|\eta|}\to{\sf S}$ and every positive real $\varepsilon$ there is a term
$t^{\prime}(x\,;\eta)$ of the same sort satisfying (1) and such that
$d(t(a\,;\alpha),t^{\prime}(a\,;\alpha))<\varepsilon$ for any standard
structure $M$, $a\in M^{|x|}$, and $\alpha\in X^{|\eta|}$.

######  Proof 21 (of the claim).

By induction on the complexity of $t$. The only nontrivial case is when $t$ is
of the form $f(t_{1},\dotsc,t_{n})$ with $f$ of sort ${\sf S}^{n}\to{\sf S}$,
so that each $t_{i}$ is of sort ${\sf H}^{|x|}\times{\sf S}^{|\eta|}\to{\sf
S}$. Since $f$ is uniformly continuous, there is $\delta$ such that for all
$\alpha,\beta\in X^{n}$, if $d_{n}(\alpha,\beta)<\delta$, where $d_{n}$
denotes the sup metric on the product $X^{n}$, then
$d(f(\alpha),f(\beta))<\varepsilon/2$. By inductive hypothesis, for each
$t_{i}$ choose $t^{\prime}_{i}$ satisfying (1) and such that
$d(t_{i}(a\,;\alpha),t^{\prime}_{i}(a\,;\alpha))<\delta$ for any standard
structure $M$, $a\in M^{|x|}$, and $\alpha\in X^{|\eta|}$. Let also
$f^{\prime}\in{\mathcal{G}}$ be of sort ${\sf S}^{n}\to{\sf S}$ and such that
$d(f(\alpha),f^{\prime}(\alpha))<\varepsilon/2$ for all $\alpha\in X^{n}$.
Finally, let $t^{\prime\prime}$ be the term
$f(t^{\prime}_{1},\dotsc,t^{\prime}_{n})$ and $t^{\prime}$ be the term
$f^{\prime}(t^{\prime}_{1},\dotsc,t^{\prime}_{n})$. Clearly, $t^{\prime}$
satisfies (1). Let $M$ be a standard structure, and fix any $a\in M^{|x|}$ and
$\alpha\in X^{|\eta|}$. Then by the choice of the $t^{\prime}_{i}$ and of
$\delta$, we have
$d(t(a\,;\alpha),t^{\prime\prime}(a\,;\alpha))<\varepsilon/2$. On the other
hand, by the choice of $f^{\prime}$ we also have
$d(t^{\prime\prime}(a\,;\alpha),t^{\prime}(a\,;\alpha))<\varepsilon/2$. Thus
$d(t(a\,;\alpha),t^{\prime}(a\,;\alpha))<\varepsilon$ by the triangle
inequality, and we are done.

Given a closed set $C\subseteq X^{n}$ and a positive real $\varepsilon$, the
$\varepsilon$-enlargement $C_{\varepsilon}$ of $C$ is the open set constituted
by the union of all the open $d_{n}$-balls with radius $\varepsilon$ and
center in $C$.

######  Claim 37.2.

For every closed set $C\subseteq X^{n}$ and every closed neighborhood $D$ of
$C$ there is some positive real $\varepsilon$ such that
$C_{\varepsilon}\subseteq D$.

######  Proof 22 (of the claim).

Suppose towards a contradiction that for every $m\in\omega$ there is
$\alpha_{m}\in C$ and $\beta_{m}\in X^{n}\setminus D$ such that
$d_{n}(\alpha_{m},\beta_{m})<1/m$. Since $C$ is compact, by passing to a
subsequence we can assume that the points $\alpha_{m}$ converge to some
$\alpha\in C$. But then there is no open neighborhood of $\alpha$ contained in
$D$, contradicting the fact that $D$ is a closed neighborhood of $C$. Indeed,
for every positive real $\delta$ one can pick $m$ large enough so that
$d_{n}(\alpha_{m},\alpha)<\delta/2$ and $1/m<\delta/2$. Then
$d_{n}(\beta_{m},\alpha)\leq
d_{n}(\beta_{m},\alpha_{m})+d_{n}(\alpha_{m},\alpha)<\delta$, and so the ball
centered in $\alpha$ with radius $\delta$ is not contained in $D$.

Fix now arbitrary formulas $\varphi\in{\mathcal{F}}$ and
$\varphi^{\prime}>\varphi$. By induction on the complexity of $\varphi$, we
show that there is $\varphi_{0}\in{\mathcal{F}}_{0}$ such that
$\varphi\to\varphi_{0}\to\varphi^{\prime}$.

If $\varphi$ is an ${\mathcal{L}}_{\sf H}$-formula, then we can let
$\varphi_{0}$ be $\varphi$ itself. Assume now that $\varphi$ is of the form
$t(x\,;\eta)\in C$, for $C\subseteq X^{n}$ closed and $t(x\,;\eta)$ an
$n$-tuple of terms $t_{i}(x\,;\eta)$ each of sort ${\sf H}^{|x|}\times{\sf
S}^{|\eta|}\to{\sf S}$. The approximation $\varphi^{\prime}$ is then of the
form $t(x\,;\eta)\in D$, for some closed neighborhood $D$ of $C$. By Claim
37.2 there is a positive real $\varepsilon_{0}$ such that
$C_{2\varepsilon_{0}}\subseteq D$. Pick a closed neighborhood
$D^{\prime}\in{\mathcal{D}}$ of $C$ such that $D^{\prime}\subseteq
C_{\varepsilon_{0}}$. Applying Claim 37.2 again, let $\varepsilon_{1}$ be such
that $C_{\varepsilon_{1}}\subseteq D^{\prime}$, and set
$\varepsilon=\min\\{\varepsilon_{0},\varepsilon_{1}\\}$. Finally, pick terms
$t^{\prime}_{i}(x\,;\eta)$ as in Claim 37.1 applied to $t_{i}(x\,;\eta)$ and
the chosen $\varepsilon$. Let $\varphi_{0}\in{\mathcal{F}}_{0}$ be the formula
$t^{\prime}(x\,;\eta)\in D^{\prime}$, where $t^{\prime}(x\,;\eta)$ is the the
$n$-tuple given by the terms $t^{\prime}_{i}(x\,;\eta)$. Fix a standard
structure $M$ and pick arbitrary $a\in M^{|x|}$ and $\alpha\in X^{|\eta|}$. If
$t(a\,;\alpha)\in C$, then $t^{\prime}(a\,;\alpha)\in C_{\varepsilon}\subseteq
D^{\prime}$ by choice of $t^{\prime}$ and $\varepsilon\leq\varepsilon_{1}$:
this proves $\varphi\to\varphi_{0}$. Similarly, if $t^{\prime}(a\,;\alpha)\in
D^{\prime}$, then there is $\beta\in C$ such that
$d_{n}(t^{\prime}(a\,;\alpha),\beta)<\varepsilon_{0}$ by $D^{\prime}\subseteq
C_{\varepsilon_{0}}$, and thus by choice of $t^{\prime}$ and
$\varepsilon\leq\varepsilon_{0}$ we also have $d_{n}(t(a\,;\alpha),\beta)\leq
d_{n}(t(a\,;\alpha),t^{\prime}(a\,;\alpha))+d_{n}(t^{\prime}(a\,;\alpha),\beta)<2\varepsilon_{0}$,
so that $t(a\,;\alpha)\in C_{2\varepsilon_{0}}\subseteq D$ and we are done.

The inductive steps for $\wedge$, $\vee$, $\exists^{\sf H}$, $\forall^{\sf
H}$, $\exists\raisebox{4.73611pt}{\scaleto{\sf S}{.8ex}\kern-0.86108pt}$, and
$\forall\raisebox{4.73611pt}{\scaleto{\sf S}{.8ex}\kern-0.86108pt}$ are easy.

###  7.3. Cauchy complete models

In this section we introduce abstract model-theoretic versions of some notions
that arise naturally in the realm of (pseudo)metric spaces. Our choice of
terminology will be justified in Section 7.4.

Let $t(x,z)$ be a parameter-free term of sort ${\sf H}^{|x|+|z|}\to{\sf S}$
with $|z|$ finite, and let $y$ be a tuple of the same length as $x$. We write
$x\sim_{t}y$ as an abbreviation for the formula $\forall z\,\ \langle
t(x,z),t(y,z)\rangle\in\Delta$, where $\Delta$ is the diagonal in $X\times X$.
By an abuse of notation, we also write $\forall z\,\ t(x,z)=t(y,z)$. We let
$x\sim_{\sf S}y$ be the type

$\left\\{x\sim_{t}y\mathbin{:}t(x,z)\text{ is a term of sort }{\sf
H}^{|x|+|z|}\to{\sf S}\text{ and }|z|\in\omega\right\\}.$

######  Proposition 38.

For all natural numbers $n\geq 1$ and all $a=\langle a_{i}\rangle_{1\leq i\leq
n}$, $b=\langle b_{i}\rangle_{1\leq i\leq n}$ in $\mathcal{U}^{n}$

($\sharp$) $a\sim_{\sf S}b\quad\Leftrightarrow\quad a_{i}\sim_{\sf
S}b_{i}\text{\ \ \ \ \ for all }1\leq i\leq n.$

######  Proof 23.

The left-to-right implication is straightforward. For the converse
implication, we proceed by induction on $n\geq 1$. The case $n=1$ is obvious.
For the inductive step, we assume that ($\sharp$ ‣ 38) holds for any two
sequences of length up to $n$, and we prove the equivalence for an arbitrary
pair of tuples $\langle a_{i}\rangle_{1\leq i\leq n+1}$, $\langle
b_{i}\rangle_{1\leq i\leq n+1}$ satisfying $a_{i}\sim_{\sf S}b_{i}$ for all
$1\leq i\leq n+1$. The inductive hypothesis gives

$\forall y,z\;\;t\big{(}\langle a_{i}\rangle_{1\leq i\leq
n},y,z\big{)}=t\big{(}\langle b_{i}\rangle_{1\leq i\leq n},y,z\big{)}$

for every term $t(x,y,z)$ with $|x|=n$, $|y|=1$, and $|z|\in\omega$. In
particular

(1) $\forall z\;\;t\big{(}\langle a_{i}\rangle_{1\leq i\leq
n},a_{n+1},z\big{)}=t\big{(}\langle b_{i}\rangle_{1\leq i\leq
n},a_{n+1},z\big{)}.$

By assumption $a_{n}\sim_{\sf S}b_{n}$, so

$\forall x,z\;\;t\big{(}x,a_{n+1},z\big{)}=t\big{(}x,b_{n+1},x\big{)},$

and in particular

(2) $\forall z\;\;t\big{(}\langle b_{i}\rangle_{1\leq i\leq
n},a_{n+1},z\big{)}=t\big{(}\langle b_{i}\rangle_{1\leq i\leq
n},b_{n+1},z\big{)}.$

Finally, from (1) and (2) we get

$\forall z\;t\big{(}\langle a_{i}\rangle_{1\leq i\leq
n+1},z\big{)}=t\big{(}\langle b_{i}\rangle_{1\leq i\leq n+1},z\big{)}.$

From now on we assume $|x|=|y|=n$ and $|z|\in\omega$. The approximations
$x\sim^{\prime}_{t}y$ of $x\sim_{t}y$ have the form

$\forall z\,\langle t(x,z),t(y,z)\rangle\in D$

for a closed neighborhood $D$ of $\Delta$, and will be denoted by
$x\sim_{t,D}y$. We let $\sim^{\prime}_{\sf S}$ be the approximation of the
type $\sim_{\sf S}$, namely, the set of formulas

$\left\\{x\sim_{t,D}y\mathbin{:}t(x,z)\text{ and }D\text{ are as
above}\right\\}.$

######  Remark 39.

For all tuples of variables $x,y$ of the same length

$x\sim_{\sf S}y\quad\Leftrightarrow\quad x\sim^{\prime}_{\sf S}y.$

This equivalence is an instantiation of Proposition 25, and holds in every
sufficiently saturated structure. However, the following topological argument
shows that, for the specific types under consideration, the equivalence holds
even without any saturation assumptions. The left-to-right implication is
trivial. The converse implication can be proved by contraposition and is a
consequence of the normality of $X$. For assume $\langle r,s\rangle\in
X^{2}\setminus\Delta$. Since both $\\{\langle r,s\rangle\\}$ and $\Delta$ are
closed sets, there are disjoint open neighborhoods $W_{1}$ and $W_{2}$ of
$\\{\langle r,s\rangle\\}$ and $\Delta$, respectively. The complement of
$W_{1}$ is a closed neighborhood of $\Delta$ that does not contain $\langle
r,s\rangle$.

We now show that the formulas $x\sim_{t,D}y$ yield a subbase of a natural
uniformity on $\mathcal{U}^{n}$. For this, we first need to close the family
of truth sets of such formulas under intersections. To simplify the notation,
if $t(x,z)=\langle t_{1}(x,z),\dotsc,t_{k}(x,z)\rangle$ is a tuple of terms
and $D=\langle D_{1},\dotsc,D_{k}\rangle$ is a tuple of closed neighborhoods
of $\Delta$, we denote by $x\sim_{t,D}y$ the conjunction $\bigwedge_{1\leq
i\leq k}x\sim_{t_{i},D_{i}}y$. This notation is well behaved with respect to
concatenation: if $t(x,z)$ is the concatenation of the tuple of terms
$t_{1}(x,z),t_{2}(x,z)$ and $D$ is the concatenation of the tuples of closed
neighborhoods $D_{1},D_{2}$ of $\Delta$ (of the appropriate length), then
$x\sim_{t_{1},D_{1}}y\wedge x\sim_{t_{2},D_{2}}y\leftrightarrow x\sim_{t,D}y$.
As $k$ ranges over the positive natural numbers and $t$ and $D$ range over the
$k$-tuples of terms and the $k$-tuples of closed neighborhoods of $\Delta$,
respectively, the formulas $x\sim_{t,D}y$ define a family $\mathcal{B}_{n}$ of
subsets of $\mathcal{U}^{n}\times\mathcal{U}^{n}$.

######  Lemma 40.

$\mathcal{B}_{n}$ is a base for a uniformity $\widehat{U}_{n}$ on
$\mathcal{U}^{n}$.

######  Proof 24.

By definition, each element of $\mathcal{B}_{n}$ contains the diagonal of
$\mathcal{U}^{n}\times\mathcal{U}^{n}$. Furthermore, for all
$X,Y\in\mathcal{B}_{n}$, we have that $X\cap Y$ belongs to $\mathcal{B}_{n}$
by the observation above on concatenation. Also, for each
$X\in\mathcal{B}_{n}$ its inverse $X^{-1}$ belongs to $\mathcal{B}_{n}$, since
for $E\subseteq X\times X$ we have that $E$ is a closed neighborhood of
$\Delta$ if and only if so is $E^{-1}$; hence if $X$ is defined by
$x\sim_{t,D}y$ then $X^{-1}$ is defined by $x\sim_{t,D^{-1}}y$, where $D^{-1}$
is the tuple obtained by replacing each entry $D_{i}$ of $D$ with
$D_{i}^{-1}$.

In order to conclude that $\mathcal{B}_{n}$ is a base for a uniformity
${\widehat{U}}_{n}$ on $\mathcal{U}^{n}$, it remains to prove that, for each
$V\in\mathcal{B}_{n}$, there exists $W\in\mathcal{B}_{n}$ such that $W\circ
W\subseteq V$. Assume first that $V$ is defined by $x\sim_{t,D}y$, for a
single term $t$ and a closed neighborhood $D$ of $\Delta$. Let $O$ be an open
neighborhood of $\Delta$ such that $\Delta\subseteq O\subseteq D$. Since $X$
is compact Hausdorff, it is also divisible, i.e. there is a (symmetric) open
neighborhood $E$ of $\Delta$ such that $E\circ E\subseteq O\subseteq D$. By
normality of $X$, there exists a closed neighborhood $F$ of $\Delta$ such that
$\Delta\subseteq F\subseteq E$, so that still $F\circ F\subseteq D$. It
follows that the set $W$ defined by $x\sim_{t,F}y$ is such that $W\circ
W\subseteq V$.

For the general case, let $V$ be the set defined by $x\sim_{t,D}y$, where
$t=\langle t_{1},\dotsc,t_{k}\rangle$ is a tuple of terms and $D=\langle
D_{1},\dotsc,D_{k}\rangle$ is a tuple of neighborhoods of $\Delta$. Note that
$V=\bigcap_{1\leq i\leq k}V_{i}$, where each $V_{i}$ is the set defined by
$x\sim_{t_{i},D_{i}}y$. By the previous paragraph, for each $1\leq i\leq k$ we
get a set $W_{i}$ defined by $x\sim_{t_{i},F_{i}}y$ such that $W_{i}\circ
W_{i}\subseteq V_{i}$. Let $F=\langle F_{1},\dotsc,F_{k}\rangle$. Then the set
$W=W_{1}\cap\ldots\cap W_{k}$ defined by $x\sim_{t,F}y$ is such that $W\circ
W\subseteq V$.

The uniformity ${\widehat{U}}_{n}$ defines a topology on $\mathcal{U}^{n}$
which we call the _${\sf S}$ -topology_. Though not needed in what follows, it
is worth mentioning that the ${\sf S}$-topology on $\mathcal{U}^{n}$ coincides
with the $n$-th product of the ${\sf S}$-topology on $\mathcal{U}$. This is
because, by Proposition 38, the $n$-fold product uniformity of
${\widehat{U}}_{1}$ is exactly ${\widehat{U}}_{n}$, and it is a known result
that the same property is inherited by the associated topologies.

######  Definition 41.

We say that a type $p(x)\subseteq{\mathcal{F}}(\mathcal{U})$ is _$\sim_{\sf
S}$ -invariant_ if the set defined by $p(x)$ is invariant with respect to the
equivalence relation defined by $x\sim_{\sf S}y$, i.e. if it is true that
$x\sim_{\sf S}y\rightarrow(p(x)\leftrightarrow p(y))$. A formula $\varphi(x)$
is $\sim_{\sf S}$-invariant if so is the type $\\{\varphi(x)\\}$.

By the remark preceding Proposition 38, it is easy to see that all formulas
not containing any $\mathcal{L}_{\sf H}$-formula as a subformula are
$\sim_{\sf S}$-invariant.

The following proposition can be regarded as a formulation of the Perturbation
Lemma [HI, Proposition 5.15].

######  Proposition 42.

For each formula $\varphi(x)\in{\mathcal{F}}(\mathcal{U})$, the following are
equivalent:

  1. (1)

$\varphi(x)$ is _$\sim_{\sf S}$_ -invariant;

  2. (2)

for every $\varphi^{\prime}>\varphi$ there are tuples $t$ and $D$ such that

${{x\sim_{t,D}y}\wedge\varphi(x)}\ \to\ \varphi^{\prime}(y).$

######  Proof 25.

(1) $\Rightarrow$ (2). Fix any $\varphi^{\prime}>\varphi.$ By (1) and Remark
39, we obtain ${{x\sim^{\prime}_{\rm S}y}\wedge\varphi(x)}\,\to\,\varphi(y)$.
Applying Proposition 28(2) gives (2).

(2) $\Rightarrow$ (1). Since ${x\sim_{\sf S}y}\leftrightarrow{y\sim_{\sf
S}x}$, it is enough to show that $x\sim_{\sf S}y\to(\varphi(x)\to\varphi(y))$.
Fix any $a,b\in\mathcal{U}^{|x|}$ such that $a\sim_{\sf S}b$ and $\varphi(a)$.
For each $\varphi^{\prime}>\varphi$, fix $t$ and $D$ as in (2). Since
$x\sim_{t,D}y$ is a conjunction of formulas in $x\sim^{\prime}_{\sf S}y$, by
Remark 39 we have $a\sim_{t,D}b$, and hence $\varphi^{\prime}(b)$ by choice of
$t$ and $D$. By Proposition 25, we conclude that $\varphi(b)$ holds.

######  Remark 43.

Let $M$ be a model and let $q(x)\subseteq{\mathcal{F}}(M)$ be a consistent
type. Unlike the classical setting, if $M$ is not sufficiently saturated we
cannot infer that $q(x)$ is finitely satisfiable in $M$, but only that
$q^{\prime}(x)$ is finitely satisfiable in $M$. Indeed, we may assume that
$q(x)$ is closed under conjunctions. Given $\psi(x)\in q(x)$ we can apply
Proposition 10 to $\exists x\,\psi(x)$ and obtain that $\psi^{\prime}(x)$ is
satisfiable in $M$ for each $\psi^{\prime}>\psi$, as desired. If instead $M$
is $\omega$-$\mathcal{F}$-saturated, than we also have that each formula
$\psi(x)\in q(x)$ is satisfiable in $M$. In fact, by the previous argument the
set $\\{\psi\\}^{\prime}=\\{\psi^{\prime}\mathbin{:}\psi^{\prime}>\psi\\}$ is
finitely satisfiable in $M$, and it contains only finitely many parameters
from $M$. Hence $\\{\psi\\}^{\prime}$ is satisfiable in $M$ by
$\omega$-$\mathcal{F}$-saturation and, by Proposition 25, so is $\psi(x)$. The
same proof shows that if a satisfiable type $q(x)$ contains only finitely many
parameters from $M$, then it is realized in $M$.

######  Definition 44.

Let $A\subseteq\mathcal{U}$. We say that $p(x)\subseteq{\mathcal{F}}(A)$ is a
_Cauchy type_ if it is consistent and $p(x)\wedge
p(y)\,\rightarrow\,x\sim_{\sf S}y$.

######  Lemma 45.

For every model $M$ and every type $p(x)\subseteq{\mathcal{F}}(M)$, the
following are equivalent:

  1. (1)

$p(x)$ is a $\sim_{\sf S}$-invariant Cauchy type;

  2. (2)

$p(x)$ is consistent, and $p(x)\leftrightarrow x\sim_{\sf S}a$ for each $a\in
p(\mathcal{U})$.

######  Proof 26.

(1) $\Rightarrow$ (2). Since $p(x)$ is a Cauchy type, it is in particular
consistent. Fix any $a\in p(\mathcal{U})$. Substituting $a$ for $y$ in the
definition of Cauchy type gives $p(x)\rightarrow x\sim_{\sf S}a$. The converse
implication follows from $p(a)$ and the $\sim_{\sf S}$-invariance of $p(x)$.

(2) $\Rightarrow$ (1). Fix any $a\in p(\mathcal{U})$. From $p(x)\wedge p(y)$,
we can derive $x\sim_{\sf S}a\wedge y\sim_{\sf S}a$ by (2). Since the type
$z\sim_{\sf S}w$ defines an equivalence relation, we conclude that $x\sim_{\sf
S}y$. This shows that $p(x)$ is Cauchy. To show that it is also $\sim_{\sf
S}$-invariant, assume that $x\sim_{\sf S}y$ and $p(x)$. From (2), we get
$x\sim_{\sf S}y\wedge x\sim_{\sf S}a$. Hence $y\sim_{\sf S}a$, and so $p(y)$
by (2) again.

######  Definition 46.

We say that a set $A\subseteq\mathcal{U}$ is _Cauchy complete_ if every
$\sim_{\sf S}$-invariant Cauchy type $p(x)\subseteq{\mathcal{F}}(A)$ is
realized by some tuple in $A^{|x|}$.

######  Proposition 47.

Let $\lambda>|{\mathcal{L}}|$ and let $M$ be a
$\lambda$-${\mathcal{F}}$-saturated model. Then $M$ is Cauchy complete.

######  Proof 27.

Let $a\in\mathcal{U}^{|x|}$ be a realization of the $\sim_{\sf S}$-invariant
Cauchy type $p(x)\subseteq{\mathcal{F}}(M)$. We may assume that $p(x)$ is
closed under conjunction. By Lemma 45 we have $p(x)\leftrightarrow x\sim_{\sf
S}a$. By Proposition 28(2), for every formula $\varphi(x)$ in the type
$x\sim_{\sf S}a$ and every $\varphi^{\prime}>\varphi$ we can pick $\psi(x)\in
p(x)$ such that $\psi(x)\rightarrow\varphi^{\prime}(x)$. Let $q(x)\subseteq
p(x)$ be the type consisting of all such formulas $\psi(x)$. By Remark 43 and
saturation of $M$, any finite conjunction of formulas in $q(x)$ is satisfiable
in $M$ . As there are at most $|{\mathcal{L}}|$ formulas in $x\sim_{\sf S}a$,
the type $q(x)$ uses less than $\lambda$ parameters from $M$, hence by
$\lambda$-$\mathcal{F}$-saturation of $M$ the type $q(x)$ is realized in $M$
by some $b\in M^{|x|}$. Then $b\sim_{\sf S}^{\prime}a$ by definition of
$q(x)$, so $b\sim_{\sf S}a$ by Remark 39. By $\sf S$-invariance of $p(x)$, we
get that $b\in M^{|x|}$ is a realization of $p(x)$.

By Corollary 26 and $\lambda$-$\mathcal{F}$-saturation of $M$, we actually get
that the element $b\in M^{|x|}$ from the end of the above proof actually
_realizes $p(x)$ in $M$_ (and not only in $\mathcal{U}$).

Moreover, when $\mathcal{L}$ is separable it suffices to require
$\lambda>\omega$ in the statement of Proposition 47.

###  7.4. Example: bounded metric spaces

Let $X=[0,1]$ be the real unit interval, equipped with the standard topology.
Let $\langle M,d\rangle$ be a metric space with $d\colon M^{2}\to X$. For each
$n>1$ we also denote by $d$ the supremum metric on $M^{n}$.

Let $\mathcal{L}$ be a language containing a symbol for $d$, and possibly for
some relations on $M$ and some uniformly continuous functions from $M^{n}$ to
$M$ or from $M^{n}$ to $X$. Let $\langle M,X\rangle$ be the standard structure
that interprets the symbols of $\mathcal{L}$ in the natural way.

For the rest of this section, we fix a monster model
$M\preccurlyeq^{\mathcal{F}}\mathcal{U}$ obtained from $M$ as in the proof of
Theorem 24. In general, $d\colon M^{2}\rightarrow X$ does not extend to a
metric on $\mathcal{U}$. For example, if $d$ takes arbitrarily small positive
values, by compactness we can find in $\mathcal{U}$ pairs of distinct elements
at distance $0$ from one another. However, it is true that the interpretation
of $d$ in $\mathcal{U}$ is a pseudometric, that we still denote by $d$.
Therefore the notions of uniformly continuous function, of convergent
sequence, and alike make sense in all finite powers of $\mathcal{U}$. To
simplify the notation, for every $\varepsilon\in[0,1]$ we use
$d(x,y)\leq\varepsilon$ as an abbreviation for the $\mathcal{F}$-atomic
formula $d(x,y)\in[0,\varepsilon]$. This is naturally adapted to product
spaces. For all $n\geq 1$, the product $\mathcal{U}^{n}$ is naturally equipped
with the supremum pseudometric, still denoted by $d$, which obviously extends
the corresponding supremum metric on $M^{n}$. For tuples of variables
$x=\langle x_{i}\rangle_{1\leq i\leq m}$ and $\langle y\rangle_{1\leq i\leq
m}$ of the same finite length, we use $d(x,y)\leq\varepsilon$ to abbreviate
the conjunction $\bigwedge_{1\leq i\leq m}d(x_{i},y_{i})\leq\varepsilon$.

The uniform continuity of a given function $f\colon M^{n}\to M$ with
$f\in\mathcal{L}$ can be formulated using a set of $\mathcal{F}$-formulas.
Indeed, by uniform continuity for all $0<\varepsilon\leq 1$ there exists
$0<\delta\leq 1$ such that the following $\mathcal{F}$-formula is satisfied in
$M$:

$\forall x\forall y\,\Big{(}d(x,y)\in[\delta,1]\vee
d(f(x),f(y))\in[0,\varepsilon]\Big{)}.$

The $\mathcal{F}$-type of all such sentences (one for each $0<\varepsilon\leq
1$, paired with any suitable $0<\delta\leq 1$) is preserved from $M$ to any
monster model $\mathcal{U}$ with $M\preccurlyeq^{\mathcal{F}}\mathcal{U}$,
hence the interpretation of $f$ in $\mathcal{U}$ remains uniformly continuous.
Similar considerations apply to uniformly continuous functions from $M^{n}$ to
$X$ belonging to $\mathcal{L}$, as well as to the functions defined in $M$ by
$\mathcal{L}$-terms (which are necessarily uniformly continuous because by
choice of $\mathcal{L}$ they are compositions of finitely many uniformly
continuous functions).

######  Lemma 48.

Let $x$ and $y$ be tuples of variables of sort $\sf H$ and of equal length
$m\geq 1$. Then

$x\sim_{\sf S}y\leftrightarrow d(x,y)=0.$

######  Proof 28.

Consider arbitrary $a,b\in\mathcal{U}^{m}$. If $a\sim_{\sf S}b$, then $\forall
z\,\ d(a,z)=d(b,z)$. Hence $d(a,a)=d(b,a)$, from which $d(a,b)=0$ follows.

For the converse implication, assume that $d(a,b)=0$. Let $t(x,z)$ be any term
of sort ${\sf H}^{m+k}\rightarrow{\sf S}$ for some $k\in\omega$. As observed
before this lemma, the term $t(x,z)$ defines a uniformly continuous function
in $\mathcal{U}$, hence for all $c\in\mathcal{U}^{k}$ we have that
$|t(a,c),t(b,c)|\leq 1/n$ holds in $\mathcal{U}$ for all $n>0$. Therefore
$\forall z\,\ t(a,z)=t(b,z)$, and since $t$ was arbitrary we get $a\sim_{\sf
S}b$.

######  Proposition 49.

Let $N\preccurlyeq^{\mathcal{F}}\mathcal{U}$ be a model and let $m\geq 1$. For
every $a\in\mathcal{U}^{m}$, the following are equivalent:

  1. (1)

$p(x)={\mathcal{F}}\mbox{-tp}(a/N)$ is a Cauchy type;

  2. (2)

$a\in\mathcal{U}^{m}$ is a realization of an $\sim_{\sf S}$-invariant Cauchy
type $q(x)\subseteq\mathcal{F}(N)$;

  3. (3)

there is a sequence $\langle a_{k}\rangle_{k\in\omega}$ in $N^{m}$ that
converges to $a$ with respect to $d$.

######  Proof 29.

(1) $\Rightarrow$ (3). As $p(x)$ is a Cauchy type, we have $p(x)\rightarrow
x\sim_{\sf S}a$ (see the first part of the proof of (1) $\Rightarrow$ (2) in
Lemma 45, which does not require $\sim_{\sf S}$-invariance). By Lemma 48 and
Proposition 25, we have $p^{\prime}(x)\rightarrow d(a,x)\leq 2^{-k}$, for all
$k\in\omega$. Since for $k\geq 1$ the interval $[0,2^{-k+1}]$ is a closed
neighborhood of $[0,2^{-k}]$ in the space $X=[0,1]$, by Proposition 28(2)
applied to $p^{\prime}(x)$ and $d(a,x)\leq 2^{-k}$ we get that for each $k\geq
1$ there is a formula $\varphi_{k}(x)\in p(x)$ and an approximation
$\varphi^{\prime}_{k}(x)\in p^{\prime}(x)$ of it such that
$\varphi^{\prime}_{k}(x)\rightarrow d(a,x)\leq 2^{-k+1}$. (Here we use that
$p(x)$ and $p^{\prime}(x)$ are closed under finite conjunctions.) Since
$\varphi_{k}(x)$ is satisfiable in $\mathcal{U}$, as witnessed by $a$, by
Remark 43 for each $k\in\omega$ there is $a_{k}\in M$ such that
$M\models\varphi^{\prime}_{k}(a_{k})$, and hence also
$\mathcal{U}\models\varphi^{\prime}_{k}(a_{k})$. As $d(a,a_{k})\leq 2^{-k+1}$
for all $k\geq 1$, the sequence $\langle a_{k}\rangle_{k\in\omega}$ converges
to $a$ with respect to the pseudometric $d$.

(3) $\Rightarrow$ (2). For each $k\in\omega$, let
$\varepsilon_{k}=d(a_{k},a)$. Then
$\langle\varepsilon_{k}\rangle_{k\in\omega}$ is a sequence of non-negative
reals converging to $0$. Let
$q(x)=\big{\\{}d(a_{k},x)\leq\varepsilon_{k}\mathbin{:}k\in\omega\big{\\}}$.
All the $\mathcal{F}$-atomic formulas $d(a_{k},x)\leq\varepsilon_{k}$ are
$\sim_{\sf S}$-invariant because they do not contain $\mathcal{L}_{\sf
H}$-subformulas, hence $q(x)$ is $\sim_{\sf S}$-invariant too, and $a$
realizes $q(x)$. It remains to prove that $q(x)$ is a Cauchy type. It is
obviously consistent, as witnessed by $a$. Moreover, by the triangle
inequality every realization $b\in\mathcal{U}$ of
$d(a_{k},x)\leq\varepsilon_{k}$ is such that $d(b,a)\leq 2\varepsilon_{k}$.
Thus every realization of $q(x)$ is at distance $0$ from $a$, hence
$q(x)\wedge q(y)\to d(x,y)=0$ by the triangle inequality. By Lemma 48, this
means that $q(x)\wedge q(y)\to x\sim_{\sf S}y$ and we are done.

(2) $\Rightarrow$ (1). Clear, since $q(x)\subseteq p(x)$.

######  Proposition 50.

For every model $N\preccurlyeq^{\mathcal{F}}\mathcal{U}$, the following are
equivalent:

  1. (1)

$N$ is Cauchy complete;

  2. (2)

$N$ is $d$-Cauchy complete, that is, every $d$-Cauchy sequence in $N$
converges to a point in $N$.

######  Proof 30.

(1) $\Rightarrow$ (2). Let $\langle a_{k}\rangle_{k\in\omega}$ be a $d$-Cauchy
sequence in $N$. By working with a subsequence if necessary, we may assume
that $d(a_{i},a_{j})\leq 2^{-k}$ for every $k\in\omega$ and every $i,j\geq k$.
The $\mathcal{F}$-type $p(x)=\\{d(a_{k},x)\leq 2^{-k}\mid k\in\omega\\}$ is
finitely realized in $\mathcal{U}$: if $k$ is largest such that
$d(a_{k},x)\leq 2^{-k}$ occurs in a given finite subset of $p(x)$, then
$a_{k}$ is a realization of such a set. By saturation,
$p(x)\subseteq\mathcal{F}(N)$ is realized by some $a\in\mathcal{U}$, and it is
thus consistent. Moreover, it is $\sim_{\sf S}$-invariant because none of its
elements contain an $\mathcal{L}_{\sf H}$-subformula, and $p(x)\wedge p(y)\to
x\sim_{\sf S}y$ by the proof of (3) $\Rightarrow$ (2) in Proposition 49 (where
now we set $\varepsilon_{k}=2^{-k}$). Thus $p(x)$ is realized by some $b\in N$
by (1). By definition of $p(x)$, the sequence $\langle
a_{k}\rangle_{k\in\omega}$ converges to $b$ and we are done.

(2) $\Rightarrow$ (1). Notice that $N$ is $d$-Cauchy complete if and only if
so is each finite product $N^{m}$ for $m\geq 1$. Let
$q(x)\subseteq\mathcal{F}(N)$, with $|x|=m$, be an $\sim_{\sf S}$-invariant
Cauchy type, and let $a\in\mathcal{U}^{m}$ be a realization of it. By
Proposition 49, there is a sequence $\langle a_{k}\rangle_{k\in\omega}$ in
$N^{m}$ which converges to $a$. We may assume that $\langle
a_{k}\rangle_{k\in\omega}$ is $d$-Cauchy; thus it also converges to some $b\in
N^{m}$ by (2). Since both $a$ and $b$ are limits of the same sequence, we have
$d(a,b)=0$, and hence $a\sim_{\sf S}b$ by Lemma 48. Since $q(x)$ is $\sim_{\sf
S}$-invariant, $b\in N^{m}$ realizes $q(x)$.

In particular, by Proposition 47 we get that $\langle\mathcal{U},d\rangle$ is
complete as a pseudometric space.

## References

  * []
BBHUBen YaacovItaïBerensteinAlexanderHensonC. Wardtitle = Model theory for
metric structuresUsvyatsov, AlexanderCambridge University
Press2010@book{BYBHU, label = {BBHU}, author = {Ben Yaacov, Ita\"i}, author =
{Berenstein, Alexander}, author = {Henson, C. Ward}, author = {{Usvyatsov,
Alexander} title = {Model theory for metric structures}}, publisher =
{Cambridge University Press}, date = {2010}} CKChangCheng-ChungKeislerJerome
H.Continuous model theoryPrinceton University Press1966@book{CK, label = {CK},
author = {Chang, Cheng-Chung}, author = {Keisler, Jerome H.}, title =
{Continuous model theory}, publisher = {Princeton University Press}, date =
{1966}} DDavisMartinApplied nonstandard analysisDover2005@book{D, label = {D},
author = {Davis, Martin}, title = {Applied Nonstandard Analysis}, publisher =
{Dover}, date = {2005}} HIHensonC. WardIovinoJoséUltraproducts in
analysistitle={Analysis and logic}, address={Mons}, date={1997},
series={London Math. Soc. Lecture Note Ser.}, volume={262},
publisher={Cambridge Univ. Press, Cambridge}, 20021–110@article{HI, label =
{HI}, author = {Henson, C. Ward}, author = {Iovino, Jos\'{e}}, title =
{Ultraproducts in Analysis}, conference = {title={Analysis and logic},
address={Mons}, date={1997}, }, book = {series={London Math. Soc. Lecture Note
Ser.}, volume={262}, publisher={Cambridge Univ. Press, Cambridge}, }, date =
{2002}, pages = {1–110}} KecKechrisAlexander S.Classical descriptive set
theorySpringer-Verlag1997@book{Kec, label = {Kec}, author = {Kechris,
Alexander S.}, title = {Classical Descriptive Set Theory}, publisher =
{Springer-Verlag}, date = {1997}} KKeislerH. JeromeModel theory for real-
valued structures2005.11851DocumentLinkarXiv2020@arXiv{K, label = {K}, author
= {Keisler, H. Jerome}, title = {Model Theory for Real-valued Structures},
eprint = {2005.11851}, doi = {10.48550/ARXIV.2005.11851}, url =
{https://arxiv.org/abs/2005.11851}, publisher = {arXiv}, date = {2020}}
KeKelleyL. JohnGeneral topologySpringer1955@book{Ke, label = {Ke}, author =
{Kelley, L. John}, title = {General Topology}, publisher = {Springer}, date =
{1955}} ZZambellaDomenicoStandard
analysis2311.15711DocumentLinkarXiv2023@arXiv{Z, label = {Z}, author =
{Zambella, Domenico}, title = {Standard analysis}, eprint = {2311.15711}, doi
= {10.48550/arXiv.2311.15711}, url = {https://arxiv.org/abs/2311.15711},
publisher = {arXiv}, date = {2023}}