1–LABEL:LastPageJan. 16, 2017Mar. 20, 2018

# Model Theory and Proof Theory of
Coalgebraic Predicate Logic

Tadeusz Litak  Friedrich-Alexander-Universität Erlangen-Nürnberg
<EMAIL_ADDRESS>,  Dirk Pattinson  Australian National University
<EMAIL_ADDRESS>,  Katsuhiko Sano  Graduate School of Letters,
Hokkaido University<EMAIL_ADDRESS>and  Lutz Schröder  Friedrich-
Alexander-Universität Erlangen-Nürnberg<EMAIL_ADDRESS>
###### Abstract.

We propose a generalization of first-order logic originating in a neglected
work by C.C. Chang: a natural and generic correspondence language for any
types of structures which can be recast as Set-coalgebras. We discuss
axiomatization and completeness results for several natural classes of such
logics. Moreover, we show that an entirely general completeness result is not
possible. We study the expressive power of our language, both in comparison
with coalgebraic hybrid logics and with existing first-order proposals for
special classes of Set-coalgebras (apart from relational structures, also
neighbourhood frames and topological spaces). Basic model-theoretic
constructions and results, in particular ultraproducts, obtain for the two
classes that allow completeness—and in some cases beyond that. Finally, we
discuss a basic sequent system, for which we establish a syntactic cut-
elimination result.

###### Key words and phrases:

coalgebraic predicate logic, coalgebraic model theory, coalgebraic proof
theory

_Dedicated to Jiří Adámek on the occasion of his seventieth birthday_

##  1\. Introduction

Modal logics are traditionally a core formalism in computer science.
Classically, their semantics is relational, i.e. a model typically comes with
a set of states and one or several binary accessibility relations on the state
set. However, non-relational semantics of various descriptions have come to
play an increasing role, e.g. in concurrency, reasoning about knowledge and
agency, description logics and ontologies. Models may involve such diverse
features as concurrent games, as in coalition logic and alternating-time
temporal logic [AlurEA02, Pauly02]; probabilities [LarsenSkou91,
FaginHalpern94, HeifetzMongin01]; integer weights as in the multigraph
semantics of graded modal logic [DAgostinoVisser02]; neighbourhoods
[Chellas80]; and selection functions or preference orderings as in the
different variants of conditional logic [Lewis73, Chellas80]. _Coalgebraic
modal logic_ serves as a unifying framework for such non-relational modal
logics [CirsteaEA11].

Relational modal logic can be seen as a subset of first-order logic,
specifically as the bisimulation-invariant fragment as shown by van Benthem
for arbitrary models and later shown for finite models by Rosen
[BenthemThesis, Rosen97]. An analogous first-order counterpart for coalgebraic
modal logic has been introduced in previous work by two of the authors
[SchroderP10fossacs]. The language described there does support a van
Benthem/Rosen-style theorem. It is quite expressive but has a fairly complex
syntax with three sorts, modelling states, sets of states, and composite
states, respectively, and is equipped with a carefully tuned Henkin-style
semantics. In the current work we develop _coalgebraic predicate logic (CPL)_
, a first-order correspondence language for coalgebraic predicate logic that
is slightly less expressive than the language proposed originally but has a
simpler syntax and a straightforward semantics that does not require any
design decisions. The naturality of CPL is further corroborated by the fact
that CPL is expressively equivalent to hybrid logic (see the overview article
by Areces and ten Cate [ArecesTenCate07]) with satisfaction operators and
universal quantification (equivalently with the downarrow binder $\downarrow$
and a global modality). Thus, CPL not only serves as a correspondence language
for coalgebraic modal logic but also arises by adding a standard set of
desirable expressive features widely used in specification and knowledge
representation.

Our proposal originates in a largely forgotten paper by C.C. Chang [Chang73]
who introduces a first-order logic of _Scott-Montague neighbourhood frames_ ,
which in coalgebraic terms can be seen as coalgebras for the doubly
contravariant powerset functor. Chang’s original motivation was to simplify
model theory for what Montague called _pragmatics_ and to replace Montague’s
many-sorted setting by a single-sorted one. Chang’s contributions were
primarily of a model-theoretic nature. He provided adaptations of the notions
of (elementary) submodel/extension, elementary chain of models and
ultraproduct and established a Tarski-Vaught theorem as well as downward and
upward Löwenheim-Skolem theorems. Our syntax is a notational variant of
Chang’s syntax; semantically, we generalize from neighbourhood frames to
coalgebras for an underlying set functor, thus capturing the full range of
non-relational modalities indicated above.

Our semantics naturally extends coalgebraic modal logic in that it is
parametrized over an interpretation of the modal operators as predicate
liftings [Pattinson03, Schroder08]. It can thus be instantiated with
modalities such as, for instance, the standard relational $\Diamond$; with
neighbourhood-based modalities as in Chang’s original setup; with
probabilistic operators $L_{p}$ ‘with probability at least $p$’; or with a
binary conditional $\Rightarrow$ ‘if – then normally’. We incorporate a unary
$\heartsuit$ into a first-order language by allowing formulas of the form

$t\heartsuit\lceil z:\phi\rceil$

where $t$ is a term, $\phi$ is a formula of coalgebraic predicate logic, $z$
is a (comprehension) variable. Such a formula stipulates that $t$ satisfies
$\heartsuit$, applied to the set of all $z$ that satisfy $\phi$. For example,
in standard modal logic over relational semantics, the formula
$x\Diamond\lceil z:z=y\rceil$ says that $x$ has $y$ as a (relational)
successor. In the probabilistic setting, the formula $xL_{p}\lceil y:y\neq
x\rceil$ states that the probability of moving from $x$ to a different state
is at least $p$.

As indicated above, CPL supports a van Benthem / Rosen type result stating
essentially that coalgebraic modal logic is the bisimulation-invariant
fragment of CPL both over the class of all structures and over the class of
finite structures; this result is proved in a companion paper
[SchroderPL15:jlc], which also establishes a Gaifman-type theorem for CPL. In
the current paper, we establish the following results on CPL:

  * •

We give a Hilbert-style axiomatization that we prove strongly complete for two
particular classes of coalgebraic structures, viz. structures that are either
neighbourhood-like or _bounded_ , where the latter type includes the
relational and the graded case as well as positive Presburger modalities. As
usual in model theory, strong completeness can be supplemented with a suitable
variant of the Omitting Types Theorem.

  * •

While boundedness is a rather strong condition on structures, we show that the
condition is fairly essential for completeness in the sense that within a much
broader type of _$\omega$ -bounded_ structures, the bounded structures are the
only ones that allow for strong completeness.

  * •

As indicated above, we establish the equivalence of CPL and several natural
variants of coalgebraic hybrid logic.

  * •

We prove some basic model-theoretic results. Specifically, we show that, under
the same (alternative) assumptions as for our completeness result,
ultraproducts exist and a downward Löwenheim-Skolem theorem holds; in fact, it
turns our that the latter is applicable more broadly, requiring as it does
only $\omega$-boundedness in place of boundedness in its corresponding
variant.

  * •

We give sequent systems complementing the above-mentioned Hilbert system, and
establish completeness, under the same (alternative) assumptions as for the
Hilbert system, and more interestingly, syntactic cut-elimination for the
“neighbourhood-like” case.

The material is organized as follows. In §2 we introduce the syntax and
semantics of CPL and give a number of intuitive examples. In § 3 we discuss
the Hilbert-style axiomatization and associated completeness results. We
proceed to clarify the relationship between CPL and several variants of
coalgebraic modal and hybrid logic in § 4. In § 5 we take first steps in the
model theory of CPL, and § 6 deals with proof theory. While our presentation
of the basic definitions in coalgebraic logic is self-contained in principle,
we do import some of its basic results. Additional information is found in
work on coalgebraic finite models [Schroder06], one-step rules
[SchroderPattinson09a, SchroderPattinson10b], and modularization of
coalgebraic logics [SchroderPattinson11].

###  1.1. Related Work.

As already discussed, the syntax of our logic follows Chang’s first-order
logic of neighbourhood frames [Chang73]. An alternative, two-sorted language
for neighbourhood frames has been proposed by Hansen et al. [HansenKP09lmcs].
Over neighbourhood frames, the language studied in the present work is a
fragment of the two-sorted one; we give details in § 2.

First-order formalisms have also been considered for topological spaces, which
are particular instances of neighbourhood frames when defined in terms of
local neighbourhood bases. In particular, Sgro [Sgro80ams] studies interior
operator logic in topology with interior modalities for finite topological
powers of the space. This language is the weakest one in the hierarchy of
topological languages considered in an early overview by Ziegler [Ziegler85].
Makowsky and Marcja [MakowskyM77:mlq] prove a range of completeness theorems
for topological logics, including a completeness result for the Chang language
itself, i.e., a special version of our Theorem 9. See also ten Cate et al.
[CateGS09apal] for a more contemporary reference. Despite the fact that CPL
combines quantifiers and modalities, it should not be confused with what is
usually termed quantified or first-order modal logic; see Remark 1.

As mentioned above, our logic is less expressive but more naturally defined
than the correspondence language used in the first van Benthen/Rosen type
characterization result for coalgebraic modal logic [SchroderP10fossacs].
Axiomatizations and model-theoretic results as we develop here are not
currently available for the more expressive language of [SchroderP10fossacs].

A different generic first-order logic largely concerned with the Kleisli
category of a monad rather than with coalgebras for a functor is introduced
and studied in [Jacobs10predicate]. Of all the languages discussed above, this
one seems least related to the present one; indeed, the study of connections
with languages like that of the original, three-sorted variant
[SchroderP10fossacs] is mentioned by Jacobs [Jacobs10predicate] as a subject
for future research.

This paper is based on results first announced in earlier conference papers
[LitakPSS12:icalp, LitakSP13:tbillc]. Compared to the conference versions, it
features full proofs and additional examples. Some results previously only
mentioned such as the Omitting Types Theorem (Theorem 18) are explicitly
stated and proved here for the first time. We also corrected a number of
errors and typos. Most notably, as reconstructing the proof of cut-elimination
for the $\mathsf{G3c}$-style system proposed in [LitakSP13:tbillc] proved
problematic, we replaced it with a $\mathsf{G1c}$-style system in this
version, with a different treatment of equality and provided all the proof
details.

##  2\. Syntax, Semantics and Examples

We proceed to give a formal definition of _coalgebraic predicate logic_ (CPL).
We fix a set $\Sigma$ of predicate symbols and a modal similarity type
$\mathrm{\Lambda}$, i.e. a set of modal operators. Modal operators
$\heartsuit\in\mathrm{\Lambda}$ and predicate symbols $P\in\Sigma$ both come
with fixed _arities_ $\mathsf{ar}{\heartsuit},\mathsf{ar}{P}\in{\mathbb{N}}$.
The set $\mathrm{CPL}(\mathrm{\Lambda},\Sigma)$ of CPL _formulas_ over
$\mathrm{\Lambda}$ and $\Sigma$ is given by the grammar

$\mathrm{CPL}(\mathrm{\Lambda},\Sigma)\owns\phi,\psi\;::=\;y_{1}=y_{2}\mid
P(\vec{x})\mid\bot\mid\phi\to\psi\mid\forall x.\phi\mid x\heartsuit\lceil
y_{1}:\phi_{1}\rceil\dots\lceil y_{n}:\phi_{n}\rceil$

where $\heartsuit\in\mathrm{\Lambda}$ is an $n$-ary modal operator and
$P\in\Sigma$ a $k$-ary predicate symbol, $x,y_{i}$ are variables from a fixed
set $\mathsf{iVar}$ we keep implicit. We just write
$\mathrm{CPL}(\mathrm{\Lambda})$ for
$\mathrm{CPL}(\mathrm{\Lambda},\emptyset)$ and sometimes we omit
$\mathrm{\Lambda}$ and $\Sigma$ altogether. Booleans and the existential
quantifier are defined in the standard way. We do not include function
symbols, which can be added in a standard way [Chang73]. We adopt the usual
convention that the scope of a quantifier extends as far to the right as
possible. In the $\lceil y_{i}:\phi_{i}\rceil$ component, $y_{i}$ is used as a
comprehension variable, i.e., $\lceil y_{i}:\phi_{i}\rceil$ denotes a subset
of the carrier of the model, to which modal operators can be applied in the
usual way. In $x\heartsuit\lceil y_{1}:\phi_{1}\rceil\dots\lceil
y_{n}:\phi_{n}\rceil$, $x$ is free and $y_{i}$ is bound in $\phi_{i}$,
otherwise the notions of freeness and boundedness are standard. We write
$\mathsf{FV}(\phi)$ for the set of free variables of a formula $\phi$. A
variable is _fresh_ for a formula if it does not have free occurrences in it;
to save space, we will also sometimes say that $x\in\mathsf{iVar}$ is fresh
for $y\in\mathsf{iVar}$ whenever it is distinct from it. A _sentence_ , as
usual, is a formula without free variables.

As usual, some care is needed when defining substitution to avoid, on the one
hand, capture of newly substituted variables by quantifiers and on the other
hand, substituting for a bound variable. We take as our model the discussion
in Enderton’s monograph [Enderton72, p. 112–113]. As we now have two ways in
which a variable can become bound and the binder $\heartsuit$ involves also a
variable/term in a non-binding way, it is desirable to spell out details. We
thus define—prima facie not necessarily capture-avoiding—substitution
$\alpha[t/x]$ with $t,x\in\mathsf{iVar}$ (had we allowed for function symbols,
$t$ could be any term) as replacing $x$ with $t$ in atomic formulas and
commuting with implication (and of course other Boolean connectives, were they
taken as primitives). For binders, the clauses are:

$\displaystyle\begin{aligned} (\forall x.\phi)[t/y]&=\begin{cases}\forall
x.\phi&x=y\\\ \forall x.\phi[t/y]&\text{ otherwise, }\end{cases}\\\
(x\heartsuit\lceil z_{1}:\phi_{1}\rceil\dots\lceil
z_{n}:\phi_{n}\rceil)[t/y]&=u\heartsuit\lceil
z_{1}:\phi^{\prime}_{1}\rceil\dots\lceil
z_{n}:\phi^{\prime}_{n}\rceil\end{aligned}$ $\displaystyle\text{ where
}\phi^{\prime}_{i}=\begin{cases}\phi_{i}&y=z_{i}\\\
\phi^{\prime}_{i}[t/y]&\text{ otherwise, }\end{cases}\text{ and
}u=\begin{cases}t&x=y\\\ x&\text{otherwise.}\end{cases}$

This of course cannot work without restrictions, so we follow Enderton in
defining the notion of _substitutability_ of $t$ for $x$ in a term. There are
no restrictions on substitutability in atomic formulas, and for implications,
it is defined as substitutability in the two argument formulas. Finally, $t$
is substitutable for $x$ in $z\heartsuit\lceil y_{1}:\phi_{1}\rceil\dots\lceil
y_{n}:\phi_{n}\rceil$ whenever for every $i$, $t$ is either

  * •

fresh for $\lceil y_{i}:\phi_{i}\rceil$ (this includes the case $t=y_{i}$) or

  * •

different from $y_{i}$ and substitutable for $x$ in $\phi_{i}$.

Note that in the first alternative, substituting $t$ for $x$ has no effect on
$\lceil y_{i}:\phi_{i}\rceil$. In a language with more general terms, the
second alternative would require that $y_{i}$ is fresh for $t$ rather than
different from $t$. Substitutability of $t$ for $x$ in $\forall
y_{1}.\phi_{1}$ is defined similarly (and standardly).

We depart from Enderton’s conventions by restricting, from now on, the usage
of the $\alpha[t/x]$ notation to the case where $t$ is substitutable for $x$
in $\alpha$ (as usual, when this is not the case the substitution can still be
applied after suitably renaming bound variables in $\alpha$). For example, the
axiom scheme $\forall\vec{y}.(\forall x.\phi\to\phi[z/x])$ denoted as En2 in
Table 1 has as its valid instances only those formulas where $z$ is
substitutable for $x$.

The semantics of CPL is parametrized over the choice of an endofunctor $T$ on
$\mathsf{Set}$ that determines the underlying system type: models are based on
_$T$ -coalgebras_, i.e. pairs $(C,\gamma:C\to TC)$ consisting of a carrier set
$C$ of worlds or _states_ and a _transition function_ $\gamma$. We think of
the elements of $TC$ as being _composite states_ ; e.g. if $T$ is the identity
functor then a composite state is just a state, and if $T$ is powerset, then a
composite state is a set of states. Thus, the transition function assigns to
each state $c$ a composite state $\gamma(c)$ that represents the successors of
$c$ and that we correspondingly refer to as the _composite successor_ of $c$.
E.g. in case $T$ is powerset, a $T$-coalgebra assigns to each state a set of
successor states, and hence is essentially a Kripke frame.

To interpret the modal operators, we extend $T$ to a _$\Lambda$ -structure_,
i.e. we associate to every $n$-ary modal operator $\heartsuit\in\Lambda$ a
set-indexed family of mappings

$\llbracket\heartsuit\rrbracket_{C}:(\mathcal{Q}C)^{n}\to\mathcal{Q}TC$

where $\mathcal{Q}$ denotes the contravariant powerset functor, subject to
_naturality_ , i.e.

$(Tf)^{-1}\circ\llbracket\heartsuit\rrbracket_{C}=\llbracket\heartsuit\rrbracket_{D}\circ(f^{-1})^{n}$

for every set-theoretic function $f:C\to D$. In categorical parlance, this
means that $\llbracket\heartsuit\rrbracket$ is a natural transformation
$\mathcal{Q}^{n}\to\mathcal{Q}\circ T^{op}$; we recall that the contravariant
powerset functor $\mathcal{Q}$ maps a set $X$ to the powerset of $X$ and a map
$X\to Y$ to the preimage map $\mathcal{Q}f:\mathcal{Q}Y\to\mathcal{Q}X$, i.e.
$\mathcal{Q}f(A)=f^{-1}[A]$ for $A\subseteq Y$. Each such
$\llbracket\heartsuit\rrbracket$ is called a _predicate lifting_ [Pattinson03,
Schroder08]. Formally speaking, we should define a $\Lambda$-structure as a
pair $(T,(\llbracket\heartsuit\rrbracket)_{\heartsuit\in\Lambda})$, but to
avoid cumbersome notation and terminology, we will speak about a
$\Lambda$-structure _based_ on $T$ (or a $\Lambda$-structure _over_ $T$) and
suppress the second component of the pair whenever
$(\llbracket\heartsuit\rrbracket)_{\heartsuit\in\Lambda}$ is clear from the
context.

