1–LABEL:LastPageJan. 02, 2017Jul. 26, 2018

# A Ghost at $\omega_{1}$

Paul Blain Levy  University of Birmingham<EMAIL_ADDRESS>
###### Abstract.

In the final chain of the countable powerset functor, we show that the set at
index $\omega_{1}$, regarded as a transition system, is not strongly
extensional because it contains a “ghost” element that has no successor even
though its component at each successor index is inhabited. The method, adapted
from a construction of Forti and Honsell, also gives ghosts at larger ordinals
in the final chain of other subfunctors of the powerset functor. This leads to
a precise description of which sets in these final chains are strongly
extensional.

_For Jirka Adámek on his 70th birthday, with thanks for his many contributions
and the inspiration he has given to our community._

##  1\. Introduction

Initial algebras and final coalgebras of endofunctors are important in many
areas of mathematics and computer science. One versatile way of constructing
an initial algebra of $F$ is to form the _initial chain_ [Adá74], a
transfinite sequence of objects $(\mu^{(i)}{F})_{i\in\mathsf{Ord}}$ where
$\mathsf{Ord}$ denotes the class of ordinals. We form the initial chain by
applying $F$ at each successor ordinal and taking a colimit at each limit
ordinal. If it stabilizes, it yields an initial algebra $\mu F$. Dually
[Bar93], we form the _final chain_ $(\nu^{(i)}{F})_{i\in\mathsf{Ord}}$, by
applying $F$ at each successor ordinal and taking a limit at each limit
ordinal. If it stabilizes, it yields a final coalgebra $\nu F$.

These constructions make sense for any endofunctor on any category, provided
the relevant colimits or limits exist. But certain endofunctors on
$\mathbf{Set}$ have received particular attention: the powerset functor
($\mathcal{P}$) and its subfunctors, notably finite powerset
($\mathcal{P}_{\mathsf{f}}$) and countable powerset
($\mathcal{P}_{\mathsf{c}}$), which send a set to its set of finite or
countable subsets respectively. That is because these functors have many
applications, e.g. nondeterministic automata, the semantics of
nondeterministic programs and the foundations of set theory. For cardinality
reasons, the powerset functor has no initial algebra or final coalgebra; when
we refer to $\mu\mathcal{P}$ or $\nu\mathcal{P}$, these are proper classes. By
contrast, $\mathcal{P}_{\mathsf{f}}$ and $\mathcal{P}_{\mathsf{c}}$ do have a
(small) initial algebra and final coalgebra.

Now the initial chains of $\mathcal{P}_{\mathsf{f}}$ and
$\mathcal{P}_{\mathsf{c}}$ are easy to understand: each is an increasing
sequence of subsets of the initial algebra. But the final chains are more
subtle. Their form was established in [ALM+15, Wor05].

  * •

$\nu^{(\omega)}{\mathcal{P}_{\mathsf{f}}}$ consists of the final coalgebra and
some extra elements. The next $\omega$ steps in the final chain of
$\mathcal{P}_{\mathsf{f}}$ remove these extra elements, and the chain
stabilizes at $\omega+\omega$.

  * •

$\nu^{(\omega_{1})}{\mathcal{P}_{\mathsf{c}}}$ consists of the final coalgebra
and some extra elements. The next $\omega$ steps in the final chain of
$\mathcal{P}_{\mathsf{c}}$ remove these extra elements, and the chain
stabilizes at $\omega_{1}+\omega$.

These descriptions may give the impression that the final chains of
$\mathcal{P}_{\mathsf{f}}$ and $\mathcal{P}_{\mathsf{c}}$ are essentially
similar. However, they tell only part of the story. For
$\nu^{(\omega)}{\mathcal{P}_{\mathsf{f}}}$, as well as being a _superset_ of
$\nu\mathcal{P}_{\mathsf{f}}$, is also a _subset_ of $\nu\mathcal{P}$. This is
because it can be endowed with a transition relation, setting
$x\rightsquigarrow y$ when $y_{n}\in x_{n+1}$ for all $n\in\mathbb{N}$, that
makes it into a _strongly extensional_ transition system, i.e. one where
bisimilarity is equality. Specifically, Worrell [Wor05] characterized
$\nu^{(\omega)}{\mathcal{P}_{\mathsf{f}}}$ as the set of _compactly branching_
elements111Elements of $\nu\mathcal{P}$ are represented in [ALM+15, Sch10,
Wor05] as strongly extensional trees modulo isomorphism. Those trees are
unrelated to the trees used in this paper. of $\nu\mathcal{P}$, also studied
in [Abr05, KKV04]. While all these elements are compactly branching, they are
not all finitely (or even countably) branching, and the extra $\omega$ steps
are required to remove those that are not, so that only the finitely branching
elements remain.

Is there a similar story for $\nu^{(\omega_{1})}{\mathcal{P}_{\mathsf{c}}}$?
The question is asked in [ALM+15]. This set too can be endowed with a
transition relation, setting $x\rightsquigarrow y$ when $y_{i}\in x_{i+1}$ for
all $i<\omega_{1}$. But the resulting transition system is not strongly
extensional. We demonstrate this by giving two distinct elements that are
“dead” in the sense of having no successor. One of these is the expected dead
element: each component at a successor index is empty. The other’s components
at successor index are all inhabited. Since the latter “appears to be alive”,
yet is dead, we call it a _ghost_.

Thus we see a significant difference between
$\nu^{(\omega)}{\mathcal{P}_{\mathsf{f}}}$ and
$\nu^{(\omega_{1})}{\mathcal{P}_{\mathsf{c}}}$. An element of
$\nu^{(\omega)}{\mathcal{P}_{\mathsf{f}}}$ may lie outside the final coalgebra
of $\mathcal{P}_{\mathsf{f}}$, but only because it is not finitely branching.
By contrast, an element of $\nu^{(\omega_{1})}{\mathcal{P}_{\mathsf{c}}}$ may
lie outside the final coalgebra of $\mathcal{P}_{\mathsf{c}}$ despite having
no successors at all.

### Structure of Paper

Before introducing the final chain, Section 2 gives preliminaries on
transitions systems, cardinals, and the sequence of approximants to
bisimilarity. Section 3 introduces the final chain of a general functor, and
in particular of the powerset and restricted powerset functors. It also
introduces the notions of channel and range that help us to understand these
final chains.

The main narrative begins in Section 4, which endows the final chain of
$\mathcal{P}$ with the structure of a transition system and describe its basic
properties. The rest of the paper is devoted to studying this system.

In Section 5 our focus is on those properties that hold specifically at
_countable_ ordinals. This leads us in Section 6 to the question of whether
these properties—most importantly, strong extensionality—hold at $\omega_{1}$.
We prove that there is a ghost and deduce that these properties do not hold.

The ghost is obtained by adapting a method in [FH89]. The next two sections
give further results that showcase the power of this method.

  * •

Section 7 answers the question: how many successors may an element of the
final chain of $\mathcal{P}_{\mathsf{c}}$ have?

  * •

Section 8 looks at larger subfunctors of $\mathcal{P}$ corresponding to
subsets of larger cardinality, and their final chain beyond $\omega_{1}$.
Remarkably, we see a sharp division: at each limit ordinal $i$, either the
$i$th set is strongly extensional or there is a ghost. We thus revisit each of
the properties we initially proved at countable ordinals, including
surjectivity of connecting maps, and completely characterize the ordinals at
which they hold.

We end with a discussion of related work in Section 9 and conclusions in
Section 10.

### Acknowledgements.

I thank David Fernandez-Breton and Benedikt Löwe for supplying the information
in footnotes 4–5.

##  2\. Preliminaries

###  2.1. Pointed Systems

A _transition system_ consists of a set $X$ and relation
$\rightsquigarrow\,\subseteq X\times X$. When $x\rightsquigarrow y$ we say
that $y$ is a _successor_ of $x$. A subset $U\subseteq X$ is a _subsystem_
when, for all $x\in U$, every successor of $x$ is in $U$. An _embedding_ of
transition systems $e\colon M\to N$ is an isomorphism from $M$ to a subsystem
of $N$.

A _pointed system_ consists of a transition system $M=(X,\rightsquigarrow)$
and an element $x\in X$. Given a family of pointed systems
$((M_{i},x_{i}))_{i\in I}$, a _parent_ of the family is a pointed system
$(N,y)$ equipped with embeddings $(e_{i}\colon M_{i}\to N)_{i\in I}$ such that
the successors of $y$ are listed without repetition as $(e_{i}(x_{i}))_{i\in
I}$. A parent may be constructed as follows: if each $M_{i}$ is
$(X_{i},\rightsquigarrow_{i})$, define

$\displaystyle N$ $\displaystyle\stackrel{{\scriptstyle\mbox{\rm{\tiny
def}}}}{{=}}$ $\displaystyle(1+\sum_{i\in I}X_{i},\rightsquigarrow)\hskip
10.00002pt\text{with $\rightsquigarrow$ given in the evident way}$
$\displaystyle y$ $\displaystyle\stackrel{{\scriptstyle\mbox{\rm{\tiny
def}}}}{{=}}$ $\displaystyle\mathsf{inl}\,*$ $\displaystyle e_{i}$
$\displaystyle\colon$ $\displaystyle z\mapsto\mathsf{inr}\,(i,z)$

We generalize transition systems to coalgebras. Let $F$ be an endofunctor on
$\mathbf{Set}$, e.g. the powerset functor $\mathcal{P}$, which sends a set $X$
to $\mathcal{P}X$ and a function $f\colon A\to B$ to $U\mapsto\\{{f(a)\mid
a\in U}\\}$. An _$F$ -coalgebra_ consists of a set $X$ and map $X\to FX$. Thus
a transition system corresponds to a $\mathcal{P}$-coalgebra. An _$F$
-coalgebra morphism_ $(X,\zeta)\to(Y,\xi)$ is a map $f\;:\;X\to Y$ such that
$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\zeta}$$\scriptstyle{f}$$\textstyle{Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\xi}$$\textstyle{FX\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Ff}$$\textstyle{FY}$
commutes. For example, an embedding of transition systems corresponds to an
injective $\mathcal{P}$-coalgebra morphism. A _pointed $F$-coalgebra_ consists
of an $F$-coalgebra $M=(X,\zeta)$ together with an element $x\in X$.

We often write a pointed system or pointed coalgebra $(M,x)$ as just $x$,
leaving $M$ implicit.

###  2.2. Cardinals

As usual, we identify a cardinal with the least ordinal of that cardinality.
Thus we identify $\aleph_{0}$ with $\omega$ and $\aleph_{1}$ with
$\omega_{1}$—the least uncountable ordinal. The special symbol $\infty\infty$
is treated as greater than every cardinal and ordinal.

Let $\kappa$ be either a cardinal or $\infty\infty$. For a set $X$, we write
$\mathcal{P}_{{<\kappa}}X$ for the set of its $<\\!\\!\kappa$-sized subsets.
This gives a subfunctor $\mathcal{P}_{{<\kappa}}$ of $\mathcal{P}$. In
particular:

$\displaystyle\mathcal{P}_{\mathsf{f}}$ $\displaystyle=$
$\displaystyle\mathcal{P}_{<\aleph_{0}}$
$\displaystyle\mathcal{P}_{\mathsf{c}}$ $\displaystyle=$
$\displaystyle\mathcal{P}_{<\aleph_{1}}$ $\displaystyle\mathcal{P}$
$\displaystyle=$ $\displaystyle\mathcal{P}_{<\infty\infty}$

We also refer to the functor $\mathcal{P}^{+}_{<\kappa}$, that sends a set $X$
to the set of $<\\!\\!\kappa$-sized subsets that are inhabited.

A pointed system $(M,x)$ is _$ <\\!\\!\kappa$-branching_ when
$x\rightsquigarrow^{*}y$ implies that $y$ has $<\\!\\!\kappa$-many successors.
This is equivalent to $(M^{\prime},x)$ being a pointed
$\mathcal{P}_{{<\kappa}}$-coalgebra, for some subsystem $M^{\prime}$ of $M$.

Henceforth we assume that $\kappa$ is _infinite and regular_. (In particular
$\aleph_{0}$ is regular, as are infinite successor cardinals such as
$\aleph_{1}$. But $\aleph_{\omega}$, for example, is not. We deem
$\infty\infty$ to be regular.) This makes $\mathcal{P}_{{<\kappa}}$ a submonad
of $\mathcal{P}$, and it also gives the following.

######  Proposition 1.

For a $<\\!\\!\kappa$-sized set $A$, any decreasing sequence of subsets
$(X_{i})_{i<\kappa}$ is eventually constant. In particular, if each $X_{i}$ is
inhabited then so is $\bigcap_{i<\kappa}X_{i}$.

###  2.3. Approximants to bisimilarity

The class of pointed systems is equipped with a decreasing sequence
$(\sim_{i})_{i\in\mathsf{Ord}}$ of equivalence relations, defined as follows
[Mal76, Mil89].

  * •

$x\sim_{i+1}x^{\prime}$ when for every $x\rightsquigarrow y$ there is
$x^{\prime}\rightsquigarrow y^{\prime}$ such that $y\sim_{i}y^{\prime}$, and
_vice versa_.

  * •

If $i$ is a limit, then $x\sim_{i}x^{\prime}$ when for all $j<i$ we have
$x\sim_{j}x^{\prime}$.

  * •

We deem $0$ a limit, so $x\sim_{0}x^{\prime}$ always.

We say that $x$ and $x^{\prime}$ are _bisimilar_ , written $x\sim x^{\prime}$,
when for all $i\in\mathsf{Ord}$ we have $x\sim_{i}x^{\prime}$. In particular,
for any embedding $e\colon M\to N$ we have $(N,e(x))\sim(M,x)$. The following
is a key tool for analyzing these relations. Pointed systems
$(v_{i})_{i\in\mathsf{Ord}}$ are defined as follows: $v_{i}$ is a parent of
$(v_{j})_{j<i}$. Essentially Definition 2.3 is the von Neumann encoding of the
ordinals. It is useful because of the following facts.

######  Proposition 2.

Let $i$ and $j$ be ordinals.

  1. (1)

For an ordinal $k$, we have $v_{i}\sim_{k}v_{j}$ iff either $i=j$ or
$k\leqslant i,j$.

  2. (2)

We have $v_{i}\sim v_{j}$ iff $i=j$.

######  Proof 2.1.

Part (1) is by induction on $k$ and part (2) follows.

The approximants to bisimilarity have the following properties.

######  Proposition 3.

  1. (1)

Let $x$ be an $<\\!\\!\kappa$-branching pointed system and $y$ a pointed
system. Then $x\sim y$ iff, for all $i<\kappa$, we have $x\sim_{i}y$.

  2. (2)

For $i<\kappa$, there are $<\\!\\!\kappa$-branching pointed systems $x$ and
$y$ such that $x\sim_{i}y$ but $x\not\sim_{i+1}y$.

######  Proof 2.2.

  1. (1)

See [BM96][Lemma 11.13] following [vG87], and also [AILS12][Theorem B.1(3)].

  2. (2)

Take $v_{i}$ and $v_{i+1}$.

######  Proposition 4.

Let $x$ be an $<\\!\\!\kappa$-branching pointed system and $y$ a pointed
system. Then $x$ has a successor $z$ such that $z\sim y$ iff, for all
$i<\kappa$, it has a successor $z$ such that $z\sim_{i}y$.

######  Proof 2.3.

($\Rightarrow$) is obvious. For ($\Leftarrow$), by Proposition 1, $x$ has a
successor $z$ such that $z\sim_{j}y$ for all $j<\kappa$, i.e. $z\sim_{k}y$.
Since $z$ is $<\\!\\!\kappa$-branching, Proposition 3 (1) gives $z\sim y$.

##  3\. The Final Chain

###  3.1. Constructing the Final Chain

