remresetThe remreset package latexFont shape declaration has incorrect series
value ‘mc’. Λ$\Lam$ Σ$\Sigma$

# Bisimulations of potentialist systems

Sam Adam-Day  Mathematical Institute, University of Oxford, Andrew Wiles
Building, Radcliffe Observatory Quarter, Woodstock Road, Oxford, OX2 6GG,
United Kingdom<EMAIL_ADDRESS>
###### Abstract

A potentialist system is a first-order Kripke model based on embeddings. I
define the notion of bisimulation for these systems, and provide a number of
examples. Given a first-order theory $T$, the system
$\operatorname{\mathrm{Mod}}(T)$ consists of all models of $T$. We can then
take either all embeddings, or all substructure inclusions, between these
models. I show that these two ways of defining
$\operatorname{\mathrm{Mod}}(T)$ are bitotally bisimilar. Next, I relate the
notion of bisimulation to a generalisation of the Ehrenfeucht-Fraïsé game, and
use this to show the equivalence of the existence of a bisimulation with
elementary equivalence with respect to an infinitary language. Finally, I
consider the question of when a potentialist system is bitotally bisimilar to
a system containing set-many models, providing too different sufficient
conditions.

†† _Keywords_ : potentialist system, bisimulation, modal model theory, first-
order Kripke model, Ehrenfeucht-Fraïssé game†† _2020 Mathematics Subject
Classification_ : 03B45, 03C07, 03C75

##  1 Introduction

The two main objects of study in this article are potentialist systems and
bisimulations. A potentialist system is a collection of first-order structures
and embeddings between them in which one can interpret first-order modal logic
(for definitions, see Section 2). Potentialist systems are closely related to
first-order Kripke models. The former differ from the latter in the following
three ways.  (1) All instances of the accessibility relation between
structures are required to be embeddings; in other words, the accessibility
relation is required to be inflationary on the domains.  (2) We allow multiple
embeddings between two structures.  (3) We allow class-many structures.

Potentialist systems provide a way of investigating a mathematical structure
within the context of other related structures, making precise the notions of
necessity and possibility. A formal treatment of these systems is given in
[HL19]. The study of potentialist systems is called ‘modal model theory’. This
name was introduced in [HW20], which conducts a thorough study of the system
$\operatorname{\mathrm{Mod}}(T)$ of models of a first-order theory $T$.
Potentialist systems of set-theoretic forcing extensions are studied in
[Ham03, HL08, HL13, HL19, HLL15]. Further systems of models of arithmetic and
set theory are studied in [HW18, Ham18, HW21]. The relationship between model
theory and modal logic is also explored in [SS18].

A bisimulation between two potentialist systems is a system of finite partial
isomorphisms between structures in one and structures in the other, such that
any increase in the size of the isomorphism or travel along the accessibility
relation on one side can be mirrored on the other. A bisimulation is bitotal
if every element of every model in both systems takes part in the relation.
This notion of bisimulation simultaneously generalises the notion of a
bisimulation between propositional Kripke models and the notion of a back-and-
forth system for first-order models. One of the key properties which
bisimulations satisfy is invariance: if two systems are bisimilar, they
satisfy the same modal sentences, even allowing for infinite disjunctions and
conjunctions.

An important class of examples of potentialist systems are those of the form
$\operatorname{\mathrm{Mod}}(T)$, consisting of every model of some first-
order theory $T$. There are two ways of defining
$\operatorname{\mathrm{Mod}}(T)$: by including all embeddings between models,
or just the substructure inclusions. As discussed in [HW20], the latter aligns
well with a potentialist philosophy on the theory $T$, in which we view the
‘universe’ as unfolding in stages, with individuals becoming actual and
persisting identically through subsequent stages. The former on the other hand
typically enjoys better algebraic properties, like directedness, amalgamation
or convergence (see [HW20, Section 5] for definitions). In Theorem 29 of that
paper, Hamkins and Wołoszyn show that the two resulting systems satisfy the
same modal sentences. I go one step further and show that the two systems are
in fact bitotally bisimilar in a particularly strong way (Theorem 28). This
provides a deeper explanation for why the two are equivalent on modal
sentences, and immediately extends the result to equivalence with respect to
an infinitary language. Moreover, the bisimulation should allow us to transfer
results from the more mathematically amenable system based on embeddings, to
the more philosophically relevant one based on inclusions.

Bisimulations have a natural interpretation in terms of infinite games. I
elaborate on this connection, defining the notion of a _modal Ehrenfeucht-
Fraïssé game_. This furnishes us with the converse of invariance: if two
systems agree on all infinitary modal sentences then they are bisimilar.

For the remainder of the article, I consider under what circumstances a class-
sized potentialist system is bitotally bisimilar with a set-sized one. First,
I restrict attention to the systems $\operatorname{\mathrm{Mod}}(T)$ for some
first-order theory $T$. I show that if $T$ has infinite models, and all its
models of size $\kappa$ are $\aleph_{0}$-saturated, then
$\operatorname{\mathrm{Mod}}(T)$ is bitotally bisimilar to a system consisting
of set-many models. In the last part I take a different tack, showing that if
a potentialist system consists of models of an $\aleph_{0}$-categorical theory
which admits quantifier elimination then it is bitotally bisimilar to a
particularly simple system containing set-many models. This result makes no
assumption on the modal structure of the system, and as such it might be
expected that it wouldn’t admit much strengthening. As evidence for this, I
provide a partial converse, and give an example where weakening the assumption
‘admits quantifier elimination’ leads to a system which is not bisimilar with
a set-sized one.

##  2 Potentialist systems

A propositional Kripke model consists of a set of ‘worlds’, a relation on this
set, and an assignment to each world of the truth values of each propositional
variable [BRV01, CZ97]. These models are used to provide a semantics for
propositional modal logic. They generalise to first-order Kripke models, in
which each world is now an entire first-order structure, and we specify how
the elements of connected worlds are related. See [HC96, FM98, Ben10] for more
on first-order Kripke models.

Potentialist systems specialise first-order Kripke models, in that we require
that all relations between worlds be embeddings. However, they also
generalise, in that we allow multiple relations between any two worlds, and
that the collection of worlds be class-sized. The terminology ‘potentialist
system’ was first used in [HL19].

######  Definition 1.

A _potentialist system_ is a collection of first-order structures together
with a collection of embeddings between them, containing the identity
embeddings and all compositions of embeddings.

I will refer to the elements of a potentialist system as ‘worlds’,
‘structures’ or ‘models’ (the latter being reserved for the context in which
we are considering models of a certain first-order theory). Note that a
potentialist system is exactly a category of first-order structures with
embeddings. A potentialist system is an instance of the more general notion of
a ‘Kripke category’, in which one considers the modal logic of an arbitrary
concrete category. Kripke categories are defined and investigated in upcoming
work by Wojciech Aleksander Wołoszyn [Woł22].

Notice that we allow multiple embeddings between worlds. Sometimes, it is
natural to consider potentialist systems in which embeddings are always
unique, so the abstracted relationship between the worlds is a partial order.

######  Definition 2.

A potentialist system is _thin_ if from any first-order structures in it to
any other there is at most one embedding.

This corresponds with the notion of ‘thinness’ for categories. Later, I will
show that restricting to thin potentialist systems does not lose generality,
in the sense that every potentialist system is bisimilar with a thin one.

######  Definition 3.

A _pointed system_ is a triple $(\mathcal{M},M,\overline{a})$, where
$\mathcal{M}$ is a potentialist system, $M\in\mathcal{M}$ and $\overline{a}$
is a finite tuple of elements of $M$. The _parameter size_ of the pointed
system is the size of $\overline{a}$. When the parameter size is $0$, write
$(\mathcal{M},M)$.

Let us now move on to consider the interpretation of formulas in potentialist
systems. We are interested in several languages. We start with some first-
order, finitary, non-modal language $L$ (specified by its signature of non-
logical symbols). The first language to meet is the standard first-order modal
language based on $L$.

######  Definition 4.

The language
$L^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}$
is formed by adding  and $\square$ as operators. In other words,
$L^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}$
is closed under boolean combinations, quantification and the follow two new
rules: whenever $\phi$ is a formula, so are
${\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}\phi$
and $\square\phi$.

Now, when we come to consider the relationship between bisimulations and
sentence satisfaction, we will need to talk about infinitary languages. The
definition generalises that of infinitary first-order (non-modal) languages
[Hod93].

######  Definition 5.

For $\kappa$ an infinite cardinal, let $L_{\kappa}$ be the first-order
language in which we allow conjunction and disjunction of size less than
$\kappa$, with the proviso that all formulas contain only finitely many free
variables. Let $L_{\infty}$ be the (class-sized) union of each $L_{\kappa}$.
The languages
$L^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}_{\kappa}$
and
$L^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}_{\infty}$
are defined similarly, this time including  and $\square$ as modal operators.

######  Remark 6.

In non-modal first-order infinitary languages, one can also consider allowing
infinitely long quantifier blocks. With this in mind the language $L_{\kappa}$
is elsewhere commonly denoted by $L_{\kappa,\omega}$, where the ‘$\omega$’
subscript makes explicit the fact that quantifier blocks are all finite;
likewise $L_{\infty}$ is written $L_{\infty,\omega}$. Similarly, in the modal
case, one might consider allowing infinitely long blocks of modal operators.
So, strictly speaking, we could write
$L^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}_{\kappa,\omega,\omega}$
for
$L^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}_{\kappa}$
and
$L^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}_{\infty,\omega,\omega}$
for
$L^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}_{\infty}$.
However, since infinitely long quantifier or modal operator blocks are not
considered here, I suppress the additional subscripts.

Finally, since formula trees are well-founded, one can assign a rank to each
formula in
$L^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}_{\infty}$.
This provides a useful complexity stratification, which will be relevant when
we come to consider modal Ehrenfeucht-Fraïssé games.

######  Definition 7.

The _modal-quantifier rank_ , $\operatorname{\mathrm{mqr}}(\phi)$, of a
formula $\phi\in
L^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}_{\infty}$
is an ordinal defined recursively on the construction of $\phi$.

$\displaystyle\operatorname{\mathrm{mqr}}(\psi)$ $\displaystyle=0$ (when
$\psi$ is atomic) $\displaystyle\operatorname{\mathrm{mqr}}(\neg\phi)$
$\displaystyle=\operatorname{\mathrm{mqr}}(\phi)$
$\displaystyle\operatorname{\mathrm{mqr}}\left(\bigvee_{i\in
I}\phi_{i}\right)=\operatorname{\mathrm{mqr}}\left(\bigwedge_{i\in
I}\phi_{i}\right)$ $\displaystyle=\sup_{i\in
I}\operatorname{\mathrm{mqr}}(\phi_{i})$
$\displaystyle\operatorname{\mathrm{mqr}}(\exists
x\phi)=\operatorname{\mathrm{mqr}}(\forall x\phi)$
$\displaystyle=\operatorname{\mathrm{mqr}}(\phi)+1$
$\displaystyle\operatorname{\mathrm{mqr}}({\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}\phi)=\operatorname{\mathrm{mqr}}(\square\phi)$
$\displaystyle=\operatorname{\mathrm{mqr}}(\phi)+1$

Write
$L^{{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}},\alpha}_{\infty}$
for the class of
$L^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}_{\infty}$-formulas
of modal-quantifier rank less than $\alpha$.

The interpretation of first-order modal formulas extends that of classical
formulas by interpreting
${\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}\phi$
as ‘$\phi$ holds in some extension’ and $\square\phi$ as the dual: ‘$\phi$
holds in every extension’.

######  Definition 8.