A triple $\mathfrak{M}=(C,\gamma,I)$ consisting of a coalgebra $\gamma:C\to
TC$ and a predicate interpretation
$I:\Sigma\to\bigcup\limits_{n\in\omega}\mathcal{Q}(C^{n})$ respecting arities
of symbols will be called a _(coalgebraic) model_. In other words, a
coalgebraic model consists simply of a $\mathsf{Set}$-coalgebra and an
ordinary first-order model whose universe coincides with the carrier of the
coalgebra. Given a model $\mathfrak{M}=(C,\gamma,I)$ and a valuation
$v:\mathsf{iVar}\to C$, we define satisfaction $\mathfrak{M},v\models\phi$ in
the standard way for first-order connectives and for $\heartsuit$ by the
clause

$\mathfrak{M},v\models x\heartsuit\lceil y_{1}:\phi_{1}\rceil\dots\lceil
y_{n}:\phi_{n}\rceil\iff\gamma(v(x))\in\llbracket\heartsuit\rrbracket_{C}(\llbracket\phi_{1}\rrbracket^{y_{1}}_{\mathfrak{M}},\dots,\llbracket\phi_{n}\rrbracket^{y_{n}}_{\mathfrak{M}})$

where

$\llbracket\phi\rrbracket^{y}_{\mathfrak{M}}=\\{c\in
C\mid\mathfrak{M},v[c/y]\models\phi\\}$ (1)

and $v[c/y]$ is $v$ modified by mapping $y$ to $c$.

######  Remark 1.

_Quantified_ or _first-order modal logic_ in the sense used widely in the
literature (see, e.g., [Garson01]) combines quantification and modalities in a
two-sorted and, effectively, two-dimensional semantics: One has an underlying
set of worlds as well as an underlying set of individuals, with modalities
interpreted as moving between worlds and quantification interpreted as ranging
over individuals in the current world. We emphasize that although CPL also
combines modalities and quantifiers, it is not a quantified modal logic in
this sense: it is interpreted over a single set of individuals, and both the
modalities and the quantifiers move within this set. In particular, the
instance of CPL induced by the standard modalities equipped with their usual
predicate liftings is standard first-order logic rather than a quantified
modal logic, as we discuss below in some detail.

In a companion paper on the van Benthem-Rosen theorem for CPL
[SchroderPL15:jlc] and in conference papers the present work is based upon
[LitakPSS12:icalp, LitakSP13:tbillc], we have focused on Chang’s original
motivation for this language [Chang73]. Namely, Chang saw his setup as a
modification of Montague’s account of _pragmatics_ , tailored to reasoning
about social situations and relationships between an individual and sets of
individuals. We have proposed a series of examples kept in the same spirit,
utilizing Facebook, Twitter and social networks. In the present paper, we
offer examples based on, so to say, networking of a more low-level character,
especially _delay-_ or _disruption-tolerant_ networking (_DTN_). We do not
claim to be very accurate with respect to specifications of concrete
protocols; our examples are of purely inspirational and illustrative
character. It is worth mentioning, though, that such routing and forwarding
protocols can be backed by social insights [HuiCY08], so in a sense we are
still following the spirit of our original examples.111In particular, Hui et
al. [HuiCY08] gave us the idea of using _subcommunities_ in this context.

### Neighbourhood Frames.

Scott/Montague _neighbourhood semantics_ is captured coalgebraically using
$\Lambda=\\{\Box\\}$ and putting $TC=\mathcal{Q}\mathcal{Q}C$ (the doubly
contravariant powerset functor), which extends to a $\Lambda$-structure by

$\llbracket\Box\rrbracket_{C}(A)=\\{\sigma\in TC\mid A\in\sigma\\}.$

A $T$-coalgebra then associates to each state a set of sets of states, i.e. a
system of neighbourhoods; thus, $T$-coalgebras are just neighbourhood frames.
In the presence of a binary relation $S(x,y)$ that we read as ‘node/router $y$
is in the forwarding table of $x$’ and interpreting $\Box$ as ‘is a recognized
subcommunity’, the formula

$\exists y.x\Box\lceil z:S(z,y)\rceil$

reads as ‘there exists a certain $y$ such that amongst the subcommunities
recognized by $x$, there is one formed exactly by those having $y$ in its
forwarding table’.

The instance of CPL that we obtain in this way is, up to quite minor syntactic
differences, Chang’s original language [Chang73]. As mentioned in § 1, it
embeds as a fragment into Hansen et al.’s two-sorted correspondence language
[HansenKP09lmcs]. We refrain from giving full syntactic details; roughly, the
setup is as follows. The two-sorted language has sorts $s$ for states and $n$
for neighbourhoods, and features binary infix predicates $\mathsf{N}$ and
$\mathsf{E}$ respectively modelling the neighbourhood relation between states
and neighbourhoods, and the inverse elementhood relation $\owns$ between
neighbourhoods and states. Then our $x\heartsuit\lceil y:\phi(y)\rceil$ can be
translated as $\exists u.(x\mathsf{N}u\wedge\forall
y.(u\mathsf{E}y\leftrightarrow\phi(y)))$.

### Relational first-order logic.

Instantiating CPL with the usual modalities of relational modal logic,
specifically the logic $K$, we obtain a notational variant of ordinary FOL
over relational structures, that is, of the usual correspondence language. The
main idea has already been indicated in the introduction: we encode the
successor relation in formulas of the form $x\Diamond\lceil z:y=z\rceil$,
which states that $y$ is a successor of $x$. Formally, we capture the standard
modality and the propositional atoms of the relational modal logic $K$ in the
similarity type

$\Lambda=\\{\Diamond\\}\cup\mathsf{At}$

where $\mathsf{At}$ is a set of propositional atoms; as expected, $\Diamond$
is unary, and $a\in\mathsf{At}$ is nullary. We interpret these operators over
the functor $T$ given on objects by

$TX=\mathcal{P}X\times\mathcal{P}\mathsf{At}$

where $\mathcal{P}$ denotes the covariant powerset functor. That is, a
coalgebra $\gamma:C\to TC$ assigns to each state $c\in C$ a set of successors
as well as a set of propositional atoms valid in $c$. The interpretation is
defined by means of predicate liftings

$\displaystyle{[\\![\Diamond]\\!]}_{X}(A)$
$\displaystyle=\\{(Y,U)\in\mathcal{P}X\times\mathcal{P}\mathsf{At}\mid A\cap
Y\neq\emptyset\\}$ $\displaystyle{[\\![a]\\!]}_{X}$
$\displaystyle=\\{(Y,U)\in\mathcal{P}X\times\mathcal{P}\mathsf{At}\mid a\in
U\\}$

where, corresponding to the arity of the modal operators, the predicate
lifting for $\Diamond$ is unary and the predicate liftings for the
$a\in\mathsf{At}$ are nullary. These predicate liftings capture precisely the
standard semantics of both $\Diamond$ and the propositional atoms. In
particular, the above-mentioned formula $x\Diamond\lceil z:y=z\rceil$ really
does say that $y$ is a successor of $x$. (Notice that in the nullary case, our
syntax instantiates to formulas $x\,a$ saying that $x$ satisfies the
propositional atom $a$).

The standard first-order correspondence language of modal logic has unary
predicates $a$ for the atoms $a\in\mathsf{At}$ and a binary predicate $R$ to
represent the successor relation. We translate
$\mathrm{CPL}(\mathrm{\Lambda})$ as defined above into the standard
correspondence language by just extending the standard translation of modal
logic to CPL, with the modification that the current state is represented by
an explicit variable in CPL so that it is no longer necessary to index the
standard translation with a variable name. That is, our translation
$\mathit{ST}$ is defined in the modal cases (which by our conventions include
the case of propositional atoms) by

$\displaystyle\mathit{ST}(x\Diamond\lceil y:\phi\rceil)$
$\displaystyle=\exists y.\,R(x,y)\land\mathit{ST}(\phi)$
$\displaystyle\mathit{ST}(x\,a)$ $\displaystyle=a(x)$
$\displaystyle(a\in\mathsf{At})$

and by commutation with all other constructs. In the converse direction, we
translate $R(x,y)$ into $x\Diamond\lceil z:z=y\rceil$ and $a(x)$ into $x\,a$.
In summary, _CPL over $\Lambda=\\{\Diamond\\}\cup\mathsf{At}$ with the above
semantics is expressively equivalent to the standard first-order
correspondence language of modal logic_.

### Graded Modal Logic.

We obtain a variant of graded modal logic [Fine72] if we consider the
similarity type $\Lambda=\\{\langle k\rangle\mid k\geq 0\\}$ where $\langle
k\rangle$ reads as ‘more than $k$ successors satisfy …’. We interpret the
ensuing logic over _multigraphs_ [DAgostinoVisser02], which are coalgebras for
the _multiset functor_ $\mathcal{B}$ given on objects by

$\mathcal{B}X=\\{\mu:X\to{\mathbb{N}}\cup\\{\infty\\}\mid f\text{ a map}\\}.$

We see such a map $\mu:X\to{\mathbb{N}}\cup\\{\infty\\}$ as an integer-valued
discrete measure on $X$, i.e. we write $\mu(A)=\sum_{x\in A}\mu(x)$ for
$A\subseteq X$. Then, $\mathcal{B}$ acts on maps $f:X\to Y$ by taking image
measures; i.e. $\mathcal{B}f(\mu)(B)=\mu(f^{-1}[B])$ for $B\subseteq Y$. We
extend $\mathcal{B}$ to a $\mathrm{\Lambda}$-structure by stipulating

$\textstyle\llbracket\langle
k\rangle\rrbracket_{X}(A)=\\{\mu\in\mathcal{B}X\mid\mu(A)>k\\}$

to express that more than $k$ successors (counted with multiplicities) have
property $A$. Note that over Kripke frame, graded operators can be coded into
standard first order logic; the difference with standard first-order logic
arises through the multigraph semantics, for which the requisite expressive
means arise only through the graded operators.

Continuing our line of routing examples, we can, given a
$\mathcal{B}$-coalgebra $\gamma:C\to\mathcal{B}C$, think of
$\gamma(c)(c^{\prime})$ as the number of packets forwarded from $c$ to
$c^{\prime}$ in the past hour. In the presence of a binary relation $S(x,y)$
interpreted as above, the formula

$\neg\exists y.(x\langle k\rangle\lceil z:S(y,z)\rceil)$

then expresses that there is no router $y$ s.t. the total number of packets
sent by $x$ to nodes in $y$’s forwarding table in the past hour exceeds $k$.

### Presburger modal logic and arithmetic.

A more general set of operators than graded modal logic is that of positive
Presburger modal logic [DemriLugiez06], which admits integer linear
inequalities $\sum_{i=1}^{n}a_{i}\cdot\\#(\phi_{i})>k$ among formulas where
$a_{i}\geq 0$ for all $i$. We see such a formula as an application of an
$n$-ary modality $L_{k}(a_{1},\dots,a_{n})$ to formulas
$\phi_{1},\dots,\phi_{n}$, and interpret this modality over the multiset
functor $\mathcal{B}$ as introduced above by the $n$-ary predicate lifting

$\textstyle{[\\![L_{k}(a_{1},\dots,a_{n})]\\!]}_{X}(A_{1},\dots,A_{n})=\\{\mu\in\mathcal{B}X\mid\sum_{i=1}^{n}a_{i}\cdot\mu(A_{i})>k\\}.$

In addition to the binary predicate $S$, let us also introduce unary predicate
$O(x)$ expressing that $x$ is an overloaded node. The formula

$\forall x.((xL_{10{,}000}(1,3)\lceil y:S(x,y)\rceil\lceil y:O(y)\rceil)\to
O(x))$

means that, if the weighted number of packets sent by $x$ to overloaded nodes
combined with packets $x$ sends to all nodes in its forwarding table exceeds
$10{,}000$, then $x$ itself is overloaded.

### Combination of Frame Classes.

Frame classes can be combined: we can take
$T=\mathcal{B}\times\mathcal{Q}\mathcal{Q}$ and combine operators for packet
counting and subcommunity recognition. A formula

$\neg x\Box\lceil y:y\langle 30\rangle\lceil u:u\neq z\rceil\rceil$

expresses then that the collection of those nodes which have forwarded more
than 30 packages to servers different than $z$ in the past hour is not a
subcommunity recognized by $x$.

### Probabilistic Modal Logic.

The _discrete distribution functor_ $\mathcal{D}$ is defined on objects by

$\textstyle\mathcal{D}X=\\{\mu:X\to[0,1]\mid\sum_{x}\mu(x)=1\\},$

and on morphisms by taking image measures exactly as for the multiset functor
$\mathcal{B}$ discussed earlier. Coalgebras for $\mathcal{D}$ thus associate
to every state a probability distribution over successor states; such
structures are known as _Markov chains_ , or _probabilistic transition
systems_ , or _type spaces_. Taking the similarity type $\Lambda=\\{\langle
p\rangle\mid p\in[0,1]\cap{\mathbb{Q}}\\}$, with $\langle p\rangle$ read as
‘with probability more than $p$’ (thus departing from the choice of operators
$L_{p}$ ‘ with probability at least $p$’ that we used in the introduction), we
formally interpret $\langle p\rangle$ using the predicate lifting

$\llbracket\langle
p\rangle\rrbracket_{X}(A)=\\{\mu\in\mathcal{D}X\mid\mu(A)>p\\}$

over $\mathcal{D}$. We thus obtain a form of probabilistic first-order logic
for probabilistic transition systems that extends probabilistic modal logic
[LarsenSkou91, FaginHalpern94, HeifetzMongin01]. Continuing our line of
routing examples, if we interpret the transition probabilities as the
likelihood of a server forwarding any given packet to another, then the
formula

$\forall x,y.(x\langle 1/2\rangle\lceil z:z=y\rceil\to y\langle
1/2\rangle\lceil z:z=x\rceil)$

expresses a partial form of symmetric connectivity: whenever a server $x$
prefers the connection to $y$ in the sense that it will more likely than not
route any given packet through $y$, then the same will hold in the other
direction.

We obtain a version of this logic with finitely many modal operators in
situations where all possible probabilities are contained in some finite set
of rationals (such as when rolling a fair die). We then consider substructures
of the form

$\mathcal{D}_{k}X=\\{\mu\in\mathcal{D}(X)\mid\mu(x)\in\\{i/k\mid
i=0,\dots,k\\}\\},$

restricting the modal operators to come from $\Lambda_{k}=\\{\langle
n/k\rangle\mid n=0,\dots,k\\}$.

### Non-Monotonic Conditionals.

An example of a binary modality is provided by (conditional) implication $>$.
Such operators are interpreted over a variety of semantic structures; one of
these involves _selection function frames_ , which in our terminology can be
defined as coalgebras for the _selection function functor_ $\mathcal{S}$. The
latter acts on objects by

$\mathcal{S}X=\\{f:\mathcal{Q}X\to\mathcal{P}X\\}$

and, correspondingly, on maps $f:X\to Y$ by
$\mathcal{S}f=\mathcal{Q}f\to\mathcal{P}f:\mathcal{S}X\to\mathcal{S}Y$, i.e.
$\mathcal{S}f(g)(A)=f[g(f^{-1}[A])]$ for $A\subseteq X$ (recall that
$\mathcal{Q}$ denotes the contravariant powerset functor). We think of
$f_{x}\in\mathcal{S}X$ as selecting the set $f_{x}(A)$ of worlds which $x$
sees as ‘most typical’ given a condition $A\subseteq X$. Over this functor, we
interpret the conditional $>$ by the predicate lifting

$\llbracket>\rrbracket_{X}(A,B)=\\{f\in\mathcal{S}X\mid f(A)\cap
B\neq\emptyset\\}.$

The formula $\phi>\psi$ expresses that $\psi$ is typically possible under
condition $\phi$. This presentation of conditional logic is dual to the
standard presentation [Chellas80] in terms of a binary operator $\Rightarrow$
‘if – then normally’, related to $>$ by $a>b\equiv\neg(a\Rightarrow\neg b)$.
For our purposes, $>$ has the technical advantage of being bounded in the
second argument in a sense that we will introduce in § 3.

We continue to interpret our examples in the context of routing: Given an
$\mathcal{S}$-coalgebra (i.e. selection function frame)
$\gamma:C\to\mathcal{S}C$, we may read $\gamma(c)(A)$ as the set of those
servers through which server $c$ will normally route an incoming packet if $c$
is currently active in the subcommunity $A\subseteq C$. Then a formula of the
form

$\forall x,u.(\phi(u)\to x>\lceil y:\phi(y)\rceil\lceil z:z=u\rceil)$

says that if $x$ is currently active in a subcommunity delineated by the
formula $\phi(y)$ and $u$ belongs to that subcommunity, then $u$ is normally a
possible target for packets forwarded by $x$.

We have not mentioned propositional atoms other than in the example on
relational first-order logic. We introduce an explicit notion of propositional
atom as part of a modal signature: A nullary modality $p\in\Lambda$ is a
_propositional atom_ if $T$ decomposes as $T=T^{\prime}\times 2$ and under
this decomposition, ${[\\![p]\\!]}_{X}=T^{\prime}X\times\\{\top\\}$.

######  Remark 2.

Propositional atoms can easily be added to all our examples by just extending
the functor with a component for their interpretation, as indicated in the
above definition. Explicitly, if $\mathsf{At}$ is a set of propositional atoms
and $T^{\prime}$ is a functor, then the atoms $p\in\mathsf{At}$ give rise to
nullary modalities $p$, interpreted over
$T=T^{\prime}\times\mathcal{P}(\mathsf{At})$ by ${[\\![p]\\!]}_{X}=\\{(t,U)\in
T^{\prime}X\times\mathcal{P}(\mathsf{At})\mid p\in U\\}$. In fact, this is an
instance of what we have called _combination of frame classes_ above: Systems
featuring only propositional atoms with pointwise valuations, and no further
transition structure, are captured as coalgebras for the constant functor
$\mathcal{P}(\mathsf{At})$, and this system type can be freely combined with
others. A coalgebraic framework for such combinations of system types and
modalities is afforded by multisorted coalgebra, essentially following the
principle of converting components of the coalgebraic type functor into sorts
[SchroderPattinson11]. General results in this framework imply that
completeness properties transfer smoothly to such logic combinations
(essentially, to _fusions_ in standard terminology). In particular,
completeness will always extend without further ado under adding propositional
atoms to a logic, so we will continue to largely elide them in the discussion
of examples.

##  3\. Completeness

In § 3.2 below, we propose an axiom system for CPL, sound wrt arbitrary
structures (Theorem 8) and in § 3.3 we show its completeness wrt structures
s.t. each operator on every coordinate is either “neighbourhood-like” or
“Kripke-like” (Theorem 9). As discussed in § 3.5, even a mild relaxation of
these conditions makes a generic completeness result impossible.

However, not only for the proof, but even for the statements of our
completeness result, or of the axiomatization itself, we need some spadework.

###  3.1. S1SC and Boundedness

In order to state our axiomatization and completeness results, we need several
notions from coalgebraic model theory. The first of them, central to the
entire edifice, is that of _one-step satisfiability_.