Our treatment of the final chain relies on the following. Let $I$ be a well-
ordered set. An _inverse $I$-chain_ is a functor $D\colon
I^{{}^{\mathsf{op}}}\to\mathbf{Set}$. Explicitly, it consists of

  * •

for all $i\in I$, a set $D_{i}$, called the $i$-th _level_

  * •

for all $j\leqslant i\in I$, a _connecting map_
$D_{{i}\geqslant{j}}\;:\;D_{j}\to D_{i}$

such that $D_{{i}\geqslant{i}}=\mathsf{id}_{D_{i}}$ for all $i\in I$, and
$\textstyle{D_{i}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{D_{{i}\geqslant{j}}}$$\scriptstyle{D_{{i}\geqslant{k}}}$$\textstyle{D_{j}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{D_{{j}\geqslant{k}}}$$\textstyle{D_{k}}$
commutes for all $k\leqslant j\leqslant i\in I$. An inverse $I$-chain is a
kind of tree [Jec03, BMSS12, BBM14]. It may be represented as a poset $A$ in
which, for every $x\in A$, the set $\\{{y\in A\mid x<y}\\}$ is well-ordered
with order-type less than that of $I$. This intuitive picture gives rise to
the following notions. Let $D$ be an inverse $I$-chain.

  1. (1)

If $I$ has a least element $0$, then an element of $D_{0}$ is a _root_.

  2. (2)

For $j\leqslant i\in I$ and $x\in D_{j}$, an _$i$ -development_ of $x$ is an
element $y\in D_{i}$ such that $D_{{i}\geqslant{j}}y=x$.

  3. (3)

A _full branch_ of $D$ is an indexed tuple $(x_{i})_{i\in I}$ with $x_{i}\in
D_{i}$ for all $i\in I$ and $D_{{i}\geqslant{j}}x_{i}=x_{j}$ for all
$j\leqslant i\in I$. (If $I$ is empty, the empty tuple $()$ is the sole full
branch.)

We now proceed to define the final chain of an endofunctor $F$ on
$\mathbf{Set}$. [Adá74, Bar93] The _final chain_ of $F$ is an inverse
$\mathsf{Ord}$-chain, with $i$th level written $\nu^{(i)}{F}$ and connecting
map written
$\nu^{({i}\geqslant{j})}F\;:\;\nu^{(i)}{F}\longrightarrow\nu^{(j)}{F}$ or
$\nu^{({i}\geqslant{j})}$ for short. These sets and maps are given as follows.

  * •

$\nu^{(i+1)}{F}=F\nu^{(i)}{F}$.

  * •

$\nu^{({i+1}\geqslant{j+1})}=F\nu^{({i}\geqslant{j})}$ for $j\leqslant i$.

  * •

If $i$ is a limit then $\nu^{(i)}{F}$ is the limit of $(\nu^{(j)}{F})_{j<i}$,
i.e. the set of full branches. For $j<i$, the map $\nu^{({i}\geqslant{j})}$ is
$\pi_{j}\;:\;(x_{j})_{j<i}\mapsto x_{j}$.

  * •

Since we deem 0 a limit ordinal, we have $\nu^{(0)}{F}=\\{{()}\\}$.

Thus

$\begin{array}[]{ccccc}\nu^{({i+1}\geqslant{j+1})}\mathcal{P}_{{<\kappa}}&\;:&a&\mapsto&\\{{\nu^{({i}\geqslant{j})}b\mid
b\in a}\\}\end{array}$

We define a full branch $(0_{i})_{i\in\mathsf{Ord}}$ through the final chain
of $\mathcal{P}_{{<\kappa}}$, as follows:

  * •

$0_{i+1}\stackrel{{\scriptstyle\mbox{\rm{\tiny def}}}}{{=}}\emptyset$.

  * •

If $i$ is a limit then $0_{i}\stackrel{{\scriptstyle\mbox{\rm{\tiny
def}}}}{{=}}(0_{j})_{j<i}$.

For $i>0$, note that $0_{i}$ is the unique $i$-development of $0_{1}$.

###  3.2. Coalgebra projections

Again let $F$ be an endofunctor on $\mathbf{Set}$. For an $F$-coalgebra
$(X,\zeta)$ and ordinal $i$, the $i$th _coalgebra projection_ , written
$p^{(X,\zeta)}_{{i}}$ or just $p_{{i}}$, is the map $X\to\nu^{(i)}{F}$ given
as follows222In the language of [CUV09], the pair
$(\nu^{(i)}{F},\nu^{({i+1}\geqslant{i})})$ is a _corecursive $F$-algebra_, and
$p^{(X,\zeta)}_{{i}}$ is the unique map from $(X,\zeta)$ to it. The connecting
maps are $F$-algebra morphisms..

  * •

The map $p_{{i+1}}$ is
$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\zeta}$$\textstyle{FX\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Fp_{{i}}}$$\textstyle{F\nu^{(i)}{F}}$

  * •

For a limit $i$, the map $p_{{i}}$ is $(p_{{j}})_{j<i}$.

We may summarize as follows.

  * •

Each pointed $F$-coalgebra $x$ gives rise to a full branch
$(p_{i}{x})_{i\in\mathsf{Ord}}$ through the final chain of $F$.

  * •

For any $F$-coalgebra morphism $f\colon(X,\zeta)\to(Y,\xi)$ and $x\in X$, the
full branches $(p_{i}{x})_{i\in\mathsf{Ord}}$ and
$(p_{i}{f(x)})_{i\in\mathsf{Ord}}$ are equal.

For a pointed system $x$, we have $p_{i+1}{x}=\\{{p_{i}{y}\mid
x\rightsquigarrow y}\\}$. The coalgebra projections are related to
bisimilarity and its approximants as follows.

######  Proposition 5.

Let $x$ and $y$ be pointed systems.

  1. (1)

For any ordinal $i$, we have $x\sim_{i}y$ iff $p_{i}{x}=p_{i}{y}$.

  2. (2)

We have $x\sim y$ iff the full branches $(p_{i}{x})_{i\in\mathsf{Ord}}$ and
$(p_{i}{y})_{i\in\mathsf{Ord}}$ are equal.

######  Proof 3.1.

Part (1) is by induction on $i$ and part (2) follows.

An element $a\in\nu^{(i)}{\mathcal{P}_{\mathsf{f}}}$ is said to be _$F$
-coalgebraic_ when it is of the form $p_{i}{x}$ for a pointed $F$-coalgebra
$x$. We write $\nu^{(i)}_{\mathrm{coalg}}{F}$ for the set of $F$-coalgebraic
elements of $\nu^{(i)}{F}$. Thus
$\nu^{(i)}_{\mathrm{coalg}}{\mathcal{P}_{{<\kappa}}}$ corresponds to the class
of $<\\!\\!\kappa$-branching pointed systems modulo $\sim_{i}$. Note that
$a\in\nu^{(i+1)}{\mathcal{P}_{{<\kappa}}}$ is
$\mathcal{P}_{{<\kappa}}$-coalgebraic iff all its elements are, by the parent
construction. Let $i$ be a limit. An element of $\nu^{(i)}{F}$ is _$F$
-Cauchy_ when all of its components are $F$-coalgebraic. Thus the set of
$F$-Cauchy elements is $\lim_{j<i}\nu^{(j)}_{\mathrm{coalg}}{F}$. Note that
$F$-coalgebraic implies $F$-Cauchy, but the converse need not be the case.
(For example, for $F\colon X\mapsto 0$, the element $()\in\nu^{(0)}{F}$ is
$F$-Cauchy but not $F$-coalgebraic.) As explained in Section 9.3, the “Cauchy”
terminology comes from the notion of Cauchy sequence.

###  3.3. Channels and Ranges

The following notions are key to understanding the final chain of
$\mathcal{P}_{{<\kappa}}$. Let $I$ be a well-ordered set, and $D$ an inverse
$I$-chain.

  1. (1)

A _channel_ through $D$ consists of a subset $C_{i}\subseteq D_{i}$ for all
$i\in I$, such that for all $j\leqslant i\in I$

     * •

if $x\in C_{i}$ then $D_{{i}\geqslant{j}}x\in C_{j}$

     * •

every $y\in C_{j}$ has an $i$-development in $C_{i}$.

  2. (2)

For any set $U$ of full branches of $D$, the _range_ of $U$ is the channel
whose $i$th level is $\\{{x_{i}\mid x\in U}\\}$.

Note the following:

  * •

Any channel through $D$ with a root has all levels inhabited.

  * •

$\lim_{i\in I}\mathcal{P}_{{<\kappa}}D_{i}$ is the set of channels through $D$
with all levels $<\\!\\!\kappa$-sized.

  * •

The function $(\mathcal{P}_{{<\kappa}}\pi_{i})_{i\in
I}\colon\mathcal{P}_{{<\kappa}}\lim_{i\in I}D_{i}\to\lim_{i\in
I}\mathcal{P}_{{<\kappa}}D_{i}$ sends a $<\\!\\!\kappa$-sized set of full
branches to its range.

For general $F$, we have the following.

######  Proposition 6.

Let $i$ be an ordinal.

  1. (1)

The map $\Psi_{i}\stackrel{{\scriptstyle\mbox{\rm{\tiny
def}}}}{{=}}(\nu^{({i}\geqslant{j})})_{j<i}\colon\nu^{(i)}{F}\cong\lim_{j<i}F\nu^{(j)}{F}$
is an isomorphism (bijection).

  2. (2)

If $i$ is a limit, the following commutes:

|  |  |
---|---|---|---
$\textstyle{\nu^{(i)}{F}}$$\textstyle{=}$$\textstyle{\lim_{j<i}\nu^{(j)}{F}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\Psi_{i}}$$\scriptstyle{\cong}$$\textstyle{F\lim_{j<i}\nu^{(j)}{F}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\nu^{({i+1}\geqslant{i})}}$$\scriptstyle{(F\pi_{j})_{j<i}}$$\textstyle{=}$$\textstyle{\nu^{(i+1)}{F}}$$\textstyle{\lim_{j<i}F\nu^{(j)}{F}}$

Consider the case $F=\mathcal{P}_{{<\kappa}}$. For a limit $i$, the elements
of $\nu^{(i)}{\mathcal{P}_{{<\kappa}}}$ are, by definition, the _full
branches_ of the inverse chain $(\nu^{(j)}{\mathcal{P}_{{<\kappa}}})_{j<i}$.
But they correspond via $\Psi_{i}$ to the _channels_ through the same inverse
chain. We repeatedly move between these two viewpoints—full branches and
channels—in this paper. For example, the map $\nu^{({i+1}\geqslant{i})}$ is
hard to grasp directly, but by Proposition 6(2) it corresponds to
$(\mathcal{P}_{{<\kappa}}\pi_{j})_{j<i}$, which sends a set of full branches
to its range.

###  3.4. Injectivity of Connecting Maps

A key question in the study of final chains (as with initial chains) is
stabilization [TAKR75, AK95, AT11, Wor05, ALM+15, AP15].

######  Proposition 7.

Suppose the final chain of $F$ is _stable_ at $i$, i.e.
$\nu^{({i+1}\geqslant{i})}$ is bijective.

  * •

$\nu^{({k}\geqslant{j})}$ is bijective for all $k\geqslant j\geqslant i$.

  * •

The $F$-coalgebra $(\nu^{(i)}{F},(\nu^{({i+1}\geqslant{i})})^{-1})$ is final,
with the unique coalgebra map from any coalgebra $M$ given by $p^{M}_{i}$.

  * •

The $j$th projection from this final coalgebra is given by
$\nu^{({i}\geqslant{j})}$ for $j\leqslant i$, and by
$(\nu^{({j}\geqslant{i})})^{-1}$ for $j\geqslant i$.

By Proposition 6(2), for any limit $i$, if $F$ preserves limits of inverse
$i$-chains then its final chain is stable at $i$. This fact is useful for a
_polynomial_ functor $F$, i.e. one of the form $X\mapsto\sum_{i\in
I}X^{A_{i}}$. Since it preserves limits of connected diagrams, its final chain
is stable at $\omega$ [Bar93]. However, $\mathcal{P}_{{<\kappa}}$ requires a
more subtle analysis, given in [Wor05], that we now reprise.

######  Proposition 8.

Let $F$ be an endofunctor on $\mathbf{Set}$ that preserves injections and
intersections (such as $\mathcal{P}_{{<\kappa}}$ or
$\mathcal{P}^{+}_{<\kappa}$). Suppose $\nu^{({i+1}\geqslant{i})}F$ is an
injection. Then $\nu^{({k}\geqslant{j})}F$ is an injection for all $k\geqslant
j\geqslant i$, and the final chain is stable at $i+\omega$.

A functor $F$ is said to preserve the limit of an inverse $I$-chain $D$ up to
an injection (surjection) when the map

$(F\pi_{i})_{i\in I}\colon F\lim_{i\in I}D_{i}\to\lim_{i\in I}FD_{i}$

is injective (surjective).

######  Proposition 9.

[Wor05] Let $\kappa<\infty\infty$. Then $\mathcal{P}_{{<\kappa}}$ and
$\mathcal{P}^{+}_{<\kappa}$ preserve, up to an injection, the limits of any
inverse $\kappa$-chain $D$. Explicitly: if $U$ and $V$ are
$<\\!\\!\kappa$-sized sets of full branches through $D$ and have the same
range, then $U=V$.

######  Proof 3.2.

Let $a\in U$. For $i<\kappa$, let $V(i)$ be the set of $b\in V$ such that
$b_{i}=a_{i}$. Since $V$ is $<\\!\\!\kappa$-sized, $\bigcap_{i<\kappa}V(i)$ is
inhabited by Proposition 1, so $a\in V$.

Thus $\nu^{({\kappa+1}\geqslant{\kappa})}(\mathcal{P}_{{<\kappa}})$ is
injective and the final chain of $\mathcal{P}_{{<\kappa}}$ is stable at
$\kappa+\omega$. As proved in [ALM+15] and reprised below (Proposition 24), it
is not stable at any smaller ordinal.

We can now say precisely which connecting maps are injective.

######  Proposition 10.

For ordinals $j\leqslant i$, the following are equivalent.

  1. (1)

The connecting map $\nu^{({i}\geqslant{j})}\mathcal{P}_{{<\kappa}}$ is an
injection.

  2. (2)

Either $j=i$ or $j\geqslant\kappa$ (for $\kappa<\infty\infty$).

######  Proof 3.3.

(2)$\Rightarrow$(1) follows from Propositions 9 and 8. For the converse, if
$j<\kappa$, then Proposition 3(2) shows that
$\nu^{({j+1}\geqslant{j})}\mathcal{P}_{{<\kappa}}$ is not injective.

###  3.5. Surjectivity of connecting maps

######  Proposition 11.

For any ordinal $i$, the following are equivalent.

  1. (1)

The map $\nu^{({i+1}\geqslant{i})}F$ is surjective.

  2. (2)

For all $h\geqslant i$, the map $\nu^{({h}\geqslant{i})}F$ is surjective.

  3. (3)

All elements of $\nu^{(i)}{F}$ are $F$-coalgebraic.

######  Proof 3.4.

(3) $\Rightarrow$ (2) $\Rightarrow$ (1):

Trivial.

(1) $\Rightarrow$ (3):

By the Axiom of Choice, $\nu^{({i+1}\geqslant{i})}$ has a section
$\zeta\;:\;\nu^{(i)}{F}\to\nu^{(i+1)}{F}$. Put $M=(\nu^{(i)}{F},\zeta)$. For
all $j\leqslant i$, we show $p^{M}_{{j}}=\nu^{({i}\geqslant{j})}$ by induction
on $j$. The limit case is trivial. For the successor case,
$p^{M}_{{j}}=\nu^{({i}\geqslant{j})}$ implies
$Fp^{M}_{{j}}=F\nu^{({i}\geqslant{j})}=\nu^{({i+1}\geqslant{j+1})}$ and hence

$\textstyle{\nu^{(i)}{F}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p^{M}_{{j+1}}}$$\scriptstyle{\zeta}$$\scriptstyle{\mathsf{id}}$$\textstyle{\nu^{(i+1)}{F}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Fp^{M}_{{j}}}$$\scriptstyle{\nu^{({i+1}\geqslant{i})}}$$\textstyle{\nu^{(j+1)}{F}}$$\textstyle{\nu^{(i)}{F}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\nu^{({i}\geqslant{j+1})}}$

commutes. We conclude that $p^{M}_{{i}}$ is the identity.

######  Proposition 12.

Let $\kappa>\aleph_{0}$. Then $\mathcal{P}_{{<\kappa}}$ and
$\mathcal{P}^{+}_{<\kappa}$ preserve, up to a surjection, the limit of any
inverse $\omega$-chain $D$. Explicitly: any channel $C$ through $D$ with all
levels $<\\!\\!\kappa$-sized is the range of some $<\\!\\!\kappa$-sized set of
full branches.

######  Proof 3.5.

For $n\in\mathbb{N}$, each $x\in C_{n}$ extends by dependent choice to a full
branch through $D$. For each $n\in\mathbb{N}$ and $x\in C_{n}$, choose such a
branch $\theta_{n}(x)$, by the Axiom of Choice. Then the set
$\\{{\theta_{n}(x)\mid n\in\mathbb{N},x\in C_{n}}\\}$ is $<\\!\\!\kappa$-sized
because $<\\!\\!\kappa$ is uncountable and regular, and has range $C$.

######  Corollary 13.

Let $\kappa>\aleph_{0}$.

  1. (1)

For $i<\omega_{1}$ and $h\geqslant i$, the connecting map
$\nu^{({h}\geqslant{i})}\mathcal{P}_{{<\kappa}}$ is surjective.

  2. (2)

For $i<\omega_{1}$, every element of $\nu^{(i)}{\mathcal{P}_{{<\kappa}}}$ is
$\mathcal{P}_{{<\kappa}}$-coalgebraic.

  3. (3)

Every element of $\nu^{(\omega_{1})}{\mathcal{P}_{{<\kappa}}}$ is
$\mathcal{P}_{{<\kappa}}$-Cauchy.

######  Proof 3.6.

We just need to prove
$\nu^{({i+1}\geqslant{i})}\colon\nu^{(i)}{\mathcal{P}_{{<\kappa}}}\to\nu^{(i+1)}{\mathcal{P}_{{<\kappa}}}$
surjective, for $i<\omega_{1}$. The case $i=0$ is evident. If $i$ is a
positive limit, take a strictly increasing sequence $(i_{n})_{n\in\mathbb{N}}$
with supremum $i$, then apply Proposition 12. The successor case follows from
the fact that $\mathcal{P}_{{<\kappa}}$ preserves surjections.

##  4\. The Final Chain as a Transition System

###  4.1. Full powerset

We shall now explain how the final chain of $\mathcal{P}$ constitutes a
transition system. The _predecessor_ of an ordinal is defined as follows:

  * •

$\mathsf{pred}({i+1})\stackrel{{\scriptstyle\mbox{\rm{\tiny def}}}}{{=}}i$.

  * •

If $i$ is a limit, $\mathsf{pred}({i})\stackrel{{\scriptstyle\mbox{\rm{\tiny
def}}}}{{=}}i$.

  * •

Since we deem $0$ a limit, $\mathsf{pred}({0})=0$.

In general, $\mathsf{pred}({i})$ is the supremum of all ordinals less than
$i$. Note, by the way, that $\mathsf{pred}$ is the left adjoint of the
successor function. We come to the main definition: The transition relation
$\rightsquigarrow_{i}$ from $\nu^{(i)}{\mathcal{P}}$ to
$\nu^{(\mathsf{pred}({i}))}{\mathcal{P}}$ is defined as follows.

  * •

For $a\in\nu^{(i+1)}{\mathcal{P}}$ and $b\in\nu^{(i)}{\mathcal{P}}$, we set
$a\rightsquigarrow_{i+1}b$ when $b\in a$.

  * •

If $i$ is a limit, then for $a,b\in\nu^{(i)}{\mathcal{P}}$, we set
$a\rightsquigarrow_{i}b$ when $b_{j}\in a_{j+1}$ for all $j<i$.

  * •

Since we deem $0$ a limit, $()\rightsquigarrow_{0}()$.

In general, $a\rightsquigarrow_{i}b$ when for all $j<i$ we have
$\nu^{({\mathsf{pred}({i})}\geqslant{j})}b\in\nu^{({i}\geqslant{j+1})}a$. Note
that connecting maps and coalgebra projections preserve transition:

######  Proposition 14.

  1. (1)

For $j\leqslant i$ and $a\in\nu^{(i)}{\mathcal{P}}$, if
$a\rightsquigarrow_{i}b$ then
$\nu^{({i}\geqslant{j})}a\rightsquigarrow_{j}\nu^{({\mathsf{pred}({i})}\geqslant{\mathsf{pred}({j})})}b$.

  2. (2)

For a pointed system $x$ and ordinal $i$, if $x\rightsquigarrow y$ then
$p_{i}{x}\rightsquigarrow_{i}p_{\mathsf{pred}({i})}{x}$.

Let us translate Definition 4.1 into the language of Section 3.3. For general
$F$, the map

$\Phi_{i}\stackrel{{\scriptstyle\mbox{\rm{\tiny
def}}}}{{=}}(\nu^{({\mathsf{pred}({i})}\geqslant{j})})_{j<i}\colon\nu^{(\mathsf{pred}({i}))}{F}\to\lim_{j<i}\nu^{(j)}{F}$

is an isomorphism (bijection)—indeed the identity if $i$ is a limit. For
$a\in\nu^{(i)}{\mathcal{P}}$ and $b\in\nu^{(\mathsf{pred}({i}))}{\mathcal{P}}$
we note that $\Psi_{i}(a)$ is a channel, and $\Phi_{i}(b)$ a full branch,
through $(\nu^{(j)}{\mathcal{P}})_{j<i}$. We have $a\rightsquigarrow_{i}b$
when $\Phi_{i}(b)$ is a full branch through $\Psi_{i}(a)$.

###  4.2. Restricted powerset

The final chain of $\mathcal{P}_{{<\kappa}}$ forms a subsystem of the final
chain of $\mathcal{P}$, in the following sense.

######  Proposition 15.

Let $a\in\nu^{(i)}{\mathcal{P}_{{<\kappa}}}$ and $a\rightsquigarrow_{i}b$ then
$b\in\nu^{(\mathsf{pred}({i}))}{\mathcal{P}_{{<\kappa}}}$.

######  Proof 4.1.

Since $\Psi_{i}(a)$ is a channel through
$(\nu^{(j)}{\mathcal{P}_{{<\kappa}}})_{j<i}$ (with all levels
$<\\!\\!\kappa$-sized), every full branch through it is a full branch through
$(\nu^{(j)}{\mathcal{P}_{{<\kappa}}})_{j<i}$.

As we shall see, the subsystem
$(\nu^{(i)}{\mathcal{P}_{{<\kappa}}})_{i\in\mathsf{Ord}}$ is not
$<\\!\\!\kappa$-branching (Proposition 23 below). Furthermore, the
$\mathcal{P}_{{<\kappa}}$-coalgebraic elements need not form a subsystem
(Proposition 58 below). However, the $\mathcal{P}_{{<\kappa}}$-Cauchy elements
do form a subsystem.

Suppose now that $\kappa<\infty\infty$. Beyond $\kappa$, we recall that
connecting maps are injections (Proposition 10). They are moreover transition
system embeddings in the following sense.

######  Proposition 16.

For $i\geqslant j\geqslant\kappa$ and
$a\in\nu^{(i)}{\mathcal{P}_{{<\kappa}}}$, the map
$\nu^{({\mathsf{pred}({i})}\geqslant{\mathsf{pred}({j})})}$ is a bijection
from the $\rightsquigarrow_{i}$-successors of $a$ to the
$\rightsquigarrow_{j}$-successors of $\nu^{({i}\geqslant{j})}a$.

######  Proof 4.2.

This says that, if $C$ is a channel through
$(\nu^{(k)}{\mathcal{P}_{{<\kappa}}})_{k<i}$ with all levels
$<\\!\\!\kappa$-sized, then each full branch $b$ of $C\restriction_{j}$
extends uniquely to a full branch $a$ of $C$. For $k<i$ we define $a_{k}$ as
follows.

  * •

If $k\geqslant\kappa$, then for each $l<\kappa$ the set $R_{l}$ of $a\in
C_{k}$ such that $a_{l}=b_{l}$ is inhabited, so $\bigcap_{l\in\kappa}R_{l}$
has an element by Proposition 1, unique since $\nu^{({k}\geqslant{\kappa})}$
is injective. Let $a_{k}$ be this element.

  * •

If $k<\kappa$, set $a_{k}\stackrel{{\scriptstyle\mbox{\rm{\tiny
def}}}}{{=}}b_{k}$.

Hence, beyond $\kappa+\omega$, the transition system agrees with the final
coalgebra structure given by Proposition 7:

######  Corollary 17.

For $i\geqslant\kappa+\omega$ and $a\in\nu^{(i)}{\mathcal{P}_{{<\kappa}}}$,
the map $\nu^{({i}\geqslant{\mathsf{pred}({i})})}$ is a bijection from the
elements of $(\nu^{({i+1}\geqslant{i})})^{-1}a$ to the
$\rightsquigarrow_{i}$-successors of $a$.

###  4.3. Examples

The following result is adapted from [FH89].

######  Proposition 18.

Let $x$ and $y$ be pointed systems and $i\in\mathsf{Ord}$. We have
$p_{i}{x}\rightsquigarrow_{i}p_{\mathsf{pred}({i})}{y}$ iff, for every $j<i$,
the pointed system $x$ has a successor $z$ such that $z\sim_{j}y$. (Cf.
Proposition 4.)

######  Proof 4.3.

Because $p_{i}{x}\rightsquigarrow_{i}p_{\mathsf{pred}({i})}{y}$ iff for every
$j<i$ we have $p_{j}{y}\in p_{j+1}{y}$, and the latter is $\\{{p_{j}{z}\mid
x\rightsquigarrow z}\\}$.

In several cases we shall precisely describe the
$\rightsquigarrow_{i}$-successors of an element.

######  Proposition 19.

For any $i>0$, the element $0_{i}$ has no successors.

######  Proof 4.4.

If $0_{i}\rightsquigarrow_{i}b$ then $b_{0}\in 0_{1}=\emptyset$.

######  Proposition 20.

Let $\kappa<\infty\infty$ and let $x$ be an $<\\!\\!\kappa$-branching pointed
system. For $i\geqslant\kappa$, the set of successors of $p_{i}{x}$ is
$\\{{p_{\mathsf{pred}({i})}{y}\mid x\rightsquigarrow y}\\}$.

######  Proof 4.5.

Let $j$ be the maximum of $i$ and $\kappa+\omega$. If
$p_{i}{x}\rightsquigarrow b$, then, by Proposition 16, $p_{j+1}{x}$ has a
unique element $c$ such that $\nu^{({j}\geqslant{\mathsf{pred}({i})})}c=b$. By
the final coalgebra property, $x$ has a successor $y$ such that $p_{j}{y}=c$
and hence $p_{\mathsf{pred}({i})}{y}=b$.

######  Proposition 21.

Let $x$ be a pointed system with a unique successor $y$. For any ordinal $i$,
the element $p_{i}{x}$ has unique successor $p_{\mathsf{pred}({i})}{y}$.

######  Proof 4.6.

If $p_{i}{x}\rightsquigarrow b$ then for all $j<i$ we have $b_{j}\in
p_{j+1}{x}=\\{{p_{j}{y}}\\}$ so $b_{j}=p_{j}{y}$. Thus
$b=p_{\mathsf{pred}({i})}{y}$.

We next consider the von Neumann ordinals.

######  Proposition 22.

For ordinals $j\leqslant i$, the successors of $p_{i}{v_{j}}$ are listed
without repetition

  * •

as $(p_{\mathsf{pred}({i})}{v_{k}})_{k<j}$, if $j<i$

  * •

as $(p_{\mathsf{pred}({i})}{v_{k}})_{k\leqslant\mathsf{pred}({i})}$, if $j=i$.

######  Proof 4.7.

Proposition 18 tells us that these are indeed successors. Uniqueness is by
Proposition 2.

Let $j\leqslant i$ and $p_{i}{v_{j}}\rightsquigarrow x$. For every $k<i$, we
have $x_{k}\in p_{k+1}{v_{j}}$, which is $\\{{p_{k}{y}\mid
v_{j}\rightsquigarrow y}\\}$. Thus $x_{k}$ is expressible as $p_{k}{y}$ for
some successor $y$ of $v_{j}$, i.e $y=v_{l}$ for some $l<j$. There is a unique
such $l$ that is $\leqslant k$; we call it $g(k)$.

Let $C$ be the set of $k<i$ such that $g(k)=k$ and $D$ its complement, i.e.
the set of $k<i$ such that $g(k)<k$.

For any $k\leqslant l<i$ we have $p_{k}{v_{g(k)}}=p_{k}{v_{g(l)}}$ i.e.
$t_{g(k)}\sim_{k}t_{g(l)}$. This can be unpacked as follows.

  1. (1)

If $k\in C$ then $g(l)\geqslant k$.

  2. (2)

if $k\in D$ then $g(l)=g(k)$.

(2) implies that $g(l)=g(k)<k\leqslant l$, so $l\in D$. Thus $D$ is upper and
$C$ is lower.

Let $k$ be the supremum of $C$. Since $\mathsf{pred}({i})$ is an upper bound
for $C$ we have $k\leqslant\mathsf{pred}({i})$.

We show that $x=p_{\mathsf{pred}({i})}{v_{k}}$, i.e. that for any $l<i$ we
have $g(l)=l\sqcap k$. If $l<k$ this holds because $l\in C$. If $l\geqslant
k$, we must show $g(l)=k$. Firstly, (1) says that $g(l)$ is an upper bound for
$C$, hence $g(l)\geqslant k$. If $l=k$ we are done. If $l>k$ then
$k+1\leqslant l<i$, and $k\leqslant g(k+1)\leqslant k+1$. Since $k+1\not\in
C$, we have $g(k+1)=k$ and hence by (2), $g(l)=k$.

Since $j$ is an upper bound for $C$, we have $k\leqslant j$. If $j<i$, then
$j\in D$ but $k\in C$ so $k<j$.

######  Proposition 23.

For $\kappa<\infty\infty$, the set $\nu^{(\kappa)}{\mathcal{P}_{{<\kappa}}}$
has a $\mathcal{P}_{{<\kappa}}$-Cauchy element with precisely $\kappa$
successors.

######  Proof 4.8.

Put $e\stackrel{{\scriptstyle\mbox{\rm{\tiny
def}}}}{{=}}p_{\kappa}{v_{\kappa}}$. For $i<\kappa$, the component $e_{i}$ is
$p_{i}{v_{\kappa}}=p_{i}{v_{i}}$, hence $\mathcal{P}_{{<\kappa}}$-coalgebraic.
By Proposition 22, the successors of $e$ are listed without repetition as
$(p_{\kappa}{v_{i}})_{i\leqslant\kappa}$, so $e$ has $\kappa$-many successors.

Thus we may characterize which connecting maps are bijective.

######  Proposition 24.

[ALM+15] For ordinals $j\leqslant i$, the following are equivalent:

  1. (1)

The connecting map $\nu^{({i}\geqslant{j})}\mathcal{P}_{{<\kappa}}$ is
bijective.

  2. (2)

Either $j=i$ or $j\geqslant\kappa+\omega$ (for $\kappa<\infty\infty$).

######  Proof 4.9.

For (2)$\Rightarrow$(1), we saw in Section 3.4 that the final chain is stable
at $\kappa+\omega$. For the converse, assuming $j<i$, Proposition 10 covers
the case where $j<\kappa$. For $j=\kappa+n$, where $n\in\mathbb{N}$, take
$a\in\nu^{(\kappa)}{\mathcal{P}_{{<\kappa}}}$ with $\kappa$ successors. Then
$\\{{-}\\}^{n}a$ is not in the range of
$\nu^{({\kappa+n+1}\geqslant{\kappa+n})}$, because for every
$b\in\nu^{(\kappa+n+1)}{\mathcal{P}_{{<\kappa}}}$, each $n$-step descendant of
$b$ has $<\\!\\!\kappa$-successors.

##  5\. Before $\omega_{1}$

This section reprises from [ALM+15] several properties that the final chain
enjoys at countable ordinals. (We have already seen one such
property—surjectivity of connecting maps.) We first mention some properties
enjoyed at _finite_ ordinals:

######  Proposition 25.

Let $n\in\mathbb{N}$.

  1. (1)

For $a,b\in\nu^{(n)}{\mathcal{P}}$, if $a\sim_{n}b$ then $a=b$.

  2. (2)

For any pointed system $x$, we can characterize $p_{n}{x}$ as the unique
$b\in\nu^{(n)}{\mathcal{P}}$ such that $b\sim_{n}x$.

  3. (3)

For any ordinal $i$ and $a\in\nu^{(i+n)}{\mathcal{P}}$, we have
$p_{n}{a}=\nu^{({i+n}\geqslant{n})}a$, and it can be characterized as the
unique $b\in\nu^{(n)}{\mathcal{P}}$ such that $b\sim_{n}a$.

######  Proof 5.1.

By induction on $n$.

The properties enjoyed at countable ordinals derive from the following fact.

######  Proposition 26.

For $j<i<\omega_{1}$ and all $a\in\nu^{(i)}{\mathcal{P}}$ we have

$\displaystyle\nu^{({i}\geqslant{j+1})}a$ $\displaystyle=$
$\displaystyle\\{{\nu^{({i}\geqslant{j})}b\mid a\rightsquigarrow_{i}b}\\}$

.

######  Proof 5.2.

Trivial if $i$ is a successor or $0$. If $i$ is a positive limit, take a
strictly increasing sequence $(i_{n})_{n\in\mathbb{N}}$ with supremum $i$. Any
$b\in\nu^{({i}\geqslant{j+1})}a$, is an element of the $j$th level of the
channel $\Psi_{i}(a)$ through $(\nu^{(k)}{\mathcal{P}_{{<\kappa}}})_{k<i}$,
and it extends by dependent choice to a full branch.

######  Lemma 27.

Let $j\leqslant i<\omega_{1}$. For $a\in\nu^{(i)}{\mathcal{P}}$ we have
$p_{j}{a}=\nu^{({i}\geqslant{j})}a$.

######  Proof 5.3.

By induction on $j$, using Proposition 26 for the successor case.

######  Proposition 28.

Let $i<\omega_{1}$.

  1. (1)

For $a\in\nu^{(i)}{\mathcal{P}}$ we have $p_{i}{a}=a$.

  2. (2)

Every element of $\nu^{(i)}{\mathcal{P}}$ is $\mathcal{P}$-coalgebraic.

  3. (3)

For $a,b\in\nu^{(i)}{\mathcal{P}}$, if $a\sim_{i}b$ then $a=b$.

  4. (4)

For $a,b\in\nu^{(i)}{\mathcal{P}}$, if $a\sim b$ then $a=b$.

######  Proof 5.4.

  1. (1)

By Lemma 27.

  2. (2)

Follows from part (1).

  3. (3)

$a=p_{i}{a}=p_{i}{b}=b$.

  4. (4)

Follows from part (3).

######  Corollary 29.

  1. (1)

Let $i<\omega_{1}$. For any pointed system $x$, we may characterize $p_{i}{x}$
as the unique $b\in\nu^{(i)}{\mathcal{P}}$ such that $b\sim_{i}x$.

  2. (2)

Let $j\leqslant i<\omega_{1}$. For any $a\in\nu^{(i)}{\mathcal{P}}$ we may
characterize $\nu^{({i}\geqslant{j})}a$ as the unique
$b\in\nu^{(j)}{\mathcal{P}}$ such that $b\sim_{j}a$.

######  Proof 5.5.

  1. (1)

$p_{i}{p_{i}{x}}=p_{i}{x}$, by Proposition 28(1), so $p_{i}{x}\sim_{i}x$.
Uniqueness is by Proposition 28(3).

  2. (2)

$p_{j}{\nu^{({i}\geqslant{j})}a}=\nu^{({i}\geqslant{j})}a=\nu^{({i}\geqslant{j})}p_{i}{a}=p_{j}{a}$,
so $\nu^{({i}\geqslant{j})}{a}\sim_{j}a$. Uniqueness is by Proposition 28(3).

A pointed system $a$ is _$ <\\!\\!\kappa$-branching at depth $<i$_ when every
$b$ such that $a\rightsquigarrow^{m}b$, for a natural number $m<i$, has
$<\\!\\!\kappa$ successors. If $i\geqslant\omega$, this just says that $a$ is
$<\\!\\!\kappa$-branching.

######  Proposition 30.

Assume $\kappa<\infty\infty$.

  1. (1)

Let $j$ be an ordinal. Every element of
$\nu^{(\kappa+j)}{\mathcal{P}_{{<\kappa}}}$ that is
$\mathcal{P}_{{<\kappa}}$-coalgebraic is $<\\!\\!\kappa$-branching, and
conversely if $\kappa=\aleph_{0}$.

  2. (2)

Let $j\leqslant i$ be ordinals. Every element of
$\nu^{(\kappa+j)}{\mathcal{P}_{{<\kappa}}}$ that is in the range of
$\nu^{({\kappa+i}\geqslant{\kappa+j})}$ is $<\\!\\!\kappa$-branching at depth
$<i$, and conversely if $\kappa=\aleph_{0}$.

######  Proof 5.6.

  1. (1)

($\Rightarrow$) follows from Proposition 20. For ($\Leftarrow$), if
$a\in\nu^{(\omega+j)}{\mathcal{P}_{\mathsf{f}}}$ is finitely branching, then
it is $\mathcal{P}_{\mathsf{f}}$-coalgebraic since $p_{\omega+j}{a}=a$.

  2. (2)

($\Rightarrow$) follows from Proposition 16, since every element of
$\nu^{(\kappa+i)}{\mathcal{P}_{{<\kappa}}}$ is $<\\!\\!\kappa$-branching at
depth $<i$. For ($\Leftarrow$), let
$a\in\nu^{(\kappa+j)}{\mathcal{P}_{{<\kappa}}}$ be $<\\!\\!\kappa$-branching
at depth $<i$. Since $b\stackrel{{\scriptstyle\mbox{\rm{\tiny
def}}}}{{=}}p_{\omega+i}{a}$ is sent by
$\nu^{({\omega+i}\geqslant{\omega+j})}$ to $a$, it suffices to show that
$b\in\nu^{(\omega+i)}{\mathcal{P}_{\mathsf{f}}}$. If $i\geqslant\omega$ this
holds because $a$ is finitely branching; we prove the case $i<\omega$ by
induction on $i$. For $i=0$ we have $j=i$ and
$b=a\in\nu^{(\kappa)}{\mathcal{P}_{\mathsf{f}}}$. For $i=i^{\prime}+1$ we have
$b=\\{{p_{\omega+i^{\prime}}{c}\mid a\rightsquigarrow c}\\}$, which is in
$\nu^{(\omega+i)}{\mathcal{P}_{\mathsf{f}}}$ because $a$ has finitely many
successors and each of them is finitely branching at depth $<i^{\prime}$.

##  6\. A Ghost at $\omega_{1}$

The previous section has established properties of
$\nu^{(i)}{\mathcal{P}_{{<\kappa}}}$ for $i<\omega_{1}$. But for
$i=\omega_{1}$, many questions remain unresolved.

  * •

For $i<\omega_{1}$, every element of $\nu^{(i)}{\mathcal{P}_{{<\kappa}}}$ is
$\mathcal{P}_{{<\kappa}}$-coalgebraic (for $\kappa>\aleph_{0}$). Is every
element of $\nu^{(\omega_{1})}{\mathcal{P}_{\mathsf{c}}}$ at least
$\mathcal{P}$-coalgebraic?

  * •

For $i<\omega_{1}$, the set $\nu^{(i)}{\mathcal{P}}$ is strongly extensional,
i.e. bisimilar elements are equal. What about
$\nu^{(\omega_{1})}{\mathcal{P}_{\mathsf{c}}}$?

  * •

For $j<i<\omega_{1}$ we saw (Proposition 26) that
$\nu^{({i}\geqslant{j+1})}\mathcal{P}$ sends $a$ to
$\\{{\nu^{({\mathsf{pred}({i})}\geqslant{j})}b\mid a\rightsquigarrow b}\\}$.
Is this true for $\nu^{({\omega_{1}}\geqslant{j+1})}\mathcal{P}_{\mathsf{c}}$,
where $j<\omega_{1}$?

  * •

The finitely branching elements of $\nu^{(\omega)}{\mathcal{P}_{\mathsf{f}}}$
are the $\mathcal{P}_{\mathsf{f}}$-coalgebraic ones. Are the countably
branching elements of $\nu^{(\omega_{1})}{\mathcal{P}_{\mathsf{c}}}$ all
$\mathcal{P}_{\mathsf{c}}$-coalgebraic?

The following result will provide a negative answer to all the above
questions.

######  Proposition 31.

The set $\nu^{(\omega_{1})}{\mathcal{P}_{\mathsf{c}}}$ has an element $a$,
distinct from $0(\omega_{1})$, that has no successor.

Such an element $a$ is called a _ghost_ because it “appears to be alive” (for
all $j<\omega_{1}$, the component $a_{j+1}$ is inhabited) yet is “dead” (has
no successors). The negative answers are deduced as follows.

  * •

For a pointed system $x$, if $a=p_{\omega_{1}}{x}$, then $()\in
a_{1}=p_{1}{x}=\\{{p_{0}{y}\mid x\rightsquigarrow y}\\}$. So $x$ has a
successor $y$, so $a=p_{\omega_{1}}{x}\rightsquigarrow p_{\omega_{1}}{y}$,
contradiction.

  * •

$a$ and $0_{\omega_{1}}$ are bisimilar (having no successors) yet distinct. So
$\nu^{(\omega_{1})}{\mathcal{P}_{\mathsf{c}}}$ is not strongly extensional.

  * •

For $j<\omega_{1}$, the set $\nu^{({i}\geqslant{j+1})}a=a_{j+1}$ has an
element $b$, but $b$ is not of the form $\nu^{({i}\geqslant{j})}c$ for a
successor $c$ of $a$.

  * •

The element $a$ is countably branching but not
$\mathcal{P}_{\mathsf{c}}$-coalgebraic.

A ghost corresponds via $\Psi_{\omega_{1}}$ to a channel through
$(\nu^{(i)}{\mathcal{P}_{\mathsf{c}}})_{i<\omega_{1}}$, with all levels
countable, that has a root but no full branch. The rest of the section is
devoted to proving that such a channel exists. Our proof involves three steps:

  1. (1)

obtaining an “Aronszajn tree”

  2. (2)

embedding it into the complete binary tree

  3. (3)

embedding the complete binary tree into the final chain.

We begin with the following notions. Let $I$ be a well-ordered set with least
element. A _tidy $I$-tree_333The set-theoretic literature commonly uses a more
general notion of tree. See Section 9.1 for a comparison. is an inverse
$I$-chain $D$ with the following properties.

  * •

For any $j\leqslant i\in I$, the connecting map $D_{{i}\geqslant{j}}$ is
surjective, i.e. every $a\in D_{j}$ has an $i$-development.

  * •

For any limit $i\in I$, every full branch through $(D_{j})_{j<i}$ has at most
one extension to a full branch through $(D_{j})_{j\leqslant i}$.

  * •

$D$ has a (necessarily unique) root.

Note that a tidy $I$-tree is a channel through itself.

It is important to know whether a tidy tree is guaranteed to have a full
branch. The following two results [HS54, Kur36] show that this is not always
the case. Our presentation follows [Ber].

######  Proposition 32.

For regular $\lambda>\aleph_{0}$, there is a tidy $\lambda$-tree that has all
levels $\leqslant\\!\\!\lambda$-sized and has no full branch.

######  Proof 6.1.

For each $i<\lambda$, let $D_{i}$ be the set of strictly increasing sequences
$0=x_{0}<\cdots<x_{n}<\lambda$ of ordinals, where $x_{n}\geqslant i$ but
$x_{m}<i$ for all $m<n$. Clearly $D_{i}$ is $\leqslant\\!\\!\lambda$-sized.
For $j\leqslant i<\lambda$, let $D_{{i}\geqslant{j}}:D_{i}\to D_{j}$ send
$x\in D_{i}$ to its unique prefix in $D_{j}$. Then $(D_{i})_{i<\lambda}$ is a
tidy $\lambda$-tree, and any full branch would give a cofinal
$\omega$-sequence in $\lambda$, contradicting regularity.

######  Theorem 33.

There is a tidy $\omega_{1}$-tree that has all levels countable and no full
branch. (Such a tree is said to be _Aronszajn_.)

######  Proof 6.2.

For $i<\omega_{1}$, let $E_{i}$ be the set of strictly increasing
$i$-sequences $x=(x_{j})_{j<i}$ of nonnegative rationals. The supremum of
$x\in E_{i}$—taken to be $0$ if $x$ is empty—is a nonnegative real or
$\infty$, and written $\mathrm{sup}({x})$.

We shall define a countable subset $D_{i}\subseteq E_{i}$ for all
$i<\omega_{1}$, with the following properties.

  1. (1)

If $x\in D_{i}$ then its supremum is (finite and) rational.

  2. (2)

If $j\leqslant i<\omega_{1}$ and $x\in D_{i}$ then the $j$-sequence prefix of
$x$ is in $D_{j}$.

  3. (3)

If $j<i<\omega_{1}$, then for any $x\in D_{j}$ and rational
$r>\mathrm{sup}({x})$, $x$ has an extension in $D_{i}$ with supremum $r$.

Suppose that we have $D_{j}$ for all $j<i$, with these properties. We define
$D_{i}$ as follows; properties (1)–(3) are easily verified in each case.

  * •

For $i=0$, let $D_{i}$ consist of the empty sequence.

  * •

Suppose $i=j+1$. Let $D_{i}$ consist of all the extended sequences $xr$ for
$x\in D_{j}$ and rational $r>\mathrm{sup}({x})$.

  * •

Suppose $i>0$ is a limit. By the Axiom of Choice, choose, for each $j<i$ and
$x\in D_{j}$ and rational $r>\mathrm{sup}({x})$, a strictly increasing
sequence of ordinals $(k_{n})_{n\in\mathbb{N}}$, where $k_{0}=j$, with
supremum $i$; and a strictly increasing sequence of rationals
$(s_{n})_{n\in\mathbb{N}}$, where $s_{0}=\mathrm{sup}({x})$, with supremum
$r$. (For example, take $s_{n}=2^{-n}\mathrm{sup}({x})+(1-2^{-n})r$.) We
define $P_{n}(j,x,r)\in D_{k_{n}}$ with supremum $s_{n}$ by induction on
$n\in\mathbb{N}$.

    * –

Let $x_{0}$ be $x$.

    * –

Let $x_{n+1}$ be an extension of $x_{n}$ in $D_{k_{n}}$ with supremum
$s_{n+1}$.

Then the $i$-sequence $\bigsqcup_{n\in\mathbb{N}}P_{n}(j,x,r)$ has supremum
$r$ and extends $x$. Let $D_{i}$ be the set of all these.

We take the inverse chain $(D_{i})_{i<\omega_{1}}$, with connecting map
$D_{{i}\geqslant{j}}$ sending $x\in D_{i}$ to its $j$-sequence prefix. The
limit property is clear. The connecting map $D_{{i}\geqslant{j}}$ is
surjective because, in the nontrivial case $j<i$, every $x\in D_{j}$ has an
extension in $D_{i}$ with supremum $\mathrm{sup}({x})+1$. The levels are
countable by construction. Finally, any full branch of
$(D_{i})_{i<\omega_{1}}$ would give a strictly increasing
$\omega_{1}$-sequence of nonnegative rationals, which does not exist.

This completes our first step. Before describing the second, we must give a
suitable notion of embedding. A _cofinal embedding_ of inverse chains
$\alpha\colon(D_{i})_{i\in I}\to(E_{j})_{j\in J}$ consists of the following.

  * •

A monotone map $f\;:\;I\to J$ (the _index map_) that is cofinal, i.e. for any
$j\in J$ there is $i\in I$ such that $fi\geqslant j$.

  * •

For each $i\in I$, an injection $\alpha_{i}\;:\;D_{i}\to E_{fi}$ (the _$i$ -th
level map_) that is natural in $i$, i.e. for $j\leqslant i$ in $I$, if $y\in
D_{i}$ is an $i$-development of $x\in D_{j}$ then $\alpha_{i}y$ must be an
$f{i}$-development of $\alpha_{i}x$.

For any channel $B$ through $D$, its _$\alpha$ -image_ is the unique channel
$C$ through $E$ such that, for all $i\in I$, the set $C_{f{i}}$ is
$\\{{\alpha_{i}x\mid x\in B_{i}}\\}$.

######  Proposition 34.

Let $\alpha\colon(D_{i})_{i\in I}\to(E_{j})_{j\in J}$ be a cofinal embedding
of inverse chains. Let $B$ be a channel through $D$, with $\alpha$-image $C$.

  1. (1)

(Assuming $I$ has a least element.) If $B$ has a root, then $C$ does too.

  2. (2)

If $B$ has all levels $<\\!\\!\kappa$-sized, then so does $C$.

  3. (3)

The map $(y_{j})_{j\in J}\mapsto(x_{\alpha_{i}})_{i\in I}$ is a bijection from
the full branches of $C$ to those of $B$.

By part (3), if $B$ has no full branch, then neither does $C$. Our second step
involves the following tidy tree.

  1. (1)

Let $\\{{0,1}\\}^{i}$ be the set of $i$-sequences $(d_{j})_{j<i}$ of bits.

  2. (2)

For $j\leqslant i$ and $x\in\\{{0,1}\\}^{i}$ we write $x\restriction_{j}$ for
the restriction of $x$ to $j$.

  3. (3)

For a positive limit $i$, the _complete binary $i$-tree_ is
$(\\{{0,1}\\}^{j})_{j<i}$, with connecting maps given by restriction.

######  Proposition 35.

Let $D$ be a tidy $\omega_{1}$-tree with all levels countable. Then there is a
cofinal embedding $\alpha$ of $D$ into the complete binary $\omega_{1}$-tree.

######  Proof 6.3.

The index map is $i\mapsto\omega\times i$, which is well-defined and cofinal
because $i<\omega_{1}$ implies $i\leqslant\omega\times i<\omega_{1}$. The
injection $\alpha_{i}\;:\;D_{i}\to\\{{0,1}\\}^{\omega\times i}$ is defined by
induction on $i$, ensuring naturality wrt all $j\leqslant i$. For the
successor case, we choose an injection from the countably many
$i+1$-developments of each $x\in D_{i}$ to the $2^{\aleph_{0}}$-many
$\omega\times(i+1)$ developments of $\alpha_{i}x\in\\{{0,1}\\}^{\omega\times
i}$. The case where $i$ is a limit is uniquely defined: each $x\in D_{i}$ is
mapped to the unique $i$-sequence that, for all $j<i$, extends
$\alpha_{i}D_{{i}\geqslant{j}}x$. This is injective because $x$ is determined
by $(D_{{i}\geqslant{j}})_{j<i}$.

######  Corollary 36.

There is a channel through the complete binary $\omega_{1}$-tree, with all
levels countable, that has a root but no full branch.

######  Proof 6.4.

Proposition 33 gives an Aronszajn tidy tree. Embed it into the complete binary
$\omega_{1}$-tree and take its image.

It remains to cofinally embed the complete binary $\omega_{1}$-tree into
$(\nu^{(i)}{\mathcal{P}_{\mathsf{c}}})_{i<\omega_{1}}$. For this we encode a
sequence of bits as a set of ordinals, following [FH89][Lemmas 2.2 and 2.3].
For any ordinal $i$, and $c\in\\{{0,1}\\}^{i}$ we define

$\overline{c}=\\{{j<i\mid c_{j}=1}\\}\cup\\{{i}\\}$

For each set of ordinals $R$, let $u_{R}$ be a parent of $(v_{i})_{i\in R}$.

######  Lemma 37.

Let $j\leqslant i$ and $c\in\\{{0,1}\\}^{j}$ and $d\in\\{{0,1}\\}^{i}$. Then
$c=d\restriction_{j}$ iff ${u_{\overline{c}}}\sim_{j+1}{u_{\overline{d}}}$.

######  Corollary 38.

There is a cofinal embedding $\beta$ from the complete binary
$\omega_{1}$-tree into $(\nu^{(i)}{\mathcal{P}_{\mathsf{c}}})_{i<\omega_{1}}$,
with index map $i\mapsto i+1$.

######  Proof 6.5.

The injection
$\beta_{j}\colon\\{{0,1}\\}^{j}\to\nu^{(j+1)}{\mathcal{P}_{{<\kappa}}}$ sends
$c$ to $p_{j+1}{{u_{\overline{c}}}}$. Injectivity and naturality follow from
Lemma 37.

We now complete our proof. Corollary 36 gives a channel $E$ through the
complete binary $\omega_{1}$-tree, with all levels countable, that has a root
but no full branch. Its $\beta$-image is a channel through
$(\nu^{(i)}{\mathcal{P}_{\mathsf{c}}})_{i<\omega_{1}}$ with the same
properties.

##  7\. The Number of Successors

We further consider the final chain of $\mathcal{P}_{\mathsf{c}}$. Proposition
23 tells us that some element of $\nu^{(\omega)}{\mathcal{P}_{\mathsf{c}}}$
has $\aleph_{0}$ successors (since
$\nu^{(\omega)}{\mathcal{P}_{\mathsf{c}}}=\nu^{(\omega)}{\mathcal{P}_{\mathsf{f}}}$),
and some element of $\nu^{(\omega_{1})}{\mathcal{P}_{\mathsf{c}}}$ has
$\aleph_{1}$ successors. Are there elements with more successors than this?
Although this question is a digression from our main narrative, it provides an
application of the infrastructure we have assembled.

######  Proposition 39.

The size of $\nu^{(i)}{\mathcal{P}_{\mathsf{c}}}$ is

  * •

finite and positive, if $i$ is finite

  * •

$2^{\aleph_{0}}$, if $\omega\leqslant i<\omega_{1}$

  * •

$2^{\aleph_{1}}$, if $i\geqslant\omega_{1}$.

######  Proof 7.1.

Induction on $i$ gives the upper bound, since $\mathcal{P}_{\mathsf{c}}$ and
countable limit preserves $\leqslant\\!2^{\aleph_{0}}$-sizedness, and
$\omega_{1}$-limit preserves $\leqslant\\!2^{\aleph_{1}}$-sizedness. From
$\omega_{1}$ onwards the sets cannot get bigger. The lower bound is proved as
follows. For a set of ordinals $R$, we write $u_{R}$ for a parent of
$(v_{i})_{i\in R}$.

  * •

For $i\geqslant\omega$ we have a family $(p_{i}{{u_{R}}})_{R\subseteq\omega}$
of $2^{\aleph_{0}}$ distinct elements of $\mathcal{P}_{\mathsf{c}}{i}$. For
distinctness, let $R,S\subseteq\omega$ with $n\in R\setminus S$. Then
${u_{R}}\not\sim_{n+2}{u_{S}}$ because there is no $m\in S$ such that
$v_{n}\sim_{n+1}v_{m}$.

  * •

For $i\geqslant\omega_{1}$ we have a family
$(p_{i}{{u_{J}}})_{J\subseteq\omega_{1}}$ of $2^{\aleph_{1}}$ distinct
elements of $\mathcal{P}_{\mathsf{c}}{i}$, by the same argument.

######  Proposition 40.

For every positive limit $i<\omega_{1}$, some element of
$\nu^{(i)}{\mathcal{P}_{\mathsf{c}}}$ has $2^{\aleph_{0}}$ successors.

######  Proof 7.2.

Let $(i_{n})_{n\in\mathbb{N}}$ be a strictly increasing sequence with supremum
$i$. We define a cofinal embedding $\alpha$ of the complete binary
$\omega$-tree into the complete binary $i$-tree with index map $n\mapsto
i_{n}$ as follows: the injection $\alpha_{n}$ sends $(c_{m})_{m<n}$ to
$(d_{j})_{j<i_{n}}$, where $d_{j}$ is $c_{m}$ if $j=i_{m}$ for some (unique)
$m<n$ and $0$ otherwise. Corollary 38 gives a cofinal embedding $\beta$ of the
complete binary $i$-tree into $(\nu^{(j)}{\mathcal{P}_{\mathsf{c}}})_{j<i}$.
The $\beta\alpha$-image of the complete binary $\omega$-tree is a channel
through $(\nu^{(j)}{\mathcal{P}_{\mathsf{c}}})_{j<i}$ with $2^{\aleph_{0}}$
full branches, corresponding across $\Psi_{i}$ to an element of
$\nu^{(i)}{\mathcal{P}_{\mathsf{c}}}$ with $2^{\aleph_{0}}$ successors.

At $\omega_{1}$ the question is harder to answer.

######  Proposition 41.

For any cardinal $\lambda$, the following are equivalent.

  1. (1)

Some element of $\nu^{(\omega_{1})}{\mathcal{P}_{\mathsf{c}}}$ has precisely
$\lambda$ successors.

  2. (2)

There is a tidy $\omega_{1}$-tree, with all levels countable, that has
precisely $\lambda$ full branches.

######  Proof 7.3.

For (1)$\Rightarrow$(2), any such element corresponds across
$\Psi_{\omega_{1}}$ to the desired tree—unless it is $0_{\omega_{1}}$, but in
that case $\lambda=0$ and Theorem 33 gives (2).

For (2)$\Rightarrow$(1), let $D$ be such a tree. We embed it cofinally into
the complete binary $\omega_{1}$-tree (Proposition 35), and embed this in turn
into $(\nu^{(i)}{\mathcal{P}_{\mathsf{c}}})_{i<\omega_{1}}$ (Corollary 38),
and the image corresponds via $\Psi_{\omega_{1}}$ to the desired element.

Thus the existence of an element of
$\nu^{(\omega_{1})}{\mathcal{P}_{\mathsf{c}}}$ with more than $\aleph_{1}$
successors is equivalent to the existence of a tidy $\omega_{1}$-tree, with
all levels countable, that has more than $\aleph_{1}$ full branches. Such a
tree is said to be _Kurepa_ and its existence is independent of ZFC, under
certain assumptions444ZFC cannot prove that a Kurepa tree exists, if ZFC $+$
an inaccessible is consistent [Sil71]. ZFC cannot prove that a Kurepa tree
does not exist, if ZFC is consistent (Solovay)..

##  8\. Beyond $\omega_{1}$

###  8.1. Properties of Ordinals and Cardinals

We have now completed our study of the final chain of the countable powerset
functor. But for $\mathcal{P}_{{<\kappa}}$ we can continue, by asking what
happens in the final chain beyond $\omega_{1}$. We shall see that,
surprisingly, there is a sharp division between those limit ordinals where
strong extensionality holds and those where there is a ghost. This is our main
result, Theorem 49 below. The same method of [FH89] is adapted to construct
all these ghosts.

Our classification relies on the following properties. An ordinal is _$\omega$
-cofinal_ when it is the supremum of a strictly increasing sequence
$(i_{n})_{n\in\mathbb{N}}$. Thus every countable limit is either $0$ or
$\omega$-cofinal. Let $\lambda$ be a regular infinite cardinal.

  1. (1)

$\lambda$ has the _tree property_ when every tidy $\lambda$-tree with all
levels $<\\!\\!\lambda$-sized has a full branch.

  2. (2)

$\lambda$ is _strongly inaccessible_ when, for every $<\\!\\!\lambda$-sized
set $A$, the set $\mathcal{P}A$ is also $<\\!\\!\lambda$-sized.

  3. (3)

$\lambda$ is _weakly compact_ when it is strongly inaccessible and has the
tree property.

Note that in Definition 8.1(1), it is essential for the levels to be
$<\\!\\!\lambda$-sized, because of Proposition 32. Only in the case
$\lambda=\aleph_{0}$ is a full branch guaranteed to exist without this
condition. By Theorem 33, $\aleph_{1}$ does not have the tree property.
Whether $\aleph_{2}$ has it is independent of ZFC under certain
assumptions555ZFC cannot prove that $\aleph_{2}$ has the tree property, if ZFC
is consistent [Spe49]. ZFC cannot prove that $\aleph_{2}$ lacks the tree
property, if ZFC $+$ a weakly compact cardinal is consistent [Mit72]..

We deem $\aleph_{0}$ to be strongly inaccessible (and hence weakly compact).
Successor cardinals such as $\aleph_{1}$ are not inaccessible. The importance
of strong inaccessibility in our story comes from the following fact.

######  Proposition 42.

If $\lambda$ is strongly inaccessible, then for all $i<\lambda$ the set
$\nu^{(i)}{\mathcal{P}}$ is $<\\!\\!\lambda$-sized.

######  Proof 8.1.

By induction on $i$. The successor case is by the definition of strong
inaccessibility. For a limit $i<\lambda$, we use the fact that if
$(A_{j})_{j<i}$ is an inverse chain of $<\\!\\!\lambda$-sized sets then its
limit is $<\\!\\!\lambda$-sized.

###  8.2. Connecting map to a successor

In Section 5 we derived several properties of countable ordinals from
Proposition 26. Accordingly, we shall begin by analyzing at which ordinals the
property described there holds. The following limit ordinals are said to be
_$\kappa$ -extensible_:

  * •

$0$.

  * •

Any $\omega$-cofinal ordinal.

  * •

Any weakly compact cardinal.

  * •

Any limit ordinal $\geqslant\kappa+\omega$, if $\kappa<\infty\infty$.

  * •

$\kappa$, if $\kappa<\infty\infty$ and $\kappa$ has the tree property.

We complete Proposition 26 as follows.

######  Proposition 43.

For ordinals $j<i$ the following are equivalent.

  1. (1)

For all $a\in\nu^{(i)}{\mathcal{P}_{{<\kappa}}}$ we have
$\nu^{({i}\geqslant{j+1})}a=\\{{\nu^{({i}\geqslant{j})}b\mid
a\rightsquigarrow_{i}b}\\}$.

  2. (2)

$i$ is either a successor or a $\kappa$-extensible limit.

######  Proof 8.2.

of (2) $\Rightarrow$ (1). The successor and zero cases are trivial, and the
case $i\geqslant\kappa+\omega$ follows from Corollary 17. Let us consider the
other cases. For $b\in\nu^{({i}\geqslant{j+1})}$, we know that $b$ is an
element of the $j$th level of the channel $\Psi_{i}(a)$ through
$(\nu^{(k)}{\mathcal{P}_{{<\kappa}}})_{k<i}$, and we want to extend it to a
full branch. We may reformulate this problem by expressing $i$ as
$j+i^{\prime}$, and defining the tidy $i^{\prime}$-tree
$(A_{k})_{k<i^{\prime}}$ where $A_{k}$ is the set of $j+k$-developments of
$b$. We want a full branch for this tree.

  * •

Suppose that $i$ is $\omega$-cofinal, so $i^{\prime}$ is too. Let
$(i_{n})_{n\in\mathbb{N}}$ be a strictly increasing sequence with supremum
$i^{\prime}$. We obtain a full branch by dependent choice. (The size of the
sets $A_{k}$ is immaterial in this case.)

  * •

Suppose that $\kappa$ has the tree property and $i=\kappa$, so
$i^{\prime}=\kappa$. For $k<\kappa$ the set $A_{k}$, being a subset of
$\nu^{(j+k)}{\mathcal{P}_{{<\kappa}}}$, is $<\\!\\!\kappa$-sized. So the tree
property gives a full branch through $(A_{k})_{k<\kappa}$.

  * •

Suppose that $i$, and therefore $i^{\prime}$, is a weakly compact cardinal
$\lambda<\kappa$. For $k<\lambda$, we have also $j+k<\lambda$, and so $A_{k}$,
being a subset of $\nu^{(j+k)}{\mathcal{P}_{{<\kappa}}}$, is
$<\\!\\!\lambda$-sized by Proposition 42. So the tree property gives a full
branch through $(A_{k})_{k<\lambda}$.

To prove the converse, we use the following notion of ghost. Let $i$ be a
limit. A _$\mathcal{P}_{{ <\kappa}}$-ghost at $i$_ is a
$\mathcal{P}_{{<\kappa}}$-Cauchy element of
$\nu^{(i)}{\mathcal{P}_{{<\kappa}}}$, distinct from $0(i)$, that has no
successor. The Cauchy condition was omitted in Proposition 31 because every
element of $\nu^{(\omega_{1})}{\mathcal{P}_{{<\kappa}}}$ is
$\mathcal{P}_{{<\kappa}}$-Cauchy (Corollary 13(3).)

Any $\mathcal{P}_{{<\kappa}}$-ghost $a$ at $i$ does not satisfy the equation
in (1), because the LHS is $a_{j+1}$, which is inhabited, but the RHS is
empty. So there cannot be a $\mathcal{P}_{{<\kappa}}$-ghost at a
$\kappa$-extensible ordinals. The following two results establish that, at all
other limits, a $\mathcal{P}_{{<\kappa}}$-ghost does exist, giving (1)
$\Rightarrow$ (2) as required.

Again we use channels: a $\mathcal{P}_{{<\kappa}}$-ghost at $i$ corresponds
via $\Psi_{i}$ to a channel through
$(\nu^{(j)}_{\mathrm{coalg}}{\mathcal{P}_{{<\kappa}}})_{j<i}$, with all levels
$<\\!\\!\kappa$-sized, that has a root but no full branch.

######  Proposition 44.

Let $\kappa<\infty\infty$ not have the tree property. Then there is a
$\mathcal{P}_{{<\kappa}}$-ghost at $\kappa$.

######  Proof 8.3.

Since $\kappa$ does not have the tree property, there is a tidy $\kappa$-tree
$D$ with no full branch. (Such a tree is said to be _$\kappa$ -Aronszajn_.)

We give a cofinal embedding $\alpha$ of $D$ into the complete binary
$\kappa$-tree as follows. The index map is $f\;:\;i\mapsto\sum_{j<i}|D_{j}|$.
This is well-defined and cofinal because $i<\kappa$ implies $i\leqslant
f{i}<\kappa$, since $1\leqslant|D_{j}|<\kappa$ and $\kappa$ is regular. We
give the $i$-th level map $\alpha_{i}\;:\;D_{i}\to\\{{0,1}\\}^{f{i}}$ by
induction on $i$, ensuring naturality wrt all $j\leqslant i$. For the
successor case, we have $f{(i+1)}=f{i}+|D_{i}|$, so we take an injection from
the $\leqslant\\!|D_{i}|$-many $i+1$-developments of each $x\in D_{i}$ to the
$2^{|D_{i}|}$-many $f{(i+1)}$-developments of
$\alpha_{i}x\in\\{{0,1}\\}^{f{i}}$. The case where $i$ is a limit is uniquely
defined, as in the proof of Proposition 35.

The image $E$ of $D$ is a channel through the complete binary $\kappa$-tree
with a root but no full branch. As in Corollary 38, we define a cofinal
embedding $\beta$ of the complete binary $\kappa$-tree into
$(\nu^{(j)}_{\mathrm{coalg}}{\mathcal{P}_{{<\kappa}}})_{j<\kappa}$, with index
map $j\mapsto j+1$. The $\beta$-image of $E$ is the desired channel.

######  Proposition 45.

Let $i<\kappa$ be a positive limit that is neither $\omega$-cofinal nor weakly
compact. Then there is a $\mathcal{P}_{{<\kappa}}$-ghost at $i$.

######  Proof 8.4.

Let $\lambda$ be the cofinality of $i$. Then $\lambda$ is a regular cardinal
$>\aleph_{0}$. There are three possibilities:

  1. (1)

$i$ is not a regular cardinal, i.e. $i>\lambda$.

  2. (2)

$i=\lambda$ and $\lambda$ is not strongly inaccessible.

  3. (3)

$i=\lambda$ and $\lambda$ does not have the tree property.

For case (1), Proposition 32 gives a tidy $\lambda$-tree $D$, with every level
$\leqslant\\!\\!\lambda$-sized, that has no full branch. Evidently there is a
cofinal embedding $\alpha$ of $D$ into the complete $\lambda$-ary
$\lambda$-tree $(\lambda^{j})_{j<\lambda}$, with index map $j\mapsto j$. We
shall give a cofinal embedding $\beta$ of the complete $\lambda$-ary
$\lambda$-tree into
$(\nu^{(j)}_{\mathrm{coalg}}{\mathcal{P}_{{<\kappa}}})_{j<i}$. Then the
$\beta\alpha$-image of $D$ is a channel through
$(\nu^{(j)}_{\mathrm{coalg}}{\mathcal{P}_{{<\kappa}}})_{j<i}$, with every
level $\leqslant\\!\\!\lambda$-sized, that has a root but no full branch.
Whereas we previously encoded a sequence of bits as a set of ordinals, we
shall now encode a sequence of elements of $\lambda$ as a set of sets of
ordinals.

Since $i>\lambda$, express $i$ as the supremum of a strictly increasing
$\lambda$-sequence $(\eta_{j})_{j<\lambda}$ in $\eta$, with
$\eta_{0}\geqslant\lambda$. The idea is to encode an ordered pair $(k,l)$,
where $k,l<\lambda$, as $\\{{\eta_{k},l}\\}$. Clearly, for
$k,k^{\prime}<j<\lambda$ and $l,l^{\prime}<\lambda$, we have

${u_{\\{{\eta_{k},l}\\}}}\sim_{\eta_{j}+1}{u_{\\{{\eta_{k^{\prime}},l^{\prime}}\\}}}\iff
k=k^{\prime}\text{ and }l=l^{\prime}$ (1)

For $j<\lambda$ and $c\in\lambda^{j}$, we set

$\overline{c}\stackrel{{\scriptstyle\mbox{\rm{\tiny
def}}}}{{=}}\\{{\\{{\eta_{k},c_{k}}\\}\mid
k<j}\\}\cup\\{{\\{{\eta_{j},l}\\}\mid l<\lambda}\\}$

For a set of ordinals $R$ we write ${u_{R}}$ for a parent of $(v_{j})_{j\in
R}$, and for a set of sets of ordinals $S$ we write ${t_{S}}$ for a parent of
$({u_{R}})_{R\in S}$. For $k\leqslant j<\lambda$ and $c\in\lambda^{k}$ and
$d\in\lambda^{j}$, we deduce from (1) that

$c=d\restriction_{k}\iff{t_{\overline{c}}}\sim_{\eta_{k}+2}{t_{\overline{d}}}$
(2)

The cofinal embedding $\beta$ of the complete $\lambda$-ary $\lambda$-tree
into $(\nu^{(j)}_{\mathrm{coalg}}{\mathcal{P}_{{<\kappa}}})_{j<i}$ has index
map $j\mapsto\eta_{j}+2$. The $j$-th level map
$\beta_{i}\lambda^{j}\to\nu^{(\eta_{j}+2)}{\mathcal{P}_{{<\kappa}}}$ sends $c$
to $p_{\eta_{j}+2}{{t_{\overline{c}}}}$. Injectivity and naturality follow
from 2.

For case (2), Proposition 32 gives a tidy $\lambda$-tree $D$, with all levels
$\leqslant\\!\\!\lambda$-sized, that has no full branch. We give a cofinal
embedding $\alpha$ of $D$ in the complete binary $\lambda$-tree as follows.
Since $\lambda$ is not strongly inaccessible, there is a cardinal
$\mu<\lambda$ such that $2^{\mu}\geqslant\lambda$. The index map is
$j\mapsto\mu\times j$. This is well-defined and cofinal because $j<\lambda$
implies $j\leqslant\mu\times j<\lambda$, since $1\leqslant\mu<\lambda$ and
$\lambda$ is regular. We give the $j$-th level map
$\alpha_{i}\;:\;D_{j}\to\\{{0,1}\\}^{\mu\times j}$ by induction on $j$,
ensuring naturality wrt all $k\leqslant j$. For the successor case, we take an
injection from the $\leqslant\\!\\!\lambda$-many $j+1$-developments of each
$x\in D_{j}$ to the $2^{\mu}$-many $\mu\times(j+1)$ developments of
$\alpha_{i}x\in\\{{0,1}\\}^{\mu\times j}$. The case where $j$ is a limit is
uniquely defined, as in the proof of Proposition 35.

Next we obtain an embedding $\beta$ of the complete binary $\lambda$-tree into
$(\nu^{(j)}_{\mathrm{coalg}}{\mathcal{P}_{{<\kappa}}})_{j<\lambda}$, with
index map $j\mapsto j+1$, as in Corollary 38. The $\beta\alpha$-image of $D$
is a channel through
$(\nu^{(j)}_{\mathrm{coalg}}{\mathcal{P}_{{<\kappa}}})_{j<\lambda}$, with all
levels $\leqslant\\!\\!\lambda$-sized, that has a root but no full branch.

For case (3), Proposition 44 gives a $\mathcal{P}_{{<\lambda}}$-ghost at
$\lambda$, which is also a $\mathcal{P}_{{<\kappa}}$-ghost at $\lambda$.

###  8.3. Consequences of the ghosts

Our aim is to revisit each of the properties listed in Section 5, to see at
which ordinals it holds. So we want to obtain many negative results from a
ghost. We begin with some methods for doing so.

######  Lemma 46.

A $\mathcal{P}$-ghost at limit $i$ is not in the image of
$\nu^{({i+1}\geqslant{i})}\mathcal{P}$.

######  Proof 8.5.

Let $\nu^{({i+1}\geqslant{i})}b$, for $b\in\nu^{(i+1)}{\mathcal{P}}$, be a
$\mathcal{P}$-ghost at $i$. It corresponds across $\Psi_{i}$ to the range of
$b$. Any element of $b$ would be a full branch of the range of $b$, which does
not exist, so $b$ is empty. But then its range is empty, contradiction.

We shall use the singleton operation $\\{{-}\\}$ applied $n$ times to a ghost.

######  Lemma 47.

Let $a$ a $\mathcal{P}$-ghost at positive limit $i$, and $n\in\mathbb{N}$.
Then $\\{{-}\\}^{n}a\in\nu^{(i+n)}{\mathcal{P}}$ has the following properties.

  1. (1)

$p_{n+1}{\\{{-}\\}^{n}a}\not=\nu^{({i+n}\geqslant{n+1})}\\{{-}\\}^{n}a$.

  2. (2)

$\\{{-}\\}^{n}a$ is not in the image of
$\nu^{({i+n+1}\geqslant{i+n})}\mathcal{P}$.

  3. (3)

$\\{{-}\\}^{n}a$ is not $\mathcal{P}$-coalgebraic.

  4. (4)

${\\{{-}\\}^{n}a}\sim{\\{{-}\\}^{n}0(i)}$ but
$\\{{-}\\}^{n}a\not=\\{{-}\\}^{n}0(i)$.

  5. (5)

${\\{{-}\\}^{n}a}\not\sim_{n+1}{\nu^{({i+n}\geqslant{j})}\\{{-}\\}^{n}a}$ for
any $j<i$ such that $j>n$.

######  Proof 8.6.

  1. (1)

Induction on $n$ gives $p_{n+1}{\\{{-}\\}^{n}a})=\\{{-}\\}^{n}\emptyset$ and
$\nu^{({i+n}\geqslant{n+1})}\\{{-}\\}^{n}a=\\{{-}\\}^{n}\\{{()}\\}$.

  2. (2)