Let $(\mathcal{M},M,\overline{a})$ be a pointed system, and $\phi$ be an
$L^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}_{\infty}$-formula.
We define what it means for $\phi$ to be true at this pointed system, which we
write as $\mathcal{M},M\vDash\phi[\overline{a}]$, by induction on the
complexity of $\phi$. The non-modal cases are as usual. We let
$\mathcal{M},M\vDash{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}\phi[\overline{a}]$
if and only if there is $\pi\colon M\to M^{\prime}$ in $\mathcal{M}$ such that
$\mathcal{M},M^{\prime}\vDash\phi[\pi(\overline{a})]$. We let
$\mathcal{M},M\vDash\square\phi[\overline{a}]$ if and only if for every
$\pi\colon M\to M^{\prime}$ in $\mathcal{M}$ we have
$\mathcal{M},M^{\prime}\vDash\phi[\pi(\overline{a})]$.

Note that $\square\phi$ is equivalent to
$\neg{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}\neg\phi$,
so in our inductions on formulas we won’t need to treat the $\square\phi$ case
separately.

######  Remark 9.

There are some definability issues here, stemming from the fact that the
collection of worlds in $\mathcal{M}$ may be a proper class. For instance, if
we take $\mathcal{M}$ to be the class of all initial segments $V_{\alpha}$ of
the cumulative hierarchy under subset inclusion, then
$L^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}$
in $\mathcal{M}$ can capture first-order truth in the ambient universe (see
[HL19, Theorem 1] and [Lin13]). This issue is discussed in Section 9 of
[HW20]. Following the discussion there, to make sense of the previous
definition we can view it as taking place within Morse-Kelley set theory, or
Von Neumann-Bernays-Gödel set theory with the axiom of elementary transfinite
recursion. Alternatively, we can choose to work with a sequence of
Grothendieck-Zermelo universes, so that the extension of some potentialist
system in one universe is a set in the next universe up. Note that
$\mathrm{ZFC}$-definability issues don’t arise for all class-sized systems.
Indeed, Sections 5 and 6 provide examples of class-sized systems which are
strongly equivalent to set-sized ones.

######  Definition 10.

The relations $\equiv$,
$\equiv^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}$,
$\equiv^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}_{\infty}$
and
$\equiv^{{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}},\alpha}_{\infty}$
between pointed systems are the elementary equivalence relations with respect
to $L$,
$L^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}$,
$L^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}_{\infty}$
and
$L^{{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}},\alpha}_{\infty}$
respectively, taking the tuples in the pointed systems as parameters. For
example,
$(\mathcal{M},M,\overline{a})\equiv^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}_{\infty}(\mathcal{N},N,\overline{b})$
means that for every
$L^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}_{\infty}$-formula
$\phi$, we have $\mathcal{M},M\vDash\phi[\overline{a}]$ if and only if
$\mathcal{N},N\vDash\phi[\overline{b}]$.

Let us meet an important class of potentialist systems, first defined in
[HW20]. Let $T$ be a first-order $L$-theory. The potentialist system
$\operatorname{\mathrm{Mod}}(T)$ will be the system based on the collection of
all models of $T$. There are two ways of defining this, depending on whether
we take the relations between structures to be inclusions or embeddings.

######  Definition 11.

The _substructure potentialist system_ , $\operatorname{\mathrm{Mod}}(T)$,
based on $T$, consists of the class of models of $T$ together with all
substructure inclusions. That is, we include all and only the substructure
inclusion maps $\iota\colon M\subseteq N$.

Of course, $\operatorname{\mathrm{Mod}}(T)$ is a thin potentialist system.
Note also that the structure of $\operatorname{\mathrm{Mod}}(T)$ depends on
the underlying domains of the models, in the sense that $M$ may be a
substructure of $N$ but not of an isomorphic copy of $N$. It is natural then
to consider allowing all embeddings between models, so that the relations
between models depend only on their isomorphism types.

######  Definition 12.

The _embedding potentialist system_ ,
$\operatorname{\operatorname{\mathrm{ModEm}}}(T)$, based on $T$ consists of
the class of models of $T$ together with all embeddings. In other words, from
$M$ to $N$ we include all maps $M\to N$ which are embeddings of
$L$-structures.

In Theorem 28 below, I will show that $\operatorname{\mathrm{Mod}}(T)$ and
$\operatorname{\operatorname{\mathrm{ModEm}}}(T)$ are bitotally bisimilar in a
strong sense. As noted in the introduction, this provides and important and
deep connection between the philosophically interesting
$\operatorname{\mathrm{Mod}}(T)$ on the one hand, and the mathematically
tractable $\operatorname{\operatorname{\mathrm{ModEm}}}(T)$ on the other.

##  3 Bisimulations

The notion of bisimulation is central in propositional modal logic (see for
example [BRV01, §2.2]). It can be extended to first-order modal logic, at the
same time generalising the notion of a back-and-forth system for first-order
structures. The following is adapted from Definition 11.4.2 in [Ben10, p.
123].

######  Definition 13.

A _bisimulation_ between potentialist systems $\mathcal{M}$ and $\mathcal{N}$
in the same language $L$ is a non-empty relation $\sim$ matching pairs
$(M,\overline{a})$ with pairs $(N,\overline{b})$, where
$(\mathcal{M},M,\overline{a})$ and $(\mathcal{N},N,\overline{b})$ are pointed
systems of the same parameter size, such that when
$(M,\overline{a})\sim(N,\overline{b})$ the following hold.

  1. (B1)

The map $\overline{a}\mapsto\overline{b}$ is a partial isomorphism between $M$
and $N$.

  2. (B2)

For any $c\in M$ there is $d\in N$ such that
$(M,\overline{a}c)\sim(N,\overline{b}d)$, and vice versa (where
$\overline{a}c$ is the result of adding $c$ at then end of the tuple
$\overline{a}$, etc.).

  3. (B3)

For any $\pi\colon M\to M^{\prime}$ in $\mathcal{M}$ there is $\rho\colon N\to
N^{\prime}$ in $\mathcal{N}$ such that:

$(M^{\prime},\pi(\overline{a}))\sim(N^{\prime},\rho(\overline{b}))$

and vice versa.

Write
$(\mathcal{M},M,\overline{a})\mathrel{\,\raisebox{1.29167pt}{$\underline{\makebox[8.99994pt]{$\leftrightarrow$}}$}\,}(\mathcal{N},N,\overline{b})$
when there is a bisimulation $\sim$ between $\mathcal{M}$ and $\mathcal{N}$
such that:

$(M,\overline{a})\sim(N,\overline{b})$

######  Definition 14.

A bisimulation $\sim$ is _left total_ if every pair $(M,\overline{a})$ on the
left is related to some pair $(N,\overline{b})$ on the right. It is _right
total_ if every pair $(N,\overline{b})$ on the right is related to some pair
$(M,\overline{a})$ on the left. It is _bitotal_ if it is both left and right
total.

A bisimulation is a kind of back-and-forth system corresponding to a modal
version of the Ehrenfeucht-Fraïssé game. This game-theoretic side will be
examined in more detail in Section 4. There, it will also be shown that
bisimulations correspond to
$L^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}_{\infty}$-elementary
equivalence. We can get a more fine-grained notion corresponding to
$L^{{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}},\alpha+1}_{\infty}$-elementary
equivalence as follows.

######  Definition 15.

Let $\alpha$ be an ordinal. An _$\alpha$ -bisimulation_ between potentialist
systems $\mathcal{M}$ and $\mathcal{N}$ in the same language $L$ is a
collection of non-empty relations $\sim_{\beta}$ for $\beta\leqslant\alpha$.
Each relates pairs $(M,\overline{a})$ with pairs $(N,\overline{b})$, where
$(\mathcal{M},M,\overline{a})$ and $(\mathcal{N},N,\overline{b})$ are pointed
systems of the same parameter size. Whenever
$(M,\overline{a})\sim_{\beta}(N,\overline{b})$ we require that the following
hold.

  1. ($\alpha$B1)

The map $\overline{a}\mapsto\overline{b}$ is a partial isomorphism between $M$
and $N$.

  2. ($\alpha$B2)

For every $\gamma<\beta$: for any $c\in M$ there is $d\in N$ such that we have
$(M,\overline{a}c)\sim_{\gamma}(N,\overline{b}d)$, and vice versa.

  3. ($\alpha$B3)

For every $\gamma<\beta$: for any $\pi\colon M\to M^{\prime}$ in $\mathcal{M}$
there is $\rho\colon N\to N^{\prime}$ in $\mathcal{N}$ such that
$(M^{\prime},\pi(\overline{a}))\sim_{\gamma}(N^{\prime},\rho(\overline{b}))$,
and vice versa.

Write
$(\mathcal{M},M,\overline{a})\mathrel{\,\raisebox{1.29167pt}{$\underline{\makebox[8.99994pt]{$\leftrightarrow$}}$}\,}_{\alpha}(\mathcal{N},N,\overline{b})$
to express the existence of an $\alpha$-bisimulation between $\mathcal{M}$ and
$\mathcal{N}$ such that $(M,\overline{a})\sim_{\alpha}(N,\overline{b})$.

######  Remark 16.

The reader might be wondering why an $\alpha$-bisimulation is defined as a
collection of relations $\sim_{\beta}$ for $\beta\leqslant\alpha$ rather than
for $\beta<\alpha$. It would appear that we lack a convenient way of
expressing that ‘$(\mathcal{M},M,\overline{a})$ and
$(\mathcal{N},N,\overline{b})$ are $\alpha$-bisimilar for every $\alpha$ less
than some limit ordinal $\delta$’. However, it is not hard to see that this
notion just described is equivalent to $(\mathcal{M},M,\overline{a})$ and
$(\mathcal{N},N,\overline{b})$ being $\delta$-bisimilar. Moreover, it is
desirable that being $0$-bisimilar should coincide with being equivalent on
atomic formulas.

######  Remark 17.

In Definition 15 there is no requirement made that the collection of relations
$\sim_{\beta}$ cohere. But note that without loss of generality we can always
assume that $\sim_{\beta}\subseteq\sim_{\gamma}$ for $\gamma<\beta$.

Now, one way of thinking about a bisimulation is as a collection of partial
isomorphisms of finite parts of first-order structures which can extended
indefinitely. A special case of this is when these partial isomorphisms
uniquely combine to a system of total isomorphisms between worlds in one
potentialist system and worlds in the other.

######  Definition 18.

An _iso-bisimulation_ between potentialist systems $\mathcal{M}$ and
$\mathcal{N}$ is a non-empty relation $\approx$ between $\mathcal{M}$ and
$\mathcal{N}$ together with a system of isomorphisms $(\xi_{M,N}\colon M\to
N\mid M\approx N)$ subject to the following condition. Whenever $\pi\colon
M\to M^{\prime}$ in $\mathcal{M}$ and $M\approx N$, there is $\rho\colon N\to
N^{\prime}$ in $\mathcal{N}$ such that $M^{\prime}\approx N^{\prime}$ and the
following diagram commutes; and vice versa.

${M^{\prime}}$${N^{\prime}}$${M}$${N}$$\scriptstyle{\xi_{M^{\prime},N^{\prime}}}$$\scriptstyle{\pi}$$\scriptstyle{\xi_{M,N}}$$\scriptstyle{\rho}$

The following allows us to convert any iso-bisimulation into an (ordinary)
bisimulation.

######  Lemma 19.

Let $(\approx,(\xi))$ be an iso-bisimulation between $\mathcal{M}$ and
$\mathcal{N}$. Define the relation $\approx^{*}$ by setting
$(M,\overline{a})\approx^{*}(N,\overline{b})$ if and only if $M\approx N$ and
$\xi_{M,N}(\overline{a})=\overline{b}$. Then $\approx^{*}$ is a bisimulation.

Hence, any iso-bisimulation gives rise to a bisimulation. The converse is not
true in general, e.g. for cardinality reasons, or because a bisimulation can
involve multiple non-compatible partial isomorphisms between structures. The
following is a simple example of two bisimilar systems which are not iso-
bisimilar.

######  Example 20.