[One-step logic]

  * •

Given a supply of primitive symbols $D$ (which can be any set), define the set
$\mathsf{Prop}(D)$ of _Boolean $D$-formulas_ (or _propositions_) as

$\boldsymbol{A},\boldsymbol{B}::=d\mid\boldsymbol{A}\to\boldsymbol{B}\mid\bot$

where $d\in D$, and the set $\Lambda(D)$ of _modalized $D$-formulas_ as

$\Lambda(D)=\\{\heartsuit d_{1}\dots d_{n}\,|\,d_{1},\dots,d_{n}\in D\text{
and }\heartsuit\in\Lambda\mbox{ is $n$-ary}\\}.$

Then the set $\mathsf{Rank1}(D)$ of _rank-1 $D$-formulas_ is defined as

$\mathsf{Rank1}(D)=\mathsf{Prop}(\Lambda(\mathsf{Prop}(D)));$

in other words, a rank-1 formula is a Boolean combination of formulas
consisting of a modality from $\Lambda$ applied to Boolean combinations of
atoms from $D$.

  * •

Given a set $C$ and a valuation $\tau:D\to\mathcal{P}(C)$, we extend $\tau$ to
$\mathsf{Prop}(D)$ using the Boolean algebra structure of $\mathcal{P}(C)$,
and then write $C,\tau\models\boldsymbol{A}$ if $\tau(\boldsymbol{A})=C$, for
$A\in\mathsf{Prop}(D)$.

  * •

Given the same data, we define the extension
${[\\![\phi]\\!]}_{TC,\tau}\subseteq TC$ of $\phi\in\mathsf{Rank1}(D)$ by
extending the assignment

$\llbracket\heartsuit\boldsymbol{A}_{1}\dots\boldsymbol{A}_{n}\rrbracket_{TX,\tau}=\llbracket\heartsuit\rrbracket_{C}(\tau(\boldsymbol{A}_{1}),\dots,\tau(\boldsymbol{A}_{n}))$

using the Boolean algebra structure of $\mathcal{P}(TC)$.

  * •

We then write $TC,\tau\models\phi$ if $\llbracket\phi\rrbracket_{TC,\tau}=TC$,
and $t\models_{TC,\tau}\phi$ if $t\in\llbracket\phi\rrbracket_{TC,\tau}$.

  * •

If $D\subseteq\mathcal{P}(C)$ and $\tau$ is just the inclusion, we will
usually drop it from the notation; in particular, for subsets
$Y_{1},\dots,Y_{n}\subseteq C$ and $\heartsuit\in\Lambda$ $n$-ary, we write
$t\models\heartsuit(Y_{1},\dots,Y_{n})$ to mean
$t\in{[\\![\heartsuit]\\!]}_{C}(Y_{1},\dots,Y_{n})$.

  * •

A set $\Xi\subseteq\mathsf{Rank1}$ is _one-step satisfiable_ w.r.t. $\tau$ if
$\bigcap_{\phi\in\Xi}\llbracket\phi\rrbracket_{TC,\tau}\neq\emptyset$.

Just like in the case of coalgebraic modal logic (see § 4 below), proof
systems for CPL are best described in terms of rank-1 rules – or, more
precisely, rule schemes –, which describe the geometry of the
$\Lambda$-structure under consideration [Schroder06].

[One-Step Rules] Fix a collection $\mathsf{sVar}$ of schematic variables
$\boldsymbol{p},\boldsymbol{q},\boldsymbol{r}\dots$

  * •

A _one-step rule_ is of the form $\boldsymbol{A}/\boldsymbol{P}$ where
$\boldsymbol{A}\in\mathsf{Prop}(\mathsf{sVar})$ and
$\boldsymbol{P}\in\mathsf{Rank1}(\mathsf{sVar})$ is a disjunctive clause over
$\Lambda(\mathsf{sVar})$, i.e. a finite disjunction of formulas that are
either in $\Lambda(\mathsf{sVar})$ or negations of formulas in
$\Lambda(\mathsf{sVar})$. As usual, we impose moreover that every schematic
variable is mentioned at most once in $\boldsymbol{P}$, and every schematic
variable occurring in $\boldsymbol{A}$ occurs also in $\boldsymbol{P}$.

  * •

A rule $\boldsymbol{A}/\boldsymbol{P}$ is _one-step sound_ if

$TC,\tau\models\boldsymbol{P}$ whenever $C,\tau\models\boldsymbol{A}$ for a
valuation $\tau:\mathsf{sVar}\to\mathcal{P}(C)$.

  * •

Given a set $\mathcal{R}$ of one-step rules and a valuation
$\tau:\mathsf{sVar}\to\mathcal{P}(C)$, a set
$\Xi\subseteq\mathsf{Rank1}(\mathsf{sVar})$ is _one-step consistent(with
respect to $\tau$)_ [SchroderPattinson10b] if the set

$\Xi\cup\\{\boldsymbol{P}\sigma\mid\sigma:\mathsf{sVar}\to\mathsf{Prop}(\mathsf{sVar})\text{
and }\boldsymbol{A}/\boldsymbol{P}\mbox{ is a rule in }\mathcal{R}\text{ s.t.
}C,\tau\models\boldsymbol{A}\sigma\\}$

is propositionally consistent, where
$\boldsymbol{A}\mapsto\boldsymbol{A}\sigma$ and
$\boldsymbol{P}\mapsto\boldsymbol{P}\sigma$ denote the obvious inductive
extensions of $\sigma$ to $\mathsf{Prop}(\mathsf{sVar})$ and
$\mathsf{Rank1}(\mathsf{sVar})$, respectively (in other words, we see $\sigma$
as a substitution, and use postfix notation to denote application of
substitutions).

For purposes of the technical development (excluding the examples), we fix
from now on a set $\mathcal{R}$ of one-step sound one-step rules.

We next introduce the two variants of _one-step_ completeness that we need for
our global completeness proof. By _one-step_ , we mean that the completeness
assumption is only made for a very simple logic that precludes nesting of
modal operators, and hence can be interpreted over single elements of $TC$
rather than full coalgebraic models. [Strong One-Step Completeness
[SchroderPattinson10b]] The rule set $\mathcal{R}$ is _strongly one-step
complete(S1SC, neighbourhood-like)_ for a $\Lambda$-structure if

for every $C\in\mathsf{Set}$, $\Xi\subseteq\mathsf{Rank1}(\mathsf{sVar})$, and
$\tau:\mathsf{sVar}\to\mathcal{P}(C)$,

$\Xi$ is one-step satisfiable wrt $\tau$ whenever $\Xi$ is one-step consistent
wrt $\tau$.

Similarly, $\mathcal{R}$ is _finitary S1SC_ if the same condition holds for
$\tau$ restricted to be of type
$\mathsf{sVar}\to\mathcal{P}_{\mathit{fin}}(C)$. By the usual argument, both
forms of strong one-step completeness imply corresponding forms of
compactness: [One-step compactness] $\Lambda$-structure is _one-step compact_
if for every set $X$, every finitely satisfiable set
$\Phi\subseteq\mathsf{Prop}(\mathrm{\Lambda}(\mathcal{P}X))$ of one-step
formulas is satisfiable. Similarly, a $\Lambda$-structure is _finitary one-
step compact_ if for every set $X$, every finitely satisfiable set
$\Phi\subseteq\mathsf{Prop}(\mathrm{\Lambda}(\mathcal{P}_{\mathit{fin}}X))$ of
one-step formulas is satisfiable.

######  Lemma 3.

Every (finitary) S1SC $\Lambda$-structure is (finitary) one-step compact. ∎

######  Remark 4.

Every (finitary) S1SC rule set derives the _congruence rule_

$\frac{\boldsymbol{p}_{1}\leftrightarrow\boldsymbol{q}_{1}\quad\dots\quad\boldsymbol{p}_{\mathsf{ar}{\heartsuit}}\leftrightarrow\boldsymbol{q}_{\mathsf{ar}{\heartsuit}}}{\heartsuit(\boldsymbol{p}_{1},\dots,\boldsymbol{p}_{\mathsf{ar}{\heartsuit}})\to\heartsuit(\boldsymbol{q}_{1},\dots,\boldsymbol{q}_{\mathsf{ar}{\heartsuit}})}$

for every modal operator $\heartsuit\in\Lambda$. The reason is that the
congruence rule is clearly one-step sound, and even under the much weaker
asssumption of _one-step completeness_ (obtained by restricting $\Xi$ to be
finite in Definition 3.1), all one-step sound rules are derivable
[SchroderVenema17].

  * •

Modal neighbourhood semantics is axiomatised by

$\Box\boldsymbol{p}\to\Box\boldsymbol{q}\boldsymbol{p}\leftrightarrow\boldsymbol{q}$

which expresses that $\Box$ is a congruential operator (where we write
$\Box\boldsymbol{p}\to\Box\boldsymbol{q}$ in place of
$\neg\Box\boldsymbol{p}\vee\Box\boldsymbol{q}$ for readability). This is the
paradigmatic example of S1SC; see the discussion in Remark 6 below.

  * •

The rule set for the normal modal logic $\mathsf{K}$ consists of the rules

$\Diamond\boldsymbol{p}\to\Diamond\boldsymbol{q}_{1}\vee\dots\vee\Diamond\boldsymbol{q}_{n}\boldsymbol{p}\to\boldsymbol{q}_{1}\vee\dots\vee\boldsymbol{q}_{n}$

for all $n\geq 0$. As we are going to see in Lemma 5, $\mathcal{R}$ is
finitary S1SC. On the other hand, for reasons detailed in Remark 6,
$\mathcal{R}$ is not S1SC. An S1SC semantics for this particular rule set
would be provided by _normal neighbourhood(i.e., filter) frames_.

  * •

For graded modal logic, the proof of one-step completeness of the rule set

$\displaystyle\Diamond_{n+1}\boldsymbol{p}\to\Diamond_{n}\boldsymbol{q}\boldsymbol{p}\to\boldsymbol{q}\qquad\Diamond_{n_{1}+n_{2}}\boldsymbol{r}\to\Diamond_{n_{1}}\boldsymbol{p}\vee\Diamond_{n_{2}}\boldsymbol{q}\boldsymbol{r}\to\boldsymbol{p}\vee\boldsymbol{q}$
$\displaystyle\Diamond_{n_{1}}\boldsymbol{p}\vee\Diamond_{n_{2}}\boldsymbol{q}\to\Diamond_{n_{1}+n_{2}+1}\boldsymbol{r}\vee\Diamond_{0}\boldsymbol{s}\boldsymbol{p}\to\boldsymbol{r}\quad\boldsymbol{q}\to\boldsymbol{r}\quad\boldsymbol{p}\wedge\boldsymbol{q}\to\boldsymbol{s}\qquad\neg\Diamond_{0}\boldsymbol{p}\neg\boldsymbol{p}$

[SchroderVenema17, Lemma 3.10] upon inspection effectively establishes
finitary S1SC.

  * •

For positive Presburger modal logic, we similarly have that the proof of one-
step completeness of a natural rule system for full Presburger modal logic
[KupkePattinson10, Lemma 4.5] straightforwardly adapts to a) positive
Presburger modal logic, and b) finitary S1SC, provided that one generalizes
the semantics to infinite multisets as we do here.

  * •

Conditional logic provides a curious mixed case, due to its being
neighbourhood-like in one coordinate and Kripke-like in another. We will
introduce adequate apparatus and analyse it further in Example 3.1.

  * •

In Remark 7, we discuss the issue of S1SC of coalition logic interpreted over
effectivity functions.

######  Lemma 5.

The $\Lambda$-structure for relational modal logic (Section 2) is finitary
S1SC.

######  Proof 3.1.

Consider any consistent
$\Xi\subseteq\mathsf{Prop}(\Lambda(\mathcal{P}_{\mathit{fin}}X))$, where
$\Lambda=\\{\Diamond\\}$; w.l.o.g., $\Xi$ is maximally consistent. We need to
find $A\in\mathcal{P}X$ s.t. $A\vDash_{\mathcal{P}X}\Xi$. Let us choose

$A=\\{x\mid\Diamond\\{x\\}\in\Xi\\}.$

One shows by induction on formulas that

$A\vDash_{\mathcal{P}X}\phi$ iff $\phi\in\Xi$.

The only non-trivial case is the modal one. For any
$B=\\{b_{1},\dots,b_{n}\\}\in\mathcal{P}_{\mathit{fin}}X$, we have that

$\displaystyle A\vDash_{\mathcal{P}X}\Diamond B$ $\displaystyle\text{ iff
}\exists i\leq n.A\vDash_{\mathcal{P}X}\Diamond\\{b_{i}\\}$
$\displaystyle\text{ iff }\exists i\leq n.\Diamond\\{b_{i}\\}\in\Xi$
$\displaystyle\text{ iff }\Diamond
B=\Diamond\\{b_{1}\\}\cup\dots\cup\Diamond\\{b_{n}\\}\in\Xi$

######  Remark 6.

As noted in [SchroderPattinson10b, Remark 55], we can give a more abstract
characterization of S1SC, recognizable also to readers familiar with more
categorical presentations of coalgebraic modal logic (cf., e.g.,
[KurzRosicky]). Every signature $\Lambda$ together with a given set of one-
step axiom schemes (equivalently, one-step rules) can be encoded disregarding
concrete syntax by its _functorial presentation_ [KupkeEA04] (cf. also
[SchroderPattinson10b, Definition 28]) as an endofunctor $L_{\Lambda}$ on the
category $\mathsf{BA}$ of Boolean algebras. $\mathsf{BA}$ is dually adjoint to
$\mathsf{Set}$, with the adjunction given by the contravariant powerset
functor222We write here $\overline{\mathcal{Q}}$ to stress that we change the
target category. $\overline{\mathcal{Q}}$ and the functor $\mathcal{S}$ taking
a Boolean algebra to the set of its ultrafilters:

$\textstyle{{\mathsf{BA}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{L_{\Lambda}}$$\scriptstyle{\mathcal{S}}$$\textstyle{{\mathsf{Set}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{\mathcal{Q}}}$$\scriptstyle{T}$
(2)

The information contained in each $\Lambda$-structure can be then more
abstractly encoded by
$\delta:L_{\Lambda}\overline{\mathcal{Q}}\to\overline{\mathcal{Q}}T$
[KupkeEA04] and the _canonical_ structure for $\Lambda$ is given by
$M_{\Lambda}=\mathcal{S}L_{\Lambda}\overline{\mathcal{Q}}$. Coalgebras for the
canonical structure can equivalently be described as generalized neighbourhood
frames (where by _generalized_ we mean that for every $n$-ary modality in
$\Lambda$, we have $n$-ary neighbourhoods, i.e. subsets of the $n$-th power of
the state set), subject to satisfaction of the frame conditions embodied in
the given one-step rules [SchroderPattinson10b, Remark 34]. For every
$\Lambda$-structure, we can define a canonical _structure morphism_
[SchroderPattinson10b, p. 1121] to $M_{\Lambda}$ by composing the counit of
the above adjunction with $\mathcal{S}\delta$, and S1SC effectively requires
that this structure morphism is surjective. In other words, a
$\Lambda$-structure is S1SC iff its functor surjects onto the canonical
neighbourhood semantics; it is for this reason that we refer to the S1SC case
as “neighbourhood-like”. In fact, as we explain in the next remark, we do not
currently have an in-the-wild example of an S1SC structure that is not
actually isomorphic to the canonical neighbourhood semantics.

######  Remark 7.

Coalition logic [Pauly02] and, essentially equivalently, the next-step
fragment of alternating-time temporal logic [AlurEA02], have modalities $[Q]$
indexed over _coalitions_ $Q$, which are subsets of a fixed finite set $N$ of
_agents_ ; the operator $[Q]$ reads ‘the coalition $Q$ of players can enforce
…in the next step’. The semantics is formulated over structures called _game
frames_ or _concurrent game structures_ , i.e., coalgebras for the functor

$\textstyle\mathcal{G}X=\\{((S_{i})_{i\in N},f:\big{(}\prod_{i\in
N}S_{i}\big{)}\to X)\mid\emptyset\neq S_{i}\subseteq{\mathbb{N}}\\}$

where $S_{i}$ is thought of as the set of moves available to agent $i\in N$
and $f$ is an _outcome function_ that determines the next state of the game,
depending on the moves chosen by the agents (we restrict to finitely many
moves per agent as in alternating-time temporal logic). For notational
convenience, given a coalition $Q=\\{q_{1},\dots,q_{k}\\}\subseteq N$ and
moves $s_{q_{1}}\in S_{q_{1}}$, …, $s_{q_{k}}\in S_{q_{k}}$, we write
$s_{Q}=(s_{q})_{q\in Q}$ and $S_{Q}=S_{q_{1}}\times\dots\times S_{q_{k}}$ (so
that $s_{Q}\in S_{Q}$). Given $s_{Q}\in S_{Q}$ and $s_{N\setminus Q}\in
S_{N\setminus Q}$, we write $(s_{Q},s_{N\setminus Q})$ for the evident induced
element of $S_{N}$.

An alternative semantics of the coalitional operators is provided by
_effectivity functions_. These are functions $E$ assigning to each coalition
$Q$ a set $E(Q)$ of properties that $Q$ can enforce. Explicitly, a concurrent
game $G=((S_{i})_{i\in P},f)\in\mathcal{G}X$ induces an effectivity function
$E_{G}$ by

$E_{G}(Q)=\\{A\subseteq X\mid\exists s_{Q}\in S_{Q}.\,\forall s_{N\setminus
Q}\in S_{N\setminus Q}.\,f(s_{Q},s_{N\setminus Q})\in A\\}.$

Effectivity functions congregate into a functor ${\mathcal{E}}$, a subfunctor
of a product of neighbourhood functors. The modal operators $[Q]$ are
interpreted over effectivity functions in the usual style of neighbourhood
semantics, i.e. by

${[\\![[Q]]\\!]}_{X}(A)=\\{E\in{\mathcal{E}}X\mid A\in E(Q)\\}.$

Composing this semantics with the above-defined projection from concurrent
games to effectivity functions yields the interpretation of the coalitional
modalities $[Q]$ over $\mathcal{G}$; this reproduces the standard semantics of
coalition logic and alternating time temporal logic.

Now Theorem 3.2 in [Pauly02] states that an effectivity function
$E\in{\mathcal{E}}(X)$ is of the form $E_{G}$ for some $G\in\mathcal{G}X$ iff
it is _playable_ , i.e. satisfies the following properties:

  * •

For all $Q$, $\emptyset\notin E(Q)\owns X$

  * •

$E$ is _outcome-mononotic_ , i.e. each $E(Q)$ is upwards closed under set
inclusion.

  * •

$E$ is _$N$ -maximal_, i.e. for all $A\subseteq X$, either $X\setminus A\in
E(\emptyset)$ or $A\in E(N)$.

  * •

$E$ is _superadditive_ , i.e. whenever $A_{1}\in E(Q_{1})$ and $A_{2}\in
E(Q_{2})$ for disjoint coalitions $Q_{1},Q_{2}$, then $A_{1}\cap A_{2}\in
E(Q_{1}\cup Q_{2})$.

If this were the case, then coalition logic interpreted over either concurrent
games or playable effectivity functions would be S1SC, and we claimed as much
in the conference version [LitakPSS12:icalp]: The above conditions amount to
playable effectivity functions being just neighbourhood systems that satisfy a
set of one-step rules:

$\displaystyle\neg[Q]\bot\qquad[Q]\top\qquad\frac{\boldsymbol{p}\to\boldsymbol{q}}{[Q]\boldsymbol{p}\to[Q]\boldsymbol{q}}$
$\displaystyle\frac{\boldsymbol{p}\vee\boldsymbol{q}}{[\emptyset]\boldsymbol{p}\lor[N]\boldsymbol{q}}\qquad\frac{\boldsymbol{p}\land\boldsymbol{q}\to\boldsymbol{r}}{[Q_{1}]\boldsymbol{p}\land[Q_{2}]\boldsymbol{q}\to[Q_{1}\cup
Q_{2}]\boldsymbol{r}}\;\text{ for }Q_{1}\cap Q_{2}=\emptyset,$

and such structures are always S1SC (this is by the development in
[SchroderPattinson10b], see in particular Remarks 34 and 55 in op. cit., and
also Remark 6 above). However, it turns out that Theorem 3.2 in [Pauly02] is
not in fact entirely correct, and once fixed no longer implies that coalition
logic is S1SC. To see this, note that for every effectivity function of the
form $E_{G}$, $E_{G}(\emptyset)$ must have a least element, equivalently be
closed under intersections: every element of $E_{G}(\emptyset)$ must contain
the set

$A=\\{f(s_{N})\mid s_{N}\in S_{N}\\},$

and this set is itself in $E_{G}(\emptyset)$. This condition is however not
satisfied by all playable effectivity functions in the above sense: take $X$
to be some infinite set, pick a non-principal ultrafilter $U$ on $X$, and put
$E(Q)=U$ for all coalitions $Q$. This defines a playable effectivity function
but $E(\emptyset)=U$ has no least element. Adding the condition that
$E(\emptyset)$ has a least element to the definition of playability does fix
the theorem, but this condition is not expressible by a finitary one-step
axiom and hence we do not obtain S1SC for coalition logic as a corollary.

As indicated above, we have alternative conditions that ensure completeness
[SchroderPattinson10]:  A modal operator $\heartsuit$ is _$k$ -bounded_ in the
$i$-th argument for $k\in{\mathbb{N}}$ and with respect to a
$\Lambda$-structure $T$ if for every $C\in\mathsf{Set}$ and every
$\vec{A}\subseteq C$,

${[\\![\heartsuit]\\!]}_{C}(A_{1},\dots,A_{n})=\bigcup_{B\subseteq
A_{i},\\#B\leq
k}{[\\![\heartsuit]\\!]}_{C}(A_{1},\dots,A_{i-1},B,A_{i+1},\dots,A_{n}).$ (3)

Boundedness of $\heartsuit$ in the $i$-th argument implies in particular that
$\heartsuit$ is monotonic in the $i$-th argument. We can replace the
assumption that the rule set $\mathcal{R}$ is S1SC with the weaker assumption
that $\mathcal{R}$ is finitary S1SC, provided that modal operators are bounded
on respective coordinates. The technical details of a suitably general setup
are as follows:

  * •

A _boundedness signature_ for $\Lambda$ is a function $\flat\Lambda$ assigning
to every $\heartsuit\in\Lambda$ a vector of elements of
${\mathbb{N}}\cup\\{\infty\\}$ of length $\mathsf{ar}{\heartsuit}$, i.e. an
element of $({\mathbb{N}}\cup\\{\infty\\})^{\mathsf{ar}{\heartsuit}}$.

  * •

Being _$\infty$ -bounded_ is a condition trivially satisfied by all operators,
i.e., every operator is “$\infty$-bounded” in each coordinate.

  * •

We say that $\flat\Lambda$ is _adequate_ for a $\Lambda$-structure over $T$ if
every modal operator $\heartsuit\in\Lambda$ is
$\flat\Lambda(\heartsuit)(i)$-bounded in $i$ every
$i\leq\mathsf{ar}{\heartsuit}$.

  * •

We say that $\Lambda$ is $\flat\Lambda$-_bounded_ w.r.t $T$ if $\flat\Lambda$
is adequate for the structure in question and the codomain of $\flat\Lambda$
does not contain $\infty$.

  * •

We say that $\Lambda$ is _bounded_ w.r.t. $T$ if it is
$\flat\Lambda$-_bounded_ w.r.t. $T$ for _some_ $\flat\Lambda$. That is, every
modal operator $\heartsuit\in\Lambda$ for every $i\leq\mathsf{ar}{\heartsuit}$
is $k_{\heartsuit,i}$-bounded in $i$ for some $k_{\heartsuit,i}<\infty$.

Here are some examples of boundedness signatures adequate for structures under
consideration:

  * •

for the neighbourhood case, $\flat\Lambda(\Box)=(\infty)$,

  * •

for the Kripke case, $\flat\Lambda(\Diamond)=(1)$:
if $B\in{[\\![\Diamond]\\!]}_{C}(A)$, then $B\cap A\neq\emptyset$ by
definition. So fix $c\in B\cap A$; then
$B\in{[\\![\Diamond]\\!]}_{C}(\\{c\\})$,

  * •

for graded modalities, $\flat\Lambda(\langle k\rangle)=(k+1)$:
if $\mu\in{[\\![\langle k\rangle]\\!]}_{C}(A)$, then $\mu(A)>k$. Hence there
exist (not necessarily distinct) elements $c_{1},\dots,c_{k+1}\in C$ such that
$\mu(\\{c_{1},\dots,c_{k+1}\\})>k$, i.e. $\mu\in{[\\![\langle
k\rangle]\\!]}_{C}(\\{c_{1},\dots,c_{k+1}\\})$,

  * •

for positive Presburger logic,

$\flat\Lambda(L_{k}(a_{1},\dots,a_{n}))=((k+1)\;\mathrm{div}\;a_{1}+1,\dots,(k+1)\;\mathrm{div}\;a_{n}+1),$

  * •

for the discrete distribution functor $\mathcal{D}$, $\flat\Lambda(\langle
p\rangle)=(\infty)$,

  * •

for its finite variant $\mathcal{D}_{k}$, $\flat\Lambda(\langle
n/k\rangle)=(n)$,

  * •

for non-monotonic conditionals, $\flat\Lambda(>)=(\infty,1)$.

Note that, e.g., the neighbourhood modality clearly fails to be bounded.
Boundedness allows us to broaden the scope of our completeness results to
setups where full S1SC would be too much to ask, i.e., to leave the
neighbourhood-like setting. This is done by requiring S1SC on suitable
coordinates only for valuations of schematic variables in _finite_ sets.
Modalities which are both finitary S1SC and bounded will be called _Kripke-
like_. In order to make this precise so that we can cover mixed cases, such as
those of non-monotonic conditionals, some care is needed.

  * •

The _colouring_ function
$\flat\kern-1.4pt\flat:{\mathbb{N}}\cup\\{\infty\\}\to\\{\mathit{fin},\infty\\}$
assigns $\mathit{fin}$ to elements of ${\mathbb{N}}$ and
$\flat\kern-1.4pt\flat(\infty)=\infty$. It is extended pointwise to
$({\mathbb{N}}\cup\\{\infty\\})^{\mathsf{ar}{\heartsuit}}$ and
$\flat\kern-1.4pt\flat\Lambda$ is defined as the composition of $\flat\Lambda$
with this pointwise extension.

  * •

Let $\mathfrak{c}:\mathsf{sVar}\to\\{\mathit{fin},\infty\\}$ be a colouring of
the set of schematic variables. Define the set of
_$\flat\kern-1.4pt\flat\Lambda,\mathfrak{c}$ -coloured modalities_ as

$\flat\kern-1.4pt\flat\Lambda_{\mathfrak{c}}=\\{\heartsuit\boldsymbol{p}_{1}\dots\boldsymbol{p}_{\mathsf{ar}{\Lambda}}\,|\,\boldsymbol{p}_{1}\dots\boldsymbol{p}_{\mathsf{ar}{\Lambda}}\in\mathsf{sVar}\text{
and
}(\mathfrak{c}\boldsymbol{p}_{1},\dots,\mathfrak{c}\boldsymbol{p}_{\mathsf{ar}{\Lambda}})=\flat\kern-1.4pt\flat\Lambda(\heartsuit)\\}.$

  * •

A valuation $\tau:\mathsf{sVar}\to\mathcal{P}(C)$ respects $\mathfrak{c}$ iff
$\tau(\boldsymbol{p}_{i})\in\mathcal{P}_{\mathfrak{c}\boldsymbol{p}_{i}}$,
where we recall that $\mathcal{P}_{\mathit{fin}}$ is finite powerset, and
$\mathcal{P}_{\infty}$ is simply $\mathcal{P}$.

  * •

A Gentzen-style one-step rule $R$ is
_$\flat\kern-1.4pt\flat\Lambda,\mathfrak{c}$ -compatible_ if it is of the form

$\frac{\Gamma_{1}\Rightarrow\Delta_{1}\qquad\cdots\qquad\Gamma_{k}\Rightarrow\Delta_{k}}{\Gamma_{R}\Rightarrow\Delta_{R}}(R)$

where

    * –

$\Gamma_{1},\dots,\Gamma_{k},\Delta_{1},\dots,\Delta_{k}$ are multisets of
elements of $\mathsf{sVar}$,

    * –

$\Gamma_{R}$ and $\Delta_{R}$ are multisets of elements of
$\flat\kern-1.4pt\flat\Lambda_{\mathfrak{c}}$.

  * •

For a Gentzen-style rule, write
$\flat\kern-1.4pt\flat\Lambda_{\mathfrak{c}}(R)$ for the set of
$\flat\kern-1.4pt\flat\Lambda,\mathfrak{c}$-compatible variants of $R$
obtained by renaming of schematic variables. For a Hilbert-style rule,
$\flat\kern-1.4pt\flat\Lambda_{\mathfrak{c}}(R)$ is obtained via its Gentzen-
style counterpart. Finally,
$\flat\kern-1.4pt\flat\Lambda_{\mathfrak{c}}(\mathcal{R})=\\{\flat\kern-1.4pt\flat\Lambda_{\mathfrak{c}}(R)\mid
R\in\mathcal{R}\\}$.

  * •

A set $\Xi\subseteq\mathsf{Rank1}(\mathsf{sVar})$ is _$\mathfrak{c}$
-consistent wrt $\tau$_ if its union with the set

$\\{\boldsymbol{P}\sigma\mid\sigma:\mathsf{sVar}\to\mathsf{Prop}(\mathsf{sVar})\text{
and
}\boldsymbol{A}/\boldsymbol{P}\in\flat\kern-1.4pt\flat\Lambda_{\mathfrak{c}}(\mathcal{R})\text{
s.t. }C,\tau\models\boldsymbol{A}\sigma\\}$

is propositionally consistent.

  * •

We say that a set of rules $\mathcal{R}$ is _$\flat\Lambda$ -S1SC_ if

for every $C\in\mathsf{Set}$, any $\Xi\subseteq\mathsf{Rank1}(\mathsf{sVar})$,
any colouring $\mathfrak{c}$ and any $\tau$ respecting $\mathfrak{c}$,

$\Xi$ is one-step satisfiable wrt $\tau$ whenever it is
$\mathfrak{c}$-consistent wrt $\tau$.

That is, the notion of $\flat\Lambda$-S1SC instantiates to finitary S1SC in
bounded arguments, and to S1SC in unbounded ones. In the case of the modal
signature $\\{>\\}$ of non-monotonic conditionals with
$\flat\Lambda(>)=(\infty,1)$, the associated one-step completeness condition
may be called _(S1SC, finitary S1SC)_ [SchroderPattinson10]. A suitable
axiomatization can be extracted from existing references [Chellas80,
SchroderPattinson10b, PattinsonSchroder10, SchroderPattinson10]:

$\boldsymbol{r}>\boldsymbol{p}\to\boldsymbol{r}>\boldsymbol{q}_{1}\vee\dots\vee\boldsymbol{r}>\boldsymbol{q}_{n}\boldsymbol{p}\to\boldsymbol{q}_{1}\vee\dots\vee\boldsymbol{q}_{n}\qquad\boldsymbol{p}>\boldsymbol{r}\to\boldsymbol{q}>\boldsymbol{r}\boldsymbol{p}\leftrightarrow\boldsymbol{q}$

A proof that this axiomatization is indeed $\flat\Lambda$-S1SC combines the
neighbourhood argument in the first coordinate (cf. Remark 6) with the Kripke
argument in the second (cf. Lemma 5).

###  3.2. Hilbert-style Calculus

Table 1. Hilbert-style Calculus $\mathcal{H}\mathcal{R}$

The axioms are modelled after those of Enderton [Enderton72].

Everywhere below, $\forall\vec{y}.$ denotes a sequence of universal
quantifiers of arbitrary length, possibly empty.

En1:

all propositional tautologies. These can be axiomatized, e.g., by

  * •:

$\forall\vec{y}.\left(\phi\to\left(\psi\to\phi\right)\right)$

  * •:

$\forall\vec{y}.\left(\left(\phi\to\left(\psi\to\chi\right)\right)\to\left(\left(\phi\to\psi\right)\to\left(\phi\to\chi\right)\right)\right)$

  * •:

$\forall\vec{y}.\left(\bot\to\phi\right)$

  * •:

$\forall\vec{y}.\left(\left(\left(\phi\to\bot\right)\to\bot\right)\to\phi\right)$

For En2 and Alpha below, recall that whenever we write a substitution we
implicitly impose the assumption that the substituted term is actually
substitutable.

En2:

$\forall\vec{y}.(\forall x.\phi\to\phi[z/x])$

En3:

$\forall\vec{y}.(\forall x.(\phi\to\psi)\to(\forall x.\phi\to\forall x.\psi))$

En4:

$\forall\vec{y}.(\phi\to\forall x.\phi)$ if $x$ is fresh for $\phi$

En5:

$\forall\vec{y}.(x=x)$

En6.1:

$\forall\vec{y}.(x=z\to P(\vec{u},x,\vec{v})\to P(\vec{u},z,\vec{v}))$ for
$P\in\Sigma\cup\\{=\\}$

En6.2:

$\forall\vec{y}.(x=z\to x\heartsuit\lceil
y_{1}\\!:\\!\phi_{1}\rceil\dots\lceil y_{n}\\!:\\!\phi_{n}\rceil\to
z\heartsuit\lceil y_{1}\\!:\\!\phi_{1}\rceil\dots\lceil
y_{n}\\!:\\!\phi_{n}\rceil)$

Alpha:

$\forall\vec{y}((x\heartsuit\dots\lceil
z:\phi\rceil\dots)\to(x\heartsuit\dots\lceil u:\phi[u/z]\rceil\dots))$

Onestep($\mathcal{R}$):

$\forall\vec{y}.\forall z.(\forall
x.\boldsymbol{A}\sigma\to[\sigma,x,z]\boldsymbol{P})$ where

  * •:

$\boldsymbol{A}/\boldsymbol{P}$ ranges over the one-step rules in
$\mathcal{R}$, and

  * •:

$\sigma$ is a substitution sending each $\boldsymbol{p}_{i}$ to a formula of
$\mathcal{L}$, and $[\sigma,x,z]$ is the inductive extension of the map
sending each $\heartsuit_{i}\vec{\boldsymbol{p}_{i}}$ to
$z\heartsuit_{i}\lceil x:\sigma(\boldsymbol{p}_{i}^{1})\rceil\cdots\lceil
x:\sigma(\boldsymbol{p}_{i}^{a(i)})\rceil)$

BdPL♭Λ:

An additional axiom scheme when $\flat\Lambda(\heartsuit)(i)\neq\infty$, with
$\vec{z}\mbox{ fresh for }y_{i},\vec{\phi}$

$\forall\vec{y}.(x\heartsuit\dots\lceil
y_{i}:\phi_{i}\rceil\dots\leftrightarrow\exists z_{1}\dots
z_{\flat\Lambda(i)}.(\bigwedge\limits_{j\leq\flat\Lambda(\heartsuit)(i)}\phi_{i}[z_{j}/y_{i}]\wedge
x\heartsuit\dots\lceil
y_{i}:\bigvee\limits_{j\leq\flat\Lambda(\heartsuit)(i)}y_{i}=z_{j}\rceil\dots))$

We are finally ready to present our axioms for CPL in Table 1. Axioms En1–En6
are just those of Enderton, with En6.2 an additional clause to cover the case
of modal formulas. The $\alpha$-renaming axiom Alpha is needed because our
syntax features separate comprehension variables. Our Onestep($\mathcal{R}$)
axiom scheme generalizes what was originally just the congruence rule (Remark
4) in Chang’s formalism, corresponding to the fact that the S1SC rule system
for neighbourhood semantics consists of only the congruence rule. Axiom BdPL♭Λ
applies to operators that are bounded in suitable coordinates. It is important
to notice that boundedness is not expressible as a _sentence_ or _formula_ in
weak frameworks; in languages like $\mathrm{H}_{\mathrm{\Lambda}}(@)$, it can
only be expressed by a non-standard rule [SchroderPattinson10].

Let $\Gamma,\Delta\subseteq\mathrm{CPL}(\mathrm{\Lambda},\Sigma)$, let
$\mathcal{R}$ be a set of one-step rules and
$\phi\in\mathrm{CPL}(\mathrm{\Lambda},\Sigma)$. Write
$\Gamma\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\phi$ if there are
$\gamma_{1},\dots,\gamma_{n}\in\Gamma$ s.t.
$\gamma_{1}\to\dots\to\gamma_{n}\to\phi$ can be deduced from En1–En6, Alpha,
Onestep($\mathcal{R}$) and BdPL♭Λ in Table 1 using only Modus Ponens. This
clearly defines _a finitary deducibility relation_ in the sense of Goldblatt
[goldblatt1993:abstract, Sec. 8.1] and being
_$\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}$ -consistent_ is equivalent
with being _finitely
$\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}$-consistent_ in his sense,
that is, $\Gamma\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\bot$ iff there
is $\Gamma_{0}\subseteq_{\mathit{fin}}\Gamma$ s.t.
$\Gamma_{0}\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\bot$.

######  Theorem 8 (Soundness).

Whenever a $\Lambda$-structure over $T$ is adequate for $\flat\Lambda$, all
the axioms in Table 1 hold in every coalgebraic $\Lambda$-model and the set of
formulas valid in such a model is closed under
$\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}$.