Induction on $n$. The case $n=0$ is Lemma 46. The inductive step follows from
$\nu^{({i+n+2}\geqslant{i+n+1})}b=\\{{\nu^{({i+n+1}\geqslant{i+n})}c\mid c\in
b}\\}$.

  3. (3)

Follows from part (2).

  4. (4)

Each part is by induction on $n$.

  5. (5)

We have
$\nu^{({i+n}\geqslant{j})}\\{{-}\\}^{n}a\rightsquigarrow^{n}\nu^{({i}\geqslant{\mathsf{pred}^{n}({j})})}a$.
Since $n<j<i$ we have $0<\mathsf{pred}^{n}({j})<i$, so
$\nu^{({i}\geqslant{\mathsf{pred}^{n}({j})})}a$ has a successor. But if
$\\{{-}\\}^{n}a\rightsquigarrow^{n}b$, then $b=a$, which has no successor.

For our results, we use the following terminology. For an ordinal $i$, let
$i=i^{\prime}+m$ where $i^{\prime}$ is a limit and $m\in\mathbb{N}$. Then we
write

$\begin{array}[]{rcll}\mathrm{LP}({i})&\stackrel{{\scriptstyle\mbox{\rm{\tiny
def}}}}{{=}}&i^{\prime},&\text{the \emph{limit part} of $i$.}\\\
\mathrm{FP}({i})&\stackrel{{\scriptstyle\mbox{\rm{\tiny
def}}}}{{=}}&m,&\text{the \emph{finite part} of $i$.}\end{array}$