Let $L$ be the empty language. Let $\mathcal{M}$ be the potentialist system
consisting of a single $\aleph_{0}$-size $L$-structure, and let $\mathcal{N}$
be the structure consisting of an $\aleph_{0}$-sized and an $\aleph_{1}$-sized
$L$-structure, with an embedding from the former to the latter. There is no
iso-bisimulation
$\mathcal{M}\mathrel{\,\raisebox{1.29167pt}{$\underline{\makebox[8.99994pt]{$\leftrightarrow$}}$}\,}\mathcal{N}$
for cardinality reasons, but there is an (ordinary) bisimulation
$\mathcal{M}\mathrel{\,\raisebox{1.29167pt}{$\underline{\makebox[8.99994pt]{$\leftrightarrow$}}$}\,}\mathcal{N}$.
Indeed, relate pairs according to their atomic types:111I use the notation
$\Delta_{0}^{M}(\overline{a})$ to denote the atomic type of $\overline{a}$ in
$M$: the set of atomic formulas true in $M$ of $\overline{a}$.

$(M,\overline{a})\sim(N,\overline{b})\quad\Leftrightarrow\quad\Delta_{0}^{M}(\overline{a})=\Delta_{0}^{N}(\overline{b})$

A key property of bisimulations is their invariance: bisimilar systems satisfy
the same formulas (c.f. [Ben10, Theorem 21, p. 124]).

######  Theorem 21 (Fundamental Theorem of Bisimulations).

If two pointed systems are bisimilar then they are
$L^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}_{\infty}$-elementarily
equivalent.

###### Proof.

The proof is by induction on formulas. Let $\sim$ be a bisimulation between
$(\mathcal{M},M,\overline{a})$ and $(\mathcal{N},N,\overline{b})$. The atomic
case follows from (B1). If we have $\mathcal{M},M\vDash\exists
x\psi([\overline{a}],x)$ then there is $c\in M$ such that
$\mathcal{M},M\vDash\psi[\overline{a},c]$; by (B2) there is $d\in N$ such that
$(M,\overline{a}c)\sim(N,\overline{b}d)$, so by induction hypothesis
$\mathcal{N},N\vDash\psi[\overline{b},d]$ and $\mathcal{N},N\vDash\exists
x\psi([\overline{b}],x)$. If
$\mathcal{M},M\vDash{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}\psi[\overline{a}]$
then for some $\pi\colon M\to M^{\prime}$ in $\mathcal{M}$ we have
$\mathcal{M},M^{\prime}\vDash\psi[\pi(\overline{a})]$. By (B3) there is
$\rho\colon N\to N^{\prime}$ in $\mathcal{N}$ with
$(M^{\prime},\pi(\overline{a}))\sim(N^{\prime},\rho(\overline{b}))$; so by
induction hypothesis $\mathcal{N},N^{\prime}\vDash\psi[\rho(\overline{b})]$
and
$\mathcal{N},N\vDash{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}\psi[\overline{b}]$.
∎

######  Corollary 22.

If $(\approx,(\xi))$ is an iso-bisimulation between $\mathcal{M}$ and
$\mathcal{N}$, then whenever $M\approx N$, for any $\overline{a}$ in $M$ and
formula $\phi$ of
$L^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}_{\infty}$:

$\mathcal{M},M\vDash\phi[\overline{a}]\Leftrightarrow\mathcal{N},N\vDash\phi[\xi_{M,N}(\overline{a})]$

######  Theorem 23 (Fundamental Theorem of $\alpha$-bisimulations).

If two pointed systems are $\alpha$-bisimilar then they are
$L^{{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}},\alpha+1}_{\infty}$-elementarily
equivalent.

###### Proof.

This is a refinement of the proof of Theorem 21. We prove by induction on
modal rank that whenever $(M,\overline{a})\sim_{\beta}(N,\overline{b})$, for
any $\phi$ with $\operatorname{\mathrm{mqr}}(\phi)\leqslant\beta$ we have:

$\mathcal{M},M\vDash\phi[\overline{a}]\quad\Leftrightarrow\quad\mathcal{N},N\vDash\phi[\overline{b}]$

As above the base case is dealt with by ($\alpha$B1). If $M\vDash\exists
x\psi([\overline{a}],x)$ there is $c\in M$ such that
$M\vDash\psi[\overline{a},c]$; by ($\alpha$B2) there is $d\in N$ such that:

$(M,\overline{a}c)\sim_{\operatorname{\mathrm{mqr}}(\psi)}(N,\overline{b}d)$

which by induction hypothesis means that $N\vDash\psi[\overline{b},d]$. The
other cases are similar. ∎

The converses of Theorem 21 and Theorem 23 will be proved in Section 4 after
we have established the connection with infinite games.

The following provide promised proofs of facts mentioned in Section 2. We
first see that any potentialist system is iso-bisimilar with a thin one, using
the ‘unravelling’ construction, a generalisation from propositional modal
logic (see [BRV01, Definition 4.51]).

######  Definition 24.

Let $\mathcal{M}$ be a potentialist system. The _unravelling_ ,
$\operatorname{\mathrm{Unrav}}(\mathcal{M})$, of $\mathcal{M}$ is the free
category on $\mathcal{M}$, regarded as a potentialist system. Concretely,
$\operatorname{\mathrm{Unrav}}(\mathcal{M})$ is specified as follows.

  * •

The objects are finite sequences of embeddings:

$\vec{\pi}=\left(M_{0}\xrightarrow{\pi_{1}}M_{1}\xrightarrow{\pi_{2}}\cdots\xrightarrow{\pi_{n-1}}M_{n-1}\xrightarrow{\pi_{n}}M_{n}\right)$

where $M_{0},\ldots,M_{n}$ are worlds from $\mathcal{M}$ and
$\pi_{1},\ldots,\pi_{n}$ are embeddings from $\mathcal{M}$. We allow singleton
sequences. The structure corresponding to $\vec{\pi}$ is
$M_{\vec{\pi}}=M_{n}$.

  * •

For every sequence $\vec{\pi}$ and every embedding $\pi_{n+1}$ with domain
$M_{\vec{\pi}}$, we obtain a new sequence $\vec{\pi}\pi_{n+1}$ by adding
$\pi_{n+1}$ at the end, and we have an arrow
$\pi_{n+1}\colon\vec{\pi}\to\vec{\pi}\pi_{n+1}$.

######  Remark 25.

This definition is slightly informal. According to Definition 1, worlds in a
potentialist system should be $L$-structures, but here they are finite
sequences. So to formally define the
$\operatorname{\mathrm{Unrav}}(\mathcal{M})$ we should take the worlds to be
the last structures $M_{\vec{\pi}}=M_{n}$, and somehow encode the sequence
structure in the domain. For example, we could rename the elements of the
domain as $M_{\vec{\pi}}\times\\{(\pi_{1}\cdots\pi_{n})\\}$. I won’t worry too
much about these technicalities from now on.

Note that the unravelling of $\mathcal{M}$ is always a thin category. The
following gives the bisimulation
$\mathcal{M}\mathrel{\,\raisebox{1.29167pt}{$\underline{\makebox[8.99994pt]{$\leftrightarrow$}}$}\,}\operatorname{\mathrm{Unrav}}(\mathcal{M})$.

######  Lemma 26.

Let $\mathcal{M}$ be a potentialist system. The relation $\approx$ between
$\mathcal{M}$ and $\operatorname{\mathrm{Unrav}}(\mathcal{M})$, given by:
$N\approx\vec{\pi}$ if and only if $M_{\vec{\pi}}=N$, together with the
identity isomorphisms, is an iso-bisimulation which is bitotal.

###### Proof.

Assume that $N\approx\vec{\pi}$. Take $\rho\colon N\to N^{\prime}$ in
$\mathcal{M}$. Then
$\vec{\pi}\rho\in\operatorname{\mathrm{Unrav}}(\mathcal{M})$ and
$N^{\prime}\approx\vec{\pi}\rho$. Furthermore, we have:

$\rho\colon\vec{\pi}\to\vec{\pi}\rho$

in $\operatorname{\mathrm{Unrav}}(\mathcal{M})$. Conversely, if
$\rho\colon\vec{\pi}\to\vec{\pi}\rho$ in
$\operatorname{\mathrm{Unrav}}(\mathcal{M})$ with codomain $N^{\prime}$, then
we have $\rho\colon N\to N^{\prime}$ in $\mathcal{M}$. ∎

######  Corollary 27.

Every potentialist system is bisimilar to thin one via a bitotal iso-
bisimulation.

Let us see now that $\operatorname{\mathrm{Mod}}(T)$ and
$\operatorname{\operatorname{\mathrm{ModEm}}}(T)$ are bisimilar.

######  Theorem 28.

Let $T$ be a first-order $L$-theory. There is a bitotal iso-bisimulation
between the systems $\operatorname{\mathrm{Mod}}(T)$ and
$\operatorname{\operatorname{\mathrm{ModEm}}}(T)$.

We first need to define a basic disjointifying bisimulation, which makes sure
that worlds are disjoint.

######  Definition 29.

Let $\mathcal{M}$ be a potentialist system. The _disjointification_ of
$\mathcal{M}$, notation $\mathcal{M}^{\bullet}$, is the potentialist system
obtained from $\mathcal{M}$ by replacing the domain of each world $M$ with
$M\times\\{M\\}$, then taking all the embeddings from $\mathcal{M}$, suitably
modified. The _disjointifying bisimulation_ $\rightthreetimes$ is the iso-
bisimulation
$\mathcal{M}\mathrel{\,\raisebox{1.29167pt}{$\underline{\makebox[8.99994pt]{$\leftrightarrow$}}$}\,}\mathcal{M}^{\bullet}$
defined by relating each world in $\mathcal{M}^{\bullet}$ with its original
copy in $\mathcal{M}$:

$M\rightthreetimes M\times\\{M\\}$

Now, the idea to prove Theorem 28 is that we first take the unravelling
$\operatorname{\mathrm{Unrav}}(\operatorname{\operatorname{\mathrm{ModEm}}}(T)^{\bullet})$,
and then start renaming the elements of its worlds so that embeddings become
inclusions. In order to do this consistently, we need to carry out this
process iteratively through sequences of embeddings. See Figure 1 for an
illustration. Fortunately, every world in
$\operatorname{\mathrm{Unrav}}(\operatorname{\operatorname{\mathrm{ModEm}}}(T)^{\bullet})$
remembers a sequence of previous embeddings, and this allows us to carry out
the process.

Figure 1: An example showing that iteratively renaming elements is necessary.
Blobs represent worlds and arrows embeddings. Hook arrows represent
inclusions. To transform the sequence on the left so that embeddings become
inclusions, we need to iteratively rename along the embeddings, as on the
right.

######  Definition 30.

Let $\mathcal{M}$ be a potentialist system, and take a sequence
$\vec{\pi}=\left(M_{0}\xrightarrow{\pi_{1}}\cdots\xrightarrow{\pi_{n}}M_{n}\right)\in\operatorname{\mathrm{Unrav}}(\mathcal{M}^{\bullet})$.
The structure $\operatorname{\mathrm{Coalesce}}(\vec{\pi})$ is the isomorphic
copy of $M_{n}$ defined iteratively by renaming $\pi_{1}[M_{0}]$ as $M_{0}$ in
$M_{1}$, then renaming $\pi_{2}[M_{1}]$ using the result of this, and so on,
as illustrated in Figure 1.

######  Remark 31.

The disjointified version $\mathcal{M}^{\bullet}$ of $\mathcal{M}$ is
necessary because the structure $\operatorname{\mathrm{Coalesce}}(\vec{\pi})$
is only sensible if no renamed element becomes the same as a non-renamed
element. For instance, in the case $n=1$, if there is $a\in
M_{0}\cap(M_{1}\setminus\pi_{1}[M_{0}])$, then the elements $a,\pi_{1}(a)\in
M_{0}$ will have collapsed to a single one
$a\in\operatorname{\mathrm{Coalesce}}(\vec{\pi})$.