Recall that by Convention 3.1, one-step soundness of $\mathcal{R}$ is not
mentioned explicitly.

For any $\Lambda$, $\mathcal{R}$ and $\flat\Lambda$, we say that the inference
system given by $\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}$ is _strongly
complete_ for a given $\Lambda$-structure based on $T$ if for any set of
sentences $\Gamma\in\mathrm{CPL}(\mathrm{\Lambda},\Sigma)$,
$\Gamma\not\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\bot$ holds if and
only if there is a coalgebraic $\Lambda$-model for $\Gamma$.

######  Theorem 9 (Strong Completeness).

Whenever a set of rules $\mathcal{R}$ is _$\flat\Lambda$ -S1SC_ for a
$\Lambda$-structure over $T$ that is adequate for $\flat\Lambda$, then
$\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}$ is strongly complete for this
structure.

For concrete instances of this completeness result, combine Examples 3.1, 3.1
and 3.1.

###  3.3. Proof of The Completeness Theorem

First, we introduce machinery proposed in [goldblatt1993:abstract]. Consider
any $Fr\subseteq\mathrm{CPL}(\mathrm{\Lambda},\Sigma)$ closed under
propositional connectives. $Fr$ can be, for example, the set of all formulas
whose free variables are contained in a fixed subset of $\mathsf{iVar}$, the
set of all sentences and the entire $\mathrm{CPL}(\mathrm{\Lambda},\Sigma)$
itself being the two borderline cases. Any set
$\emph{Inf}\subseteq\mathcal{P}(Fr)\times Fr$ will be called, following
Goldblatt, _a set of inferences_. For any
$\mathit{inf}=(\Pi,\chi)\in\mathit{Inf}$ and any $\Gamma\subseteq Fr$, we say
that

  * •

$\Gamma$ _respects_ $\mathit{inf}$ if
$\Gamma\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\chi$ whenever
$\Gamma\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\phi$ for all
$\phi\in\Pi$,

  * •

$\Gamma$ _is closed under_ $\mathit{inf}$ if $\chi\in\Gamma$ whenever
$\Pi\subseteq\Gamma$,

  * •

$\Gamma$ respects $\mathit{Inf}$ iff it respects each member of
$\mathit{Inf}$,

  * •

$\Gamma$ is closed under $\mathit{Inf}$ iff it is closed under each member of
$\mathit{Inf}$.

######  Theorem 10 (Goldblatt’s Abstract Henkin Principle
[goldblatt1993:abstract]).

If $\mathit{Inf}$ is a set of inferences in $Fr$ of an infinite cardinality
$\kappa$ and $\Gamma$ is a
$\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}$-consistent subset of $Fr$
satisfying in addition:

$\forall X\subseteq Fr.|X|<\kappa\text{ implies that }\Gamma\cup X\text{
respects }\mathit{Inf}$ (4)

(i.e., _every $\kappa$-finite extension of $\Gamma$ respects $\mathit{Inf}$_),
then $\Gamma$ has a maximally
$\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}$-consistent extension in $Fr$
which is closed under $\mathit{Inf}$.

######  Remark 11.

We emphasize that speaking about _inferences_ in Goldblatt’s sense being
infinite sets does _not_ mean that _deductions_ in the axiom system for for
CPL use infinitary rules. As stated above, the only inference rule in our
system is ordinary Modus Ponens. Even the one-step rules defined above (which
are not infinitary anyway) can be written as sentence schemes Onestep thanks
to the use of quantifiers.

We further point out that an Enderton-style axiomatization does not involve
the generalization rule: if $x$ is a free variable in $\phi$, it is not
necessarily the case that
$\phi\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\forall x.\phi$ (this is
not in contradiction to completeness: the rule is sound in the sense that
validity of the premise implies validity of the conclusion, but its conclusion
is not a logical consequence of its premise). This makes it enjoy a rather
rare property for an axiomatization of FOL: a deduction theorem in exactly the
same form as propositional logic, i.e.,
$\Gamma\cup\\{\phi\\}\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\psi$ iff
$\Gamma\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\phi\to\psi$ (cf.
[Enderton72, p. 118]). This will also allow us to give our Henkin-style proofs
_without introducing additional constants_ —the role of Henkin constants for
existentially quantified variables will be played by the variables
themselves.333Recall that we have been working in a setup without functions
symbols (including $0$-ary ones) anyway; extending our original syntax with
constants just for the sake of this particular proof does not even seem
particularly hygienic. The only disadvantage of this approach would be that if
we consider uncountable $\mathrm{\Lambda}$ or $\Sigma$, we would also need to
allow uncountably many elements of $\mathsf{iVar}$, something we highlight in
the statement of several lemmas and claims below.

Let us recall the crucial ingredient in Henkin-style completeness proofs: the
notion of quasi-Henkin model and its associated Truth Lemma. This is inspired
by previously announced completeness proofs for coalgebraic hybrid logic
[SchroderPattinson10]; we discuss the relationship in detail in Remark 17 and
§ 4 below.

Let $\Gamma$ be a maximal consistent set (MCS) of formulas. Define
$C_{\Gamma}$ = $\\{|x|:x\text{ is a variable}\\}$, where $|x|$ =
$\\{z:x=z\in\Gamma\\}$, and put $I_{\Gamma}(P)$
=$\\{(|x_{1}|,\dots,|x_{n}|):P(x_{1},\dots,x_{n})\in\Gamma\\}$. Set
$\widehat{\phi}^{y_{i}}$ =$\\{|z|:\phi[z/y_{i}]\in\Gamma\\}$, to be thought of
as _the set of variables satisfying $\phi$ according to $\Gamma$_ (when
$y_{i}$ is taken to be the _argument variable_ or the _context hole_). Given a
$T$-coalgebra structure $\gamma:C_{\Gamma}\to TC_{\Gamma}$, we say that
$(C_{\Gamma},\gamma,I_{\Gamma})$ is a quasi-Henkin coalgebraic model if, for
any variables $x$, $y_{1}$, …, $y_{n}$ and any formulas $\psi$, $\phi_{1}$, …,
$\phi_{n}$,

$\exists x.\psi\in\Gamma\Longrightarrow\text{ for some
}y_{i},y_{i}\in\widehat{\psi}^{x}.$ (5)

(note that the converse implication holds for any MCS) and

$x\heartsuit\lceil y_{1}:\phi_{1}\rceil\cdots\lceil
y_{n}:\phi_{n}\rceil\in\Gamma\Longleftrightarrow\gamma(|x|)\in\llbracket\heartsuit\rrbracket_{C_{\Gamma}}(\widehat{\phi_{1}}^{y_{1}},\dots,\widehat{\phi_{n}}^{y_{n}}).$
(6)

In a quasi-Henkin model, define the _canonical variable assignment_
$v_{\Gamma}$ by $v_{\Gamma}(x)$ = $|x|$.

######  Lemma 12 (Truth Lemma).

Let $\Gamma$ be a maximal consistent set of formulas and
$\mathfrak{M}_{\Gamma}$ = $(C_{\Gamma},\gamma,I_{\Gamma})$ a quasi-Henkin
coalgebraic model. Then, for every formula $\phi$,

$\mathfrak{M}_{\Gamma},v_{\Gamma}\models\phi\Longleftrightarrow\phi\in\Gamma.$
(7)

######  Proof 3.2.

By induction on $\phi$. An auxiliary fact we need is that whenever $\phi$
satisfies the inductive claim (7), then

$\llbracket\phi\rrbracket^{y}_{\mathfrak{M}_{\Gamma}}=\widehat{\phi}^{y}$ (8)

(recall $\llbracket\phi\rrbracket^{y}$ is defined in (1)), which can be shown
in the following way. Let $|z|\in C_{\Gamma}$. Then we have

$\displaystyle\mathfrak{M}_{\Gamma},v_{\Gamma}[|z|/y]\models\phi$
$\displaystyle\Longleftrightarrow\mathfrak{M}_{\Gamma},v_{\Gamma}\models\phi[z/y]$
$\displaystyle\Longleftrightarrow\phi[z/y]\in\Gamma\qquad\text{by
\eqref{eq:truth},}$

as desired.

The base case of induction for atomic formulas follows now from the
definitions of $C_{\Gamma}$ and $I_{\Gamma}$, the Boolean cases from the fact
that we are dealing with a MCS, and the case for quantifiers directly from
Condition 5. For the modal case, where $\phi\equiv x\heartsuit\lceil
y_{1}:\phi_{1}\rceil\dots\lceil y_{n}:\phi_{n}\rceil$:

$\displaystyle\mathfrak{M}_{\Gamma},v_{\Gamma}\models x\heartsuit\lceil
y_{1}:\phi_{1}\rceil\dots\lceil y_{n}:\phi_{n}\rceil$
$\displaystyle\Longleftrightarrow\gamma(v_{\Gamma}(x))\in\llbracket\heartsuit\rrbracket_{\mathfrak{M}_{\Gamma}}(\llbracket\phi_{1}\rrbracket^{y_{1}}_{\mathfrak{M}_{\Gamma}},\dots,\llbracket\phi_{n}\rrbracket^{y_{n}}_{\mathfrak{M}_{\Gamma}})$
by def.
$\displaystyle\Longleftrightarrow\gamma(|x|)\in\llbracket\heartsuit\rrbracket_{\mathfrak{M}_{\Gamma}}({\widehat{\phi_{1}}}^{y_{1}},\dots,{\widehat{\phi_{n}}}^{y_{n}})$
by (8) $\displaystyle\Longleftrightarrow x\heartsuit\lceil
y_{1}:\phi_{1}\rceil\cdots\lceil y_{n}:\phi_{n}\rceil\in\Gamma$ by (6).

Next, we need to find a suitable candidate for an MCS from which to build our
quasi-Henkin model. Consider the following sets of inferences:

$\displaystyle\mathit{Inf}_{\textsc{name}a}=$
$\displaystyle\\{\langle\\{\phi[z/x]\mid z\in\mathsf{iVar}\\},\forall
x.\phi\rangle\mid\phi\in\mathrm{CPL}(\mathrm{\Lambda},\Sigma),x\in\mathsf{iVar}\\}$
$\displaystyle\mathit{Inf}_{\textsc{name}b}=$
$\displaystyle\\{\langle\\{\left(\phi_{1}\leftrightarrow\psi_{1}\right)[z/x],\dots,\left(\phi_{n}\leftrightarrow\psi_{n}\right)[z/x]\mid
z\in\mathsf{iVar}\\},$ $\displaystyle\forall x.$
$\displaystyle\left(x\heartsuit\lceil x:\phi_{1}\rceil\dots\lceil
x:\phi_{n}\rceil\leftrightarrow x\heartsuit\lceil x:\psi_{1}\rceil\dots\lceil
x:\psi_{n}\rceil\right)\rangle\mid\vec{\phi},\vec{\psi}\in\mathrm{CPL}(\mathrm{\Lambda},\Sigma),x\in\mathsf{iVar}\\}$
$\displaystyle\mathit{Inf}_{\textsc{name}}=$
$\displaystyle\mathit{Inf}_{\textsc{name}a}\cup\mathit{Inf}_{\textsc{name}b}$
$\displaystyle\mathit{Inf}_{\flat\Lambda}=$
$\displaystyle\\{\langle\\{\bigwedge\limits_{j\leq\flat\Lambda(\heartsuit)(i)}\phi_{i}[z_{j}/y_{i}]\to\neg
x\heartsuit\dots\lceil
y_{i}:\bigvee\limits_{j\leq\flat\Lambda(\heartsuit)(i)}y_{i}=z_{j}\rceil\dots\mid\vec{z}\in\mathsf{iVar}\\},$
$\displaystyle\qquad\qquad\neg x\heartsuit\dots\lceil
y_{i}:\phi_{i}\rceil\dots\rangle\mid\vec{\phi}\in\mathrm{CPL}(\mathrm{\Lambda},\Sigma),x\in\mathsf{iVar},\heartsuit\in\Lambda,\flat\Lambda(\heartsuit)(i)\neq\infty\\}$
$\displaystyle\mathit{Inf}=$
$\displaystyle\mathit{Inf}_{\textsc{name}}\cup\mathit{Inf}_{\flat\Lambda}$

Let us begin with

######  Claim 13.

Assume $|\mathsf{iVar}|=\kappa\geq|\mathrm{\Lambda}\cup\Sigma\cup\omega|$.
Then any $\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}$-consistent set of
formulas $\Gamma$ s.t. $|\\{x\in\mathsf{iVar}\mid x\mbox{ fresh for
}\Gamma\\}|=\kappa$ (in particular, any consistent set of sentences) satisfies
condition 4 of Theorem 10 for $\mathit{Inf}_{\textsc{name}}$.

######  Proof 3.3.

We begin by observing that

(a) If
$\Gamma^{\prime}\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\phi[z/x]$ and
$z$ is fresh for $\Gamma^{\prime},x,\phi$, then
$\Gamma^{\prime}\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\forall x.\phi$

The proof of this fact is perfectly standard, but working with an Enderton-
style axiomatization is particularly convenient for such reasoning: We have a
finite $\Gamma^{\prime}_{0}\subseteq_{\mathit{fin}}\Gamma^{\prime}$ s.t.
$\Gamma^{\prime}_{0}\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\phi[z/x]$.
Then one uses the Deduction Theorem (cf. Remark 11) to obtain
$\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\bigwedge\Gamma^{\prime}_{0}\to\phi[z/x]$.
However, even with an Enderton-style axiomatization it is still the case444In
fact, a variant of the Generalization Theorem is available even for non-empty
contexts as long as the quantified variable does not occur freely therein, cf.
[Enderton72, p. 117]. that
$\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\chi$ implies
$\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\forall z.\chi$, hence
$\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\forall
z.(\bigwedge\Gamma^{\prime}_{0}\to\phi[z/x])$. The rest is an easy exercise
using En3, En4 and renaming of bound variables thanks to En2.

The condition (a) tells us that $\Gamma$ itself does respect
$\mathit{Inf}_{\textsc{name}a}$ by assumption. But if $|X|<\kappa$, then there
are $\kappa$-many $z\in\mathsf{iVar}$ that are fresh for $\Gamma\cup
X\cup\\{\phi\\}$. For any such $z$, (a) would hold also for
$\Gamma^{\prime}=\Gamma\cup X$. This gives condition 4 for
$\mathit{Inf}_{\textsc{name}a}$.

For $\mathit{Inf}_{\textsc{name}b}$, let us observe that (a) allows to infer
that

If
$\Gamma^{\prime}\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\left(\phi_{1}\leftrightarrow\psi_{1}\right)[z/x]\wedge\dots\wedge\left(\phi_{n}\leftrightarrow\psi_{n}\right)[z/x]$
and $z\mbox{ fresh for }\Gamma^{\prime},\vec{\phi},\vec{\psi},x$, then
$\Gamma\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\forall
x.\left(\left(\phi_{1}\leftrightarrow\psi_{1}\right)\wedge\dots\wedge\left(\phi_{n}\leftrightarrow\psi_{n}\right)\right)$.

Now an application of the congruence rule (Remark 4) completes the proof of
the claim.

######  Claim 14.

Assume $|\mathsf{iVar}|=\kappa\geq|\mathrm{\Lambda}\cup\Sigma\cup\omega|$.
Then any $\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}$-consistent set of
formulas $\Gamma$ s.t. $|\\{x\in\mathsf{iVar}\mid x\mbox{ fresh for
}\Gamma\\}|=\kappa$ (in particular, a consistent set of _sentences_) satisfies
condition 4 of Theorem 10 for $\mathit{Inf}_{\flat\Lambda}$.

######  Proof 3.4.

We begin by observing that

(b) If
$\Gamma^{\prime}\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\neg(\bigwedge\limits_{j\leq\flat\Lambda(\heartsuit)(i)}\phi_{i}[z_{j}/y_{i}]\wedge
x\heartsuit\dots\lceil
y_{i}:\bigvee\limits_{j\leq\flat\Lambda(\heartsuit)(i)}y_{i}=z_{j}\rceil\dots)$
for some $\vec{z}\mbox{ fresh for }\Gamma^{\prime},x,y_{i},\vec{\phi}$, then
$\Gamma^{\prime}\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\neg
x\heartsuit\dots\lceil y_{i}:\phi_{i}\rceil\dots$

This is shown by first following the proof of (a) and finding a finite
$\Gamma^{\prime}_{0}\subseteq_{\mathit{fin}}\Gamma^{\prime}$ s.t.

$\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\Gamma^{\prime}_{0}\to\neg\exists
z_{1},\dots,z_{\flat\Lambda(\heartsuit)(i)}.(\bigwedge\limits_{j\leq\flat\Lambda(\heartsuit)(i)}\phi_{i}[z_{j}/y_{i}]\wedge
x\heartsuit\dots\lceil
y_{i}:\bigvee\limits_{j\leq\flat\Lambda(\heartsuit)(i)}y_{i}=z_{j}\rceil\dots).$

Applying BdPL♭Λ proves (b).

The condition (b) tells us that $\Gamma$ itself does respect
$\mathit{Inf}_{\flat\Lambda}$ by assumption. But if $|X|<\kappa$, then there
are $\kappa$-many $z\in\mathsf{iVar}$ which are fresh for $\Gamma\cup
X\cup\\{\phi_{1},\dots,\phi_{\mathsf{ar}{\heartsuit}}\\}$ and distinct from
$x$ and $\vec{y}$. For any tuple of such $z$’s, (b) would hold also for
$\Gamma^{\prime}=\Gamma\cup X$. This gives condition 4 for
$\mathit{Inf}_{\flat\Lambda}$.

######  Claim 15.

Assume $|\mathsf{iVar}|=\kappa\geq|\mathrm{\Lambda}\cup\Sigma\cup\omega|$.
Then any $\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}$-consistent set of
formulas $\Gamma$ s.t. $|\\{x\in\mathsf{iVar}\mid x\mbox{ fresh for
}\Gamma\\}|=\kappa$ (in particular, a consistent set of _sentences_) can be
extended to a maximally
$\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}$-consistent set of formulas
$\Gamma^{\prime}$ s.t.

  * •

whenever $\exists x.\phi\in\Gamma^{\prime}$, then
$\phi[z/x]\in\Gamma^{\prime}$ for some $z\in\mathsf{iVar}$

  * •

whenever $\exists x.\left(x\heartsuit\lceil x:\phi_{1}\rceil\dots\lceil
x:\phi_{n}\rceil\wedge\neg x\heartsuit\lceil x:\psi_{1}\rceil\dots\lceil
x:\psi_{n}\rceil\right)\in\Gamma^{\prime}$, then there is
$z~{}\in~{}\mathsf{iVar}$ and $i\leq n$ s.t.
$\neg\left(\phi_{i}\leftrightarrow\psi_{i}\right)[z/x]\in\Gamma^{\prime}$.

  * •