The following completes Lemma 27.

######  Theorem 48.

For $j\leqslant i$, the following are equivalent.

  1. (1)

For all $a\in\nu^{(i)}{\mathcal{P}_{{<\kappa}}}$ we have
$p_{i}{a}=\nu^{({i}\geqslant{j})}a$.

  2. (2)

Either $j\leqslant\mathrm{FP}({i})$ or $\mathrm{LP}({i})$ is
$\kappa$-extensible.

######  Proof 8.7.

For (2)$\Rightarrow$(1), the case ($j\leqslant\mathrm{FP}({i})$) is
Proposition 25(3), and the case of $\kappa$-extensible $\mathrm{LP}({i})$ is
proved the same way as Lemma 27.

For the converse, let $a$ be a $\mathcal{P}_{{<\kappa}}$-ghost $a$ at
$\mathrm{LP}({i})$. If
$p_{j}{\\{{-}\\}^{\mathrm{FP}({i})}a}=\nu^{({i}\geqslant{j})}{\\{{-}\\}^{\mathrm{FP}({i})}a}$
then (since $\mathrm{FP}({i})+1\leqslant j$) we have
$p_{\mathrm{FP}({i})+1}{\\{{-}\\}^{\mathrm{FP}({i})}a}=\nu^{({i}\geqslant{\mathrm{FP}({i})+1})}{\\{{-}\\}^{\mathrm{FP}({i})}a}$,
contradicting Lemma 47(1).