######  Definition 32.

Let $T$ be any first-order $L$-theory. Let the _renaming bisimulation_
$\varpropto$ between $\operatorname{\mathrm{Mod}}(T)^{\bullet}$ and
$\operatorname{\mathrm{Unrav}}(\operatorname{\operatorname{\mathrm{ModEm}}}(T)^{\bullet})$
be the iso-bisimulation defined as follows. For any
$\vec{\pi}\in\operatorname{\mathrm{Unrav}}(\operatorname{\operatorname{\mathrm{ModEm}}}(T)^{\bullet})$
put:

$\operatorname{\mathrm{Coalesce}}(\vec{\pi})\varpropto\vec{\pi}$

The isomorphism
$\operatorname{\mathrm{Rename}}_{\vec{\pi}}\colon\operatorname{\mathrm{Coalesce}}(\vec{\pi})\to
M_{\vec{\pi}}$ is the natural renaming isomorphism.

######  Theorem 33.

The renaming bisimulation is a bitotal iso-bisimulation.

###### Proof.

First note that for any $M_{0}\in\operatorname{\mathrm{Mod}}(T)^{\bullet}$, we
have a length-$0$ sequence
$\epsilon_{M_{0}}\in\operatorname{\mathrm{Unrav}}(\operatorname{\operatorname{\mathrm{ModEm}}}(T)^{\bullet})$
with $M_{0}$ as the initial world, and $M_{0}\varpropto\epsilon_{M_{0}}$;
hence $\varpropto$ is left total. It is clearly right total. So we need to
check the isomorphism extension property for iso-bisimulations. Take
$\vec{\pi}\in\operatorname{\mathrm{Unrav}}(\operatorname{\mathrm{Mod}}(T)^{\bullet})$,
so that $\operatorname{\mathrm{Coalesce}}(\vec{\pi})\varpropto\vec{\pi}$.

Assume that $\operatorname{\mathrm{Coalesce}}(\vec{\pi})\subseteq N$ in
$\operatorname{\mathrm{Mod}}(T)$. Define $\rho\colon M_{\vec{\pi}}\to N$ to be
the result of renaming in $M_{\vec{\pi}}$ via
$\operatorname{\mathrm{Rename}}_{\vec{\pi}}^{-1}$, then applying the inclusion
embedding into $N$. Then in fact:

$N=\operatorname{\mathrm{Coalesce}}(\vec{\pi}\rho)$

We have $\rho\colon\vec{\pi}\to\vec{\pi}\rho$ in
$\operatorname{\mathrm{Unrav}}(\operatorname{\operatorname{\mathrm{ModEm}}}(T)^{\bullet})$,
and the following commutative diagram, where the hook arrow represents an
inclusion. See also Figure 2 for a picture-based commutative diagram.

${{N=\operatorname{\mathrm{Coalesce}}(\vec{\pi}\rho)}}$${N}$${{\operatorname{\mathrm{Coalesce}}(\vec{\pi})}}$${M_{\vec{\pi}}}$$\scriptstyle{\operatorname{\mathrm{Rename}}_{\vec{\pi}\rho}}$$\scriptstyle{\operatorname{\mathrm{Rename}}_{\vec{\pi}}}$$\scriptstyle{\rho}$

$\operatorname{\mathrm{Coalesce}}(\vec{\pi})$$N=\operatorname{\mathrm{Coalesce}}(\vec{\pi}\rho)$$M_{\vec{\pi}}$$N$$\operatorname{\mathrm{Rename}}_{\vec{\pi}}$$\operatorname{\mathrm{Rename}}_{\vec{\pi}\rho}$$\rho$
Figure 2: Defining $\rho\colon M_{\vec{\pi}}\to N$ from
$\operatorname{\mathrm{Coalesce}}(\vec{\pi})\subseteq N$. The hook arrow
represents an inclusion.

Conversely, take $\rho\colon\vec{\pi}\to\vec{\pi}\rho$ in
$\operatorname{\mathrm{Unrav}}(\operatorname{\operatorname{\mathrm{ModEm}}}(T)^{\bullet})$
with codomain $N$. Note that by definition
$\operatorname{\mathrm{Coalesce}}(\vec{\pi})\subseteq\operatorname{\mathrm{Coalesce}}(\vec{\pi}\rho)$,
and this is a substructure relation. Moreover, the following diagram commutes.

${{\operatorname{\mathrm{Coalesce}}(\vec{\pi}\rho)}}$${N}$${{\operatorname{\mathrm{Coalesce}}(\vec{\pi})}}$${M_{\vec{\pi}}}$$\scriptstyle{\operatorname{\mathrm{Rename}}_{\vec{\pi}\rho}}$$\scriptstyle{\operatorname{\mathrm{Rename}}_{\vec{\pi}}}$$\scriptstyle{\rho}$

∎

###### Proof of Theorem 28.

Indeed:

$\operatorname{\mathrm{Mod}}(T)\mathrel{\,\raisebox{1.29167pt}{$\underline{\makebox[8.99994pt]{$\leftrightarrow$}}$}\,}\operatorname{\mathrm{Mod}}(T)^{\bullet}\mathrel{\,\raisebox{1.29167pt}{$\underline{\makebox[8.99994pt]{$\leftrightarrow$}}$}\,}\operatorname{\mathrm{Unrav}}(\operatorname{\operatorname{\mathrm{ModEm}}}(T)^{\bullet})\mathrel{\,\raisebox{1.29167pt}{$\underline{\makebox[8.99994pt]{$\leftrightarrow$}}$}\,}\operatorname{\operatorname{\mathrm{ModEm}}}(T)^{\bullet}\mathrel{\,\raisebox{1.29167pt}{$\underline{\makebox[8.99994pt]{$\leftrightarrow$}}$}\,}\operatorname{\operatorname{\mathrm{ModEm}}}(T)$

via bitotal iso-bisimulations. ∎

##  4 Modal Ehrenfeucht-Fraïssé games

We now turn to the connection between bisimulations and games. Modal
Ehrenfeucht-Fraïssé games generalise their non-modal cousins (see [Hod93,
§3.2]).

######  Definition 34.

Let $(\mathcal{M},M,\overline{a})$ and $(\mathcal{N},N,\overline{b})$ be
pointed systems of the same parameter size. The _modal Ehrenfeucht-Fraïssé
game_ :

$\operatorname{\mathrm{MEF}}(\mathcal{M},M,\overline{a},\mathcal{N},N,\overline{b})$

is played by Eloise and Abelard. The positions of the game are quadruples
$(U,\overline{c},Q,\overline{d})$, where $(\mathcal{M},U,\overline{c})$ and
$(\mathcal{N},V,\overline{d})$ are pointed systems of the same parameter size.
The initial position is $(M,\overline{a},N,\overline{b})$. The game proceeds
in moves alternating between Abelard and Eloise. From position
$(U,\overline{c},V,\overline{d})$, Abelard can make one of the following two
kinds of moves.

  1. (a)

Choose $u\in U$ or $v\in V$.

  2. (b)

Choose $\pi\colon U\to U^{\prime}$ in $\mathcal{M}$ or $\rho\colon V\to
V^{\prime}$ in $\mathcal{N}$.

Eloise then responds, respectively, as follows.

  1. (a)

When Abelard chose $u\in U$, choose $v\in V$; otherwise choose $u\in U$. The
new position is then $(U,\overline{c}u,V,\overline{d}v)$.

  2. (b)

When Abelard chose $\pi\colon U\to U^{\prime}$, choose $\rho\colon V\to
V^{\prime}$; otherwise choose $\pi\colon U\to U^{\prime}$. The new position is
then $(U^{\prime},\pi(\overline{c}),V^{\prime},\rho(\overline{d}))$.

A play in the game, consisting of an $\omega$-sequence of positions, is a win
for Eloise if and only if for every position $(U,\overline{c},V,\overline{d})$
in the play, the atomic types agree (in other words
$\overline{c}\mapsto\overline{d}$ is a partial isomorphism):

$\Delta_{0}^{U}(\overline{c})=\Delta_{0}^{V}(\overline{d})$

Often, we want to consider just the set of all positions in the game based on
$\mathcal{M}$ and $\mathcal{M}^{\prime}$, together with the winning
conditions, without fixing an initial position. I will call this the _board_
and denote it by
$\operatorname{\mathrm{MEF}}(\mathcal{M},\mathcal{M}^{\prime})$. This becomes
a game when we specify an initial position.

The following theorem demonstrates the connection between bisimulations and
modal Ehrenfeucht-Fraïssé games. It simultaneously generalises the connection
between non-modal Ehrenfeucht-Fraïssé games (based on two fixed structures)
and back-and-forth systems, on the one hand [Hod93, Lemma 3.2.2], and
bisimulation games and (propositional) bisimulations, on the other [Ben14,
§15.7].

######  Theorem 35.

Eloise has a winning strategy in the game
$\operatorname{\mathrm{MEF}}(\mathcal{M},M,\overline{a},\mathcal{N},N,\overline{b})$
if and only if $(\mathcal{M},M,\overline{a})$ is bisimilar with
$(\mathcal{N},N,\overline{b})$.

###### Proof.

Let $\sim$ be a bisimulation
$(\mathcal{M},M,\overline{a})\mathrel{\,\raisebox{1.29167pt}{$\underline{\makebox[8.99994pt]{$\leftrightarrow$}}$}\,}(\mathcal{N},N,\overline{b})$.
Eloise uses $\sim$ to see how she should play. Note that the conditions (B2)
and (B3) guarantee that no matter what Abelard plays, Eloise can always ensure
the play stays at positions $(U,\overline{c},V,\overline{d})$ such that
$(\mathcal{M},U,\overline{c})\sim(\mathcal{N},V,\overline{d})$.222Note that in
general we need global choice in order to define Eloise’s strategy from the
bisimulation. Then (B1) guarantees that for such positions:

$\Delta_{0}^{U}(\overline{c})=\Delta_{0}^{V}(\overline{d})$

meaning that the resulting play is a win for Eloise.

Now assume that Eloise has a winning strategy in
$\operatorname{\mathrm{MEF}}(\mathcal{M},M,\overline{a},\mathcal{N},N,\overline{b})$.
We can construct a bisimulation by playing as Abelard and seeing what Eloise
does. Put $(U,\overline{c})\sim(V,\overline{d})$ if and only if the position
$(U,\overline{c},V,\overline{d})$ occurs in some play in which Eloise plays
her winning strategy. Let us see that this is a bisimulation. Condition (B1)
follows from the fact that the atomic types of such positions must agree. As
for condition (B2), take $u\in U$. We make Abelard choose this $u\in U$, and
then according to her winning strategy Eloise then plays some $v\in V$, with
the result that $(U,\overline{c}u)\sim(V,\overline{d}v)$. The converse
direction, and condition (B3), are similar. ∎

In the first-order case, the existence of a winning strategy for Eloise in the
Ehrenfeucht-Fraïssé game can be expressed by a formula in an infinitary
language (see [Hod93, §3.5]). An analogous result holds for modal Ehrenfeucht-
Fraïssé games, allowing us to show that two pointed systems are bisimilar if
and only if they are
$L^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}_{\infty}$-elementarily
equivalent. This further yields a converse to the Fundamental Theorem of
Bisimulations (Theorem 21).

######  Theorem 36.

The following are equivalent.

  1. (1)

Eloise has a winning strategy in
$\operatorname{\mathrm{MEF}}(\mathcal{M},M,\overline{a},\mathcal{N},N,\overline{b})$.

  2. (2)

$(\mathcal{M},M,\overline{a})$ is
$L^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}_{\infty}$-elementarily
equivalent to $(\mathcal{N},N,\overline{b})$.

  3. (3)

There is a bisimulation
$(\mathcal{M},M,\overline{a})\mathrel{\,\raisebox{1.29167pt}{$\underline{\makebox[8.99994pt]{$\leftrightarrow$}}$}\,}(\mathcal{N},N,\overline{b})$.