whenever $x\heartsuit\dots\lceil y_{i}:\phi_{i}\rceil\dots\in\Gamma^{\prime}$
and $\flat\Lambda(\heartsuit)(i)\neq\infty$, then there are
$z_{1},\dots,z_{\flat\Lambda(\heartsuit)(i)}$ s.t. $x\heartsuit\dots\lceil
y_{i}:\bigvee\limits_{j\leq\flat\Lambda(\heartsuit)(i)}y_{i}=z_{j}\rceil\dots\in\Gamma^{\prime}$
and moreover $\phi_{i}[z_{j}/y_{i}]\in\Gamma^{\prime}$ for each
$j\leq\flat\Lambda(\heartsuit)(i)$.

######  Proof 3.5.

This immediately follows from the preceding Claim, Theorem 10 and the fact
$\Gamma^{\prime}$ is a MCS.

######  Proof 3.6 (Proof of Theorem 9).

Recall Definition 3.3. We will build our quasi-Henkin model using
$\Gamma^{\prime}$. Satisfaction of condition 5 follows then directly from the
first item in Claim 15, i.e., from being closed under
$\mathit{Inf}_{\textsc{name}a}$. Hence, we just need to define a transition
structure $\gamma$ on $C_{\Gamma^{\prime}}$ and for this purpose, we need to
find for each $|x|$ a suitable $t\in TC_{\Gamma^{\prime}}$ s.t. when
$\gamma(|x|)$ is defined as $t$, the condition 6 is satisfied.

Assume then $\mathsf{Rank1}$ has enough schematic variables to name all
elements of $\mathrm{CPL}(\mathrm{\Lambda},\Sigma)$; let
$\boldsymbol{p}_{\phi}$ be the schematic variable corresponding to $\phi$
under some fixed assignment. For each $x$, we can define an evaluation
$\tau_{x}(\boldsymbol{p}_{\psi})=\widehat{\psi}^{x}$. Note that for each pair
of distinct $x$ and $y$ we have that $\tau_{x}(\boldsymbol{p}_{x=y})$ is a
singleton, thanks to the definition of $C_{\Gamma^{\prime}}$.

Thus, let us define for each $x\in\mathsf{iVar}$ the set

$\Psi_{x}:=\\{\epsilon\heartsuit\boldsymbol{p}_{\psi^{\circ}_{1}}\dots\boldsymbol{p}_{\psi^{\circ}_{n}}\mid\psi_{1},\dots,\psi_{n}\in\mathrm{CPL}(\mathrm{\Lambda},\Sigma)\text{
and }\epsilon(x\heartsuit\lceil x\\!:\\!\psi^{\circ}_{1}\rceil\dots\lceil
x\\!:\\!\psi^{\circ}_{n}\rceil)\in\Gamma^{\prime}\\},$

where $\epsilon$ is either nothing or negation and for each
$i\leq\mathsf{ar}{\heartsuit}$, $\psi^{\circ}_{i}$ is either:

  * •

$\psi_{i}$ itself, if $\flat\Lambda(\heartsuit)(i)=\infty$ or

  * •

$\bigvee\limits_{j\leq\flat\Lambda(\heartsuit)(i)}x=z_{j}$ otherwise, where
$z_{1},\dots,z_{\flat\Lambda(\heartsuit)(i)}$ are s.t.

    * –

$x\heartsuit\dots\lceil
x:\bigvee\limits_{j\leq\flat\Lambda(\heartsuit)(i)}x=z_{j}\rceil\dots\in\Gamma^{\prime}$
and moreover

    * –

$\psi_{i}[z_{j}/x]\in\Gamma^{\prime}$ for each
$j\leq\flat\Lambda(\heartsuit)(i)$.

Furthermore, let us define a colouring $\mathfrak{c}_{x}$ of schematic
variables which assigns $fin$ to every $\boldsymbol{p}_{\bigvee\limits_{j\leq
m}x=z_{m}}$, where $z_{1},\dots,z_{m}$ is any finite sequence of variables and
$\infty$ to every other $\boldsymbol{p}_{\psi}$. It is clear that $\tau_{x}$
respects $\mathfrak{c}_{x}$. We have:

######  Claim 16.

$\Psi_{x}$ is $\mathfrak{c}_{x}$-consistent wrt $\tau_{x}$, i.e.,

$\Psi_{x}\cup\\{\boldsymbol{P}\sigma\mid\sigma:\mathsf{sVar}\to\mathsf{Prop}(\mathsf{sVar})\text{
and
}\boldsymbol{A}/\boldsymbol{P}\in\flat\kern-1.4pt\flat\Lambda_{\mathfrak{c}}(\mathcal{R})\text{
s.t. }C_{\Gamma^{\prime}},\tau_{x}\models\boldsymbol{A}\sigma\\}.$

is propositionally consistent.

######  Proof 3.7.

Assume it is not. By compactness of the classical propositional calculus, a
contradiction can be then derived already from a certain finite subset of
$\Psi_{x}$ and finitely many $\boldsymbol{P}\sigma$ s.t.
$\boldsymbol{A}/\boldsymbol{P}\in\flat\kern-1.4pt\flat\Lambda_{\mathfrak{c}}(\mathcal{R})$
and $C_{\Gamma^{\prime}},\tau_{x}\models\boldsymbol{A}\sigma$. Given the
definition of $\tau_{x}$ and $\Psi_{x}$, this directly contradicts the fact
that $\Gamma^{\prime}$ is supposed to be a MCS closed under all instances of
axioms Onestep($\mathcal{R}$) and BdPL♭Λ in Table 1.

By Definition 3.1 of $\flat\Lambda$-S1SC, Claim 16 implies that $\Psi_{x}$ is
one-step satisfiable wrt $\tau_{x}$, i.e.,

$\textstyle\bigcap_{\phi\in\Psi_{x}}\llbracket\phi\rrbracket_{TC_{\Gamma^{\prime}},\tau_{x}}=\\{\epsilon{[\\![\heartsuit]\\!]}_{C_{\Gamma}^{\prime}}\widehat{\psi^{\circ}_{1}}^{x}\dots\widehat{\psi^{\circ}_{n}}^{x}\mid\psi_{1},\dots,\psi_{n}\in\mathrm{CPL}(\mathrm{\Lambda},\Sigma)\text{
and }\\\ \epsilon(x\heartsuit\lceil x\\!:\\!\psi^{\circ}_{1}\rceil\dots\lceil
x\\!:\\!\psi^{\circ}_{n}\rceil)\in\Gamma^{\prime}\\}\neq\emptyset.$

Now use the Axiom of Choice to define $\gamma(|x|)$ to be a representative of
this non-empty intersection for every $|x|$ (strictly speaking, for an
arbitrarily chosen representative of this equivalence relation), automatically
yielding the condition 6 of Definition 3.3.

######  Remark 17.

The similarities and differences between CPL and languages like
$\mathrm{H}_{\mathrm{\Lambda}}(@)$ and its extensions to be discussed in § 4
are best appreciated by comparing the proof of Theorem 9 with earlier hybrid
ones [SchroderPattinson10]. In the predicate case:

  * •

not only one-step rules, but also non-standard naming and pasting rules of
[SchroderPattinson10] can be expressed as ordinary first-order axioms.

  * •

As we are going to discuss now, the Henkin-style completeness proof directly
leads to the Omitting Types theorem. It is not clear how to obtain such a
result for a language like $\mathrm{H}_{\mathrm{\Lambda}}(@)$ studied in
[SchroderPattinson10]; the presence of a binding and/or quantification
mechanism seems essential in the proof. Recall again that the presence of such
a mechanism also allowed us to reuse (equivalence classes of) variables as
building block of models instead of Henkin-style constants.

###  3.4. Omitting Types Theorem

The Omitting Types Theorem is a standard result of model theory. Goldblatt
[goldblatt1993:abstract, § 8.2] shows how to establish it using the Abstract
Henkin Principle. Here is a more detailed description how to obtain it in our
setting. In this section, we assume that the entire
$\mathrm{CPL}(\mathrm{\Lambda},\Sigma)$ is countable and we keep these
countable $\mathrm{\Lambda}$ and $\Sigma$ fixed and implicit.

Fix a finite subset of $\mathsf{iVar}$ $\\{x_{1},\dots,x_{k}\\}$ and denote
the set of all formulas whose free variables are contained in
$\\{x_{1},\dots,x_{k}\\}$ as $\mathrm{CPL}(k)$. Thus, the set of sentences can
be written as $\mathrm{CPL}(0)$. Recall that a $k$-_type_ (sometimes called a
_complete type_) is a maximal consistent subset of $\mathrm{CPL}(k)$;
sometimes, one also uses the term _partial type_ for consistent yet not
maximal subsets of $\mathrm{CPL}(k)$. For any given
$\Gamma\subseteq\mathrm{CPL}(0)$ and any (partial or total) $k$-type $\Delta$,
say that $\Delta$ is _principal over $\Gamma$_ if there is
$\phi\in\mathrm{CPL}(k)$ consistent with $\Gamma$ s.t.
$\forall\psi\in\Delta.\Gamma\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\phi\to\psi$.
Note here that for complete types, we can assume that $\phi\in\Delta$. Say
that a model $\mathfrak{M}=(C,\gamma,I)$ _realizes_ a (partial or total)
$k$-type $\Delta$ if
$\bigcap\limits_{\psi\in\Delta}\llbracket\psi\rrbracket^{x_{1},\dots,x_{k}}_{C}\neq\emptyset$,
where as before

$\llbracket\phi\rrbracket^{x_{1},\dots,x_{k}}_{C}=\\{(c_{1},\dots,c_{k})\in
C\mid\mathfrak{M},v[c_{1}/x_{1}]\dots[c_{k}/x_{k}]\models\phi\\};$

a $k$-type is _omitted_ by $\mathfrak{M}$ if it is not realized by it.

Note that for complete types, one consequence of being non-principal is that
$\Delta$ is neither entailed by $\Gamma$ nor inconsistent with it (maximal
consistent sets are closed under finite conjuctions).

######  Theorem 18 (Omitting Types).

Whenever a set of rules $\mathcal{R}$ is _$\flat\Lambda$ -S1SC_ for a
$\Lambda$-structure over $T$ that is adequate for $\flat\Lambda$, $\Gamma$ is
a consistent set of sentences and $\Delta$ is a (complete or partial)
$k$-type non-principal over $\Gamma$, $\Gamma$ has a model omitting $\Delta$.

######  Proof 3.8.

We only need to refine somewhat the proof of the completeness theorem by using
a richer set of inferences than $Inf$. Consider

$Inf_{\Delta}=Inf\cup\\{\langle\\{\sigma[z_{1}\dots z_{k}/x_{1}\dots
x_{k}]\mid\sigma\in\Delta\\},\bot\rangle\mid z_{1},\dots,z_{k}\text{ distinct
els. of }\mathsf{iVar}\\}$

(we have not formally defined simultaneous substitution, but it should be
clear how to extend conventions introduced in § 2). We claim that the
condition 4 of Theorem 10 is satisfied with $\kappa=\omega$. For assume it is
not. Then there exists a finite set $\Delta\subseteq\mathrm{CPL}$ and a finite
tuple of distinct variables $z_{1},\dots,z_{k}$ s.t. (*) $\Gamma\cup\Delta$ is
consistent but

$\Gamma\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\bigwedge\Delta\to\sigma[z_{1}\dots
z_{k}/x_{1}\dots x_{k}]$ for every $\sigma\in\Delta$.

Let $\vec{z^{\prime}}$ be a sequence containing all the variables in $\Delta$
different from $z_{1}\dots z_{k}$ and
$\delta=\exists\vec{z^{\prime}}.\bigwedge\Delta$. Then we have

(**)
$\Gamma\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\delta\to\sigma[z_{1}\dots
z_{k}/x_{1}\dots x_{k}]$ for every $\sigma\in\Delta$

and consequently, setting $\delta^{\prime}$ to be $\delta[x_{1}\dots
x_{k}/z_{1}\dots z_{k}]$

(***)
$\Gamma\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\delta^{\prime}\to\sigma$
for every $\sigma\in\Delta$

(in deriving (**) and (***) we obviously use the fact that $\Gamma$ is a set
of _sentences_).

At the same time, $\Gamma$ being a set of sentences yields that
$\delta^{\prime}$ is consistent with $\Gamma$ by virtue of (*). This entails a
contradiction with non-principality of $\Delta$ over $\Gamma$. The rest
proceeds as in the completeness proof.

######  Remark 19.

Goldblatt [goldblatt1993:abstract, § 8.2] points out this can be extended to
simultaneously omitting a countable set of non-principal types.

Here is a typical application adapted from the monograph of Chang and Keisler
[ChangK90, Ch 2.2, p. 83]: $\omega$-logic, $\omega$-rule and
$\omega$-completeness.

Given any $T$, $\Lambda$ and $\mathcal{R}$ within the scope of our
completeness result, extend $\Lambda$ with a countable family of propositional
atoms (cf. Definition 2) $\\{\,\mathsf{is}\,\underline{n}\mid
n\in{\mathbb{N}}\\}\cup\\{\,\mathsf{is}\,\mathsf{nat}\\}$. By similar
considerations as in Remark 2, the completeness result is not affected by such
extensions.

######  Remark 20.

Of course, we could alternatively extended $\Sigma$ with corresponding
predicate symbols, which would be even easier from the point of view of
directly applying Theorems 10 and 18, but would also have a less coalgebraic
flavour.

Consider now the following set of sentences in the extended language:

$\displaystyle\Gamma_{N}=$ $\displaystyle\,\\{\forall
x.x\,\mathsf{is}\,\underline{n}\to(x\,\mathsf{is}\,\mathsf{nat}\wedge\neg
x\,\mathsf{is}\,\underline{m})\mid n,m\in{\mathbb{N}},n\neq m\\}\,\cup$
$\displaystyle\,\\{\forall x,y.x\,\mathsf{is}\,\underline{n}\wedge
y\,\mathsf{is}\,\underline{n}\to x=y\mid n\in{\mathbb{N}}\\}\,\cup$
$\displaystyle\\{\exists x.x\,\mathsf{is}\,\underline{n}\mid
n\in{\mathbb{N}}\\}.$

An $\omega$-_model_ is any model of $\Gamma_{N}$ where, moreover, the
denotation of $\,\mathsf{is}\,\mathsf{nat}$ is the set-theoretical sum of all
“$\,\mathsf{is}\,\underline{n}$”. A theory $\Gamma$ is $\omega$-_complete_ if
$\Gamma\cup\Gamma_{N}$ is closed under the $\omega$-_rule_ :

$\forall x.x\,\mathsf{is}\,\mathsf{nat}\to\phi(x)\forall
x.x\,\mathsf{is}\,\underline{n}\to\phi(x)\quad n\in{\mathbb{N}}$

One can use the Omitting Types theorem to show the following:

######  Corollary 21.

Assume that a set of rules $\mathcal{R}$ is _$\flat\Lambda$ -S1SC_ for a
$\Lambda$-structure over $T$ is adequate for $\flat\Lambda$, and $\Gamma$ is a
set of sentences s.t. $\Gamma\cup\Gamma_{N}$ is consistent. If $\Gamma$ is
$\omega$-complete, then $\Gamma$ has an $\omega$-model.

######  Proof 3.9 (Sketch).

Consider

$\Delta(x)=\\{\neg(x\,\mathsf{is}\,\underline{n})\mid
n\in{\mathbb{N}}\\}\cup\\{x\,\mathsf{is}\,\mathsf{nat}\\}.$

Pick any $\phi(x)\in\mathrm{CPL}(1)$ s.t.
$x\,\mathsf{is}\,\mathsf{nat}\wedge\phi(x)$ is consistent with
$\Gamma\cup\Gamma_{N}$. Then

$\displaystyle\Gamma\cup\Gamma_{N}\not\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\forall
x.(x\,\mathsf{is}\,\mathsf{nat}\to\neg\phi(x))$
$\displaystyle\Longrightarrow\qquad$
$\displaystyle\Gamma\cup\Gamma_{N}\not\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\forall
x.(x\,\mathsf{is}\,\underline{n}\to\neg\phi(x))\text{ for some
}n\in{\mathbb{N}}$ $\displaystyle\text{(by }\omega-\text{completeness),}$
$\displaystyle\Longleftrightarrow\qquad$
$\displaystyle\Gamma\cup\Gamma_{N}\not\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\phi(x)\to\neg(x\,\mathsf{is}\,\underline{n})\text{
for some }n\in{\mathbb{N}}.$

On the other hand, if

$\Gamma\cup\Gamma_{N}\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}x\,\mathsf{is}\,\mathsf{nat}\to\neg\phi(x)$

and at the same time

$\Gamma\cup\Gamma_{N}\vdash^{\mathcal{H}\mathcal{R}}_{\flat\Lambda}\phi(x)\to
x\,\mathsf{is}\,\mathsf{nat},$

then $\phi(x)$ is inconsistent with $\Gamma\cup\Gamma_{N}$. Thus, $\Delta(x)$
is non-principal over $\Gamma\cup\Gamma_{N}$ and hence, $\Gamma\cup\Gamma_{N}$
has a model omitting it. Such a model is an $\omega$-model.

As discussed by Chang and Keisler [ChangK90, Ch 2.2], it follows that we can
extend our deductive apparatus with $\Gamma_{N}$ as additional axioms and
$\omega$-rule as an additional rule of proof and consistency in this extended
system is equivalent to the existence of an $\omega$-model.

Such examples are worth contrasting with the incompleteness result (Theorem
22) we are going to present next.

###  3.5. $\omega$-boundedness and Failure of Completeness

In this subsection, we show that there is a substantial gap between S1SC and
finitary S1SC as conditions allowing for strong completeness, by proving that
within a larger class of _$\omega$ -bounded_ structures, the bounded
structures are the only ones that satisfy compactness. Here,
$\omega$-boundedness of an operator means informally that its satisfaction can
always be established by looking only at a finite subset of the successors,
without however requiring a fixed bound on their number. In examples for this
property, we concentrate on cases additionally satisfying finitary one-step
compactness (Definition 3.1), a condition essentially necessary for overall
compactness and that will moreover become important in our forays into model
theory (§ 5). In the whole subsection, to keep things simple we work with
unary $\heartsuit\in\mathrm{\Lambda}$.

[$\omega$-Bounded operators] A modal operator $\heartsuit$ is _$\omega$
-bounded_ if for each set $X$ and each $A\subseteq X$,

${[\\![\heartsuit]\\!]}_{X}(A)=\bigcup_{B\subseteq_{\mathit{fin}}A}{[\\![\heartsuit]\\!]}_{X}(B).$