We come to the main result of the paper, which completes Proposition 28.

######  Theorem 49.

For any ordinal $i$, the following are equivalent.

  1. (1)

For all $a\in\nu^{(i)}{\mathcal{P}_{{<\kappa}}}$ we have $p_{i}{a}=a$.

  2. (2)

Every $a\in\nu^{(i)}{\mathcal{P}_{{<\kappa}}}$ is $\mathcal{P}$-coalgebraic.

  3. (3)

For $a,b\in\nu^{(i)}{\mathcal{P}_{{<\kappa}}}$, if $a\sim_{i}b$ then $a=b$.

  4. (4)

For $a,b\in\nu^{(i)}{\mathcal{P}_{{<\kappa}}}$, if $a\sim b$ then $a=b$.

  5. (5)

$\mathrm{LP}({i})$ is $\kappa$-extensible.

######  Proof 8.8.

Proposition 48 gives (5)$\Leftrightarrow$(1). Parts (2)–(4) follow just as in
Proposition 28.

If $\mathrm{LP}({i})$ is not $\kappa$-extensible, let $a$ be a
$\mathcal{P}_{{<\kappa}}$-ghost at $\mathrm{LP}({i})$. By Lemma 47(3),
$\\{{-}\\}^{\mathrm{FP}({i})}a$ is not $\mathcal{P}$-coalgebraic, and is
bisimilar to but distinct from $0(i)$.