The version of the equivalence $\text{\ref{item:winning; thm:MEF
tfae}}\Leftrightarrow\text{\ref{item:elem equiv; thm:MEF tfae}}$ for non-modal
Ehrenfeucht-Fraïssé games is Theorem 3.5.2 in [Hod93]. I follow the proof
structure given there, modifying to account for:  (1) the additional modal
aspect, and  (2) the fact that potentialist systems can be class-sized.  We
first need some terminology concerning the ranks of game positions.

######  Definition 37.

The _rank_ , notation $\operatorname{\mathrm{Rank}}(p)$, of a position
$p=(M,\overline{a},N,\overline{b})$ in
$\operatorname{\mathrm{MEF}}(\mathcal{M},\mathcal{N})$ is either $-1$, an
ordinal, or $\infty$, and is determined as follows.

  * •

$\operatorname{\mathrm{Rank}}(p)\geqslant 0$ if and only if
$\Delta_{0}^{M}(\overline{a})=\Delta_{0}^{N}(\overline{a})$.

  * •

$\operatorname{\mathrm{Rank}}(p)\geqslant\alpha+1$ if and only if for every
possible move made by Abelard from $p$, Eloise can then move to a position of
rank at least $\alpha$.

  * •

$\operatorname{\mathrm{Rank}}(p)\geqslant\lambda$, for $\lambda$ a limit
ordinal, if and only if $\operatorname{\mathrm{Rank}}(p)\geqslant\alpha$ for
all $\alpha<\lambda$.

######  Lemma 38.

For any ordinal $\alpha$ and pointed systems $(\mathcal{M},M,\overline{a})$
and $(\mathcal{N},N,\overline{b})$ of the same parameter size we have:

$\operatorname{\mathrm{Rank}}(M,\overline{a},N,\overline{b})\geqslant\alpha\text{
in
}\operatorname{\mathrm{MEF}}(\mathcal{M},\mathcal{N})\quad\Leftrightarrow\quad(\mathcal{M},M,\overline{a})\mathrel{\,\raisebox{1.29167pt}{$\underline{\makebox[8.99994pt]{$\leftrightarrow$}}$}\,}_{\alpha}(\mathcal{N},N,\overline{b})$

###### Proof.

This is a refinement of the proof of Theorem 35. Put
$(U,\overline{c})\sim_{\beta}(V,\overline{d})$ if and only if
$\beta\leqslant\min\\{\operatorname{\mathrm{Rank}}(U,\overline{c},V,\overline{d}),\alpha\\}$.
This then gives an $\alpha$-bisimulation
$(\mathcal{M},M,\overline{a})\mathrel{\,\raisebox{1.29167pt}{$\underline{\makebox[8.99994pt]{$\leftrightarrow$}}$}\,}_{\alpha}(\mathcal{N},N,\overline{b})$.
Conversely, if if we have any $\alpha$-bisimulation
$(\mathcal{M},M,\overline{a})\mathrel{\,\raisebox{1.29167pt}{$\underline{\makebox[8.99994pt]{$\leftrightarrow$}}$}\,}_{\alpha}(\mathcal{N},N,\overline{b})$,
then any instance $(U,\overline{c})\sim_{\beta}(V,\overline{d})$ witnesses
that
$\beta\leqslant\operatorname{\mathrm{Rank}}(U,\overline{c},V,\overline{d})$. ∎

######  Lemma 39.

  1. (1)

If $\alpha$ is an ordinal such that every position of rank at least $\alpha$
is also at least $\alpha+1$, then every position of rank at least $\alpha$ is
winning for Eloise.

  2. (2)

A position has rank $\infty$ if and only if it is winning for Eloise. Hence:

$(\mathcal{M},M,\overline{a})\mathrel{\,\raisebox{1.29167pt}{$\underline{\makebox[8.99994pt]{$\leftrightarrow$}}$}\,}(\mathcal{N},N,\overline{b})\quad\Leftrightarrow\quad\forall\alpha\colon(\mathcal{M},M,\overline{a})\mathrel{\,\raisebox{1.29167pt}{$\underline{\makebox[8.99994pt]{$\leftrightarrow$}}$}\,}_{\alpha}(\mathcal{N},N,\overline{b})$

###### Proof.

These facts are proved more generally in Lemma 3.4.1 and Theorem 3.4.2 of
[Hod93]. ∎

As mentioned above, we can express the property of having rank at least
$\alpha$ using an
$L^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}_{\infty}$-formula
of modal-quantifier rank $\alpha$. I will omit the $\mathcal{M}$ from the
superscript of $\theta$ whenever possible.

######  Theorem 40.

Let $(\mathcal{M},M,\overline{a})$ be a pointed system of parameter size $n$.
Take an ordinal $\alpha$. There is an $n$-variable formula
$\theta^{\mathcal{M},M,\overline{a}}_{\alpha}$ in
$L^{{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}}_{\infty}$
of modal-quantifier rank exactly $\alpha$ such that for every pointed system
$(\mathcal{N},N,\overline{b})$ of parameter size $n$, we have:

$\mathcal{N},N\vDash\theta^{\mathcal{M},M,\overline{a}}_{\alpha}\left[\overline{b}\right]\quad\Leftrightarrow\quad\operatorname{\mathrm{Rank}}(M,\overline{a},N,\overline{b})\geqslant\alpha\text{
in }\operatorname{\mathrm{MEF}}(\mathcal{M},\mathcal{N})$

###### Proof.

The formula $\theta^{M,\overline{a}}_{\alpha}$ is defined by recursion on
$\alpha$.

  * •

First:

$\theta^{M,\overline{a}}_{0}(\overline{x})\vcentcolon=\bigwedge\Delta_{0}^{M}(\overline{a})$

  * •

For successor ordinals $\alpha+1$, we need to make sure that Eloise can always
force to a position of rank at least $\alpha$, no matter what Abelard chooses.
Considering the definition of the game, this requires expressing the
following.

    1. (i)

For every $u\in M$ there is $y\in N$ such that
$\theta^{M,(\overline{a}u)}_{\alpha}(\overline{x},y)$ holds at $N$.

    2. (ii)

For every $y\in N$ there is $u\in M$ such that
$\theta^{M,(\overline{a}u)}_{\alpha}(\overline{x},y)$ holds at $N$.

    3. (iii)

For every $\pi\colon M\to M^{\prime}$ there is $\rho\colon N\to N^{\prime}$
such that $\theta^{M,\pi(\overline{a})}_{\alpha}(\rho(\overline{x}))$ holds at
$N^{\prime}$.

    4. (iv)

For every $\rho\colon N\to N^{\prime}$ there is $\pi\colon M\to M^{\prime}$
such that $\theta^{M,\pi(\overline{a})}_{\alpha}(\rho(\overline{x}))$ holds at
$N^{\prime}$.

The first two conditions can be expressed by replacing quantification over $M$
with conjunctions and disjunctions. For the other two conditions, this
strategy does not immediately work, since there may be class-many embeddings
$\pi\colon M\to M^{\prime}$, but we are only allowed to take set-sized
conjunctions and disjunctions. Fortunately, it will follow from the induction
that there are only set-many formulas of the form
$\theta^{M,\pi(\overline{a})}_{\alpha}(\overline{x})$.333In fact, one can show
that there are only set-many formulas of rank $\alpha$ up to equivalence. Let
$\Phi$ be the set of formulas
$\theta^{M,\pi(\overline{a})}_{\alpha}(\overline{x})$ for $\pi\colon M\to
M^{\prime}$ (Even though there may be class-many _names_
$\theta^{M,\pi(\overline{a})}_{\alpha}$, there are only set-many formulas
named by them.). We can now define:

$\theta^{M,\overline{a}}_{\alpha+1}(\overline{x})\vcentcolon=\left(\begin{array}[]{ll}&\bigwedge_{u\in
M}\exists y\theta^{M,(\overline{a}u)}_{\alpha}(\overline{x},y)\\\\[3.00003pt]
\wedge&\forall y\bigvee_{u\in
M}\theta^{M,(\overline{a}u)}_{\alpha}(\overline{x},y)\\\\[3.00003pt]
\wedge&\bigwedge_{\phi\in\Phi}{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}\phi\\\\[3.00003pt]
\wedge&\square\bigvee_{\phi\in\Phi}\phi\end{array}\right)$

  * •

Finally, when $\gamma$ is a limit, we define:

$\theta^{M,\overline{a}}_{\gamma}(\overline{x})\vcentcolon=\bigwedge_{\alpha<\gamma}\theta^{M,\overline{a}}_{\alpha}(\overline{x})$

Note that at each stage the definition of $\theta^{M,\overline{a}}_{\alpha}$
corresponds with the condition that
$\operatorname{\mathrm{Rank}}(M,\overline{a},N,\overline{b})\geqslant\alpha$.
∎

With this key piece we can establish a correspondence between all of the
notions we have of ‘equivalence up to rank $\alpha$’.

######  Theorem 41.

Let $(\mathcal{M},M,\overline{a})$ and $(\mathcal{N},N,\overline{b})$ be
pointed systems of the same parameter size, and let $\alpha$ be an ordinal.
The following are equivalent.

  1. (1)

$\mathcal{M},M\vDash\theta^{\mathcal{N},N,\overline{b}}_{\alpha}[\overline{a}]$.

  2. (2)

$\operatorname{\mathrm{Rank}}(M,\overline{a},N,\overline{b})\geqslant\alpha\text{
in }\operatorname{\mathrm{MEF}}(\mathcal{M},\mathcal{N})$.

  3. (3)

$(\mathcal{M},M,\overline{a})\mathrel{\,\raisebox{1.29167pt}{$\underline{\makebox[8.99994pt]{$\leftrightarrow$}}$}\,}_{\alpha}(\mathcal{N},N,\overline{b})$.

  4. (4)

$(\mathcal{M},M,\overline{a})\equiv^{{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}},\alpha+1}_{\infty}(\mathcal{N},N,\overline{b})$.

###### Proof.

$\text{\ref{item:theta alpha; thm:theta alpha iff alpha elem equiv iff alpha
equiv}}\Leftrightarrow\text{\ref{item:alpha equiv; thm:theta alpha iff alpha
elem equiv iff alpha equiv}}$ is by Theorem 40, $\text{\ref{item:alpha equiv;
thm:theta alpha iff alpha elem equiv iff alpha
equiv}}\Leftrightarrow\text{\ref{item:alpha bis; thm:theta alpha iff alpha
elem equiv iff alpha equiv}}$ is by Lemma 38, and $\text{\ref{item:alpha bis;
thm:theta alpha iff alpha elem equiv iff alpha
equiv}}\Rightarrow\text{\ref{item:elem equiv; thm:theta alpha iff alpha elem
equiv iff alpha equiv}}$ is by Theorem 23.

$\text{\ref{item:elem equiv; thm:theta alpha iff alpha elem equiv iff alpha
equiv}}\Rightarrow\text{\ref{item:theta alpha; thm:theta alpha iff alpha elem
equiv iff alpha equiv}}$. Note that $(N,\overline{b},N,\overline{b})$ is
winning for Eloise in $\operatorname{\mathrm{MEF}}(\mathcal{N},\mathcal{N})$,
and hence has rank at least $\alpha$ by (2) of Lemma 39. Hence by Theorem 40
we have:

$\mathcal{N},N\vDash\theta^{\mathcal{N},N,\overline{b}}_{\alpha}\left[\overline{b}\right]$

But $\theta^{\mathcal{N},N,\overline{b}}_{\alpha}$ has modal-quantifier rank
$\alpha$, whence by assumption:

$\mathcal{M},M\vDash\theta^{\mathcal{N},N,\overline{b}}_{\alpha}[\overline{a}]\qed$

Putting everything together, we can now prove the main result.

###### Proof of Theorem 36.

We have:

$\displaystyle
M,\overline{a}\equiv^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}_{\infty}N,\overline{b}$
$\displaystyle\quad\Leftrightarrow\quad\forall\alpha\colon
M,\overline{a}\equiv^{{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}},\alpha+1}_{\infty}N,\overline{b}$
$\displaystyle\quad\Leftrightarrow\quad\forall\alpha\colon(\mathcal{M},M,\overline{a})\mathrel{\,\raisebox{1.29167pt}{$\underline{\makebox[8.99994pt]{$\leftrightarrow$}}$}\,}_{\alpha}(\mathcal{N},N,\overline{b})$
(Theorem 41) $\displaystyle\quad\Leftrightarrow\quad\text{Eloise will win
}\operatorname{\mathrm{MEF}}(\mathcal{M},M,\overline{a},\mathcal{N},N,\overline{b})$
(Lemma 39)
$\displaystyle\quad\Leftrightarrow\quad(\mathcal{M},M,\overline{a})\mathrel{\,\raisebox{1.29167pt}{$\underline{\makebox[8.99994pt]{$\leftrightarrow$}}$}\,}(\mathcal{N},N,\overline{b})$
(Theorem 35)

∎

##  5 $\operatorname{\mathrm{Mod}}(T)$ and set-sized potentialist systems

The remainder of this article will consider following the question.

######  Question 42.

When is a potentialist system bitotally bisimilar to one consisting of set-
many worlds?

In this section, I focus on those systems of the form
$\operatorname{\mathrm{Mod}}(T)$ for some first-order $L$-theory $T$, and ask
the following specialisation of this question.

######  Question 43.

For which first-order theories $T$ is $\operatorname{\mathrm{Mod}}(T)$
bitotally bisimilar a set-sized potentialist system?

In this section and the next I make use of basic model theoretic terminology
and techniques, such as $\aleph_{0}$-saturated models and the method of
diagrams. For a reference see [Hod93].

Let us first see that answer to 43 is not “all of them”, by considering the
theory of directed graphs. Indeed, this potentialist system has a very rich
structure; see [HW20] for further details.

######  Proposition 44.

Let $L=\\{R\\}$ and let $T$ be the $L$-theory of directed graphs. Then
$\operatorname{\mathrm{Mod}}(T)$ is not bitotally bisimilar with a set-sized
system.

###### Proof.

Using the Fundamental Theorem of Bisimulations (Theorem 21), it suffices to
show that there is a proper class of directed graphs which are pair-wise
distinguishable using
$L^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}_{\infty}$-formulas.
In fact we don’t need to use any modalities for this.

For every ordinal $\alpha$ the set $(\alpha+1,\in)$ is a model of $T$. The
structure of each ordinal can be encoded in an $L_{\infty}$-sentence as
follows. Define the formula $\xi_{\alpha}(x)$ inductively by:

$\xi_{\alpha}(x)\vcentcolon=\bigwedge_{\beta<\alpha}\left(\exists
y(yRx\wedge\xi_{\beta}(y))\right)\wedge\forall
y\left(yRx\rightarrow\bigvee_{\beta<\alpha}\xi_{\beta}(y)\right)$

It can be shown by induction that $(\alpha+1,\in)\vDash\xi_{\beta}[\alpha]$ if
and only if $\alpha=\beta$. Now let:

$\nu_{\alpha}\vcentcolon=\exists x(\forall y\neg xRy\wedge\xi_{\alpha}(x))$

Since every structure $(\alpha+1,\in)$ has a unique top element $\alpha$, we
then have that $(\alpha+1,\in)\vDash\nu_{\beta}$ if and only if
$\alpha=\beta$. ∎

To provide a positive answer to 43, we seek a property of first-order theories
which ensures that $\operatorname{\mathrm{Mod}}(T)$ is not ‘unboundedly
complicated’. The following notion provides a sufficient condition.

######  Definition 45.

Say that a theory $T$ is _$\kappa$ -rich_ for some cardinal
$\kappa\geqslant|L|+\aleph_{0}$ if it has infinite models, and all its models
of size $\kappa$ are $\aleph_{0}$-saturated.

Let us first see a couple of basic results about this notion.

######  Lemma 46.

If $T$ is $\kappa$-rich, and $\lambda\geqslant\kappa$, then $T$ is also
$\lambda$-rich.

###### Proof.

Indeed, let $M\vDash T$ be a $\lambda$-model. Take $S\subseteq M$ finite. By
the Downward Löwenheim-Skolem Theorem, there is an elementary substructure
$N\preccurlyeq M$ of size $\kappa$, containing $S$, which is a model of $T$.
Since $T$ is $\kappa$-rich, every type over $S$ is realised in $N$, and hence
too in $M$. ∎

######  Lemma 47.

Let $T$ be such that every completion is $\kappa$-categorical. Then $T$ is
$\kappa$-rich.

###### Proof.

If all completions are $\kappa$-categorical, then all $\kappa$-models are
saturated, so in particular $\aleph_{0}$-saturated. ∎

Note that the converse doesn’t hold for $\kappa>|L|$. For example, if $T$ is
$|L|$-categorical then it is $|L|^{+}$-rich, but it need not be
$|L|^{+}$-categorical.

We will see that when $T$ is $\kappa$-rich $\operatorname{\mathrm{Mod}}(T)$ is
bisimilar with a certain set-sized system. This system is defined by removing
all the worlds from $\operatorname{\mathrm{Mod}}(T)$ of size greater than
$\kappa$, as follows.

######  Definition 48.

Let $\lambda$ be a cardinal. Define $\operatorname{\mathrm{Mod}}_{\lambda}(T)$
to be the subsystem of $\operatorname{\mathrm{Mod}}(T)$ consisting of those
models of cardinality less than $\lambda$. The system
$\operatorname{\mathrm{ModEm}}_{\lambda}(T)$ is defined similarly.

######  Lemma 49.

The renaming bisimulation
$\varpropto\colon\operatorname{\mathrm{Mod}}(T)\mathrel{\,\raisebox{1.29167pt}{$\underline{\makebox[8.99994pt]{$\leftrightarrow$}}$}\,}\operatorname{\mathrm{ModEm}}(T)$
restricts to a bitotal iso-bisimulation:

$\operatorname{\mathrm{Mod}}_{\lambda}(T)\mathrel{\,\raisebox{1.29167pt}{$\underline{\makebox[8.99994pt]{$\leftrightarrow$}}$}\,}\operatorname{\mathrm{ModEm}}_{\lambda}(T)$

Finally, potentialist systems such as $\operatorname{\mathrm{Mod}}(T)$ and
$\operatorname{\mathrm{Mod}}_{\lambda}(T)$ contain class-many isomorphic
copies of each model. Since we are interested in reducing the size of such
systems, it will be necessary to consider the equivalent system containing
only one model for each isomorphism type.

######  Definition 50.

Let $\mathcal{M}$ be a potentialist system. Its _skeleton_ ,
$\operatorname{\mathrm{Skel}}(\mathcal{M})$, is the skeleton in the category-
theoretic sense, i.e. the quotient under the relation which identifies $M$ and
$M^{\prime}$ if there are mutually inverse embeddings between them in
$\mathcal{M}$. Concretely, for each equivalence class, we pick one
representative, and let $\operatorname{\mathrm{Skel}}(\mathcal{M})$ be the
subsystem of $\mathcal{M}$ consisting of these worlds and all embeddings
between them.

######  Remark 51.

Giving $\operatorname{\mathrm{Skel}}(\mathcal{M})$ a concrete realisation in
general requires some class-level choice, like the Axiom of Global Choice.
This can be avoided here, since we will only consider
$\operatorname{\mathrm{Skel}}(\operatorname{\mathrm{Mod}}_{\lambda}(T))$ for
some $T$, which can be realised by considering a set models of $T$ whose
domain is a subset of some fixed set of size $\lambda$.

######  Lemma 52.

The relation between $\mathcal{M}$ and
$\operatorname{\mathrm{Skel}}(\mathcal{M})$ which associates each structure to
its equivalence class is a bitotal iso-bisimulation.

With the preliminaries in place, the main theorem for this section is ready to
be proved.

######  Theorem 53.

If $T$ is $\kappa$-rich then $\operatorname{\mathrm{Mod}}(T)$ is bitotally
bisimilar with $\operatorname{\mathrm{Mod}}_{\kappa^{+}}(T)$, and thus with a
set-sized potentialist system.

######  Remark 54.

Note that $\operatorname{\mathrm{Mod}}(T)$ is not _iso_ -bisimilar with a set-
sized system, for cardinality reasons.

###### Proof of Theorem 53.

Define $\sim$ between $\operatorname{\mathrm{ModEm}}(T)$ and
$\operatorname{\mathrm{ModEm}}_{\kappa^{+}}(T)$ as follows. Take
$(M,\overline{a})$ from $\operatorname{\mathrm{ModEm}}(T)$ and
$(N,\overline{b})$ from $\operatorname{\mathrm{ModEm}}_{\kappa^{+}}(T)$. There
are two cases.

  * •

Case 1: $|M|\leqslant\kappa$. Put $(M,\overline{a})\sim(N,\overline{b})$ if
and only if $M,\overline{a}\cong N,\overline{b}$.

  * •

Case 2: $|M|>\kappa$. Put $(M,\overline{a})\sim(N,\overline{b})$ if and only
if $|N|=\kappa$ and $\overline{a}$ and $\overline{b}$ have the same $L$-types:
$\operatorname{\mathrm{Tp}}_{M}(\overline{a})=\operatorname{\mathrm{Tp}}_{N}(\overline{b})$.
For each $(M,\overline{a})$, such a $(N,\overline{b})$ must exist in
$\operatorname{\mathrm{ModEm}}_{\kappa^{+}}(T)$ by the Downward Löwenheim-
Skolem Theorem.

Note that $\sim$ is bitotal. Let us verify that it is a bisimulation. Assume
that $(M,\overline{a})\sim(N,\overline{b})$. First note that, by definition,
$M,\overline{a}\equiv N,\overline{b}$. Let us now consider condition (B2) on
bisimulations. There are two cases.

Condition (B2), case 1: $|M|\leqslant\kappa$. Then $M,\overline{a}\cong
N,\overline{b}$. Hence for each $c\in M$, there is $d\in N$ such that
$(M,\overline{a}c)\sim(N,\overline{b}d)$, and conversely.

Condition (B2), case 2: $|M|>\kappa$. Then
$\operatorname{\mathrm{Tp}}_{M}(\overline{a})=\operatorname{\mathrm{Tp}}_{N}(\overline{b})$.
By assumption on $T$ and Lemma 46, both $M$ and $N$ are
$\aleph_{0}$-saturated. Hence for any $c\in M$ there is $d\in N$ such that
$\operatorname{\mathrm{Tp}}_{N}(\overline{b}d)=\operatorname{\mathrm{Tp}}_{M}(\overline{a}c)$,
and conversely.

For condition (B3), there are again two cases.

Condition (B3), case 1: $|M|\leqslant\kappa$. Then by definition there is an
isomorphism $f\colon(M,\overline{a})\to(N,\overline{b})$. Assume that there is
$\pi\colon M\to M^{\prime}$ in $\operatorname{\mathrm{ModEm}}(T)$. If
$|M^{\prime}|\leqslant\kappa$, then by definition there is $\rho\colon N\to
N^{\prime}$ in $\operatorname{\mathrm{ModEm}}_{\kappa^{+}}(T)$ such that $f$
extends to an isomorphism $M^{\prime}\cong N^{\prime}$. If, on the other hand,
$|M^{\prime}|>\kappa$, then by the Downward Löwenheim-Skolem Theorem, there is
$N^{\prime}\preccurlyeq M^{\prime}$ of cardinality $\kappa$ with
$\pi(M)\subseteq N^{\prime}$; note that
$N^{\prime}\in\operatorname{\mathrm{ModEm}}_{\kappa^{+}}(T)$. Then we get an
embedding $\rho\vcentcolon=\pi\circ f^{-1}\colon N\to N^{\prime}$, with the
property that:

$\operatorname{\mathrm{Tp}}_{N^{\prime}}(\rho(\overline{b}))=\operatorname{\mathrm{Tp}}_{N^{\prime}}(\pi(\overline{a}))=\operatorname{\mathrm{Tp}}_{M^{\prime}}(\pi(\overline{a}))$

Whence $(M^{\prime},\pi(\overline{a}))\sim(N^{\prime},\rho(\overline{b}))$.
See Figure 3 for a commutative diagram representing the situation. Conversely,
any morphism $\rho\colon N\to N^{\prime}$ in
$\operatorname{\mathrm{ModEm}}_{\kappa^{+}}(T)$ immediately gives a morphism
$\pi\colon M\to M^{\prime}$, which is the same up to isomorphism.

${M^{\prime}}$${N^{\prime}}$${M}$${N}$$\scriptstyle{f}$$\scriptstyle{\pi}$$\scriptstyle{\pi}$$\scriptstyle{\rho}$
Figure 3: The commutative diagram for (B3), case 1

Condition (B3), case 2: $|M|>\kappa$. Take $\pi\colon M\to M^{\prime}$ in
$\operatorname{\mathrm{ModEm}}(T)$. By a compactness argument, we can see that
that the following is satisfiable (substituting the constants for
$\overline{b}$ from $\operatorname{\mathrm{Diag}}(N)$ for the free variables
in $\operatorname{\mathrm{Tp}}_{M^{\prime}}(\pi(\overline{a}))$).

$T\cup\operatorname{\mathrm{Diag}}(N)\cup\operatorname{\mathrm{Tp}}_{M^{\prime}}(\pi(\overline{a}))(\overline{b})$

Therefore, by the method of diagrams, there is a structure $N^{\prime}\vDash
T$ of cardinality $\kappa$ with and an embedding $\rho\colon N\to N^{\prime}$
such that:

$\operatorname{\mathrm{Tp}}_{N^{\prime}}(\rho(\overline{b}))=\operatorname{\mathrm{Tp}}_{M^{\prime}}(\pi(\overline{a}))$

Whence $(M^{\prime},\pi(\overline{a}))\sim(N^{\prime},\rho(\overline{b}))$.
Conversely, given any morphism $\rho\colon N\to N^{\prime}$ in
$\operatorname{\mathrm{ModEm}}_{\kappa^{+}}(T)$ we can find a corresponding
morphism $\pi\colon M\to M^{\prime}$ by a very similar argument.

Finally, by Theorem 33 and Lemma 52, we have bitotal bisimulations:

$\displaystyle\operatorname{\mathrm{Mod}}(T)$
$\displaystyle\mathrel{\,\raisebox{1.29167pt}{$\underline{\makebox[8.99994pt]{$\leftrightarrow$}}$}\,}\operatorname{\mathrm{ModEm}}(T)$
$\displaystyle\mathrel{\,\raisebox{1.29167pt}{$\underline{\makebox[8.99994pt]{$\leftrightarrow$}}$}\,}\operatorname{\mathrm{ModEm}}_{\kappa^{+}}(T)$
$\displaystyle\mathrel{\,\raisebox{1.29167pt}{$\underline{\makebox[8.99994pt]{$\leftrightarrow$}}$}\,}\operatorname{\mathrm{Mod}}_{\kappa^{+}}(T)$
$\displaystyle\mathrel{\,\raisebox{1.29167pt}{$\underline{\makebox[8.99994pt]{$\leftrightarrow$}}$}\,}\operatorname{\mathrm{Skel}}(\operatorname{\mathrm{Mod}}_{\kappa^{+}}(T))$

the latter of which consists of set-many models. ∎

######  Corollary 55.

Let $T$ be $\kappa$-categorical. Then $\operatorname{\mathrm{Mod}}(T)$ is
bitotally bisimilar with a system consisting of models of size ${<}\kappa$ and
a single $\kappa$-model.

###### Proof.

Note that
$\operatorname{\mathrm{Skel}}(\operatorname{\mathrm{Mod}}_{\kappa^{+}}(T))$
contains a single $\kappa$-size model. ∎

##  6 $\aleph_{0}$-categorical theories

In this section, I investigate 42 from a different direction. Given a
potentialist system $\mathcal{M}$, we can consider its _theory_
$\operatorname{\mathrm{Th}}(\mathcal{M})$: the set of (finitary and non-modal)
$L$-sentences which hold in all of its worlds. I first show that when
$\operatorname{\mathrm{Th}}(\mathcal{M})$ is $\aleph_{0}$-categorical and has
quantifier elimination, then $\mathcal{M}$, irrespective its modal structure,
is bisimilar to a very small potentialist system. On the other hand, I give an
example showing that the result no longer holds when we drop the condition
‘has quantifier elimination’.

######  Theorem 56.

Let $\mathcal{M}$ be a potentialist system which contains an infinite world,
and let $T=\operatorname{\mathrm{Th}}(\mathcal{M})$. Assume that $T$ is
$\aleph_{0}$-categorical and has quantifier elimination. Then $\mathcal{M}$ is
bitotally bisimilar to a system which contains exactly one infinite world,
which is countable, and which has no self-embeddings except the identity.

In particular, when $T$ has no finite models, $\mathcal{M}$ is bitotally
bisimilar to a singleton system consisting of a countable world with just the
identity embedding.

######  Remark 57.

In Theorem 16 of [HW20] it is shown that if a theory $T$ admits quantifier
elimination, then it admits ‘modality elimination’ over
$\operatorname{\mathrm{Mod}}(T)$: every
${\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}\phi\in
L^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}$
is equivalent in $\operatorname{\mathrm{Mod}}(T)$ to $\phi$. When $T$ is
$\aleph_{0}$-categorical, this can be seen as a special case of our Theorem
56, using the Fundamental Theorem of Bisimulations (Theorem 21). Indeed, if
$M$ is a world in a potentialist system which sees only the identity
embedding, then for every $\phi\in
L^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}_{\infty}$
and $\overline{a}$ in $M$ we have that $\mathcal{M},M\vDash\phi[\overline{a}]$
if and only if
$\mathcal{M},M\vDash{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}\phi[\overline{a}]$.

###### Proof of Theorem 56.

Define the system $\mathcal{N}$ as follows. Start with all the finite worlds
of $\mathcal{M}$ together with the embeddings between them. Let $Q$ be a
countable model of $T$. Add $Q$ to $\mathcal{N}$, together with the identity
embedding. Furthermore, for every finite world $M$ in $\mathcal{M}$ and
embedding $\pi\colon M\to M^{\prime}$ into an infinite world, by the Downward
Lowenheim-Skolem Theorem we can realise $\pi$ as an embedding $\pi^{*}\colon
M\to Q$. Add $\pi^{*}$ into $\mathcal{N}$. Note that multiple embeddings may
result in the same starred versions which are added to $\mathcal{N}$.

Now define the relation $\sim$ between $\mathcal{M}$ and $\mathcal{N}$ from
two cases (c.f. the proof of Theorem 53).

  * •

Case 1: $M$ is finite. Relate $(M,\overline{a})$ and $(N,\overline{b})$ if and
only if they are equal.

  * •

Case 2: $M$ is infinite. Relate $(M,\overline{a})$ and $(N,\overline{b})$ if
and only if $N=Q$ and $\overline{a}$ and $\overline{b}$ agree on all atomic
formulas: $\Delta_{0}^{M}(\overline{a})=\Delta_{0}^{N}(\overline{b})$.

It is not hard to see using the Downward Lowenheim-Skolem Theorem that this is
a bitotal relation. Let us verify that it is a bisimulation. Assume that
$(M,\overline{a})\sim(N,\overline{b})$.

  * (B1)

The first condition follows by definition.

  * (B2)

When $M$ is finite this condition is immediate, so assume that $M$ is
infinite. By the Ryll-Nardzewski Theorem applied to
$\operatorname{\mathrm{Th}}(M)$, the type of every tuple is principal.
Moreover, since $T$ has quantifier elimination, the complete types of
$\overline{a}$ and $\overline{b}$ are the same. Hence any extension of one can
be mirrored in the other.

  * (B3)

There are several cases to consider. If $M$ is infinite, then since any
embedding preserves atomic types, any modal extension on one side can be
mirrored on the other. So we can assume that $M$ is finite (and hence $N=M$).
Now any embedding from a finite world to a finite world on on side can be
identically mirrored on the other, since $\mathcal{N}$ includes all embeddings
from $\mathcal{M}$ between finite worlds. So we are left with two cases.  (i)
If we have $\pi\colon M\to M^{\prime}$ in $\mathcal{M}$ with $M^{\prime}$
infinite, then as above we can realise this as $\pi^{*}\colon M\to Q$. Note
that the atomic types of $\pi(\overline{a})$ and $\pi^{*}(\overline{b})$ are
the same.  (ii) If we have $\pi^{*}\colon N\to Q$ in $\mathcal{N}$, then by
definition there is $\pi\colon M\to M^{\prime}$ in $\mathcal{M}$ from which
$\pi^{*}$ was obtained. Again the atomic types of $\pi(\overline{a})$ and
$\pi^{*}(\overline{b})$ are the same.∎

######  Corollary 58.

Let $T$ be an $\aleph_{0}$-categorical first-order $L$-theory which has
quantifier elimination and no finite models. Then between any two potentialist
systems which consist of models of $T$ there is a bitotal bisimulation.

A partial converse can be obtained to Theorem 56. In order to make it work, we
need to make sure that $\mathcal{M}$ has ‘enough structure’ from
$\operatorname{\mathrm{Mod}}(T)$.

######  Theorem 59.

Let $\mathcal{M}$ be a potentialist system and let
$T=\operatorname{\mathrm{Th}}(\mathcal{M})$. Assume that $\mathcal{M}$ has a
isomorphic copy of every countable model of $T$, together with all embeddings
between these isomorphic copies. Assume further that $\mathcal{M}$ is
bitotally bisimilar to a system $\mathcal{N}$ which contains exactly one
infinite world which has no self-embeddings except the identity. Then $T$ is
$\aleph_{0}$-categorical and has quantifier elimination.

Note that we don’t need the infinite world in $\mathcal{N}$ to be countable.

###### Proof.

Let $Q$ be the unique infinite world in $\mathcal{N}$, and let $\sim$ be the
bisimulation between $\mathcal{M}$ and $\mathcal{N}$. Note that if $M$ in
$\mathcal{M}$ is infinite, then every pair $(M,\overline{a})$ is related to a
pair with $Q$.

First, let us see that $T$ is $\aleph_{0}$-categorical. Take $X,Y$ any
countable models of $T$. We can assume without loss of generality that $X$ and
$Y$ are in $\mathcal{M}$. We will build up an isomorphism $X\cong Y$ using a
back-and-forth argument. First, using that $\sim$ is bitotal, for any
$x_{0}\in X$ the pair $(X,(x_{0}))$ is related to some pair $(Q,(q_{0}))$,
which must in turn be related some pair $(Y,(y_{0}))$. Going the other
direction, for any $y_{1}\in Y$, the pair $(Y,(y_{0},y_{1}))$ is related to
some $(Q,(q_{0},q_{1}))$, which is related to some $(X,(x_{0},x_{1}))$.
Proceeding in this way, using enumerations of $X$ and $Y$, we obtain a
bijection $X\to Y$. Using condition (B1) on bisimulations, each finite
correspondence is a partial isomorphism. Hence the whole correspondence $X\to
Y$ is an isomorphism.