[Nonstandard subdistributions] We generally write $\mathcal{S}$ for the
discrete subdistribution functor, i.e. $\mathcal{S}(X)$ consists of real-
valued discrete measures $\mu$ on $X$ such that $\mu(X)\leq 1$, and for maps
$f$, $\mu(f)$ takes image measures. As a variant of this functor, we consider
the the discrete subdistributions functor $\mathcal{S}^{\mathit{rc}}$ where
measures take values in real-closed fields. Explicitly: we intend to model
Markov chains with non-standard probabilities; these consist of a set $X$ of
states, and at each state $x$ an $R_{x}$-valued transition distribution
$\mu_{x}$, where $R_{x}$ is a real-closed field (i.e. a model of the first-
order theory of the reals). These structures are coalgebras for the functor
$T$ which maps a set $X$ to the set of pairs $(R,\mu)$ where $R$ is a real-
closed field and $\mu$ is an $R$-valued discrete subdistribution on $X$ (again
meaning that $\mu(X)\leq 1$). This functor is in fact class-valued, which
however does not affect the applicability of our coalgebraic analysis (which
never requires iterated application of the coalgebraic type functor, e.g. it
does not use the terminal sequence). We take the modal signature $\Lambda$ to
consist of the operators $\langle p\rangle$ (‘with probability more than $p$’)
for $p\in[0,1]\cap{\mathbb{Q}}$.

We show that the $\langle p\rangle$ are $\omega$-bounded and that the arising
logic $\mathcal{L}$ is finitary one-step compact. To see the former, let
$(R,\mu)\in TX$ and let $A\subseteq X$ such that $\mu\models\langle p\rangle
A$, i.e. $\sum_{x\in A}\mu(x)>p$. Then there exists
$B\subseteq_{\mathit{fin}}A$ such that $\sum_{x\in B}\mu(x)>p$, i.e.
$\mu\models\langle p\rangle B$. Since $\langle p\rangle$ is clearly monotone,
this implies that ${[\\![\langle
p\rangle]\\!]}_{X}(A)=\bigcup_{B\subseteq_{\mathit{fin}}A}{[\\![\langle
p\rangle]\\!]}_{X}(B)$, as required.

To show that $\mathcal{L}$ is finitary one-step compact, let
$\Phi\subseteq\mathsf{Prop}(\Lambda(\mathcal{P}_{\mathit{fin}}(X)))$ be
finitely satisfiable. Extend the standard language of real arithmetic with a
constant symbol $c_{x}$ for each element of $X$, obtaining a language $L$.
Then satisfaction of a formula in
$\mathsf{Prop}(\Lambda(\mathcal{P}_{\mathit{fin}}(X)))$ by $\mu\in TX$
translates into a first-order formula over $L$ with $c_{x}$ representing
$\mu(x)$; specifically, the translation $t$ commutes with the Boolean
connectives and translates formulas $\langle p\rangle A$ with
$A\in\mathcal{P}_{\mathit{fin}}(X)$ into $\sum_{x\in A}c_{x}>p$. Applying $t$
to $\Phi$ and introducing additional formulas $c_{x}\geq 0$ for all $x\in X$
and $\sum_{x\in A}c_{x}\leq 1$ for all $A\in\mathcal{P}_{\mathit{fin}}(X)$
thus produces a finitely satisfiable, and hence satisfiable, set of first-
order formulas over $L$. A model of this set consists of a real-closed field
$R$ and interpretations $\hat{c}_{x}\in R$ of the constants $c_{x}$ such that
putting $\mu(x)=\hat{c}_{x}$ defines a discrete subdistribution (note that
$\sum_{x\in A}\hat{c}_{x}\leq 1$ for all $A\in\mathcal{P}_{\mathit{fin}}(X)$
implies $\sum_{x\in X}\hat{c}_{x}\leq 1$), which then yields a model $(R,\mu)$
of $\Phi$.

[Zero-dimensional subdistributions] Fix a zero-dimensional closed (hence
compact) subset $Z\subseteq[0,1]$, e.g. a discrete set or the Cantor space,
and let $\mathcal{S}^{Z}$ be the associated _zero-dimensional discrete
subdistributions functor_ , i.e. the subfunctor of the subdistribution functor
$\mathcal{S}$ where probabilities of finite sets of states are restricted to
take values in $Z$:

$\mathcal{S}^{Z}(X)=\\{\mu\in\mathcal{S}(X)\mid\forall
A\in\mathcal{P}_{\mathit{fin}}(X).\,\mu(A)\in Z\\}.$

Moreover, we restrict the probabilities $p$ in operators $\langle p\rangle$ to
be such that $(p,1]\cap Z$ is clopen in $Z$; since $Z$ is zero-dimensional,
there exist enough such $p$ to separate all values in $Z$. As before, all
these operators are $\omega$-bounded. It remains to show that the logic is
finitary one-step compact. So let
$\Phi\subseteq\mathsf{Prop}(\Lambda(\mathcal{P}_{\mathit{fin}}(X)))$ be
finitely satisfiable. Note that the space $Z^{X}$, equipped with the product
topology, is compact. We equip $\mathcal{S}^{Z}(X)$ with the subspace topology
in $Z^{X}$. Observe that the condition $\forall
A\in\mathcal{P}_{\mathit{fin}}(X).\,\mu(A)\in Z$ already implies $\mu(X)\leq
1$; since for $A\in\mathcal{P}_{\mathit{fin}}(X)$, the summation map $Z^{A}\to
Z$ is continuous (this would fail for infinite $A$), it follows that
$\mathcal{S}^{Z}(X)$ is closed in $Z^{X}$, hence compact.

By the restriction placed on the indices $p$ in modal operators $\langle
p\rangle$, and again using continuity of finite summation, we have that for
every formula $\langle p\rangle A$ with $A\in\mathcal{P}_{\mathit{fin}}(X)$,
the extension

${[\\![\langle p\rangle A]\\!]}=\\{\mu\in\mathcal{S}^{Z}(X)\mid\mu(A)>p\\}$

is clopen in $\mathcal{S}^{Z}(X)$. As clopen sets are closed under Boolean
combinations, we thus have that the extension of every formula in
$\mathsf{Prop}(\Lambda(\mathcal{P}_{\mathit{fin}}(X)))$ is clopen in
$\mathcal{S}^{Z}(X)$. Let $\mathfrak{A}$ denote the family of clopens induced
in this way by formulas in $\Phi$. Finite satisfiability of $\Phi$ implies
that $\mathfrak{A}$ has the finite intersection property, and hence has non-
empty intersection by compactness of $\mathcal{S}^{Z}(X)$. It follows that
$\Phi$ is satisfiable. Structures which are $\omega$-bounded without being
$k$-bounded fail strong completeness. To state this observation in full
generality, we require the notion of _propositional atom_ as defined
previously (Definition 2).

######  Theorem 22.

Whenever a $\Lambda$-structure makes some $\heartsuit\in\mathrm{\Lambda}$
$\omega$-bounded without being $k$-bounded for any $k\in\omega$, strong
completeness fails whenever either $\Sigma$ contains a predicate symbol of
positive arity or $\mathrm{\Lambda}$ contains a propositional atom.

######  Proof 3.10.

Assume $P\in\Sigma$ is a predicate symbol of positive arity, w.l.o.g. unary,
and $\heartsuit\in\mathrm{\Lambda}$ is as in the statement of theorem.
Consider

$\displaystyle\Delta(x)=$ $\displaystyle\\{\neg x\heartsuit\lceil
y:P(y)\rceil\\}\;\cup$ $\displaystyle\\{\forall
y_{1},...,y_{k}.(P(y_{1})\wedge\dots\wedge P(y_{k})\to\neg x\heartsuit\lceil
y:y=y_{1}\vee...\vee y=y_{k}\rceil)\mid k\in\omega\\}.$

Clearly, every finite subset of $\Delta(x)$ is satisfiable in a model based on
a coalgebra witnessing the failure of $k$-boundedness for a suitably large
$k$. However, a coalgebraic model satisfying the whole $\Delta(x)$ would
witness the failure of $\omega$-boundedness. This means that $\Delta(x)$ is a
counterexample to compactness, and hence no finitary deduction system can be
strongly complete. The proof for the case where $\mathrm{\Lambda}$ contains a
propositional atom is entirely analogous.

The probabilistic instances of CPL given by interpreting the probabilistic
modalities $\langle p\rangle$ over nonstandard or zero-dimensional
subdistributions, respectively, and are $\omega$-bounded but fail to be
$k$-bounded for any $k$. Hence they fail to be compact by Theorem 22 (once
equipped with propositional atoms) although they satisfy finitary one-step
compactness (Examples 3.5 and 3.5).

##  4\. Correspondence with Coalgebraic Modal Logic

We next compare the expressivity of CPL with that of various coalgebraic modal
and hybrid logics.

###  4.1. Coalgebraic Standard Translation for CML

The formulas $\mathrm{CML}_{\mathrm{\Lambda}}\Sigma$ of pure (coalgebraic)
modal logic in the modal signature $\mathrm{\Lambda}$ over $\Sigma$ (now all
elements of $\Sigma$ are assumed to be of arity 1) are given by the grammar:

$\mathrm{CML}_{\mathrm{\Lambda}}\Sigma\quad\phi,\psi::=P\mid\bot\mid\phi\to\psi\mid\heartsuit(\phi_{1},\dots,\phi_{n}),$

where $P\in\Sigma$.

Satisfaction is defined with respect to $\mathfrak{M}=(C,\gamma,I)$ and a
specific point $c\in C$ in a standard way, see e.g. [SchroderP10fossacs,
SchroderPattinson10].

######  Definition and Proposition 23.

Define the _coalgebraic standard translation_ as

$\displaystyle\mathit{ST}_{x}(P)$ $\displaystyle=P(x),$
$\displaystyle\mathit{ST}_{x}(\heartsuit(\phi_{1},\dots,\phi_{n}))$
$\displaystyle=x\heartsuit\lceil x:\mathit{ST}_{x}(\phi_{1})\rceil\dots\lceil
x:\mathit{ST}_{x}(\phi_{n})\rceil,$ $\displaystyle\mathit{ST}_{x}(\bot)$
$\displaystyle=\bot,$ $\displaystyle\mathit{ST}_{x}(\phi\to\psi)$
$\displaystyle=\mathit{ST}_{x}(\phi)\to\mathit{ST}_{x}(\psi).$

Then for any $\phi\in\mathrm{CML}_{\mathrm{\Lambda}}\Sigma$ and any
$\mathfrak{M}=(C,\gamma,I),v,c$, we have $\mathfrak{M},c\vDash\phi$ iff
$\mathfrak{M},v[x\mapsto c]\vDash\mathit{ST}_{x}(\phi)$.

For example, $\mathit{ST}_{x}(\heartsuit\heartsuit P)=x\heartsuit\lceil
x:x\heartsuit\lceil x:P(x)\rceil\rceil$. This definition is more
straightforward than the standard translation into FOL of modal logic over
ordinary Kripke frames. Moreover, $\mathit{ST}_{x}$ uses only one variable
from $\mathsf{iVar}$, namely $x$ itself. In fact, we can immediately observe
that

######  Proposition 24.

Whenever $\Sigma$ consists entirely of _unary_ predicate symbols, the subset
of $\phi\in\mathrm{CPL}(\Sigma)$ obtained as the image of $\mathit{ST}_{x}$
for a fixed $x\in\mathsf{iVar}$ consists precisely of equality-free and
quantifier-free formulas in the variable $x$.

###  4.2. Hybrid Languages

In this section, we establish the equivalence of CPL with the hybrid languages
$\mathrm{H}_{\mathrm{\Lambda}}(\downarrow\\!,\mathsf{A})$ and
$\mathrm{H}_{\mathrm{\Lambda}}(\forall,@)$. Both correspondences also hold for
ordinary predicate logic over relational structures (FOL) and extend to CPL.
We take this as yet another indication that CPL is natural and well-designed
both as a generalization of FOL and “the” predicate logic cousin of existing
coalgebraic formalisms.

This is our main, but not the only motivation. We progress towards this result
step-by-step, extending the modal language gradually with new hybrid
constructs. In this way, we reveal that a similar correspondence exists
between natural fragments of CPL and weaker hybrid languages, most importantly
between quantifier-free CPL and
$\mathrm{H}_{\mathrm{\Lambda}}(\downarrow\\!,@)$.

Again, obviously the correspondence between fragments of CPL and extensions of
CML is tighter than in the case of FOL and ML only due to the modal flavour of
CPL. However, results such as Corollary 27 are useful spadework: any model-
theoretic tool to be developed—say, a variant of E-F games—would be adequate
for an extended coalgebraic modal formalism (e.g.,
$\mathrm{H}_{\mathrm{\Lambda}}(\downarrow\\!,@)$) iff it is adequate for the
corresponding fragment of CPL (e.g., the variable-free fragment), so we are
free to work with whichever formalism we find more convenient at a given
moment. The straightforward correspondence also provides a good starting point
for an extension of research programme sketched in [tencate2005:model]—see
Remark 31 at the end of this section.

Given a supply of _world variables_ $\mathsf{wVar}$ that we are going to keep
fixed and implicit—in fact, as stated below, _near_ identical to
$\mathsf{iVar}$—we define the following _coalgebraic hybrid languages_

$\rule{0.0pt}{12.91663pt}\par\mathrm{H}_{\mathrm{\Lambda}}(\downarrow\\!,@)$ $\phi,\psi::=$ |  $z\mid P\mid\bot\mid\phi\to\psi\mid\heartsuit(\phi_{1},\dots,\phi_{n})\mid@_{z}\phi$ $\mid$ | $\downarrow\\!z.\phi$
---|---|---
$\mathrm{H}_{\mathrm{\Lambda}}(\downarrow\\!,\mathsf{A})$ $\phi,\psi::=$ |  $z\mid P\mid\bot\mid\phi\to\psi\mid\heartsuit(\phi_{1},\dots,\phi_{n})\mid\mathsf{A}\phi$ $\mid$ | $\downarrow\\!z.\phi$
$\mathrm{H}_{\mathrm{\Lambda}}(\forall,@)$ $\phi,\psi::=$ |  $z\mid P\mid\bot\mid\phi\to\psi\mid\heartsuit(\phi_{1},\dots,\phi_{n})\mid@_{z}\phi$ $\mid$ | $\forall z.\phi$

where $z\in\mathsf{wVar}$. We refer the reader to, e.g, [SchroderPattinson10,
BlackburnC06sl, tencate2005:model] for the semantics. The extension of the
standard translation to these formalism is unproblematic in some cases, just
like in the case of ordinary hybrid logic over Kripke frames:

$\mathit{ST}_{x}(z)=x=z,\quad\mathit{ST}_{x}(\mathsf{A}\phi)=\forall
x.\mathit{ST}_{x}(\phi),\quad\mathit{ST}_{x}(\forall z.\phi)=\forall
z.\mathit{ST}_{x}(\phi).$

One is tempted to put forward also

$\mathit{ST}_{x}(@_{z}\phi)=\mathit{ST}_{x}(\phi)[z/x],\quad\mathit{ST}_{x}(\downarrow\\!z.\phi)=\mathit{ST}_{x}(\phi)[x/z].$

However, with other clauses remaining the same, this would violate our
convention that $[z/x]$ is used only when $z$ is _substitutable_ for $x$; we
would need to interpret it as _capture-avoiding_ substitution. Sadly, this in
turn would entail forsaking the luxury of using just one designated variable
for comprehension. Guillame Malod (see [Cate:2005:CHL]) observed that if we
restrict the supply of variables, a translation along the above lines—indeed
first proposed in the literature, which also goes to show that the present
discussion is less trivial than it might seem—would fail even when embedding
the hybrid logic over Kripke frames in the two-variable fragment of FOL.
Malod’s counterexample used nesting of modalities of level two, but as our
translation uses just one designated variable, $\mathit{ST}$ would go wrong
already on formulas of depth one. Just consider
$\mathit{ST}_{x}(\downarrow\\!z.\Diamond z)$: were we careless about capture
of bound variables, we would obtain $x\Diamond\lceil x:x=x\rceil$, which is a
formula with a completely different meaning. There are two ways out. First is
to redefine

$\displaystyle\mathit{STmod}_{x}(@_{z}\phi)$ $\displaystyle=\forall
x.(x=z\to\mathit{ST}_{x}(\phi)),$ (9)
$\displaystyle\mathit{STmod}_{x}(\downarrow\\!z.\phi)$ $\displaystyle=\forall
z.(x=z\to\mathit{ST}_{x}(\phi)).$ (10)

The second is to keep $\mathit{ST}$ for hybrid formulas as defined above and
change the modal clause instead:

$\mathit{ST}_{x}(\heartsuit(\phi_{1},\dots,\phi_{n}))=x\heartsuit\lceil
y:\mathit{ST}_{y}(\phi_{1})\rceil\dots\lceil
y:\mathit{ST}_{y}(\phi_{n})\rceil,\\\ $ (11)

where $y$ is the first (in some fixed enumeration) variable _not used_ in
$\mathit{ST}_{x}(\phi_{1}),\dots,\mathit{ST}_{x}(\phi_{n})$; by _not used_
here we mean both free and bound usage. Furthermore, to ensure that the
translation works correctly, we have to assume that _neither $x$ nor $y$_
appears in $\mathsf{wVar}$. While the requirement to use more bound variables
can be cumbersome—particularly for infinite sets of formulas—we prefer this
option, as it makes it easier to characterize weaker hybrid languages as
suitable syntactic fragments of CPL.

We can now state a generalization of both Proposition 23 and corresponding
results from the hybrid logic literature—see, e.g., [BlackburnC06sl] for
references:

######  Proposition 25.

For any hybrid formula $\phi$ and any $\mathfrak{M}=(C,\gamma,I),v,c$, we have
$\mathfrak{M},v,c\vDash\phi$ iff $\mathfrak{M},v[x\mapsto
c]\vDash\mathit{ST}_{x}(\phi)$.

As is well-known in the hybrid logic community—see again [BlackburnC06sl] for
references—there is also a translation in the reverse direction for
sufficiently expressive hybrid languages. This also generalizes to our
setting, see Table 2.

Table 2. Coalgebraic Hybrid Translation from quantifier-free CPL to
$\mathrm{H}_{\mathrm{\Lambda}}(\downarrow\\!,@)$

$\mathit{HT}(P(x))$ = |  $@_{x}P$ |  $\mathit{HT}(x=y)$ = | $@_{x}y$
---|---|---|---
$\mathit{HT}(\bot)$ = |  $\bot$ |  $\mathit{HT}(\phi\to\psi)$ = | $\mathit{HT}(\phi)\to\mathit{HT}(\psi)$
$\mathit{HT}(x\heartsuit\lceil y_{1}:\phi_{1}\rceil\dots\lceil
y_{n}:\phi_{n}\rceil)\quad=\quad@_{x}\heartsuit(\downarrow\\!y_{1}.\mathit{HT}(\phi_{1}),\dots,\downarrow\\!y_{n}.\mathit{HT}(\phi_{n}))$