Another way of obtaining negative results from a ghost is the following.

######  Lemma 50.

Let $i<\kappa$ be a positive limit, and let $a$ be a
$\mathcal{P}_{{<\kappa}}$-ghost at $i$. There is a sequence
$(x_{m})_{m\in\mathbb{N}}$ of $<\\!\\!\kappa$-branching pointed systems such
that

  * •

$p_{i}{x_{0}}\rightsquigarrow a$

  * •

every successor of $x_{0}$ has a successor

  * •

$x_{m+1}$ is a parent of just $x_{m}$.

######  Proof 8.9.

The only difficulty is to obtain $x_{0}$, for we can then obtain $x_{m}$ by
induction on $m$. Since $a$ is $\mathcal{P}_{{<\kappa}}$-Cauchy, we may
choose, for each positive $j<i$, a $<\\!\\!\kappa$-branching pointed system
$y_{j}$ such that $a_{j+1}=p_{j+1}{y_{j}}$ (and hence $a_{j}=p_{j}{y_{j}}$).
Let $x_{0}$ be a parent of $(y_{j})_{j<i}$. Then for $j<i$, we have
$(p_{i}{x_{0}})_{j+1}=p_{j+1}{x_{0}}=\\{{p_{j}{y}\mid x_{0}\rightsquigarrow
y}\\}\ni a_{j}$, so $p_{i}{x_{0}}\rightsquigarrow a$. Any successor $y$ of
$x_{0}$ is, for some $j<i$, an embedding applied to $y_{j}$. Since
$p_{j+1}{y_{j}}$ is inhabited, $y_{j}$ and hence $y$ must have a successor.