Second, let us check that $T$ admits quantifier elimination. First note that
since $T$ is $\aleph_{0}$-categorical, it is complete. Let $r$ be any atomic
type over $T$, and let $p$ and $q$ be extensions of $r$ to a complete type.
The goal is to show that $p=q$. Let $W\in\mathcal{M}$ be a countable model
with $\overline{w}$ in $W$ realising $r$. Since $\sim$ is bitotal, there is a
pair $(Q,\overline{q})$ related to $(W,\overline{w})$. By a compactness
argument, using that $T$ is complete, there are countable models $X$ and $Y$
of $T$ and embeddings $\pi\colon W\to X$ and $\rho\colon W\to Y$ such that
$\pi(\overline{w})$ realises $p$ and $\rho(\overline{w})$ realises $q$. We can
assume that $X,Y,\pi,\rho$ are in $\mathcal{M}$. Now, since in $\mathcal{N}$
the only embedding from $Q$ is the identity, we have that:

$(X,\rho(\overline{w}))\sim(Q,\overline{q})\sim(Y,\rho(\overline{w}))$

By the Fundamental Theorem of Bisimulations (Theorem 21), in particular:

$X,\rho(\overline{w})\equiv Y,\rho(\overline{w})$

Hence $p=q$ as required. ∎

Let us see that it is necessary to assume that $\mathcal{M}$ has a isomorphic
copy of every countable model of $T$. Let $T$ be the theory of non-zero
$\mathbb{Q}$-vector spaces, and let $\mathcal{M}$ be the subsystem of
$\operatorname{\mathrm{Mod}}(T)$ consisting of the uncountable worlds. Then
$\mathcal{M}$ is bitotally bisimilar with the system consisting just of the
$\aleph_{0}$-dimensional $\mathbb{Q}$-vector space with the identity
embedding. However $T=\operatorname{\mathrm{Th}}(\mathcal{M})$ is not
$\aleph_{0}$-categorical.

I conclude this section with an example of how things can go wrong for Theorem
56 when we don’t require that $T$ admit quantifier elimination. The point is
that once we are allowed to play with slightly more intricate first-order
models, we can start arranging them to produce a rich modal structure.

Let $L=\\{\approx\\}$, and let $T$ specify that $\approx$ is an equivalence
relation with infinitely many size-$1$ and size-$2$ equivalence classes, and
no other classes. Then $T$ is $\aleph_{0}$-categorical, but does not have
quantifier elimination. However every one-variable formula is equivalent to
either an existential or a universal formula.

We construct for every ordinal $\alpha$ a pointed system
$(\mathcal{M}_{\alpha},M_{\alpha})$ of countable models of $T$. See Figure 4
for a representation of the system $\mathcal{M}_{3}$. The underlying modal
structure of $\mathcal{M}_{\alpha}$ is the result of viewing $\alpha$ as a
well-founded tree $X_{\alpha}$. (That is, $X_{\alpha}$ consists of a root
sitting below disjoint copies of each $X_{\beta}$ for $\beta<\alpha$.) We
place countable models of $T$ along this structure as follows. First let $N$
be any countable model. At the root of $X_{\alpha}$ we place a model
consisting of $N$ plus new elements $u_{0},u_{1},\ldots$, each in a singleton
equivalence class. On the next level up we place disjoint copies of the same
model with a new element $v_{0}$, which appears in an equivalence class with
$u_{0}$. The model at the root embeds into those above it via the inclusion
embedding. The construction proceeds upwards in this fashion. Let $M_{\alpha}$
be the model appearing at the root in this system.

$N$$u_{0}$$u_{1}$$u_{2}$$\cdots$$N$$u_{0}$$v_{0}$$u_{1}$$u_{2}$$\cdots$$N$$u_{0}$$v_{0}$$u_{1}$$u_{2}$$\cdots$$N$$u_{0}$$v_{0}$$u_{1}$$v_{1}$$u_{2}$$\cdots$$N$$u_{0}$$v_{0}$$u_{1}$$u_{2}$$\cdots$$N$$u_{0}$$v_{0}$$u_{1}$$v_{1}$$u_{2}$$\cdots$$N$$u_{0}$$v_{0}$$u_{1}$$v_{1}$$u_{2}$$\cdots$$N$$u_{0}$$v_{0}$$u_{1}$$v_{1}$$u_{2}$$v_{2}$$\cdots$$\mathcal{M}_{3}$
Figure 4: The potentialist system $\mathcal{M}_{3}$

######  Theorem 60.

Each $(\mathcal{M}_{\alpha},M_{\alpha})$ satisfies a different
$L^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}_{\infty}$-theory.
Hence the system consisting of the disjoint union of each
$\mathcal{M}_{\alpha}$ cannot be bitotally bisimilar with a set-sized system.

###### Proof.

The idea is that each pair $(u_{m},v_{m})$ acts as a ‘button’. The lowest
model has all $\aleph_{0}$-many buttons unpushed. Each time we move up a
level, we push an extra button (i.e. add the element $v_{m}$ to make a
$2$-element equivalence class). Of course, each model is isomorphic, so the
first-order structure cannot tell us how many buttons have been pushed, or how
far up the tree we are. However, using the modal language, we can indeed talk
about pushing a button, to get to a higher level.

Let:

$\displaystyle p(x)\vcentcolon=\neg\exists y(x\neq y\wedge x\approx y)$
$\displaystyle q(x)\vcentcolon=\exists y(x\neq y\wedge x\approx y)$

Define for each $\alpha$ the sentence $\theta_{\alpha}$ by induction:

$\theta_{\alpha}\vcentcolon=\exists
x\left(p(x)\wedge\bigwedge_{\beta<\alpha}{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}(q(x)\wedge\theta_{\beta})\right)\wedge\forall
x\left(p(x)\rightarrow\square\left(q(x)\rightarrow\bigvee_{\beta<\alpha}\theta_{\beta}\right)\right)$

In words: “there is a button which is pushed in future models satisfying
$\theta_{\beta}$ for all $\beta<\alpha$, and whenever a button gets pushed in
the future, that model satisfies $\theta_{\beta}$ for some $\beta<\alpha$”. By
induction we see that:

$\mathcal{M}_{\beta},M_{\beta}\vDash\theta_{\alpha}\quad\Leftrightarrow\quad\beta=\alpha$

Therefore, each $(\mathcal{M}_{\alpha},M_{\alpha})$ satisfies a different
$L^{\mathchoice{\raisebox{0.8pt}{$\displaystyle\meddiamond$}}{\raisebox{0.8pt}{$\textstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptstyle\meddiamond$}}{\raisebox{0.8pt}{$\scriptscriptstyle\meddiamond$}}}_{\infty}$-theory.

Now, let $\mathcal{M}$ be the disjoint union of every $\mathcal{M}_{\alpha}$.
If this were bitotally bisimilar with a set-sized system $\mathcal{N}$, then
class-many of the $M_{\alpha}$’s would be related to the same world in $N$.
But this is impossible by the Fundamental Theorem of Bisimulations (Theorem
21). ∎

##  7 Open questions

The first part of this article presented a number of foundational results
concerning bisimulations of potentialist systems. The second part considered
42: when is a potentialist system $\mathcal{M}$ bisimilar with a set-sized
one? In Section 5, I showed that if $T$ is $\kappa$-rich for some $\kappa$
then $\operatorname{\mathrm{Mod}}(T)$ is bisimilar with a set-sized system.
Does the converse hold? An iteration argument shows that if
$\operatorname{\mathrm{Mod}}(T)$ is bisimilar with a set-sized system, is it
necessarily bisimilar with some $\operatorname{\mathrm{Mod}}_{\lambda}(T)$.
Will it further be bisimilar with some
$\operatorname{\mathrm{Mod}}_{\kappa^{+}}(T)$?

Section 6 seeks to give answers to 42 based solely on
$\operatorname{\mathrm{Th}}(\mathcal{M})$. This is a rather crude measure, and
takes no account of the modal structure of $\mathcal{M}$. Theorem 56 shows
that if $\operatorname{\mathrm{Th}}(\mathcal{M})$ is $\aleph_{0}$-categorical
and admits quantifier elimination, then $\mathcal{M}$ is bisimilar with a set-
sized system. Is this the best result possible? If instead of
$\operatorname{\mathrm{Th}}(\mathcal{M})$ we consider the set of (finitary)
first-order modal sentences satisfied by $\mathcal{M}$, can we obtain a more
general characterisation?

##  8 Acknowledgements

I would like to thank my supervisor, Joel David Hamkins, for helpful guidance
and proof-reading throughout the process of writing this article. This work
was supported by the EPSRC [studentship with project reference _2271793_].

## References

  * [Ben10] Johan Benthem  “Modal logic for open minds”, CSLI lecture notes 199  Stanford, California: CSLI, 2010
  * [Ben14] Johan Benthem  “Logic in Games”  The MIT Press, 2014  DOI: 10.7551/mitpress/9674.001.0001
  * [BRV01] Patrick Blackburn, Maarten de Rijke and Yde Venema  “Modal logic”, Cambridge tracts in theoretical computer science 53  Cambridge: Cambridge University Press, 2001
  * [CZ97] Alexander Chagrov and Michael Zakharyaschev  “Modal logic”, Oxford logic guides 35  Oxford: Clarendon Press, 1997
  * [FM98] Melvin Fitting and Richard L Mendelsohn  “First-order modal logic”, Synthese library 277  Dordrecht; London: Kluwer Academic, 1998
  * [Ham03] Joel David Hamkins  “A simple maximality principle”  In _Journal of Symbolic Logic_ 68.2 Cambridge University Press, 2003, pp. 527–550  DOI: 10.2178/jsl/1052669062
  * [Ham18] Joel David Hamkins  “The modal logic of arithmetic potentialism and the universal algorithm”, 2018  arXiv:1801.04599 [math.LO]
  * [HC96] G.. Hughes and M.. Cresswell  “A new introduction to modal logic”  London: Routledge, 1996
  * [HL08] Joel David Hamkins and Benedikt Löwe  “The modal logic of forcing”  In _Transactions of the American Mathematical Society_ 360.4, 2008, pp. 1793–1817  DOI: 10.1090/S0002-9947-07-04297-3
  * [HL13] Joel David Hamkins and Benedikt Löwe  “Moving up and down in the generic multiverse”  In _Logic and its Applications, ICLA 2013 LNCS_ 7750 Springer, 2013, pp. 139–147  DOI: 10.1007/978-3-642-36039-8_13
  * [HL19] Joel David Hamkins and Øystein Linnebo  “The modal logic of set-theoretic potentialism and the potentialist maximality principles”  In _Review of Symbolic Logic_ , 2019, pp. 1–36  DOI: 10.1017/S1755020318000242
  * [HLL15] Joel David Hamkins, George Leibman and Benedikt Löwe  “Structural connections between a forcing class and its modal logic” E-print available: https://eprints.illc.uva.nl/id/eprint/461/ In _Israel Journal of Mathematics_ 207.2 Springer, 2015, pp. 617–651
  * [Hod93] Wilfrid Hodges  “Model theory”, Encyclopedia of mathematics and its applications 42  Cambridge: Cambridge University Press, 1993
  * [HW18] Joel David Hamkins and W. Woodin  “The universal finite set”, 2018  arXiv:1711.07952 [math.LO]
  * [HW20] Joel David Hamkins and Wojciech Aleksander Wołoszyn  “Modal model theory”, 2020  arXiv:2009.09394 [math.LO]
  * [HW21] Joel David Hamkins and Kameryn J. Williams  “The Σ1-definable universal finite sequence”  In _The Journal of Symbolic Logic_ Cambridge University Press, 2021, pp. 1–19  DOI: 10.1017/jsl.2020.59
  * [Lin13] Øystein Linnebo  “The potential hierarchy of sets”  In _The Review of Symbolic Logic_ 6.2 Cambridge University Press, 2013, pp. 205–228  DOI: 10.1017/S1755020313000014
  * [SS18] Denis I. Saveliev and Ilya B. Shapirovsky  “On modal logics of model-theoretic relations”, 2018  DOI: 10.48550/ARXIV.1804.09810
  * [Woł22] Wojciech Aleksander Wołoszyn  “Modal theory of the category of sets” Preprint in preparation, 2022