######  Proposition 26.

For any $\phi\in\mathrm{CPL}$ and any $\mathfrak{M}=(C,\gamma,I),v,c$, we have

$\mathfrak{M},v,c\vDash\mathit{HT}(\phi)$ iff $\mathfrak{M},v[x\mapsto
c]\vDash\phi$.

Combining Propositions 26 and 25, we get:

######  Corollary 27.

Whenever $\Sigma$ consists purely of unary predicates (and no function
symbols), $\mathrm{H}_{\mathrm{\Lambda}}(\downarrow\\!,@)$ is expressively
equivalent to the quantifier-free fragment of $\mathrm{CPL}$, assuming
$\mathsf{iVar}$ contains $\mathsf{wVar}$ plus a disjoint infinite supply of
additional individual variables (used for comprehension).

######  Remark 28 (Quantifier-free CPL as the bounded fragment of FOL).

In the case of ordinary FOL, the fragment equivalent to
$\mathrm{H}_{\mathrm{\Lambda}}(\downarrow\\!,@)$ is characterized as the
_bounded fragment_ , see, e.g., [ArecesTenCate07]. In fact, our formula
$x\heartsuit\lceil y:\phi\rceil$, despite being quantifier-free on the
surface, can be described as a form of bounded quantification. This can be
formalized as a result stating that over coalgebras for the covariant powerset
functor (Kripke frames), quantifier-free $\mathrm{CPL}$ is equivalent to the
bounded-fragment of ordinary FOL, where the role of $\heartsuit$ in
$\mathrm{CPL}$ is played by the binary relation symbol $R$ in FOL; details are
left to the reader.

######  Remark 29 (Chang’s original syntax).

As already mentioned, our syntax is slightly different to the original one
proposed by Chang [Chang73]. In that paper, there were no explicit
comprehension variables and even in the enriched syntax which allowed
constants and function terms, the term on the left-hand side of $\heartsuit$
had to be a variable. This variable was reused then on the right side of
$\heartsuit$ as the comprehension variable. In other words, Chang’s
$x\heartsuit\phi(x)$ was equivalent to ours $x\heartsuit\lceil
x:\phi(x)\rceil$. In presence of quantifiers, which can be used to simulate
the effect of capture-avoiding substitution as in $\mathit{STmod}$ (this trick
in fact stems back to Alfred Tarski), the two languages are obviously
equivalent. But when considering fragments, as we do here, the equivalence
breaks down; without quantifiers, Chang’s syntax does not allow (10) and
simple renaming of the comprehension variable on the right-hand side of
$\heartsuit$ as in (11) is not possible either.

There are two usual routes in hybrid logic to achieve full first-order
expressivity. One is to add universal quantifiers over $\mathsf{wVar}$ in
presence of the satisfaction operator $@$. The other is to add the global
modality $\mathsf{A}$ in presence of the downarrow binder $\downarrow\\!$ .
The hybrid translation is extended then as follows:

$\displaystyle\mathit{HT}_{\forall@}(\forall x.\phi)$ $\displaystyle=\forall
x.\mathit{HT}(\phi)$
$\displaystyle\mathit{HT}_{\mathsf{A}\downarrow\\!}(\forall x.\phi)$
$\displaystyle=\downarrow\\!y.\mathsf{A}\downarrow\\!x.\mathsf{A}(y\to\phi)$

In $\mathit{HT}_{\mathsf{A}\downarrow\\!}$ we need the proviso that $y$ is not
occurring in the whole formula.

######  Theorem 30.

$\mathrm{H}_{\mathrm{\Lambda}}(\downarrow\\!,\mathsf{A})$,
$\mathrm{H}_{\mathrm{\Lambda}}(\forall,@)$ and $\mathrm{CPL}$ are expressively
equivalent.

As we can use $\mathit{STmod}_{x}$ now and keep reusing $x$ as the
comprehension variable, it is enough to assume that
$\mathsf{iVar}=\mathsf{wVar}\cup\\{x\\}$. Since $@_{z}\phi$ is definable in
presence of $\mathsf{A}$ (as $\mathsf{A}(z\to\phi)$), $\downarrow\\!$ is
definable by the universal quantifier over $\mathsf{wVar}$ (as $\forall
z.(z\to\phi)$) and $\mathsf{A}$ is definable by combination of $\forall$ and
$@$ (as $\forall y.@_{y}\phi$, where $y$ is not used in $\phi$), we get in
fact seven equivalent languages: $\mathrm{CPL}$, Chang’s original language,
$\mathrm{H}_{\mathrm{\Lambda}}(\downarrow\\!,\mathsf{A})$,
$\mathrm{H}_{\mathrm{\Lambda}}(\forall,@)$,
$\mathrm{H}_{\mathrm{\Lambda}}(\downarrow\\!,\mathsf{A})$ with $@$,
$\mathrm{H}_{\mathrm{\Lambda}}(\forall,@)$ with $\downarrow\\!$ and the jumbo
hybrid language with all connectives introduced above.

######  Remark 31.

The equivalences stated here extend to the case of hybrid languages and
$\mathrm{CPL}$ enriched with quantification over predicates (i.e., second-
order languages). It would be interesting to follow more thoroughly the
program of _coalgebraic abstract model theory_ both above and below
$\mathrm{CPL}$. See Ten Cate’s PhD Thesis [tencate2005:model] for spadework in
abstract model theory below first-order logic.

###  4.3. Semantic Correspondence: The Van Benthem-Rosen Theorem

Our Proposition 24 provides a _syntactic_ characterization of the modal
fragment of our language. In a companion paper [SchroderPL15:jlc], we develop
a _semantic_ , Van Benthem-Rosen style characterization. To compare these two
characterizations, let us briefly recall the details.

In the context of standard Kripke models, expressiveness of modal logic is
characterized by van Benthem’s theorem: modal logic is the bisimulation
invariant fragment of first-order logic in the corresponding signature. The
finitary analogue of this theorem [Rosen97] states that every formula that is
bisimulation invariant _over finite models_ is equivalent _over finite models_
to a modal formula. In the coalgebraic context, replace bisimilarity with
behavioural equivalence [Staton11:lmcs]. Moreover, we need to assume that the
language has ‘enough’ expressive power; e.g., we cannot expect that
bisimulation invariant formulas are equivalent to CML formulas over the empty
similarity type. This is made precise as follows:

A $\Lambda$-structure is _separating_ if, for every set $X$, every element
$t\in TX$ is uniquely determined by the set
$\\{(\heartsuit,A)\mid\heartsuit\in\Lambda\mbox{
$n$-ary},A\in\mathcal{P}(X)^{n},t\in\llbracket\heartsuit\rrbracket_{X}(A)\\}$.

Separation is in general a less restrictive condition than those we needed for
completeness proofs. In particular, separation automatically obtains for
Kripke semantics. It was first used to establish the Hennessy-Milner property
for coalgebraic logics [Pattinson04, Schroder08].

######  Theorem 32 ([SchroderPL15:jlc]).

Suppose that the structure is separating and $\phi(x)$ is a CPL formula with
one free variable. Then $\phi$ is invariant under behavioural equivalence
(over finite models) iff it is equivalent to an infinitary CML formula with
finite modal rank (over finite models).

If we deal with finite similarity types only, the conclusion can be
strengthened:

######  Theorem 33 ([SchroderPL15:jlc]).

Suppose that the structure is separating, $\Lambda$ is finite and $\phi(x)$ is
a CPL formula with one free variable. Then $\phi$ is invariant under
behavioural equivalence (over finite models) iff $\phi$ is equivalent to a
finite CML formula (over finite models).

In fact, we can combine Theorem 33 with the syntactic characterization of
Proposition 24 to obtain

######  Corollary 34.

Whenever $\Sigma$ consists entirely of _unary_ predicate symbols and the
structure is separating, the behaviourally-invariant (over finite structures)
formulas of $\mathrm{CPL}$ in one-free variable are up to equivalence (over
finite structures) precisely the equality-free and quantifier-free formulas in
the single-variable fragment of $\mathrm{CPL}$.

##  5\. First Steps in Coalgebraic Model Theory

We proceed to outline the beginning of coalgebraic model theory, taking a look
at ultraproducts and the downwards Löwenheim-Skolem theorem. In the course of
the technical development, we will import a result on one-step cutfree
complete rule sets established in earlier work [Schroder06,
PattinsonSchroder10].

Recall that if $\mathfrak{U}$ is an ultrafilter on an index set $I$ and
$(X_{i})$ is an $I$-indexed family of nonempty sets, then the _ultraproduct_
$\prod_{\mathfrak{U}}X_{i}$ is defined as

$\textstyle\prod_{\mathfrak{U}}X_{i}=\big{(}\prod_{i\in I}X_{i}\big{)}/\sim$

where $\sim$ is the equivalence relation on $\prod_{i\in I}X_{i}$ defined by

$(x_{i})\sim(y_{i})\iff\\{i\in I\mid x_{i}=y_{i}\\}\in\mathfrak{U}.$

One may regard $\mathfrak{U}$ as a $\\{0,1\\}$-valued measure on $I$; under
this reading, the above definition says that $(x_{i})$ and $(y_{i})$ are
identified under $\sim$ if they are almost everywhere equal. We write elements
of $\prod_{\mathfrak{U}}X_{i}$ and $\prod_{i\in I}X_{i}$ just as $x$, omitting
notation for equivalence classes and accessing the $i$-th component as
$x_{i}$.

Observe that if $X=\prod_{\mathfrak{U}}X_{i}$ is an ultraproduct of sets and
$(A_{i})$ is a family of subsets $A_{i}\subseteq X_{i}$, then

$A=\textstyle\prod_{\mathfrak{U}}A_{i}:=\\{x\mid\\{i\mid x_{i}\in
A_{i}\\}\in\mathfrak{U}\\}$ (12)

is a well-defined subset of $X$ (this is in fact just the way unary predicates
are standardly extended from the components to the ultraproduct). Subsets of
ultraproducts that are of this form are called _admissible_.

######  Lemma 35.

All finite subsets of ultraproducts are admissible.

Ultraproducts of coalgebras will not be determined uniquely; instead, we give
a property-oriented definition and later show existence.

[Quasi-Ultraproducts of Coalgebras] Let $(C_{i})=(X_{i},\xi_{i})_{i\in I}$ be
a family of $T$-coalgebras, and let $\mathfrak{U}$ be an ultrafilter on $I$. A
coalgebra $\xi$ on the set-ultraproduct $X=\prod_{\mathfrak{U}}X_{i}$ is
called a _quasi-ultraproduct_ of the $C_{i}$ if for every family $(A_{i})$ of
subsets $A_{i}\subseteq X_{i}$, every $x\in\prod_{\mathfrak{U}}X_{i}$, and
every $\heartsuit\in\Lambda$,

$\xi(x)\in{[\\![\heartsuit]\\!]}_{X}\textstyle\prod_{\mathfrak{U}}A_{i}\iff\\{i\in
I\mid\xi_{i}(x_{i})\in\llbracket\heartsuit\rrbracket_{C_{i}}(A_{i})\\}\in\mathfrak{U}.$
(13)

The notion of quasi-ultraproduct extends naturally to coalgebraic models using
the standard definition to extend the interpretation of predicates (as
indicated above, Equation (12) recalls the case of unary predicates).

The definition of quasi-ultraproducts is designed in such a way that Łoś’s
theorem, which in the view of ultrafilters as $\\{0,1\\}$-valued measures
states that the ultraproduct satisfies exactly those formulas that hold in
almost all its components, extends to coalgebras:

######  Theorem 36 (Coalgebraic Łoś’s Theorem).

If $\mathfrak{M}=(C,\gamma,V)$ is a quasi-ultraproduct of
$\mathfrak{M}_{i}=(C_{i},\gamma_{i},V_{i})$ for the ultrafilter
$\mathfrak{U}$, then for every tuple $(a^{1},\dots,a^{n})$ of states in $C$,
where $a^{k}=(a^{k}_{i})_{i\in I}$, and for every CPL formula
$\phi(x_{1},\dots,x_{n})$, $C\models\phi(a^{1},\dots,a^{n})\iff\\{i\mid
C_{i}\models\phi(a^{1}_{i},\dots,a^{k}_{i})\\}\in\mathfrak{U}$.

######  Proof 5.1.

Induction over formulas. The cases for Boolean operators and quantifiers are
as in the classical case, and the case for modal operators is exactly by the
quasi-ultraproduct property.

From this theorem, we obtain the usual applications, in particular compactness
(the latter with literally the same proof as in the classical case). The
question is, of course, when quasi-ultraproducts exist. A core observation is

######  Lemma 37.

In the notation of Definition 35, the demands placed on $\xi(x)$ by Condition
(13) constitute a finitely satisfiable set of one-step formulas.

In the proof of this lemma, and on several further occasions, we will need the
fact that the set of all one-step sound one-step rules is _one-step cutfree
complete_ [PattinsonSchroder10]. Instead of repeating the definition of this
term, we state the relevant property directly.

######  Lemma 38.

[Schroder06, Theorem 18 with proof] Let $\Phi$ be a finite subset of
$\Lambda(\mathcal{P}(C))\cup\neg\Lambda(\mathcal{P}(C))$, where
$\neg\Lambda(\mathcal{P}(C))=\\{\neg\heartsuit A\mid\heartsuit
A\in\Lambda(\mathcal{P}(C))\\}$. If $\Phi$ is one-step unsatisfiable, then
there exists a sound one-step rule $\boldsymbol{A}/\boldsymbol{P}$ and a
valuation $\tau:\mathsf{sVar}\to\mathcal{P}(C)$ such that
$C\models\boldsymbol{A}\tau$ and $\boldsymbol{P}\tau=\neg\bigwedge\Phi$.

We then proceed as follows with the open proof of Lemma 37:

######  Proof 5.2 (Proof (Lemma 37)).

Fix finitely many instances of (13) (keeping the same notation) for families
of sets $(A^{j}_{i})_{i\in I}$ and sets $A^{j}=\prod_{\mathfrak{U}}A^{j}_{i}$,
$j=1,\dots,k$. We regard these sets as extensions of unary predicates $P^{j}$
over the $X_{i}$ and over $X$, respectively. If the corresponding instances of
(13) do not have a solution $\xi(x)$ in $TX$, then by Lemma 38 we have a sound
one-step rule $\boldsymbol{A}/\boldsymbol{P}$ and a valuation
$\tau:\mathsf{sVar}\to\mathcal{P}(X)$ such that $X\models\boldsymbol{A}\tau$
but the instances of (13) for $A^{1},\dots,A^{k}$ demand
$\xi(x)\models\neg\boldsymbol{P}\tau$. Let
$\boldsymbol{p}_{1},\dots,\boldsymbol{p}_{k}$ be the schematic variables
appearing in $\boldsymbol{A}/\boldsymbol{P}$; w.l.o.g.
$\tau(\boldsymbol{p}_{j})=A^{j}$ for $j=1,\dots,k$. Then $X$ satisfies the
first-order sentence $\forall z.(\boldsymbol{A}\sigma)$ where
$\sigma(\boldsymbol{p}_{j})=P^{j}(y)$. By Łoś’s theorem (in fact already by
its classical version), there exists $B\in\mathfrak{U}$ such that
$X_{i}\models\forall z.(\boldsymbol{A}\sigma)$ and hence
$X_{i}\models\boldsymbol{A}\tau_{i}$ for all $i\in B$, where
$\tau_{i}(\boldsymbol{p}_{j})=A^{j}_{i}$. By one-step soundness of
$\boldsymbol{A}/\boldsymbol{P}$ this implies
$TX_{i}\models\boldsymbol{P}\tau_{i}$ for all $i\in B$. But our formulation
above that the instances of (13) for $A^{1},\dots,A^{k}$ demand
$\xi(x)\models\neg\boldsymbol{P}\tau$ means more explicitly (and using the
fact that $\mathfrak{U}$ is an ultrafilter) that $\\{i\in
I\mid\xi_{i}(x_{i})\models\neg\boldsymbol{P}\tau_{i}\\}\in\mathfrak{U}$, so
that we have a contradiction.

From Lemma 37, our first existence criterion for quasi-ultraproducts is
immediate:

######  Theorem 39.

If a $\Lambda$-structure is one-step compact (Definition 3.1), then it has
quasi-ultraproducts.

The above criterion applies in particular to all neighbourhood-like logics. It
thus subsumes Chang’s original ultraproduct construction [Chang73] Like for
our completeness results, an alternative is to require bounded operators:

######  Theorem 40.

If a $\Lambda$-structure is finitary one-step compact (Definition 3.1) and
all its operators are bounded, then it has quasi-ultraproducts.

The proof needs the following lemma.

######  Lemma 41.

Let $(C_{i})=(X_{i},\xi_{i})_{i\in I}$ be a family of $T$-coalgebras, and let
$\mathfrak{U}$ be an ultrafilter on $I$. Let $X$ be the ultraproduct
$\prod_{\mathfrak{U}}X_{i}$, and let $x\in X$. Then the set

$\Psi=\\{\epsilon\heartsuit\\{y^{1},\dots,y^{k}\\}\mid\\{i\mid\xi_{i}(x_{i})\models\epsilon\heartsuit\\{y^{1}_{i},\dots,y^{k}_{i}\\}\\}\in\mathfrak{U}\\}$

of one-step formulas (where $\heartsuit$ ranges over $\mathrm{\Lambda}$, the
$y^{i}$ range over $X$, and $\epsilon$ stands for either negation or nothing)
is finitely satisfiable.

######  Proof 5.3.

Analogous to Lemma 37, using atoms of the form $z=c$ in place of unary
predicates. In more detail: if a finite subset $\Phi$ of $\Psi$ is one-step
unsatisfiable, then by Lemma 38 there exist a one-step sound rule
$\boldsymbol{A}/\boldsymbol{P}$ and a valuation $\tau$ such that
$\boldsymbol{P}\tau=\neg\bigwedge\Phi$ and $X\models\boldsymbol{A}\tau$. Now
$X\models\boldsymbol{A}\tau$ is semantically equivalent to $X\models\forall
z.\boldsymbol{A}_{0}$ where $\boldsymbol{A}_{0}$ is propositional formula over
atoms of the form $z=c$, where $c$ ranges over constants denoting elements of
the involved finite subsets of $X$ in an extended first-order structure based
on $X$. Then $\\{i\mid X_{i}\models\forall
z.\,\boldsymbol{A}_{0}\\}\in\mathfrak{U}$ by (the classical version of) Łoś’s
theorem, where we interpret constants in $X_{i}$ by taking the $i$-th
component of the interpretation in $X$ (this is just the way the
interpretation of constants in the factors relates to that in the
ultraproduct, classically). Hence $\\{i\mid