We shall complete Corollary 29, which characterizes $p_{i}{x}$ and
$\nu^{({i}\geqslant{j})}a$, in two parts: firstly considering when these
elements have the required property (Proposition 51), and secondly considering
when no other element has it (Proposition 52).

######  Proposition 51.

  1. (1)

For an ordinal $j$, the following are equivalent.

    1. (a)

For any $<\\!\\!\kappa$-branching pointed system $x$ we have
$x\sim_{j}p_{j}{x}$.

    2. (b)

Either $j\geqslant\kappa$ (for $\kappa<\infty\infty$) or $\mathrm{LP}({j})$ is
$\kappa$-extensible.

  2. (2)

For ordinals $j\leqslant i$, the following are equivalent.

    1. (a)

For any $a\in\nu^{(i)}{\mathcal{P}_{{<\kappa}}}$, we have
$\nu^{({i}\geqslant{j})}a\sim_{j}a$.

    2. (b)

Either $j=i$ or $j\leqslant\mathrm{FP}({i})$ or $j\geqslant\kappa$ (for
$\kappa<\infty\infty$) or both $\mathrm{LP}({j})$ and $\mathrm{LP}({i})$ are
$\kappa$-extensible.

######  Proof 8.10.

For (1b)$\Rightarrow$(1a), the $\kappa$-extensible case is proved as in
Corollary 29(1 and the case $j\geqslant\kappa$ holds by Proposition 20. For
(2b)$\Rightarrow$(2a), the $\kappa$-extensible case is proved as in Corollary
29(2, the case $j\geqslant\kappa$ is by Proposition 16 and the case
$j\leqslant\mathrm{FP}({i})$ follows from Proposition 25(3).

For the converse we proceed as follows.

  1. (1)

If $j<\kappa$ and $\mathrm{LP}({j})$ is not $\kappa$-extensible, let $a$ be a
$\mathcal{P}_{{<\kappa}}$-ghost at $\mathrm{LP}({j})$ and form the sequence
$(x_{m})_{m\in\mathbb{N}}$ as in Lemma 50. Put
$n\stackrel{{\scriptstyle\mbox{\rm{\tiny def}}}}{{=}}\mathrm{FP}({j})$. Then
$p_{j}{x_{n}}\rightsquigarrow^{n}p_{j}{x_{0}}\rightsquigarrow a$ and $a$ has
no successor, whereas if $x_{n}\rightsquigarrow^{n+1}y$ then $y$ has a
successor. So $p_{j}{x_{n}}\not\sim_{n+2}x_{n}$.

  2. (2)

Suppose $\mathrm{FP}({i})<j<i,\kappa$, and $\mathrm{LP}({j})$ and
$\mathrm{LP}({i})$ are not both $\kappa$-extensible. We consider three cases.

     * •

If $\mathrm{LP}({j})=\mathrm{LP}({i})$, put $L=\mathrm{LP}({j})$ and $j=L+n$
and $i=L+m+n+1$. Let $a$ be a $\mathcal{P}_{{<\kappa}}$-ghost at $L$ and form
the sequence $(x_{m})_{m\in\mathbb{N}}$ as in Lemma 50. Put
$b\stackrel{{\scriptstyle\mbox{\rm{\tiny def}}}}{{=}}p_{i}{x_{n}}$. Then
$\nu^{({i}\geqslant{j})}b=p_{L+n}{x_{n}}\rightsquigarrow^{n+1}a$, which has no
successor. On the other hand, if $b\rightsquigarrow^{n+1}c$ then
$c=p_{L+m}{y}$, for some successor $y$ of $x_{0}$, and since $y$ has a
successor, $c$ does too. So $b\not\sim_{n+2}\nu^{({i}\geqslant{j})}b$.

     * •

If $\mathrm{LP}({i})$ is not $\kappa$-extensible and $j<\mathrm{LP}({i})$, let
$a$ be a $\mathcal{P}_{{<\kappa}}$-ghost at $\mathrm{LP}({i})$. Put
$n\stackrel{{\scriptstyle\mbox{\rm{\tiny def}}}}{{=}}\mathrm{FP}({i})$ and
apply Lemma 47(5).

     * •

If $\mathrm{LP}({i})$ is $\kappa$-extensible then $\mathrm{LP}({j})$ is not,
so let $a$ be a $\mathcal{P}_{{<\kappa}}$-ghost at $\mathrm{LP}({j})$ and form
the sequence $(x_{m})_{m\in\mathbb{N}}$ as in Lemma 50. Put
$n\stackrel{{\scriptstyle\mbox{\rm{\tiny def}}}}{{=}}\mathrm{FP}({j})$ and
$b\stackrel{{\scriptstyle\mbox{\rm{\tiny def}}}}{{=}}p_{i}{x_{n}}$. Then
$b\sim_{i}x_{n}$ but
$\nu^{({i}\geqslant{j})}b=p_{j}{x_{n}}\not\sim_{n+2}x_{n}$, as we saw in the
proof of part 1. So $b\not\sim_{n+1}\nu^{({i}\geqslant{j})}b$.

######  Proposition 52.

  1. (1)

For any ordinal $j$, the following are equivalent.

    1. (a)

For any $<\\!\\!\kappa$-branching pointed system $x$, any
$b\in\nu^{(j)}{\mathcal{P}_{{<\kappa}}}$ such that $b\sim_{j}x$ is $p_{j}{x}$.

    2. (b)

For any $<\\!\\!\kappa$-branching pointed system $x$, we can characterize
$p_{j}{x}$ as the unique $b\in\nu^{(j)}{\mathcal{P}_{{<\kappa}}}$ such that
$b\sim_{j}x$.

    3. (c)

$\mathrm{LP}({j})$ is $\kappa$-extensible.

  2. (2)

For any ordinals $j\leqslant i$, the following are equivalent.

    1. (a)

For any $a\in\nu^{(i)}{\mathcal{P}_{{<\kappa}}}$, any
$b\in\nu^{(j)}{\mathcal{P}_{{<\kappa}}}$ such that $b\sim_{j}a$ is
$\nu^{({i}\geqslant{j})}a$.

    2. (b)

For any $a\in\nu^{(i)}{\mathcal{P}_{{<\kappa}}}$, we can characterize
$\nu^{({i}\geqslant{j})}a$ as the unique
$b\in\nu^{(j)}{\mathcal{P}_{{<\kappa}}}$ such that $b\sim_{j}a$.

    3. (c)

Either $j\leqslant\mathrm{FP}({i})$ or both $\mathrm{LP}({j})$ and
$\mathrm{LP}({i})$ are $\kappa$-extensible.

######  Proof 8.11.

The proof of (1c)$\Rightarrow$(1b) and (2c)$\Rightarrow$(2b) is proved the
same way as Corollary 29. For the converse parts, we form a sequence
$(z_{m})_{m\in\mathbb{N}}$ where $z_{0}$ is a parent of nothing, i.e. a
pointed system with no successor, and $z_{m+1}$ a parent of just $z_{m}$.
(Essentially this is the Zermelo encoding of the natural numbers.)

In both parts, if $\mathrm{LP}({j})$ is not $\kappa$-extensible, let $a$ be a
$\mathcal{P}_{{<\kappa}}$-ghost at $\mathrm{LP}({j})$ and put
$n\stackrel{{\scriptstyle\mbox{\rm{\tiny def}}}}{{=}}\mathrm{FP}({j})$. Then
$p_{j}{z_{n}}=\\{{-}\\}^{n}0_{\mathrm{LP}({j})}$ (lemma:
$p_{k+n}{z_{n}}=\\{{-}\\}^{n}0_{k}$, by induction on $n$), which is bisimilar
to but distinct from $\\{{-}\\}^{n}a$, so (1a) is false. And, in part 2, this
is also $\nu^{({i}\geqslant{j})}{p_{i}{z_{n}}}$, so (2a) is false.

In part (2), if $\mathrm{LP}({i})$ is not $\kappa$-extensible and
$j>m\stackrel{{\scriptstyle\mbox{\rm{\tiny def}}}}{{=}}\mathrm{FP}({i})$, let
$a$ be a $\mathcal{P}_{{<\kappa}}$-ghost at $\mathrm{LP}({i})$. Then
$p_{j}{z_{m}}$ is bisimilar to $z_{m}$ (this is a lemma for all $j>m$, by
induction on $m$) and hence to $\\{{-}\\}^{m}a$. But
$p_{j}{z_{m}}=\nu^{({i}\geqslant{j})}\\{{-}\\}^{m}a$ would imply, by applying
$\nu^{({j}\geqslant{m+1})}$, that
$p_{m+1}{z_{m}}=\nu^{({i}\geqslant{m+1})}\\{{-}\\}^{m}a$ i.e.
$\\{{-}\\}^{m}=\\{{-}\\}^{m}()$, contradiction. So (2a) is false.

We complete Proposition 30 as follows.

######  Proposition 53.

Assume $\kappa<\infty\infty$.

  1. (1)

Let $j$ be an ordinal. Every element of
$\nu^{(\kappa+j)}{\mathcal{P}_{{<\kappa}}}$ that is
$\mathcal{P}_{{<\kappa}}$-coalgebraic is $<\\!\\!\kappa$-branching, and
conversely iff either $j\geqslant\omega$ or $\kappa$ has the tree property .

  2. (2)

Let $j\leqslant i$ be ordinals. Every element of
$\nu^{(\kappa+j)}{\mathcal{P}_{{<\kappa}}}$ that is in the range of
$\nu^{({\kappa+i}\geqslant{\kappa+j})}$ is $<\\!\\!\kappa$-branching at depth
$<i$, and conversely iff either $j=i$ or $j\geqslant\omega$ or $\kappa$ has
the tree property.

######  Proof 8.12.

We only need to prove the converse parts. If $j\geqslant\omega$ then every
element of $\nu^{(\kappa+j)}{\mathcal{P}_{{<\kappa}}}$ is
$<\\!\\!\kappa$-branching. If $\kappa$ has the tree property, we proceed as
for $\aleph_{0}$. Otherwise, let $a$ be a $\mathcal{P}_{{<\kappa}}$-ghost at
$\kappa$. The element $\\{{-}\\}^{j}a$ is $<\\!\\!\kappa$-branching but not
$\mathcal{P}_{{<\kappa}}$-coalegebraic and not in the image of
$\nu^{({\kappa+j+1}\geqslant{\kappa+j})}$, by Lemma 47(2)–(3).

###  8.4. Surjectivity and $\mathcal{P}_{{<\kappa}}$-coalgebraicity

We next consider which connecting maps are surjective.

######  Proposition 54.

Let $\lambda$ be a regular infinite cardinal with the tree property that is
less than $\kappa$. Then $\mathcal{P}_{{<\kappa}}$ and
$\mathcal{P}^{+}_{<\kappa}$ preserve, up to a surjection, the limit of any
inverse $\lambda$-chain $D$ with all levels $<\\!\\!\lambda$-sized.
Explicitly, any channel $C$ through $D$ is the range of a
$<\\!\\!\kappa$-sized set of full branches.

######  Proof 8.13.

It suffices to prove the case where $D_{i}=\lim_{j<i}D_{j}$ for each limit
$i<\lambda$. For $i<\lambda$, each $x\in C_{i}$ extends by the tree property
to a full branch through $D$, because all levels are $<\\!\\!\lambda$-sized.
For each $i<\lambda$ and $x\in C_{i}$, choose such a branch $\theta_{i}(x)$,
by the Axiom of Choice. The set $\\{{\theta_{i}(x)\mid i<\lambda,x\in
C_{i}}\\}$ has size $\leqslant\lambda\times\lambda=\lambda<\kappa$ and has
range $C$.

######  Proposition 55.

For ordinals $j\leqslant i$, the following are equivalent.

  1. (1)

The connecting map $\nu^{({i}\geqslant{j})}\mathcal{P}_{{<\kappa}}$ is an
surjection.

  2. (2)

Either $j=i$ or $\mathrm{LP}({j})$ is either $0$ or $\omega$-cofinal or weakly
compact or $\geqslant\kappa+\omega$ (for $\kappa<\infty\infty$).

######  Proof 8.14.

By Proposition 11 we may assume $i=j+1$. The case $j\geqslant\kappa$ has been
treated (Proposition 10 and 24), so we assume $j<\kappa$. Since
$\mathcal{P}_{{<\kappa}}$ preserves and reflects surjectivity, we may assume
$j$ is a limit.

For (2)$\Rightarrow$(1), it suffices by Proposition 6 for
$\mathcal{P}_{{<\kappa}}$ to preserve the limit of any inverse $j$-chain up to
a surjection. The $j=0$ case is trivial, the $\omega$-cofinal case is by
Proposition 12, and the weakly compact case is by Proposition 54. For the
converse, if $j<\kappa$ and $j$ is not $\kappa$-extensible then there is a
$\mathcal{P}_{{<\kappa}}$-ghost at $j$, which is not even
$\mathcal{P}$-coalgebraic.

######  Corollary 56.

For an ordinal $i$, the following are equivalent.

  * •

Every element of $\nu^{(i)}{\mathcal{P}_{{<\kappa}}}$ is
$\mathcal{P}_{{<\kappa}}$-coalgebraic.

  * •

$\mathrm{LP}({i})$ is either $0$ or $\omega$-cofinal or weakly compact or
$\geqslant\kappa+\omega$ (for $\kappa<\infty\infty$).

######  Proof 8.15.

Follows from Proposition 55 by Proposition 11.

We next see that $\mathcal{P}_{{<\kappa}}$-Cauchy is weaker than
$\mathcal{P}_{{<\kappa}}$-coalgebraic.

######  Proposition 57.

For a limit ordinal $i$, the following are equivalent.

  1. (1)

Every $\mathcal{P}_{{<\kappa}}$-Cauchy element of
$\nu^{(i)}{\mathcal{P}_{{<\kappa}}}$ is $\mathcal{P}_{{<\kappa}}$-coalgebraic.

  2. (2)

$i$ is either $0$ or $\omega$-cofinal or weakly compact or
$\geqslant\kappa+\omega$ (for $\kappa<\infty\infty$).

######  Proof 8.16.

For (2)$\Rightarrow$(1), every element of $\nu^{(i)}{\mathcal{P}_{{<\kappa}}}$
is $\mathcal{P}_{{<\kappa}}$-coalgebraic. For the converse: if $i<\kappa$ and
is neither $0$ nor $\omega$-cofinal nor weakly compact, let $a$ be a
$\mathcal{P}_{{<\kappa}}$-ghost at $i$. It is $\mathcal{P}_{{<\kappa}}$-Cauchy
but not $\mathcal{P}$-coalgebraic. For $i=\kappa$, Proposition 23 gives a
$\mathcal{P}_{{<\kappa}}$-Cauchy element of
$\nu^{(\kappa)}{\mathcal{P}_{{<\kappa}}}$ that has $\kappa$ successors and so
is not $\mathcal{P}_{{<\kappa}}$-coalgebraic.

We substantiate our claim in Section 4.2 that the coalgebraic elements need
not form a subsystem of the final chain.

######  Proposition 58.

For a limit ordinal $i$, the following are equivalent.

  1. (1)

The $\mathcal{P}_{{<\kappa}}$-coalgebraic elements form a subsystem of
$\nu^{(i)}{\mathcal{P}_{{<\kappa}}}$.

  2. (2)

$i$ is either $0$ or $\omega$-cofinal or weakly compact or $\geqslant\kappa$
(for $\kappa<\infty\infty$).

######  Proof 8.17.

For (2)$\Leftarrow$(1), if $i\geqslant\kappa$, we apply Proposition 20. In the
other cases, all elements are $\mathcal{P}_{{<\kappa}}$-coalgebraic. For the
converse, if the conclusion is false let $a$ be a
$\mathcal{P}_{{<\kappa}}$-ghost at $i$. It is not $\mathcal{P}$-coalgebraic,
and by Lemma 50 it is a successor of a $\mathcal{P}_{{<\kappa}}$-coalgebraic
element.

##  9\. Related Work

###  9.1. Trees vs tidy trees

Our formulation of the Aronszajn and Kurepa properties used the notion of
_tidy_ tree. This suited our purposes, but to avoid confusion it must be
compared with the following more general notion that commonly appears in the
set-theoretic literature. Let $I$ be a well-ordered set. An _$I$ -tree_ is an
inverse $I$-chain where every level is inhabited. If $I$ has a least element,
then clearly every tidy $I$-tree is an $I$-tree; but there is also a kind of
converse, as follows. (Cf. [Jec03][Lemma 9.13].)

######  Proposition 59.

Let $\lambda$ be a regular infinite cardinal. For any $\lambda$-tree $D$ with
all levels $<\\!\\!\lambda$-sized, there is a tidy $\lambda$-tree $E$ with all
levels $<\\!\\!\lambda$-sized and a bijection from the full branches of $E$ to
those of $D$.

######  Proof 9.1.

We first construct a channel through $D$, with all levels inhabited, that
contains all the full branches. For each $i<\lambda$, let $C_{i}$ be the set
of all $x\in D_{i}$ that have a $k$-development for all $k<\lambda$ such that
$k\geqslant i$. To see that $C$ is a channel, let $j\leqslant i<\lambda$ and
$x\in C_{j}$. For each $k<\lambda$ such that $k\geqslant i$, let $R(k)$ be the
set of $i$-developments of $x$ that has an $k$-development in $C$. Since
$C_{i}$ is $<\\!\\!\lambda$-sized the subset $\bigcap_{i\leqslant
k<\lambda}R(k)$ has an element, which is an $i$-development of $x$ in $C_{i}$.
We likewise prove for all $i<\lambda$ that $C_{i}$ is inhabited. Evidently
every full branch of $D$ is a full branch of $C$.

Next we form the inverse chain $E$, whose $i$th level, for $i<\lambda$, is
$\lim_{j<i}D_{j}$, and whose connecting maps are given by restriction. Let
$\alpha\colon D\to E$ be the cofinal embedding with index map $i\mapsto i+1$
and $i$-th level map sending $x\in D_{i}$ to
$(D_{{i}\geqslant{j}}x)_{j\leqslant i}\in E_{i+1}$. The $\alpha$-image of $C$
is a tidy tree, and by Proposition 34 has the required properties.

######  Corollary 60.

  1. (1)

There is a Kurepa tree (an $\omega_{1}$-tree with all levels countable that
has more than $\aleph_{1}$ full branches) iff there is a tidy one.

  2. (2)

Let $\lambda$ be a regular infinite cardinal. There is a $\lambda$-Aronszajn
tree (a $\lambda$-tree with all levels $<\\!\\!\lambda$-sized that has no full
branch) iff there is a tidy one.

So our use of tidy trees is not a significant change from the usual
formulation.

###  9.2. Saturation

In [ALM+15], an account is given of the final chain of $\mathcal{P}$ at
countable ordinals. Elements of the final chain are observed to be
_saturated_. At limit ordinals, this property may be expressed as follows.

######  Proposition 61.

Let $i$ be a $\kappa$-extensible (e.g. countable) limit. For any
$a\in\nu^{(i)}{\mathcal{P}}$ and pointed system $x$, if for all $j<i$, $a$ has
a $\rightsquigarrow_{i}$-successor $y$ such that $y\sim_{j}x$, then $a$ has a
$\rightsquigarrow_{i}$-successor $y$ such that $y\sim_{i}x$.

######  Proof 9.2.

By Theorem 49, $a=p_{i}{a}$, and transitions to $p_{i}{x}$ by Proposition 18
since $\mathsf{pred}({i})=i$. Lastly, $p_{i}{x}\sim_{i}x$ by Proposition
51(1).

It is not known whether this property holds in the case $i=\omega_{1}$. We
conjecture that it does not, even in the case where
$a\in\nu^{(\omega_{1})}{\mathcal{P}_{\mathsf{c}}}$ and $x$ is countably
branching.

###  9.3. Cauchy completeness

To enable comparison with [FH89, LR96], let us formulate Proposition 57 in
terms of Cauchy sequences.

  * •

An $i$-sequence of pointed systems $(x_{j})_{j<i}$ is _Cauchy_ when for all
$j\leqslant k<i$ we have $x_{j}\sim_{j}x_{k}$.

  * •

A _limit_ for a Cauchy $i$-sequence $(x_{j})_{j<i}$ is a pointed system $y$
such that for all $j<i$ we have $x_{j}\sim_{i}y$.

We then have the following.

######  Proposition 62.

For an ordinal $i$, the following are equivalent.

  1. (1)

Every Cauchy $i$-sequence of $<\\!\\!\kappa$-branching pointed systems has a
$<\\!\\!\kappa$-branching limit.

  2. (2)

$i$ is either a successor or $0$ or $\omega$-cofinal or weakly compact or
$\geqslant\kappa+\omega$ (for $\kappa<\infty\infty$).

######  Proof 9.3.

The successor case is evident. For the limit case, (1) corresponds to
Proposition 57(1). To see this, note that a Cauchy sequence $(x_{j})_{j<i}$
gives a $\mathcal{P}_{{<\kappa}}$-Cauchy element
$a=(p_{j}{x})_{j<i}\in\nu^{(i)}{\mathcal{P}_{{<\kappa}}}$, and every
$\mathcal{P}_{{<\kappa}}$-Cauchy element arises in this way. Moreover, $y$ is
a limit for $(x_{j})_{j<i}$ iff $a=p_{i}{y}$, so $(x_{j})_{j<i}$ has a limit
iff $a$ is $\mathcal{P}_{{<\kappa}}$-coalgebraic.

###  9.4. Comparison

As stated, the work of [FH89] provides the basis of the method we have used to
obtain ghosts. Because that paper is concerned with models of set theories, it
treats primarily the full powerset functor. It studies systems that resemble
the final chain system in satisfying Proposition 18, but differ from it by
including only coalgebraic elements. As we have seen—Proposition 58—these do
not form a subsystem of the final chain, so the difference is considerable.

The work of [LR96] treats not only systems of coalgebraic elements but also
systems of Cauchy elements (and the latter do form a subsystem of the final
chain), specifically for the full powerset functor. A more elaborate proof of
Cauchy incompleteness is given in order to obtain additional negative results.
Relating that work to the present paper is a matter for future research.

##  10\. Conclusions

We have investigated several properties that the final chain of
$\mathcal{P}_{{<\kappa}}$, viewed as a transition system, enjoys at countable
ordinals. In particular, the _strong extensionality_ property: bisimilar
elements are equal. We have seen that these properties do not hold at
$\omega_{1}$, because of an element distinct from $0_{\omega_{1}}$ that has no
successor—a “ghost”. Using the same method, we have precisely identified those
ordinals at which each of these properties does hold.

## References

  * [Abr05] S. Abramsky.  A Cook’s tour of the finitary non-well-founded sets.  In Sergei N. Artëmov, Howard Barringer, Artur S. d’Avila Garcez, Luís C. Lamb, and John Woods, editors, We Will Show Them! Essays in Honour of Dov Gabbay, Volume One, pages 1–18. College Publications, 2005.
  * [Adá74] J. Adámek.  Free algebras and automata realizations in the language of categories.  Comment. Math. Univ. Carolinae, 15(3):589–609, 1974.
  * [AILS12] L. Aceto, A. Ingolfsdottir, P. B. Levy, and J. Sack.  Characteristic formulae: A general approach.  Mathematical Structures in Computer Science, 22(2):125–173, 2012\.  special issue devoted to papers from SOS 2009.
  * [AK95] J. Adamek and V. Koubek.  On the greatest fixed point of a set functor.  TCS: Theoretical Computer Science, 150, 1995.
  * [ALM+15] J. Adámek, P. B. Levy, S. Milius, L. S. Moss, and L. Sousa.  On final coalgebras of power-set functors and saturated trees - to George Janelidze on the occasion of his sixtieth birthday.  Applied Categorical Structures, 23(4):609–641, 2015.
  * [AP15] J. Adámek and T. Palm.  How many steps does a terminal coalgebra need?  Talk given at Domains XII, Cork, Ireland, 2015.
  * [AT11] J. Adámek and V. Trnková.  Initial algebras and terminal coalgebras in many-sorted sets.  Mathematical Structures in Computer Science, 21(2):481–509, 2011\.
  * [Bar93] M. Barr.  Terminal coalgebras in well-founded set theory.  Theoretical Computer Science, 114(2):299–315, 21 June 1993.
  * [BBM14] A. Bizjak, L. Birkedal, and M. Miculan.  A model of countable nondeterminism in guarded type theory.  In Gilles Dowek, editor, Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8560 of Lecture Notes in Computer Science, pages 108–123. Springer, 2014.
  * [Ber] G. Bergman.  Some empty inverse limits.  Manuscript available at http://math. berkeley. edu/~gbergman/papers/unpub/emptylim. pdf.
  * [BM96] J. Barwise and L. S. Moss.  Vicious Circles.  CSLI, 1996.
  * [BMSS12] L. Birkedal, R. E. Møgelberg, J. Schwinghammer, and K. Støvring.  First steps in synthetic guarded domain theory: step-indexing in the topos of trees.  Logical Methods in Computer Science, 8(4), 2012.
  * [CUV09] V. Capretta, T. Uustalu, and V. Vene.  Corecursive algebras: A study of general structured corecursion.  In M. Oliveira and J. Woodcock, editors, SBMF, volume 5902 of LNCS, pages 84–100. Springer, 2009.
  * [FH89] M. Forti and F. Honsell.  Models of self-descriptive set theories.  In Partial Differential Equations and the Calculus of Variations: Essays in Honor of Ennio De Giorgi, pages 473–518. Birkhäuser Boston, 1989.
  * [HS54] G. Higman and A. H. Stone.  On inverse systems with trivial limits.  J. London Math. Soc., 29:233–236, 1954.
  * [Jec03] T. Jech.  Set Theory, the Third Millennium Edition, Revised and Expanded.  Springer, 2003.
  * [KKV04] C. Kupke, A. Kurz, and Y. Venema.  Stone coalgebras.  Theor. Comput. Sci, 327(1-2):109–134, 2004.
  * [Kur36] G. Kurepa.  Ensembles linéaires et une classe de tableaux ramifiés (tableaux ramifiés de M. Aronszajn).  Publ. Math. Univ. Belgrade, 6:129–160, 1936.  http://elib.mi.sanu.ac.rs/files/journals/publ/6/14.pdf.
  * [LR96] R. S. Lazic and A. W. Roscoe.  On transition systems and non-well-founded sets.  In Papers on General Topology and Applications: 11th Summer Conference at the University of Southern Maine, 1995 Annals of the New York Academy of Sciences, volume 806, pages 238–264, 1996.
  * [Mal76] R. J. Malitz.  Set theory in which the axiom of foundations fails.  PhD thesis, UCLA, 1976.  (unpublished).
  * [Mil89] R. Milner.  Communication and Concurrency.  Prentice-Hall, 1989.
  * [Mit72] W. Mitchell.  Aronszajn trees and the independence of the transfer property.  Annals of Mathematical Logic, 5(1):21–46, 1972.
  * [Sch10] Daniel Schwencke.  Coequational logic for accessible functors.  Information and Computation, 208(12):1469–1489, 2010.
  * [Sil71] Jack Silver.  The independence of Kurepa’s conjecture and two-cardinal conjectures in model theory.  In D. S. Scott, editor, Axiomatic Set Theory, volume 13 of Proceedings of Symposia in Pure Mathematics, pages 383–390. AMS, 1971.
  * [Spe49] E. Specker.  Sur un problème de Sikorski.  Colloquium Mathematicae, 2(1):9–12, 1949.
  * [TAKR75] V. Trnková, J. Adámek, V. Koubek, and J. Reiterman.  Free algebras, input processes and free monads.  Commentationes Mathematicae Universitatis Carolinae, 016(2):339–351, 1975.
  * [vG87] R. J. van Glabbeek.  Bounded nondeterminism and the approximation induction principle in process algebra.  In F. J. Brandenburg, G. Vidal-Naquet, and M. Wirsing, editors, Proceedings of the 4th Annual Symposium on Theoretical Aspects of Computer Science, STACS’87 (Passau, Germany, February 19-21, 1987), volume 247 of LNCS, pages 336–347. Springer-Verlag, Berlin-Heidelberg-New York-London-Paris-Tokyo-Hong Kong, 1987.
  * [Wor05] J. Worrell.  On the final sequence of a finitary set functor.  Theoretical Computer Science, 338(1–3):184–199, June 2005.