Moss' logic for ordered coalgebras

TL;DR

This paper introduces a finitary coalgebraic logic for ordered coalgebras using a single modality, establishing its semantics, properties, and a complete proof system, extending Moss's logic to a finitary setting.

Contribution

It develops a finitary version of Moss' coalgebraic logic for ordered coalgebras, including semantics, a proof system, and the Hennessy-Milner property, under specific functor preservation conditions.

Findings

The logic has the Hennessy-Milner property for similarity.

A complete sequent proof system is constructed.

Semantics are given via relation lifting with functor preservation assumptions.

Abstract

We present a finitary version of Moss' coalgebraic logic for $T$-coalgebras, where $T$ is a locally monotone endofunctor of the category of posets and monotone maps. The logic uses a single cover modality whose arity is given by the least finitary subfunctor of the dual of the coalgebra functor $T_\omega^\partial$, and the semantics of the modality is given by relation lifting. For the semantics to work, $T$ is required to preserve exact squares. For the finitary setting to work, $T_\omega^\partial$ is required to preserve finite intersections. We develop a notion of a base for subobjects of $T_\omega X$. This in particular allows us to talk about the finite poset of subformulas for a given formula. The notion of a base is introduced generally for a category equipped with a suitable factorisation system. We prove that the resulting logic has the Hennessy-Milner property for the notion of similarity based on the notion of relation lifting. We define a sequent proof system for the logic, and prove its completeness.

Equations

$$T::=E\mid Id\mid T+T\mid T\times T\mid T^E\mid T^{\partial }\mid \mathbb{L}T.$$

$$T^{\partial }X=(T{X}^{op}{)}^{op}$$

$$\forall x\in w\exists x^{\prime }\in w^{\prime }(x\le x^{\prime })\text{mbox}and\forall x^{\prime }\in w^{\prime }\exists x\in w(x\le x^{\prime }).$$

$$T_{\omega}X:=\bigcup\limits_{\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 9.62927pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\crcr}}}\ignorespaces{\hbox{\kern-9.62927pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 1.0pt\raise 0.0pt\hbox{$\textstyle{m:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 8.12927pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\hbox{{}{\hbox{\kern 3.0pt\hbox{\ignorespaces\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}}}}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 25.22931pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 25.22931pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 1.0pt\raise 0.0pt\hbox{$\textstyle{X}$}}}}}}}\ignorespaces}}}}\ignorespaces}\mathsf{img}(Tm).$$

$$T_{\omega }X\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$X\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$R(x,y,z)\text{mbox}and{x}^{\prime }\le x\text{mbox}and{y}^{\prime }\le y\text{mbox}andz\le z^{\prime }\text{mbox}impliesR(x^{\prime },y^{\prime },z^{\prime }).$$

$$x⊩a_0\otimes a_1$$

$$x⊩a\to b$$

$$x⊩\square a$$

$$x⊩⧫a$$

$$c:X⟶\mathbb{U}X\text{mbox}andd:X⟶\mathbb{L}X$$

$$c:X⟶{\mathbb{U}}_{\omega }X\text{mbox}andd:X⟶{\mathbb{L}}_{\omega }X$$

$$x⊩\square a$$

$$x⊩◊a$$

$${\square }_R(u)$$

$${◊}_R(u)$$

$$\le \cdot R\subseteq R\cdot \le \text{mbox}and\ge \cdot R\subseteq R\cdot \ge .$$

$$C:=A|\top |C\sqcap D|\exists r.C$$

$$c:\Delta ⟶(\mathbb{L}\Delta {)}^{N^r}\times 2^{N^c}$$

$$A\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$Z\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$1\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$${\mathsf{Sub}}_{\mathcal{M}}(X)$$

$$⋮$$

$${\bigcap }_{i\in I}{m}_i:Z\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$${\bigcup }_{i\in I}{m}_i:C\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$⋮$$

$$\alpha \subseteq T{\mathsf{base}}_X(\alpha )$$

$${\mathsf{base}}_X(Tm)\subseteq m$$

$$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 9.47626pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\crcr}}}\ignorespaces{\hbox{\kern-9.47626pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 1.0pt\raise 0.0pt\hbox{$\textstyle{\alpha:{\mathbb{1}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 7.97627pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\hbox{{}{\hbox{\kern 3.0pt\hbox{\ignorespaces\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}}}}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 25.0763pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 25.0763pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 1.0pt\raise 0.0pt\hbox{$\textstyle{{\mathbb{L}}\mathbb{Z}}$}}}}}}}\ignorespaces}}}}\ignorespaces,\quad*\mapsto\mathbb{Z},$$

Full text

We prove that the resulting logic has the Hennessy-Milner property for the notion of similarity based on the notion of relation lifting. We define a sequent proof system for the logic, and prove its completeness.

Marta Bílková acknowledges the support by the grant No. P202/11/P304 of the Czech Science Foundation, and (for the revised version of the paper) by the grant From Shared Evidence to Group Attitudes of Czech Science Foundation and DFG, no. 16-07954J, and RVO: 67985807. M. Dostál acknowledges the support by the Grant Agency of the Czech Republic under the grant 19-0092S and the grant 22-02964S

1. Introduction

Shortly after the theory of coalgebras emerged as a useful conceptual tool for a uniform study of various kinds of dynamic systems, there has been an interest in finding logics expressive enough to describe the behaviour of the coalgebras up to bisimilarity.

For the case of coalgebras for endofunctors $T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ preserving weak pullbacks, this goal has been achieved by Larry Moss in his pioneering paper [Mos99], where he introduces a coalgebraic logic expressive for bisimulation, uniformly in the choice of the coalgebra functor $T$. The language of the logic contains a single cover modality $\nabla_{T}$, whose arity is given by the coalgebra functor $T$, and whose semantics is given by relation lifting. The original Moss’ logic is infinitary: not only it allows for infinite conjunctions and disjunctions, but also modal formulas $\nabla\alpha$ for $\alpha\in T{\mathcal{L}}$ can be infinitary, depending on the functor $T$.

After that, attention turned to the question how to obtain expressive coalgebraic languages based on more standard modalities [Jac01, Kur01], the current mainstream approach being based on modalities described by predicate liftings [Pat03, Sch08].

Moss’ logic itself has soon become a lively field of study. Using similar ideas as Moss, Baltag in [Bal00] describes an infinitary coalgebraic logic capturing both the notion of bisimulation and simulation for ${\mathsf{Set}}$ coalgebras. Neither Moss nor Baltag provide a complete axiomatization for their respective infinitary logics, as completeness might not be available in general, depending again on the coalgebra functor.

A finitary version of Moss’ logic has consequently been explored by various authors, resulting in an almost full picture, including (among others) its axiomatization and completeness proof parametric in the coalgebra functor [KKV12b], a structural Gentzen-style proof theory [BPV14], applications to automata theory [KV05, KV08, KV09], and applications to fixpoint logics [SV10, Ven06]. The two formalisms, languages based on predicate liftings and Moss’ finitary languages, have been compared in detail in [KL12].

Much of the theory that has been built around Moss’ idea uses heavily that endofunctors of ${\mathsf{Set}}$ are well understood. This is not quite the case for the endofunctors on the categories of preorders and posets. One encounters them naturally when interested in similarity alone, rather then bisimilarity [KKV12a, Lev11]. For this reason (among others), poset extensions and liftings of set functors were investigated in [BK11, BKV13]. Also a coalgebraic logic for poset coalgebras, based on monotone predicate liftings, has been considered and proved to be expressive in [KKV12a].

It therefore seems natural to investigate the possibilities of extending the above mentioned techniques and results on finitary Moss’ logic for set coalgebras beyond the category of sets. This paper is a step in this direction, developing Moss’ logic in the the category ${\mathsf{Pos}}$ of posets and monotone maps, building mainly on results obtained in [BKPV11]. Namely, we use the existence of a functorial relation lifting for functors preserving exact squares in the category ${\mathsf{Pos}}$. This provides us, as we show below, with the technical background for the development of Moss’ logic for poset coalgebras.

Since the results about relation lifting in [BKPV11] were further generalised in [BKPV13] to the enriched case of ${\mathscr{V}}$-categories, where ${\mathscr{V}}$ is a commutative quantale, it is also possible to define Moss’ logic in this level of generality. However, the commitment to the enriched setting in particular means that everything, including the language, forms a ${\mathscr{V}}$-category and if we are to be truly general, we deal with a highly unusual syntax. We feel that restricting to the case of preorderes (${\mathscr{V}}$-categories where ${\mathscr{V}}={\mathbb{2}}$) or posets is the right level of enrichment for presentation of Moss’ coalgebraic logic in full detail at the moment.

The commitment to the enriched setting of the category ${\mathsf{Pos}}$ has similar consequences worth mentioning out front. First, every object we work with is going to be a poset, including a poset of atomic propostions or the poset of formulas. Arities of connectives and of the modality will be given by finitary poset functors. This alone opens possibilities to a rather unusual definition of syntax. Second, the usual notion of finite objects will be replaced by that of finitely generated objects. This affects notions of formulas, sequents and proofs.

Contribution of this paper.

We present a finitary Moss’ coalgebraic language for coalgebras for a locally monotone functor $T:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$ that preserves exact squares. The logic is based on the language of logic of distributive lattices equipped with a single cover modality $\nabla$ (and for the sake of proof theory later also with its dual modality $\Delta$). The arity of both cover modalities is the least finitary subfunctor $T^{\partial}_{\omega}$ of the dual of the coalgebra functor $T$, and the semantics of the cover modalities essentially uses the notion of relation lifting, proven to exist for our choice of coalgebra functors in [BKPV11].

For the finitary setting to work, we need to adopt an appropriate notion of a base. In the “classical” case of a finitary coalgebraic functor $T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$, the base is a natural transformation from $T$ to the finitary powerset functor. In the context of Moss’ coalgebraic language, it in particular allows us to consider subformulas of objects in $T{\mathcal{L}}$. Bases of endofunctors, in a more general categorial setting, have recently been studied in the context of reachability in automata (see e.g. the approach taken in [BKR19, WMKJD19]). We have independently developed an appropriate notion of base of a locally monotone finitary functor $T_{\omega}:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$. Some additional assumptions on the category ${\mathsf{Pos}}$ and the functor $T_{\omega}$ seem inevitable. First of all, one has to choose a suitable factorisation system $({\mathcal{E}},{\mathcal{M}})$ on the category ${\mathsf{Pos}}$ and the functor $T$ should behave well with regard to the factorisation system. We prove that if we equip ${\mathsf{Pos}}$ with the factorisation system $({\mathcal{E}},{\mathcal{M}})$ of monotone surjections and order embeddings, then a base can be computed for every finitary functor $T_{\omega}$ that preserves order embeddings and their finite intersections. In particular, bases can be used to produce, for each subobject of the poset $T_{\omega}X$, a finite poset of its “generators”, e.g., a poset of subformulas of a formula of arity $T_{\omega}$, or a poset of successors of a state in a coalgebra for $T_{\omega}$.

The resulting finitary Moss’ logic has the Hennessy-Milner property — it is expressive for a notion of simulation and similarity based on the relation lifting. This notion of similarity coincides with the notion of similarity given, e.g., in [Wor00, HJ04, BK11, Lev11]. The result matches the similar result for Moss’ logic for coalgebras on the category of sets and bisimilarity. It can also be seen as a counterpart to the result proved in [KKV12a] for positive coalgebraic logics in the category of posets, stating that the logic of all monotone predicate liftings is expressive for any endofunctor of posets that satisfies our conditions.

We present the resulting logic in a form of a cut-free two-sided sequent proof calculus, and we prove its completeness. To be able to define such a proof system, we essentially use a dual cover modality delta and its semantical relation to the nabla modality. This part of the paper very closely follows previous work of the first author [BPV14] on proof theory of classical Moss’ logic in ${\mathsf{Set}}$.

Comparison to related work.

The work we present in this paper is firmly rooted in previous work on various Moss’ logics. From the original work [Mos99] of Moss it takes the idea of a modality whose arity is given by the coalgebra functor and whose semantics by the relation lifting. There are differences worth mentioning: Moss’ language does not use propositional variables, and it is inherently infinitary. Moss does not provide any proof calculus for the logic. In this sense, our work is much closer to the finitary version of Moss’ logic studied in detail in [KKV12b], and can be understood as the poset-based version of this logic. [KKV12b] addressed an important open problem at the time and provided a sound and complete derivation system for the finitary Moss’ logic in terms of a Hilbert-style calculus parametric in the coalgebra functor, and proven completeness in a one-step manner. We differ from this approach and opt to present the logic in terms of a cut-free sequent calculus. In this we closely follow previous work by the first author on Gentzen style proof theory for Moss’ logic of Kripke frames [BPV08], and consequently proof theory for general Moss’ logic parametric in the coalgebra functor [BPV14]. One difference is that [BPV14] assumes the coalgebra functor to be finitary, while we, following [KKV12b], do not do so and use finitary functors on the syntactic side of matters only. In Section 7 we briefly describe how our approach relates to positive fragments of logics covered in [BPV14].

One possible motivation to move from ${\mathsf{Set}}$ to ${\mathsf{Pos}}$ is to study similarity. This can be done in ${\mathsf{Set}}$ [Bal00] in case one is interested in studying bisimilarity and similarity together (first one is represented by equality on the final coalgebra, while the other by a preorder on the final coalgebra). However, as argued by Levy [Lev11], if we are exclusively interested in similarity, we would want the universe of final coalgebra to be a poset: if two nodes are mutually similar, they should be equal. We employ the notion of similarity given by relation lifting of monotone relation between posets studied in [BKPV11]. This coincides with the notion of similarity given elsewhere in literature, in particular in [Wor00, HJ04, BK11, Lev11].

Comparing with the logic for similarity developed in Baltag’s paper [Bal00], we can, not surprisingly, find striking resemblances. The functorial relation lifting (called strong relator in [Bal00]) is weakened to capture similarity. For example, while the strong relator extending the powerset funstor yields the lifting pattern of the Egli-Milner lifting, the relator $({\mathbb{P}},\subseteq)$ extending the powerset functor yields the same lifting pattern as the ${\mathbb{L}}$-relation lifting by the lowerset functor developed in [BKPV11] and used in this paper, namely, the first half of Egli-Milner lifting. Similarly, the relator $({\mathbb{P}},\supseteq)$ yields the same lifting pattern as the ${\mathbb{U}}$-relation lifting by the upperset functor, namely, the second half of Egli-Milner lifting. Similarly, the cover operator in [Bal00] corresponds the the modality $\nabla_{\mathbb{P}}$ of Moss, and can be somewhat related the the modality $\nabla_{{\mathbb{P}}^{c}}$ for the convex powerset functor of this paper, the box operator in [Bal00] can be related to the modality $\nabla_{{\mathbb{L}}}$ of this paper, and the diamond operator can be related to the modality $\nabla_{\mathbb{U}}$ of this paper. The similarities are not surprising because the ${\mathsf{Set}}$ powerset functor ${\mathbb{P}}$ and the ${\mathsf{Pos}}$ functors ${\mathbb{L}},{\mathbb{U}},{\mathbb{P}}^{c}$ can meaningfully be related [BK11]: while the finitary convex powerset functor is the canonical extension (the posetification) of the powerset functor, the functors ${\mathbb{L}},{\mathbb{U}}$ can be obtained as quotients of certain liftings of the powerset functor to the category of preorders and monotone maps. However, the obvious differences between [Bal00] and this paper are that the logic of this paper is finitary, genuinely developed in ${\mathsf{Pos}}$, and equipped with a sound and complete derivation system.

As for the techniques applied in this paper, we rely on: (1) the results on relation lifting of monotone relation between posets developed in [BKPV11], and do not provide new results in this respect, (2) an appropriate notion of base of a locally monotone finitary functor $T_{\omega}:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$ developed in this paper in a slightly more general categorial setting. Bases of endofunctors have recently been studied in the context of reachability in automata (see e.g. the approach taken in [BKR19, WMKJD19]), and we relate to their work in detail throughout the Section 3.

Organisation of the paper

• •

We start by listing examples of poset endofunctors and examples of ordered coalgebras in Section 2.

• •

In Section 3 we study the notion of a base in a general category equipped with a factorisation system. We describe the conditions under which an endofunctor of a category ${\mathscr{K}}$ admits a base, and we show that a large class of ${\mathsf{Pos}}$-endofunctors admits a base.

• •

Section 4 introduces monotone relations and the notion of relation lifting of monotone relations. It states the main result of [BKPV11], that is, the characterisation of locally monotone ${\mathsf{Pos}}$-endofunctors that admit a relation lifting.

• •

We define the syntax and semantics of Moss’ logic for ordered coalgebras in Section 5. The syntax and semantics of this logic is parametric in the type of coalgebras involved. We prove that the logic has Hennessy-Milner property for the notion of a simulation of coalgebras defined by relation lifting.

• •

In Section 6 we develop a sequent calculus for Moss’ logic that is again parametric in the type of coalgebras involved. We give a proof of soundness and completeness of the calculus.

• •

Section 7 concludes with possible topics for future study, and clarifies how the current setting can capture positive fragments of finitary Moss’ logic in ${\mathsf{Set}}$ studied in [BPV14].

Acknowledgements

We would like to thank Jiří Velebil for his substantial help. His insights were crucial in the development of the paper. We are also thankful for the helpful comments of the three anonymous referees.

2. Functors and coalgebras in ${\mathsf{Pos}}$

In this section we fix the basic notation and introduce the running examples that are used throughout the paper. Firstly we introduce an important class of endofunctors of posets, namely the locally monotone Kripke polynomial functors. In the second part of this section we introduce the notion of a coalgebra and show several examples of coalgebras for Kripke polynomial functors.

2.A. Basic notions and Kripke polynomial functors

We denote by ${\mathsf{Pos}}$ the category of all posets and all monotone maps, i.e. maps $f$ satisfying $x\leq y$ implies $f(x)\leq f(y)$. A monotone map $f$ is an order embedding if moreover $f(x)\leq f(y)$ implies $x\leq y$. For a poset $(X,\leq)$, we denote by $X^{\mathit{op}}$ the opposite poset $(X,\geq)$. For every pair $X$ and $Y$ of posets, the hom-set ${\mathsf{Pos}}(X,Y)$ of monotone maps from $X$ to $Y$ carries a natural partial order: given two monotone maps $f$ and $g$ in ${\mathsf{Pos}}(X,Y)$, we define that $f\leq g$ holds if and only if $f(x)\leq g(x)$ holds for every $x\in X$ (i.e. we introduce a pointwise order). The category ${\mathsf{Pos}}$ therefore can be seen as enriched in posets. In cases where we need to emphasise this extra structure of ${\mathsf{Pos}}$, we will speak of ${\mathsf{Pos}}$ as of a 2-category.

A functor $T:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$ is then called a locally monotone functor (or a 2-functor), if it preserves the additional structure present in ${\mathsf{Pos}}$: that is, if for any pair $f$, $g$ of comparable morphisms in ${\mathsf{Pos}}$ the inequality $f\leq g$ implies that the inequality $T(f)\leq T(g)$ holds.

The Kripke polynomial endofunctors of ${\mathsf{Pos}}$ are those defined by the following grammar:

[TABLE]

We give an explanation of the building blocks of the grammar.

1. (1)

Let $E$ be an arbitrary poset. Slightly abusing the notation, we denote by $E$ the constant-at-$E$ functor. The functor ${\mathit{Id}}$ is the identity functor. 2. (2)

Given two Kripke polynomial functors, their product and coproduct (in the category of poset endofunctors) is again a Kripke polynomial functor. 3. (3)

Given a poset $E$, we define that $T^{E}(X)=(TX)^{E}$ is the poset of all monotone maps from $E$ to $TX$ with the pointwise ordering. The obvious action on morphisms makes $T^{E}$ into a functor. 4. (4)

Given a functor $T$, the functor $T^{\partial}$ is the dual of $T$, defined by putting

[TABLE]

and again extending to the obvious action on morphisms. (Recall that $X^{\mathit{op}}$ denotes the opposite poset with the same underlying set satisfying $x\leq y$ in $X^{\mathit{op}}$ precisely when $y\leq x$ in $X$.) 5. (5)

We denote by ${\mathbb{L}}$ the lowerset functor, with ${\mathbb{L}}X=[X^{\mathit{op}},{\mathbb{2}}]$ being the poset of all lowersets on the poset $X$, and the order is given by inclusion. (By ${\mathbb{2}}$ we denote the two-element chain.) The lowerset functor ${\mathbb{L}}$ acts on morphisms as the direct image followed by closure: given $f:X\longrightarrow Y$, a lowerset $l\in{\mathbb{L}}X$ is mapped by ${\mathbb{L}}f$ to ${\downarrow}f[l]$, i.e., to the lowerset generated by the image $f[l]$ of $l$.

All Kripke polynomial endofunctors of ${\mathsf{Pos}}$ are locally monotone, as seen by a routine induction.

Observe that the dual of ${\mathbb{L}}$ is the upperset functor ${\mathbb{U}}$: for any poset $X$ we have that ${\mathbb{L}}^{\partial}X=[X,{\mathbb{2}}]^{\mathit{op}}$, and the latter is the set of all uppersets on $X$, ordered by reversed inclusion. Therefore, the upperset functor ${\mathbb{U}}$ is Kripke polynomial as well. For a monotone map $f:X\longrightarrow Y$, the map ${\mathbb{U}}f:{\mathbb{U}}X\longrightarrow{\mathbb{U}}Y$ sends an upperset $u\in{\mathbb{U}}X$ to the upperset ${\uparrow}f[u]$ generated by the image $f[u]$ of $u$.

Apart from Kripke polynomial functors, we will list an additional functor we will briefly need at the very end of the paper: the convex powerset functor ${\mathbb{P}}^{c}$. For a poset $X$, ${\mathbb{P}}^{c}X$ is the poset of convex subsets of $X$ (i.e. subsets $w$ such that if $x,y\in w$ and $x\leq z\leq y$, then $z\in w$) partially ordered by the Egli-Milner preorder: $w\leq^{EM}w^{\prime}$ iff

[TABLE]

Its action on morphisms ${\mathbb{P}}^{c}f$ is the direct image map. Observe that this functor is self-dual: $({\mathbb{P}}^{c})^{\partial}={\mathbb{P}}^{c}$. This functor comes from the powerset functor ${\mathbb{P}}:{\mathsf{Pre}}\longrightarrow{\mathsf{Pre}}$ in the category of preorders and monotone maps, via the $Q\dashv I$ adjunction (of the quotient and inclusion functors) as $Q{\mathbb{P}}I$ [BKPV11].

We will systematically use finitary functors on the syntactic side of the logics, i.e. functors that are completely determined by their action on finite posets. Formally, finitary functors are those preserving filtered colimits (see [Kel82b]), but we will use the following elementary definition in this paper:

For a functor $T$, let $T_{\omega}$ be its least finitary subfunctor, with \textstyle{\nu^{T}:T_{\omega}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{T} being the natural inclusion. Categorically, $T_{\omega}$ is the finitary coreflection of the functor $T$. It can be defined in an elementary manner as follows: let $m$ range through finite subobjects

\textstyle{m:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X} of $X$ (i.e. with $Z$ being a finite poset) and put

[TABLE]

For a map $f:X\longrightarrow Y$, $T_{\omega}f$ is the restriction of $Tf$ to $T_{\omega}Y$.

[TABLE]

The functors $T$ and $T_{\omega}$ agree on finite posets (i.e., the corresponding natural inclusion is the identity on finite posets). We say that $T$ is finitary if $T$ and $T_{\omega}$ coincide.

We will often explicitly use the finitary lowerset functor ${\mathbb{L}}_{\omega}$. For a poset $X$, the poset ${\mathbb{L}}_{\omega}X$ consists of finitely generated lowersets on $X$ ordered by inclusion. Analogously, the finitary upperset functor ${\mathbb{U}}_{\omega}$ assigns to a poset $X$ the poset of its finitely generated uppersets, ordered by reversed inclusion. Both functors are finitary subfunctors of the usual lowerset and upperset functors. We will use the notation $g(l)$ for the minimal discrete finite poset (i.e. finite set) of generators of the lowerset $l\in{\mathbb{L}}_{\omega}X$, and in the same way $g(u)$ will denote the minimal finite set of generators for the upperset $u\in{\mathbb{U}}_{\omega}X$. When a lowerset is generated by a single element, we call it a principal lowerset and denote such principal loweset generated by $x$ by $x{\downarrow}$. Similarly, principal upperset generated by $x$ is denoted by $x{\uparrow}$.

Similarly, the finitary convex powerset functor ${\mathbb{P}}^{c}_{\omega}$ assigns, to a poset $(X,\leq)$, the poset of the finitely generated convex subsets of $X$ ordered by the Egli-Milner partial order $\leq^{EM}$. The functor ${\mathbb{P}}^{c}_{\omega}$ is the natural counterpart — the posetification — of the finitary powerset functor ${\mathbb{P}}_{\omega}:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ (see [BK11]).

2.B. Coalgebras for a functor

Given a (not necessarily locally monotone) functor $T:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$, we define coalgebras and their homomorphisms in the usual manner.

Explicitly, a coalgebra for $T$ is a monotone map $c:X\longrightarrow TX$, and a monotone map $h:X\longrightarrow Y$ is a homomorphism from $c:X\longrightarrow TX$ to $d:Y\longrightarrow TY$ if the following square

[TABLE]

commutes.

There are various interesting structures from computer science and logic that can be modelled as coalgebras for a suitable Kripke polynomial functor. We show some of the examples below.

{exa}

Examples of ordered coalgebraic structures.

1. (1)

Consider the functor $T=A\times{\mathit{Id}}$ for some fixed poset $A$. Coalgebras for the functor $T$ are the monotone maps $c=\langle{\mathit{out}},{\mathit{next}}\rangle:X\longrightarrow A\times X$ that can be seen as a particularly trivial kind of automata with the set of states $X$ and an (ordered) output alphabet $A$. Hence the monotone map $\mathit{out}:X\longrightarrow A$ produces an output in $A$ for every state in $X$ and the monotone map $\mathit{next}:X\longrightarrow X$ produces the next state of the automaton. 2. (2)

A complete deterministic ordered automaton (as considered in Chapter 2 of [PP04]) is a Büchi automaton $(X,A,E,I,F)$ where $X$ is equipped with a partial order $\leq$, $A$ is the alphabet, $E$ the set of $A$-labelled (deterministic) transitions on $X$ of the form $x\cdot a=y$, and $F$ is an order-ideal of final states. For each $x,y,y^{\prime}\in X$ and $a\in A$, $x\leq y$ and $y\cdot a$ is defined, implies $x\cdot a$ is defined and $x\cdot a\leq y\cdot a$.

In a Büchi automaton, the words in the semigroup $A^{+}$ can bee seen to generate a morphism to the semigroup of binary relations on $X$, mapping a word $w$ to the accessibility relation labelled by (the letters) of $w$. We can think of a state $x$ as accepting $w$ if there is a $w$-labelled path from $x$ to a final state. In this sense, the partial order on the states of automata from this example corresponds to the reverse inclusion of the accepted languages: if $x\leq y$ and $y$ accepts $w$, then $x$ accepts $w$. The order on states in a precise technical sense generates a congruence order on the semigroup $A^{+}$.

A complete deterministic ordered automaton can be seen as a coalgebra of the form $c:X\longrightarrow X^{A}\times{\mathbb{2}}$ where $X$ is a partial order of states, $A$ the (discrete) input alphabet, the left-hand component of the monotone map $c$ is a monotone transition map $x\mapsto(a\mapsto x\cdot a)$ and its right-hand component is a monotone map from $X$ to the two-element chain ${\mathbb{2}}$, determining the accepting states. (In the poset setting, there would be no problem in considering the more general case of ordered automata with an ordered input alphabet; we however stick to the definition already used in literature for this example.)

Ordered automata have been considered as a counterpart of ordered semigroups in [PP04], to deal with some natural classes of recognizable sets of words closed under finite unions and intersection, but not under complement. 3. (3)

Consider the functor $T={\mathbb{L}}_{\omega}^{A}\times{\mathbb{2}}$ (with $A$ being discrete). A coalgebra $c:X\longrightarrow({\mathbb{L}}_{\omega}X)^{A}\times{\mathbb{2}}$ is a nondeterministic automaton consisting of an upperset $F\subseteq X$ of accepting states, and a set $C$ of transitions of the form $(x,a,y)$ with $x,y\in X$ and $a\in A$, satisfying two confluence properties:

1. (a)

Whenever $(x,a,y)\in C$ and $x\leq x^{\prime}$ in $X$, it follows that $(x^{\prime},a,y)\in C$. 2. (b)

Whenever $(x,a,y)\in C$ and $y\leq y^{\prime}$ in $X$, it follows that $(x,a,y^{\prime})\in C$.

Let moreover $d:Z\longrightarrow({\mathbb{L}}_{\omega}Z)^{A}\times{\mathbb{2}}$ be an automaton with an upperset $G\subseteq Z$ of accepting states and a set $D$ of transitions. A monotone map $h:X\longrightarrow Z$ is a homomorphism between $c$ and $d$ if the following three conditions are satisfied:

1. (a)

$h[F]=G$ and $h[X\setminus F]\cap G=\emptyset$ ($h$ preserves the set of accepting states). 2. (b)

For every transition $(x,a,y)\in C$ there is a transition $(h(x),a,h(y))\in D$. 3. (c)

For every transition $(h(x),a,z)\in D$ there is a transition $(x,a,y)\in C$ with $z\leq h(y)$.

We will call coalgebras for the functor ${\mathbb{L}}_{\omega}^{A}\times{\mathbb{2}}$ lowerset automata. 4. (4)

Frames for distributive substructural logics [Res00] are frames consisting of a poset $X$ of states, together with a ternary relation on $X$, satisfying the following monotonicity condition:

[TABLE]

In the notation of monotone relations of Section 4 below, $R$ is a monotone relation of the form

\textstyle{R:X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X\times X} .

Given a set ${\mathsf{At}}$ of atomic formulas and a monotone valuation $X\times{\mathsf{At}}\longrightarrow{\mathbb{2}}$ of the atomic formulas, we can interpret the fusion and implication connectives as follows:

[TABLE]

It has been shown in [BHV12] that such frames can be treated as coalgebras in a natural way so that the coalgebraic morphisms coincide with the frame morphisms. In particular, $R$ generates a natural coalgebraic structure $c_{\otimes}:X\longrightarrow{\mathbb{L}}(X\times X)$ for a locally monotone functor ${\mathbb{L}}({\mathit{Id}}\times{\mathit{Id}})$, when we understand $R$ as interpreting the fusion connective. We call $R$ finitary when the generated coalgebraic structure is in fact of the form $c_{\otimes}:X\longrightarrow{\mathbb{L}}_{\omega}(X\times X)$, i.e. when we can use the finitary lowerset functor. 5. (5)

Consider a poset $X$ equipped with a monotone relation

\textstyle{R:X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X} . This can be seen as a frame for modal logic with adjoint modalities. More in detail, such frames with a monotone valuation enable one in principle to interpret conjunction, disjunction, and two monotone modalities: a forward-looking $\Box$ and a backward-looking $\blacklozenge$. We put

[TABLE]

The modalities $\Box$ and $\blacklozenge$ are adjoint in a sense that will be explained in Remark 15. The relation $R$ generates two coalgebras

[TABLE]

defined by $c(x)=\{y\ |\ R(x,y)\}$ and $d(x)=\{y\ |\ R(y,x)\}$. We say that the frame $(X,R)$ is finitary if $R$ in fact generates coalgebras

[TABLE]

for the finitary functors ${\mathbb{U}}_{\omega}$ and ${\mathbb{L}}_{\omega}$.

While the ${\mathbb{U}}$-coalgebras can be seen as models of the box fragment of positive modal logic (i.e. the logic one obtains by extending the logic of distributve lattices with a box operator), the ${\mathbb{L}}$-coalgebras can be seen as models of the logic of distributive lattices extended with a backward looking diamond operator (which is the common fragment of substructural epistemic logics considered in [BMP16]). 6. (6)

Consider a ${\mathbb{P}}^{c}$-coalgebra $c:X\longrightarrow{\mathbb{P}}^{c}$, assigning to a state $x$ a convex subset $c(x)$ so that whenever $x\leq y$, we have $c(x)\leq^{EM}c(y)$. Equipped with a monotone valuation $X\times{\mathsf{At}}\longrightarrow{\mathbb{2}}$ assigning uppersets to the atomic formulas, it enables us to interpret (conjunction and disjunction and) the box and diamond modalities:

[TABLE]

creating the following operations on ${\mathbb{U}}X$:

[TABLE]

When seen as a relational assignment on the underlying set given by $xRy:=y\in c(x)$, the above monotonicity condition does not make $R$ monotone per se, but translates to the following two conditions on $R$, familiar from the theory of partially ordered frames $(X,\leq)$ with valuations taking values in ${\mathbb{U}}X$ (see e.g. [Pal04]):

[TABLE]

The first condition corresponds to ${\mathbb{U}}X$ being closed under $\Box_{R}$, the second condition corresponds to ${\mathbb{U}}X$ being closed under $\Diamond_{R}$, thus ensuring the persistence of the semantics.

It is not hard to work out that this is an alternative semantics to the positive modal logic, i.e. the positive fragment of modal logic K. 7. (7)

Semantics for description logic EL. The small description logic EL is a lite description logic whose language allows for conjunction, existential restrictions, and the top-concept (see e.g. [Baa03]). While its semantics itself is not based on a poset, the syntax employs concept and role subsumptions in the form of inclusions.

In a simple case, and when formulated in the poset setting, the syntax works as follows: we fix a poset $N^{c}$ of concept names ordered by concept subsumptions of the form $A\sqsubseteq B$, a poset $N^{r}$ of role names ordered by role subsumptions of the form $r\sqsubseteq s$, and generate the following grammar of concepts:

[TABLE]

The semantics is based on a discrete poset (i.e. a set) $\Delta$ together with: (ii) interpretations $C^{I}$ of concept names by lowersets of $\Delta$ (i.e. subsets of $\Delta$) respecting their order: $C\sqsubseteq D$ implies $C^{I}\subseteq D^{I}$, (ii) interpretations $r^{I}$ of role names by binary relations on $\Delta$, again respecting their order: $r\sqsubseteq s$ implies $r^{I}\subseteq s^{I}$. We can see each structure of this kind as a coalgebra

[TABLE]

which, for each $d\in\Delta$, assigns: for each role name $r$ the lowerset (i.e. subset) $\{e\ |\ (d,e)\in r^{I}\}$, and for each concept name $C$ the value $1$ if $d\in C^{I}$, and the value [math] otherwise. Both assignments are monotone.

We shall use some of the above coalgebras as running examples to illuminate concretely the general theory.

3. Base in a category ${\mathscr{K}}$ with a factorisation system

When studying finitary coalgebraic logics for finitary endofunctors of ${\mathsf{Set}}$, the notion of a base is of central importance. On the level of models, the base allows us to produce a finite set of successors of a state of the model. On the level of the logical syntax, the base yields a finite set of subformulas of a given formula.

Technically, given a functor $T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$, a base is a natural transformation ${\mathsf{base}}^{T}_{X}:TX\longrightarrow{\mathbb{P}}_{\omega}X$, assigning to each element $\alpha$ of $TX$ a finite subset of $X$, called the base of $\alpha$. The idea is to define ${\mathsf{base}}^{T}_{X}(\alpha)$ as the smallest finite $Z\subseteq X$ such that $\alpha\in TZ$ holds. For this idea to work, $T$ has to satisfy additional conditions: it has been shown in [Gum05] that when $T$ preserves intersections and weakly preserves inverse images, then the base exists and it is natural. For various properties of bases for endofunctors of ${\mathsf{Set}}$ we refer to, e.g., [KKV12b].

In this section we explain how to define and compute a base for an endofunctor $T:{\mathscr{K}}\longrightarrow{\mathscr{K}}$ of an arbitrary category ${\mathscr{K}}$ that is equipped with a factorisation system $({\mathcal{E}},{\mathcal{M}})$ for morphisms. The factorisation system is used in order to be able to imitate the powerset: the set of all subsets is going to be replaced by the poset of ${\mathcal{M}}$-subobjects.

Remark 1** (Comparison to related work).**

In [WMKJD19, BKR19], the notion of base has been used to relate reachability within a coalgebra to a monotone operator on the (complete) lattice of subobjects of the carrier of the coalgebra. [BKR19] assumes the category ${\mathscr{K}}$ to be complete (which may limit applications), while [WMKJD19] (and us) do not do so. Both [WMKJD19, BKR19] however define base for any $f:X\longrightarrow TY$, while we do so only for ${\mathcal{M}}$-subobjects \textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{TX} .

Both [WMKJD19, BKR19] developed the notion independently, almost at the same time: the relation is described in Remark 5.17 in [WMKJD19]. We have developed the notion independently of the two (a preliminary version of the current paper has been available on arXiv since 2019), and only got aware of their related work recently. Credit for our contribution should go mainly to J. Velebil, who closely cooperated on a previous version of this paper.

By applying our definition of a base to the epi-mono factorisation system on the category of sets and mappings, we then obtain the above notion of a base, see Example 3.B. By applying our definition of a base to the category of all posets and all monotone maps, equipped with a suitable factorisation system, we will be able to speak of bases in the ordered case as well. See Examples 3.A and 3.B below.

3.A. Factorisation systems

For more details on the general theory of factorisation systems we refer to the book [AHS06].

{defi}

Suppose ${\mathscr{K}}$ is a category and let ${\mathcal{E}}$ and ${\mathcal{M}}$ be classes of morphisms in ${\mathscr{K}}$. We say that $({\mathcal{E}},{\mathcal{M}})$ is a factorisation system on ${\mathscr{K}}$ (and that ${\mathscr{K}}$ is an $({\mathcal{E}},{\mathcal{M}})$-category), provided the following conditions are satisfied:

1. (1)

The classes ${\mathcal{E}}$ and ${\mathcal{M}}$ are closed under composition with isomorphisms. 2. (2)

Every morphism in ${\mathscr{K}}$ can be factorised as a morphism in ${\mathcal{E}}$ followed by a morphism in ${\mathcal{M}}$. 3. (3)

${\mathscr{K}}$ has the $({\mathcal{E}},{\mathcal{M}})$-diagonalisation property, i.e., for every commutative square

[TABLE]

where $e$ is in ${\mathcal{E}}$ and $m$ is in ${\mathcal{M}}$, there exists a unique diagonal $d:B\longrightarrow X$, making both triangles in the diagram

[TABLE]

commutative.

A factorisation system $({\mathcal{E}},{\mathcal{M}})$ is called proper if members of ${\mathcal{E}}$ are (some) epimorphisms and members of ${\mathcal{M}}$ are (some) monomorphisms.

Remark 2**.**

Any factorisation system $({\mathcal{E}},{\mathcal{M}})$ on any category ${\mathscr{K}}$ satisfies the following (see Proposition 14.6 of [AHS06]):

1. (1)

The classes ${\mathcal{E}}$ and ${\mathcal{M}}$ are closed under composition. 2. (2)

The intersection ${\mathcal{E}}\cap{\mathcal{M}}$ is the class of all isomorphisms in ${\mathscr{K}}$.

{exa}

The following are examples of $({\mathcal{E}},{\mathcal{M}})$-categories ${\mathscr{K}}$:

1. (1)

${\mathscr{K}}$ is the category ${\mathsf{Set}}$ of all sets and mappings, ${\mathcal{E}}$ is the class of all epis (=surjections) and ${\mathcal{M}}$ is the class of all monos (=injections). 2. (2)

${\mathscr{K}}$ is the category ${\mathsf{Pos}}$ of all posets and monotone mappings, ${\mathcal{E}}$ is the class of all monotone surjections and ${\mathcal{M}}$ is the class of all monotone maps that reflect the order. 3. (3)

If ${\mathscr{K}}$ is the category ${\mathsf{Pre}}$ of all preorders and monotone mappings, one can choose from at least one of the following three prominent factorisation systems:

1. (a)

${\mathcal{E}}$ is the class of all monotone maps that are bijective on the level of elements and ${\mathcal{M}}$ is the class of all monotone maps that reflect the order. 2. (b)

${\mathcal{E}}$ is the class of all monotone surjections and ${\mathcal{M}}$ is the class of all monotone injections that reflect the order. 3. (c)

${\mathcal{M}}$ is the class of monotone injections. The class ${\mathcal{M}}$ is the class of all monomorphisms, hence the corresponding ${\mathcal{E}}$ necessarily coincides with the class of all strong epimorphisms, see [AHS06].

All of the above cases, except for (3a), are proper factorisation systems.

1. (4)

If ${\mathscr{K}}$ is an $({\mathcal{E}},{\mathcal{M}})$-category, then ${\mathscr{K}}^{\mathit{op}}$ is an $({\mathcal{M}},{\mathcal{E}})$-category. If the factorisation system $({\mathcal{E}},{\mathcal{M}})$ on ${\mathscr{K}}$ is proper, so is the factorisation system $({\mathcal{M}},{\mathcal{E}})$ on ${\mathscr{K}}^{\mathit{op}}$.

For a factorisation system $({\mathcal{E}},{\mathcal{M}})$ on ${\mathscr{K}}$, the morphisms in ${\mathcal{M}}$ will serve as “subobjects”. It is however more useful to define subobjects as equivalence classes. More precisely: we fix an object $X$ and we denote a morphism in ${\mathcal{M}}$ into $X$ by \textstyle{m:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X} . We define a preorder on such morphisms by putting $m\subseteq m^{\prime}$ if there is a factorisation

[TABLE]

The preorder defines an equivalence $m\sim m^{\prime}$ iff $m\subseteq m^{\prime}$ and $m^{\prime}\subseteq m$. We denote the equivalence classes by $[m]$. If the category ${\mathscr{K}}$ has a final object ${\mathbb{1}}$, we denote the situation

[TABLE]

by writing that $x\in m$ holds.

{defi}

The equivalence class $[m]$ of \textstyle{m:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}

is called an ${\mathcal{M}}$-subobject of $X$.

The class of all subobjects of $X$ is denoted by

[TABLE]

and we consider it ordered by $[m]\subseteq[m^{\prime}]$ if $m\subseteq m^{\prime}$.

{defi}

We say that an $({\mathcal{E}},{\mathcal{M}})$-category ${\mathscr{K}}$ is ${\mathcal{M}}$-wellpowered, if every ${\mathsf{Sub}}_{\mathcal{M}}(X)$ has a set of elements. And ${\mathscr{K}}$ is ${\mathcal{E}}$-cowellpowered, if ${\mathscr{K}}^{\mathit{op}}$ (equipped with the factorisation system $({\mathcal{M}},{\mathcal{E}})$, see Example 3.A) is ${\mathcal{E}}$-wellpowered.

Remark 3**.**

1. (1)

We will abuse the notation and write $m$ instead of $[m]$, and $m\subseteq m^{\prime}$ instead of $[m]\subseteq[m^{\prime}]$. 2. (2)

An $({\mathcal{E}},{\mathcal{M}})$-category need not be ${\mathcal{M}}$-wellpowered, even for a proper factorisation system $({\mathcal{E}},{\mathcal{M}})$. Indeed, suppose ${\mathscr{K}}$ is the class of all ordinals with the reversed order (so that the ordinal [math] becomes the top element) and consider ${\mathscr{K}}$ as a category. Put ${\mathcal{E}}$ to be the class of identity morphisms, ${\mathcal{M}}$ to be the class of all morphisms. The factorisation system $({\mathcal{E}},{\mathcal{M}})$ on ${\mathscr{K}}$ is proper, since every morphism in ${\mathscr{K}}$ is both a monomorphism and an epimorphism. Then it follows that ${\mathsf{Sub}}_{\mathcal{M}}(0)$ is a proper class. 3. (3)

If ${\mathsf{Sub}}_{\mathcal{M}}(X)$ has a set of elements, then it is a complete lattice whenever ${\mathscr{K}}$ has enough limits. In fact, it suffices to establish the existence of infima in ${\mathsf{Sub}}_{\mathcal{M}}(X)$. The infima can be computed as limits of diagrams of the form

[TABLE]

that are called wide pullbacks of ${\mathcal{M}}$-morphisms (or, intersections of ${\mathcal{M}}$-subobjects).

We denote by \textstyle{p_{i}:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Z_{i}} the limit cone. Every $p_{i}$ belongs to ${\mathcal{M}}$ by the general properties of (proper) factorisation systems, see [AHS06], Proposition 14.15. The composite

\textstyle{m_{i}\cdot p_{i}:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}

represents the ${\mathcal{M}}$-subobject that is the intersection of $m_{i}$’s. We denote the intersection by

[TABLE]

The existence of suprema in ${\mathsf{Sub}}_{\mathcal{M}}(X)$ then follows from the existence of infima by the usual argument. 4. (4)

When, moreover, coproducts exist in ${\mathscr{K}}$, suprema in ${\mathsf{Sub}}_{\mathcal{M}}(X)$ can be computed by an explicit formula. Namely, the supremum $\bigcup_{i\in I}m_{i}$ (called the union of $m_{i}$’s) can be computed as the ${\mathcal{M}}$-part

[TABLE]

of the $({\mathcal{E}},{\mathcal{M}})$-factorisation of the unique cotupling morphism $m:\coprod_{i\in I}Z_{i}\longrightarrow X$ as follows:

[TABLE] 5. (5)

When dealing with a pair \textstyle{m:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X} , \textstyle{n:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X} of subobjects of $X$, we denote their intersection and union as $m\cap n$ and $m\cup n$, respectively.

3.B. General bases

{asm}

For the rest of this section we assume the following three conditions:

1. (1)

${\mathscr{K}}$ is an $({\mathcal{E}},{\mathcal{M}})$-category for a proper factorisation system $({\mathcal{E}},{\mathcal{M}})$. 2. (2)

${\mathscr{K}}$ is ${\mathcal{M}}$-wellpowered (i.e., we assume that every ${\mathsf{Sub}}_{\mathcal{M}}(X)$ has a set of elements). 3. (3)

$T:{\mathscr{K}}\longrightarrow{\mathscr{K}}$ is a functor which preserves ${\mathcal{M}}$-morphisms.

The reader might compare our assumption 3.B (and what we have said in the item (6) of Remark 3 above) with Assumption 5.1 of [WMKJD19], where ${\mathscr{K}}$ is assumed to be complete, wellpowered, with arbitrary (small) coproducts, equipped with a factorisation system $({\mathcal{E}},{\mathcal{M}})$ where ${\mathcal{M}}$ is a class of monomorphisms.

Also, compare with Assumption of Proposition 12 in [BKR19], where ${\mathscr{K}}$ is assumed to be complete and well-powered. {defi}

An ${\mathcal{M}}$-subobject \textstyle{{\mathsf{base}}_{X}(\alpha):\widetilde{Z}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}

is called a base of an ${\mathcal{M}}$-subobject \textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{TX}

provided that the following holds for every \textstyle{m:Z^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}

${\mathsf{base}}_{X}(\alpha)\subseteq m$ holds in ${\mathsf{Sub}}_{\mathcal{M}}(X)$

iff

$\alpha\subseteq Tm$ holds in ${\mathsf{Sub}}_{\mathcal{M}}(TX)$.

Again, the reader might compare this with Definition 5.7 of [WMKJD19], where $T$ is assumed to preserve monos (like we do here), but base is defined for every arrow $f:X\longrightarrow TY$, while we do so only for subobjects. For the class of all monomorphisms such notion was first introduced by Alwin Block [Blo12] and called a base.

Compare also with [BKR19, Proposition 12], where for any endofunctor $T$ which preserves (wide) intersections, base of every arrow $f:X\longrightarrow TY$ is shown to exist.

Remark 4**.**

Since ${\mathsf{Sub}}_{\mathcal{M}}(X)$ is a poset, the base ${\mathsf{base}}_{X}(\alpha)$ is determined uniquely, whenever it exists. The base satisfies the unit property

[TABLE]

for every $\alpha$ in ${\mathsf{Sub}}_{\mathcal{M}}(TX)$, and satisfies the counit property

[TABLE]

for every $m$ in ${\mathsf{Sub}}_{\mathcal{M}}(X)$. These properties are immediate consequences of the definition of base.

We shall characterise functors admitting a base in Proposition 5. Before we state the result, let us show that some functors do not admit a base.

{exa}

Consider the category ${\mathsf{Pos}}$ equipped with the factorisation system of Example 3.A (2), and the lowerset functor ${\mathbb{L}}:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$. We claim that

[TABLE]

where $\mathbb{Z}$ is the poset of integers with the usual order, does not admit a base.

Indeed, for any \textstyle{m:Z^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathbb{Z}} , the inequality $\alpha\subseteq{\mathbb{L}}m$ states that (the image of) $Z^{\prime}$ is a cofinal subset of $\mathbb{Z}$. Had \textstyle{{\mathsf{base}}(\alpha):\widetilde{{\mathbb{1}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathbb{Z}} existed, its image would yield the least cofinal subset of $\mathbb{Z}$ — a contradiction.

Recall that meet-preserving maps between complete lattices have left adjoints. The proof of the following characterisation is a simple application of this fact (cf. Proposition 5.9 of Wissmann et al [WMKJD19]).

Proposition 5**.**

Suppose ${\mathscr{K}}$ has intersections of ${\mathcal{M}}$-subobjects. For $T:{\mathscr{K}}\longrightarrow{\mathscr{K}}$, the following are equivalent:

1. (1)

For every $X$ and every \textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{TX} , the base

\textstyle{{\mathsf{base}}_{X}(\alpha):\widetilde{Z}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X} exists. 2. (2)

$T$ preserves intersections of ${\mathcal{M}}$-subobjects.

Moreover, under any of the above conditions, ${\mathsf{base}}_{X}(\alpha)$ can be computed as the intersection

[TABLE]

of all ${\mathcal{M}}$-subobjects \textstyle{m:Z^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X} such that $\alpha\subseteq Tm$ holds in ${\mathsf{Sub}}_{\mathcal{M}}(TX)$.

Proof 3.1**.**

Observe that the assignment $f\mapsto Tf$ induces a monotone map

[TABLE]

since $T$ is assumed to preserve ${\mathcal{M}}$-morphisms. The assignment $\alpha\mapsto{\mathsf{base}}_{X}(\alpha)$ is then simply the value of a left adjoint

[TABLE]

to $T_{X}$ at a point $\alpha$. Moreover, ${\mathsf{Sub}}_{\mathcal{M}}(X)$ and ${\mathsf{Sub}}_{\mathcal{M}}(TX)$ are complete lattices, since ${\mathscr{K}}$ is assumed to have intersections of ${\mathcal{M}}$-subobjects.

Then (1) is equivalent to (2), since (1) asserts that ${\mathsf{base}}_{X}\dashv T_{X}$ holds for any $X$ and (2) asserts that $T_{X}$ preserves infima for any $X$.

The final assertion is true since the value of the left adjoint ${\mathsf{base}}_{X}$ can be computed by the formula

[TABLE]

In practical applications it may be the case that one is interested in the existence of ${\mathsf{base}}_{X}(\alpha)$ only for particular $\alpha$’s. For example, in [Ven06] the base is computed only for finite subsets of $TX$ for functors $T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$.

We imitate this approach here. Namely, besides our standing assumptions, we assume further that a full subcategory ${\mathscr{K}}_{\lambda}$ of ${\mathscr{K}}$ is given, where $\lambda$ is a regular cardinal. We want to think of the objects of ${\mathscr{K}}_{\lambda}$ as being “smaller than $\lambda$”. Our goal is to construct the value of a left adjoint

\textstyle{{\mathsf{base}}_{X}(\alpha):\widetilde{Z}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X} only for those ${\mathcal{M}}$-subobjects \textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{TX}

with $Z$ in ${\mathscr{K}}_{\lambda}$, and such that $\widetilde{Z}$ is in ${\mathscr{K}}_{\lambda}$ as well.

For every $X$, denote by

[TABLE]

the inclusion of the subposet spanned by ${\mathcal{M}}$-subobjects having a domain in ${\mathscr{K}}_{\lambda}$.

One can refine the existence of the base by applying the ideas of Freyd’s Adjoint Functor Theorem [Fre03]. In the formulation we use the terminology $\lambda$-small to abbreviate “of cardinality less than $\lambda$”. For example, a $\lambda$-small set is one of less than $\lambda$ elements, a $\lambda$-small intersection is one indexed by a $\lambda$-small set, etc.

Proposition 6**.**

Suppose that for every $X$, the poset ${\mathsf{Sub}}_{\mathcal{M}}(X)$ has $\lambda$-small infima, and suppose that ${\mathsf{Sub}}_{{\mathcal{M}},\lambda}(X)$ is a subset in ${\mathsf{Sub}}_{\mathcal{M}}(X)$ that is closed under $\lambda$-small infima.

Suppose further that the following two conditions are satisfied:

1. (1)

$T$ preserves $\lambda$-small intersections. 2. (2)

For any \textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{TX} with $Z$ in ${\mathscr{K}}_{\lambda}$ there exists a $\lambda$-small set

[TABLE]

such that for every $m$ in ${\mathsf{Sub}}_{{\mathcal{M}}}(X)$ with $\alpha\subseteq Tm$ there exists $f\in F$ with $Tf\subseteq Tm$.

Then ${\mathsf{base}}_{X}(\alpha)$ exists for every

\textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{TX}

with $Z$ in ${\mathscr{K}}_{\lambda}$, it is an element of ${\mathsf{Sub}}_{{\mathcal{M}},\lambda}(X)$, and it is computed by the formula

[TABLE]

Proof 3.2**.**

By hypothesis, ${\mathsf{Sub}}_{{\mathcal{M}},\lambda}(X)$ has $\lambda$-small infima, and the map $T_{X}$ preserves them by condition (1). Condition (2) now ensures that

[TABLE]

holds. The latter infimum is $\lambda$-small and $T_{X}$ is assumed to preserve such infima. The result now follows.

We show how Proposition 6 is applied in the classical case when ${\mathscr{K}}={\mathsf{Set}}$. Recall that a category ${\mathscr{D}}$ is $\lambda$-filtered if every $\lambda$-small diagram in ${\mathscr{D}}$ has a cocone in ${\mathscr{D}}$. A colimit is $\lambda$-filtered if its scheme is a $\lambda$-filtered category.

{exa}

Let ${\mathscr{K}}$ be the category ${\mathsf{Set}}$ of all sets and mappings with the factorisation system of surjections and injections. Let $T:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ be a finitary functor that preserves injections and finite intersections. Then, for every \textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{TX}

with the set $Z$ finite,

\textstyle{{\mathsf{base}}_{X}(\alpha):\widetilde{Z}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}

exists and the set $\widetilde{Z}$ is finite.

It suffices to verify conditions (1) and (2) of Proposition 6 (where $\lambda=\aleph_{0}$ and ${\mathsf{Set}}_{\aleph_{0}}$ are the finite sets). Condition (1) is well-known to hold for ${\mathsf{Set}}$111In fact, one has to be slightly careful here: every endofunctor of ${\mathsf{Set}}$ preserves all finite (thus even empty) intersections provided it is sound, see [AGT10] for an explanation or [Trn71] for the original result. Any non-sound endofunctor of ${\mathsf{Set}}$ can easily be “repaired” to be sound [AGT10].. Condition (2) is verified as follows. Given \textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{TX} with $Z$ a finite set, express $X$ as a filtered colimit $\mathop{{\mathrm{colim}}}\nolimits_{i\in I}X_{i}$ of subobjects

\textstyle{m_{i}:X_{i}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X} with all $X_{i}$ finite. Since $T$ is finitary and is assumed to preserve injections, $TX$ is a filtered colimit $\mathop{{\mathrm{colim}}}\nolimits_{i\in I}TX_{i}$ of injections. Since $Z$ is finite, there exists $i_{0}$ such that the triangle

[TABLE]

commutes. Denote by $F$ the set

[TABLE]

of elements of ${\mathsf{Sub}}_{\mathcal{M}}(X)$.

Observe first that $F$ is nonempty and finite. Secondly, if $\alpha\subseteq Tm$, then

[TABLE]

since $T$ preserves finite intersections. Since the subobject $m_{i_{0}}\cap m$ is in $F$, condition (2) has been verified.

More generally, Proposition 6 and the technique of Example 3.B can be applied to the case when ${\mathscr{K}}$ is a locally $\lambda$-bounded category for some regular cardinal $\lambda$ and a proper factorisation system $({\mathcal{E}},{\mathcal{M}})$, see [Kel82a]. In particular, we will use the results for ${\mathscr{K}}={\mathsf{Pos}}$ equipped with the factorisation system of monotone surjections and order-embeddings, see Example 3.B.

{defi}

A category ${\mathscr{K}}$ is locally $\lambda$-bounded w.r.t. a proper factorisation system $({\mathcal{E}},{\mathcal{M}})$, if the following two conditions hold:

1. (1)

There is an essentially small full subcategory ${\mathscr{K}}_{\lambda}$ of ${\mathscr{K}}$ such that:

1. (a)

Every object $Z$ in ${\mathscr{K}}_{\lambda}$ is $\lambda$-bounded, i.e., the functor ${\mathscr{K}}(Z,{-})$ preserves colimits of $\lambda$-filtered diagrams of ${\mathcal{M}}$-subobjects. 2. (b)

A morphism \textstyle{m:X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Y} is an isomorphism iff the map ${\mathscr{K}}(Z,m):{\mathscr{K}}(Z,X)\longrightarrow{\mathscr{K}}(Z,Y)$ is a bijection for every $\lambda$-bounded $Z$. (I.e., ${\mathscr{K}}_{\lambda}$ is an $({\mathcal{M}},{\mathcal{E}})$-generator of ${\mathscr{K}}$.) 2. (2)

The category ${\mathscr{K}}$ is cocomplete and has all ${\mathcal{E}}$-cointersections. This means that the opposite category ${\mathscr{K}}^{\mathit{op}}$ (that is equipped with $({\mathcal{M}},{\mathcal{E}})$ as a factorisation system) has all intersections of ${\mathcal{E}}$-subobjects.

A category ${\mathscr{K}}$ is called $\lambda$-ranked, if it is locally $\lambda$-bounded and ${\mathcal{E}}$-cowellpowered.

{exa}

Examples of locally $\lambda$-bounded categories w.r.t. a factorisation system $({\mathcal{E}},{\mathcal{M}})$ include the following:

1. (1)

All locally $\lambda$-presentable categories when we take ${\mathcal{E}}$ to be strong epimorphisms and ${\mathcal{M}}$ to be monomorphisms, see [Kel82a].

In particular, the categories ${\mathsf{Pos}}$ and ${\mathsf{Pre}}$ are locally $\aleph_{0}$-bounded, if we take ${\mathcal{M}}$ to consist of all monotone injections (not necessarily reflecting order). A preorder or a poset $X$ is $\aleph_{0}$-bounded iff it is finite. 2. (2)

The category ${\mathsf{Pos}}$ of posets and monotone maps is locally finitely presentable, and thus it is locally $\aleph_{0}$-bounded for ${\mathcal{E}}$ consisting of surjective monotone maps and ${\mathcal{M}}$ of monotone maps reflecting the order, see e.g. Proposition 1.61 in [AR94]. A poset is $\aleph_{0}$-bounded iff it is finite. 3. (3)

The category ${\mathsf{Pre}}$ of preorders and monotone maps can be equipped with a variety of factorisation systems, see Example 3.A. The category ${\mathsf{Pre}}$ is locally $\aleph_{0}$-bounded w.r.r. the factorisation system where ${\mathcal{E}}$ consists of all monotone surjections and ${\mathcal{M}}$ consists of all monotone injections that reflect the order, see Theorem 5.6 of [KL01]. A preorder $X$ is $\aleph_{0}$-bounded iff it is finite.

{defi}

Let ${\mathscr{K}}$ be a $\lambda$-bounded category w.r.t. a factorisation system $({\mathcal{E}},{\mathcal{M}})$. We say that $T:{\mathscr{K}}\longrightarrow{\mathscr{K}}$ admits $\lambda$-bounded bases, provided that \textstyle{{\mathsf{base}}^{T}_{X}:\widetilde{Z}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X} exists for any

\textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{TX} with $Z$ in ${\mathscr{K}}_{\lambda}$ and, moreover, $\widetilde{Z}$ is in ${\mathscr{K}}_{\lambda}$.

Proposition 7**.**

Suppose that ${\mathscr{K}}$ is locally $\lambda$-bounded w.r.t. a factorisation system $({\mathcal{E}},{\mathcal{M}})$. Then $T:{\mathscr{K}}\longrightarrow{\mathscr{K}}$ admits $\lambda$-bounded bases, whenever the following four conditions are satisfied:

1. (1)

Every subposet ${\mathsf{Sub}}_{{\mathcal{M}},\lambda}(X)$ in ${\mathsf{Sub}}_{\mathcal{M}}(X)$ is closed under $\lambda$-small infima. 2. (2)

The principal lowersets in every poset ${\mathsf{Sub}}_{{\mathcal{M}},\lambda}(X)$ are $\lambda$-small. 3. (3)

$T$ preserves colimits of $\lambda$-filtered diagrams of ${\mathcal{M}}$-subobjects. 4. (4)

$T$ preserves $\lambda$-small intersections of ${\mathcal{M}}$-subobjects.

Proof 3.3**.**

It is proved in [KL01] that every locally $\lambda$-bounded category is necessarily complete. Hence every ${\mathsf{Sub}}_{\mathcal{M}}(X)$ is a complete lattice. Every object $X$ of ${\mathscr{K}}$ can be represented as a filtered colimit of its $\lambda$-subobjects; consider the canonical filtered diagram $D:{\mathscr{D}}\longrightarrow{\mathscr{K}}$ of $X$. Its colimit $\mathop{{\mathrm{colim}}}\nolimits D$ yields a unique comparison morphism $\mathop{{\mathrm{colim}}}\nolimits D\longrightarrow X$ by the couniversal property of the colimit. This comparison is an isomorphism since ${\mathscr{K}}_{\lambda}$ is an $({\mathcal{M}},{\mathcal{E}})$-generator. We can thus use Proposition 6 and the same argument as in Example 3.B to conclude the result.

3.C. Bases in posets

We will apply the general theory of Subsection 3.B to the particular case of the category ${\mathsf{Pos}}$. In more detail, we consider ${\mathsf{Pos}}$ as an $({\mathcal{E}},{\mathcal{M}})$-category for ${\mathcal{E}}$ = monotone surjections and ${\mathcal{M}}$ = order-embeddings (i.e. monotone maps $f$ satisfying $x\leq y$ iff $f(x)\leq f(y)$). Then the following conditions hold:

1. (1)

$({\mathcal{E}},{\mathcal{M}})$ is a proper factorisation system, see Example 3.A. 2. (2)

${\mathsf{Pos}}$ is ${\mathcal{M}}$-wellpowered. 3. (3)

${\mathsf{Pos}}$ is locally $\aleph_{0}$-bounded, see Example 3.B. The category ${\mathsf{Pos}}_{\aleph_{0}}$ consists of finite posets.

Hence, by Proposition 7, a functor $T:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$ admits $\aleph_{0}$-bounded (=finite) bases, whenever $T$ preserves order-embeddings and their finite intersections. Next we survey which functors preserve those properties. From now on, all bases will be considered finite. We start with a negative example: {exa} Not all locally monotone endofunctors $T:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$ preserve order-embeddings. See e.g. Example 6.1 of [BKPV13].

Moreover, a locally monotone endofunctor of ${\mathsf{Pos}}$ that preserves order-embeddings does not necessarily preserve finite intersections. The reasoning is the same as in the case of ${\mathsf{Set}}$-endofunctors, as empty intersections are not necessarily preserved. Suppose $T:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$ assigns the two-element chain ${\mathbb{2}}$ to every nonempty poset and it assigns the one-element poset ${\mathbb{1}}$ to the empty poset. On morphisms $T$ sends the unique morphism $!_{X}:\emptyset\longrightarrow X$ to $\ulcorner 1\urcorner:{\mathbb{1}}\longrightarrow{\mathbb{2}}$, all other morphisms are mapped to the identity morphism. The intersection

[TABLE]

is clearly not preserved by $T$.

Preservation of order embeddings.

We now list examples of endofunctors of the category ${\mathsf{Pos}}$ that admit finite bases. We start with the preservation of order-embeddings.

{exa}

All Kripke-polynomial endofunctors (2.1) of the category ${\mathsf{Pos}}$ preserve order-embeddings. This is essentially proved in [BKPV13], Examples 5.3 and 6.3, for the case of Kripke polynomial endofunctors of ${\mathsf{Pre}}$. One only needs to notice that order-embeddings in ${\mathsf{Pos}}$ are precisely the order-reflecting monotone injective maps of the underlying preorders.

In fact, the class of endofunctors of ${\mathsf{Pos}}$ that preserve order-embeddings is quite large. It includes all functors that preserve certain lax diagrams called exact squares, see [Gui80] or [BKPV11].

{defi}

A lax square

[TABLE]

in ${\mathsf{Pos}}$ is called exact, if $fa\leq_{C}gb$ entails the existence of $w$ in $P$ such that both $a\leq_{A}p_{0}w$ and $p_{1}w\leq_{B}b$ hold.

A functor $T$ which preserves exact squares will be also called a functor satisfying the Beck-Chevalley Condition, or BCC for short.

{exa}

All endofunctors of ${\mathsf{Pos}}$ satisfying BCC preserve order-embeddings. In particular, all Kripke-polynomial endofunctors of ${\mathsf{Pos}}$ satisfy BCC, as does the convex powerset functor ${\mathbb{P}}^{c}$. See [BKPV11].

For an example of an endofunctor of ${\mathsf{Pos}}$ not satisfying BCC, consider the connected components functor $C:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$ that takes a poset $P$ to the discrete poset consisting of connected components of $P$. The functor $C$ does not preserve (e.g.) the order-embedding from the discrete poset on $\{a,b\}$ to the poset on $\{a,b,c\}$ with the ordering $a<c$, $b<c$. (This is Example 6.7 of [BKPV11].)

Preservation of finite intersections.

The following series of results deals with preservation of finite intersections. As the next example shows, not all Kripke polynomial functors preserve finite intersections.

{exa}

The lowerset functor ${\mathbb{L}}$ does not preserve intersections of order-embeddings. Consider the poset ${\mathbb{Z}}$ of integers and its subposets

\textstyle{m:E\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathbb{Z}} and

\textstyle{n:O\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathbb{Z}} of even and odd integers, respectively. The intersection of $m$ and $n$ is empty, as it is shown in the diagram on the left below:

[TABLE]

Then the one-element poset ${\mathbb{L}}\emptyset$ in the diagram on the right above is not the intersection of ${\mathbb{L}}m$ and ${\mathbb{L}}n$. Namely, the intersection of ${\mathbb{L}}m$ and ${\mathbb{L}}n$ contains at least two elements, since ${\mathbb{L}}m(\emptyset)=\emptyset={\mathbb{L}}n(\emptyset)$ and ${\mathbb{L}}m(E)={\mathbb{Z}}={\mathbb{L}}n(O)$.

The functor ${\mathbb{L}}$ does not, in general, preserve non-empty intersections of order-embeddings as well. Consider again the above example, and take as $m:E\longrightarrow{\mathbb{Z}}$ the poset of even integers and $n:O\longrightarrow{\mathbb{Z}}$ of odd integers and zero. Then the domain of $m\cap n$ is the one-element set $\{0\}$ and ${\mathbb{L}}\{0\}$ has two elements, while the domain of ${\mathbb{L}}m\cap{\mathbb{L}}n$ contains $\emptyset$, ${\downarrow}0$, and ${\mathbb{Z}}$.

Proposition 8**.**

All finitary Kripke-polynomial endofunctors of ${\mathsf{Pos}}$ preserve finite intersections of order-embeddings.

Proof 3.4**.**

The proof is trivial for all the formation steps (2.1) except for $T^{E}$ and ${\mathbb{L}}_{\omega}T$. For the induction hypothesis, suppose $T$ preserves finite intersections of order-embeddings.

1. (1)

Since $T^{E}X=(TX)^{E}$, it suffices to observe that the diagram

[TABLE]

is a pullback whenever the following diagram is:

[TABLE]

This is true because the functor $(-)^{E}:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$ preserves all limits: it is a right adjoint by cartesian closedness of ${\mathsf{Pos}}$ (see Example 27.3 of [AHS06]). 2. (2)

It suffices to prove that ${\mathbb{L}}_{\omega}$ preserves finite intersections of order-embeddings.

[TABLE]

Given an intersection in the diagram on the left above, we show that the diagram in the center above is again an intersection of the morphisms ${\mathbb{L}}_{\omega}m$ and ${\mathbb{L}}_{\omega}n$. For any two lowersets $\alpha$ in ${\mathbb{L}}_{\omega}A$ and $\beta$ in ${\mathbb{L}}_{\omega}B$ satisfying ${\mathbb{L}}_{\omega}m(\alpha)=\chi={\mathbb{L}}_{\omega}n(\beta)$ it is enough to find a lowerset $\lambda$ in ${\mathbb{L}}_{\omega}L$ as shown in the diagram above on the right. All of the depicted lowersets are determined by their minimal sets of generators. Recall that the minimal set of generators of the lowerset $\alpha$ is denoted by $g(\alpha)$. Since $m$ and $n$ are inclusions, we see that $g(\alpha)=g(\chi)=g(\beta)$. The equality of sets of generators implies that $g(\chi)\subseteq L$. Defining $\lambda$ in ${\mathbb{L}}_{\omega}L$ to be the lowerset generated by $g(\chi)$ yields the unique witness in ${\mathbb{L}}_{\omega}L$.

Observe that the preceding argument works even in the case of $g(\chi)$ being empty.

By the above, all finitary Kripke-polynomial functors $T$ admit finite bases.

{exa}

We will show how the bases for Kripke-polynomial functors can be computed.

1. (1)

Constant functor $E$: For an arbitrary subobject \textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{E} , we have that its base is of the form \textstyle{{\mathsf{base}}(\alpha):\emptyset\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X} , with ${\mathsf{base}}(\alpha)$ being the empty mapping. 2. (2)

Identity functor ${\mathit{Id}}:$ Given a subobject \textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X} , its base \textstyle{{\mathsf{base}}(\alpha):\widetilde{Z}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X} is the mapping $\alpha$ itself. 3. (3)

Sum and product of functors: Fix two functors $T_{1}$ and $T_{2}$. Given a subobject

[TABLE]

it is equally well a subobject \textstyle{\alpha_{1}+\alpha_{2}:Z_{1}+Z_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{T_{1}X+T_{2}X} for some choice of posets $Z_{1}$ and $Z_{2}$. Then ${\mathsf{base}}(\alpha)={\mathsf{base}}(\alpha_{1})\cup{\mathsf{base}}(\alpha_{2})$. For the case of the product of functors, given a subobject \textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{T_{1}X\times T_{2}X} , denote by $p_{i}:T_{1}X\times T_{2}X\longrightarrow T_{i}X$ the $i$-th projection from the product ($i\in\{1,2\}$). Then ${\mathsf{base}}(\alpha)={\mathsf{base}}(p_{1}\cdot\alpha)\cup{\mathsf{base}}(p_{2}\cdot\alpha)$. 4. (4)

Power of a functor: Given a functor $T^{E}$ and a subobject \textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{(TX)^{E}} , we denote by $p_{e}:TX^{E}\longrightarrow TX$ the obvious projection (with $e\in E$). Then ${\mathsf{base}}(\alpha)=\bigcup_{e\in E}{\mathsf{base}}(p_{e}\cdot\alpha)$. 5. (5)

The dual of a functor: A straightforward computation yields that the base of

[TABLE]

is $({\mathsf{base}}(\alpha^{\mathit{op}}))^{\mathit{op}}$. 6. (6)

The lowerset functor: Given a lowerset \textstyle{\alpha:{\mathbb{1}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\mathbb{L}}_{\omega}X} , the base

\textstyle{{\mathsf{base}}(\alpha):\widetilde{{\mathbb{1}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X} is the (discrete) finite poset of generators of $\alpha$. More generally, the base of \textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\mathbb{L}}_{\omega}X} is $\bigcup_{z\in Z}{\mathsf{base}}(\alpha\cdot z)$.

4. Monotone relations and their lifting

In the current section, we summarise the notation and the necessary facts that concern monotone relations between posets. We will use these facts and the facts about liftings of monotone relations in Section 5 to introduce the semantics of a coalgebraic logic over posets. For a more detailed treatment of the theory of relation liftings in the categories ${\mathsf{Pre}}$ and ${\mathsf{Pos}}$ we refer to [BKPV11].

The category ${\mathsf{Rel}}$ of monotone relations over ${\mathsf{Pos}}$ has the same objects as the category ${\mathsf{Pos}}$, and has monotone relations as arrows. A monotone relation $R$ from $X$ to $Y$ will be denoted by

\textstyle{R:X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Y}

and it will be identified with a monotone map $R:Y^{\mathit{op}}\times X\longrightarrow{\mathbb{2}}$. We shall often write $R(y,x)$ or $y\mathrel{R}x$ to denote that $R$ relates $x$ to $y$. Using this notation, a relation $R$ is monotone if it satisfies the following monotonicity condition:

[TABLE]

The composition in ${\mathsf{Rel}}$ is computed in the usual manner: $(S\cdot R)(z,x)$ holds if and only if $S(z,y)$ and $R(y,x)$ hold for some $y$. The identity morphism on a poset $X$ is the order $\leq_{X}$ of $X$, considered as the monotone map ${\leq_{X}}:X^{\mathit{op}}\times X\longrightarrow{\mathbb{2}}$. For any two posets $X$ and $Y$, the hom-set ${\mathsf{Rel}}(X,Y)$ of all monotone relations from $X$ to $Y$ carries a poset structure given by the inclusion of relations.

{exa}

We shall often use two special kinds of relations: graph relations and membership relations.

1. (1)

Graph relations. For a monotone map $f:X\longrightarrow Y$ we define two graph relations

[TABLE]

by putting

[TABLE]

The assignment

[TABLE]

can be extended to a locally monotone functor

[TABLE] 2. (2)

Membership relations. For a poset $X$, we use the following two membership relations:

[TABLE]

defined by \mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}_{X}(x,l)=1 iff $x$ is in $l$ and \mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}_{X}(u,x)=1 iff $x$ is in $u$.

As in the case of ordinary relations, there are various operations that we can perform on monotone relations.

{defi}

[Operations on relations]

Suppose

\textstyle{R:X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Y}

is a monotone relation.

1. (1)

The converse

\textstyle{R^{{\mathit{con}}}:Y^{\mathit{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X^{\mathit{op}}}

of $S$ is defined by putting $R^{\mathit{con}}(x,y)$ iff $R(y,x)$. 2. (2)

The negation

\textstyle{\neg R:X^{\mathit{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Y^{\mathit{op}}}

is defined by putting $\neg R(y,x)$ iff it is not the case that $(y,x)\in R$. 3. (3)

Given monotone maps $f:A\longrightarrow X$, $g:B\longrightarrow Y$, the composite

[TABLE]

is called a restriction of $R$ along $f$ and $g$.

Remark 9**.**

Observe that \mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}_{X} is the converse of \mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}_{X^{\mathit{op}}}. We omit the subscript $X$ whenever it is clear from the context. We also often use the notation

[TABLE]

instead of the notation \neg{\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}} and \neg{\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}} for the negation of the respective membership relations. Whenever it is possible, we use the infix notation for the membership relations.

Any locally monotone functor $T:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$ that satisfies BCC (see Definition 3.C) can be lifted to a locally monotone functor $\overline{T}:{\mathsf{Rel}}\longrightarrow{\mathsf{Rel}}$. In fact, BCC is equivalent to the existence of such a lifting. The following theorem was proved in [BKPV11] for the category ${\mathsf{Pre}}$, but the proof goes through verbatim for the case of ${\mathsf{Pos}}$.

{thmC}

[[BKPV11]]

For a locally monotone functor $T:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$ the following are equivalent:

1. (1)

The functor $T$ has a locally monotone functorial relation lifting $\overline{T}$, i.e., there is a 2-functor $\overline{T}:{\mathsf{Rel}}\longrightarrow{\mathsf{Rel}}$ such that the square

[TABLE]

commutes. 2. (2)

The functor $T$ satisfies the Beck-Chevalley Condition. (i.e., it preserves exact squares).

A relation lifting $\overline{T}$ of a locally a locally monotone functor $T$ satisfying the BCC is computed in the following way. A relation

\textstyle{R:X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Y}

can be represented by a certain span

[TABLE]

of monotone maps such that the equality $R=(p_{1})_{\diamond}\cdot(p_{0})^{\diamond}$ holds (see [BKPV11] or [BKPV13] for details). Then the lifting $\overline{T}$ is computed by the following composition of graph relations:

[TABLE]

In elementary terms, we can check if the elements $\alpha\in TX$ and $\beta\in TY$ are related by the lifted relation $\overline{T}R$ as follows:

[TABLE]

Relation lifting behaves well with respect to graph relations, converse relations and restrictions of relations. The easy proofs of these properties follow immediately from the formula (4.3). We also give explicit explicit instances of relation liftings for Kripke-polynomial functors, and the convex powerset functor.

{exa}

Suppose $T:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$ is a locally monotone functor satisfying BCC, and

\textstyle{R:X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Y}

is a given relation.

1. (1)

The relation lifting commutes with graph relations, i.e., the equalities $\overline{T}f_{\diamond}=(Tf)_{\diamond}$ and $\overline{T}f^{\diamond}=(Tf)^{\diamond}$ hold. 2. (2)

Relation lifting commutes with converses, i.e., the equality $\overline{T}R^{\mathit{con}}=(\overline{T^{\partial}}R)^{\mathit{con}}$ (or, equivalently, $\overline{T^{\partial}}R=(\overline{T}R^{\mathit{con}})^{\mathit{con}}$) holds for every monotone relation $R$. 3. (3)

Relation lifting commutes with taking restrictions. Given a restriction

[TABLE]

of \textstyle{R:X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Y} along $f:A\longrightarrow X$ and $g:B\longrightarrow Y$, we can apply $\overline{T}$ to obtain

[TABLE]

since $\overline{T}$ commutes with taking the graphs by (1) above. 4. (4)

Relation lifting for Kripke-polynomial functors can be computed inductively:

[TABLE] 5. (5)

Relation lifting for the convex powerset functor is computed as follows:

[TABLE]

Remark 10**.**

Let the least finitary subfunctor $T_{\omega}$ of a locally monotone functor $T:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$ satisfying BCC be given via the natural transformation \textstyle{\nu^{T}:T_{\omega}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{T} . We can take any relation

\textstyle{R:X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Y}

and restrict its lifting

\textstyle{\overline{T}R:TX\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{TY} along $\nu^{T}$ to obtain the relation

[TABLE]

Thus defined, the operation $\overline{T_{\omega}}$ need not be functorial. In general, we only obtain lax functoriality $\overline{T_{\omega}}R\cdot\overline{T_{\omega}}S\subseteq\overline{T_{\omega}}(R\cdot S)$ (this follows from $(\nu^{T}_{Y})^{\diamond}\cdot(\nu^{T}_{Y})_{\diamond}$ being the identity $\leq_{TY}$ for every $Y$). In case $R=f_{\diamond}$, we even obtain $\overline{T_{\omega}}(f_{\diamond})\cdot\overline{T_{\omega}}S=\overline{T_{\omega}}(f_{\diamond}\cdot S)$. The operation $\overline{T_{\omega}}$ commutes with converses and with graph relations. To sum up, $\overline{T_{\omega}}$ is a lax extension of $T_{\omega}$.

Being only a lax extension is not a real obstacle — in ${\mathsf{Set}}$, the coalgebraic logic based on a cover modality can be meaningfully defined for an arbitrary lax extension, as shown in [MV15]. Apart from the case when $T_{\omega}=T$ in Proposition 17 (2) (and $T_{\omega}$ is therefore assumed to satisfy BCC) we only use the operation $\overline{T_{\omega}}$ on the syntax side of matters in formulating the modal rules of the calculus (this part roughly starts with Definition 5.D in 5.D, and continues in Section 6). There we mostly use the fact that $\overline{T_{\omega}}R$ is the indicated restriction of $\overline{T}R$ and that the relations $\overline{T}R$ and $\overline{T_{\omega}}R$ coincide whenever $R$ is a relation between finite posets.

It is worth mentioning though that the finitary Kripke polynomial functors satisfy the BCC, and therefore they admit functorial relation lifting. For example, $\overline{{\mathbb{L}}_{\omega}}$ is the appropriate restriction of $\overline{{\mathbb{L}}}$, and therefore is computed in the same way. The same goes for the finitary convex powerset functor ${\mathbb{P}}^{c}_{\omega}$.

The above calculus of relation liftings allows us to explicitly describe the relation liftings for functors introduced in Section 2.

{exa}

Recall the various ordered coalgebraic structures from Example 2.B.

1. (1)

The lifting of the functor $T=A\times{\mathit{Id}}$ is particularly easy. Given a relation

\textstyle{R:X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Y} , let us denote the lifted relation

[TABLE]

by $\overline{R}$. Then the relation $\overline{R}((b,y),(a,x))$ holds if and only if $b\leq a$ and $R(y,x)$ holds. 2. (2)

The coalgebras for the functor $T={\mathit{Id}}^{A}\times{\mathbb{2}}$ model deterministic ordered automata. Given a monotone relation

\textstyle{R:X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Y}

the elements $\alpha=(f,i)\in X^{A}\times{\mathbb{2}}$ and $\beta=(g,j)\in Y^{A}\times{\mathbb{2}}$ are related by the lifted relation

\textstyle{\overline{T}R:TX\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{TY}

if and only if $j\leq i$ and $R(g(a),f(a))$ for every $a\in A$. 3. (3)

Given the functor $T={\mathbb{L}}^{A}\times{\mathbb{2}}$ (with $A$ discrete) for lowerset automata and a relation

\textstyle{R:X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Y} , its lifted relation

\textstyle{\overline{T}R:TX\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{TY}

is defined as follows: For an element $\alpha=(l,i)$ in $({\mathbb{L}}X)^{A}\times{\mathbb{2}}$ and $\beta=(o,j)$ in $({\mathbb{L}}Y)^{A}\times{\mathbb{2}}$ we have that $\overline{T}R(\beta,\alpha)$ holds if and only if

[TABLE]

holds, with the latter condition meaning that for every $y$ such that y\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}o(a) there is an element $x$ with x\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}l(a) such that $R(y,x)$ holds.

In the finitary case, and due to the monotonicity of the relation $R$, the condition can be weakened further using the sets of minimal generators of the lowersets $l$ and $o$. For every $y\in g(o(a))$ there has to be some $x\in g(l(a))$ such that $R(y,x)$ holds. The computation of the lifting stays the same even for an ordered set $A$ of “inputs”. 4. (4)

Given the functor $T={\mathbb{U}}$, two coalgebras $c:X\longrightarrow{\mathbb{U}}X$ and $c^{\prime}:Y\longrightarrow{\mathbb{U}}Y$, and a relation \lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 13.53639pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\crcr}}}\ignorespaces{\hbox{\kern-13.53639pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 1.0pt\raise 0.0pt\hbox{\textstyle{R:X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 25.53639pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\scriptstyle{\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\ignorespaces\lx@xy@stopper}}}}}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 37.53639pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 37.53639pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 1.0pt\raise 0.0pt\hbox{\textstyle{Y}}}}}}}}\ignorespaces}}}}\ignorespaces, The lifted relation $\overline{{\mathbb{U}}}R$ is defined as follows:

[TABLE]

Given the functor $T={\mathbb{L}}$, two coalgebras $c:X\longrightarrow{\mathbb{L}}X$ and $c^{\prime}:Y\longrightarrow{\mathbb{L}}Y$,

[TABLE]

Given the functor $T={\mathbb{P}}^{c}$, two coalgebras $c:X\longrightarrow{\mathbb{P}}^{c}X$ and $c^{\prime}:Y\longrightarrow{\mathbb{P}}^{c}Y$,

[TABLE]

5. Moss’ logic for ordered coalgebras

In this section we introduce a logic for ordered coalgebras parametric in the coalgebra functor $T$. The syntax of the logic will be finitary, the propositional part will be given by the conjunction and disjunction connectives, and the modal part will consist, up to Subsection 5.D, of a single modality $\nabla$ of arity $T_{\omega}^{\partial}$. The semantics of the logic will be given by monotone valuations over $T$-coalgebras, with the semantics of the modality $\nabla$ given by $T^{\partial}$ relation lifting. We will show that this language is always adequate for $T$-coalgebras, and adequate and expressive for $T_{\omega}$-coalgebras. This means that the logic, in case of finitary coalgebras, has the Hennessy-Milner property.

{asm}

From this section on, we fix a locally monotone functor $T:{\mathsf{Pos}}\longrightarrow{\mathsf{Pos}}$, its least finitary subfunctor \textstyle{\nu^{T}:T_{\omega}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{T} , and assume $T$ (and therefore $T^{\partial}$) preserve exact squares. We assume that $T_{\omega}^{\partial}$ preserves finite intersections, and therefore admits a finite base.

In particular, all Kripke polynomial functors of 2.1 in place of the functor $T$ comply with this assumption.

5.A. The syntax of the coalgebraic language

The syntax of Moss’ logic for ordered coalgebras will be based on finitary conjunction and disjunction connectives, and a single finitary modality. It will be convenient to regard the arities of both the connectives and the modality as finitary functors. A similar approach has been already used in [KKV12b] for the Moss’ logic in sets. There are some differencies worth mentioning though: First, when passing from sets to the enriched setting of posets, to be as general as possible, one should start with a poset of propositional variables. Second, one has to be more careful about the precise shape of the arities, namely:

1. (1)

In ${\mathsf{Set}}$, the arity of the finitary conjunction and disjunction is given by the finitary powerset functor $P_{\omega}:{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$. This means that, e.g., the conjunction is a map $\bigwedge:P_{\omega}{\mathcal{L}}\longrightarrow{\mathcal{L}}$ where ${\mathcal{L}}$ denotes the set of all formulas. In ${\mathsf{Pos}}$, the natural choice for the arity of the conjunction is ${\mathbb{U}}_{\omega}$, whereas for the disjunction it is ${\mathbb{L}}_{\omega}$. 2. (2)

In ${\mathsf{Set}}$, the cover modality $\nabla$ has the coalgebraic functor $T_{\omega}$ as its arity. In ${\mathsf{Pos}}$, one needs to use the dual $T^{\partial}_{\omega}$ of $T_{\omega}$ for type-checking reasons, as will become clear in Subsection 5.B below.

Remark 11**.**

Propositional variables are proposition place-holders. As such, the most natural (and the most free) choice is to simply start with a set of them (i.e., a discrete poset). This is indeed the setting of the most of our examples. The poset setting however allows to provide place-holder patterns, which consequently the semantics must respect. This can be seen and used as prescribing order between formulas (which is normally done afterwords by the logic and induced by semantics of logical connectives, usually in a form of assuming implications — and we can do so by using theories). But what if implications are not at hand, or, we do not want to use (possibly infinite) theories? What if we used place-holder patterns instead? Not many examples are out there, but let us provide some simple intuition behind the possibilities this opens:

Consider the $\{\wedge,\vee\}$-fragment of classical propositional logic, but take $\{p_{i}\leq q_{i}|i\in N\}$ for the poset of propositional variables. This would produce a situation where “p’s always entail q’s”.

• -

Similarly, atomic propositions can “code” scalable properties often used in questionnaires (where mostly 3–7 options in a form of “degrees” are given — e.g. heavy smoker, smoker, occasional smoker). For such settings, the poset of propositional variables can be chosen as e.g. $\{p_{i}\leq q_{i}\leq r_{i}|i\in N\}$.

Examples where a partial order (namely inclusion) is built in syntax can be found in literature which consider ordered sorts or predicates: Order-Sorted Predicate Logic has been proposed as a formal knowledge representation languages for handling structural knowledge, such as the classification of objects [Obe90, Coh87], and extended by [Kan04] which formalizes a logic programming language with not only a sort hierarchy, but also a predicate hierarchy.

Remark 12**.**

The naturality of the choice of the arity of the finitary conjunction to be ${\mathbb{U}}_{\omega}$, i.e. a finitely generated upwards closed set of formulas, can be demonstrated for example as follows: Assume we have a poset of atomic formulas at hand, and think of a conjunction as eventually becoming the infimum in the free algebra of formulas. Whenever $\bigwedge\varphi\leq b$, we expect $\bigwedge(\varphi\cup b)\equiv\bigwedge\varphi$ — the conjunction is immune to adding arguments greater than the conjunction. Similarly for disjunction and its arity being ${\mathbb{L}}_{\omega}$.

The choice of arities is in accord with how the free distributive lattice over a poset $X$ can be constructed on ${\mathbb{L}}_{\omega}{\mathbb{U}}_{\omega}X$: first take the free finite meet completion on ${\mathbb{U}}_{\omega}X$, then the free finite join completion (cf. [Joh82]).

Therefore the formulas of the coalgebraic language should have the following intuitive description in BNF:

[TABLE]

where $p$ is an atom, $\varphi={\uparrow}\{a_{1},\dots,a_{k}\}$ is a finitely generated upperset of formulas, $\psi={\downarrow}\{a_{1},\dots,a_{k}\}$ is a finitely generated lowerset of formulas, and $\alpha$ is a “$T^{\partial}$-tuple” of formulas. There is a slight technicality however: since we work in posets we expect to obtain a poset of formulas. The precise definition of formulas is achieved by the free algebra construction in the category ${\mathsf{Pos}}$.

{defi}

[Formulas]

Fix a poset ${\mathsf{At}}$ of propositional atoms. The language ${\mathcal{L}}$ is given as an algebra for ${\mathbb{U}}_{\omega}+{\mathbb{L}}_{\omega}+T^{\partial}_{\omega}$, free on ${\mathsf{At}}$. The components of the algebraic structure $a:{\mathbb{U}}_{\omega}{\mathcal{L}}+{\mathbb{L}}_{\omega}{\mathcal{L}}+T^{\partial}_{\omega}{\mathcal{L}}\longrightarrow{\mathcal{L}}$ will be denoted by

[TABLE]

Remark 13**.**

1. (1)

The language ${\mathcal{L}}$ is a poset by its construction. Moreover, an algebra for $F={\mathbb{U}}_{\omega}+{\mathbb{L}}_{\omega}+T^{\partial}$ free on ${\mathsf{At}}$ can be defined by a colimit of a transfinite chain

[TABLE]

where $W_{0}={\mathsf{At}}$, $W_{i+1}=F(W_{i})+{\mathsf{At}}$ and the connecting morphisms are defined in the obvious way: $w_{0,1}:{\mathsf{At}}\longrightarrow F({\mathsf{At}})+{\mathsf{At}}$ is the coproduct injection and $w_{i+1,i+2}=F(w_{i,i+1})+{\mathsf{At}}$.

The above chain $w_{i,i+1}$ has ${\mathcal{L}}$ as its colimit; we denote the colimit injections by $w_{i}:W_{i}\longrightarrow{\mathcal{L}}$. 2. (2)

The transfinite construction of ${\mathcal{L}}$ also shows that the “intuitive BNF” of (5.4) works. More in detail, one can show that each formula $a$ in ${\mathcal{L}}$ has a unique finite depth. Indeed, for every \textstyle{a:{\mathbb{1}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{L}} there is a least $i$ such that $a\in w_{i}$. There are two cases for a fixed $a$ in ${\mathcal{L}}$:

1. (a)

$i=0$ means that $a$ is an atom. 2. (b)

$i$ is positive, i.e., $i=k+1$. Then $a\in w_{k+1}$ holds. The formula $a$ is not an atom by the definition of $i$; hence $a$ is either a conjunction, a disjunction or a nabla of an object in $W_{k}$.

The finite poset of direct subformulas of $a$ can be obtained as the subobject ${\mathsf{base}}^{F}_{F(W_{k})}(w_{k+1}(a))$. 3. (3)

We defined the arity of a conjunction to be a finitely generated upperset of formulas, which itself may not be finite. We often abuse the notation in writing the formulas, and list only the finite set of generators of the upperset to keep the description finite. For example, by $\bigwedge\{a,b\}$ we implicitly mean the conjunction applied to the upperset ${\uparrow}{\{a,b\}}$ generated by $a$ and $b$.

Notice that, for finite sets $A$ and $B$ of formulas such that ${\uparrow}A={\uparrow}B$ holds, the equality $\bigwedge A=\bigwedge B$ is built into the relaxed notation. Similarly for disjunctions, the equality ${\downarrow}A={\downarrow}B$ implies the syntactic equality $\bigvee A=\bigvee B$. In both conjunction and disjunction, the commutativity, associativity and idempotence properties are built into the notation as well, due to the choice of their arity. Moreover, whenever $\varphi\subseteq\varphi^{\prime}$ in ${\mathbb{U}}_{\omega}{\mathcal{L}}$, $\bigwedge\varphi^{\prime}\leq_{\mathcal{L}}\bigwedge\varphi$, and, similarly whenever $\psi\subseteq\psi^{\prime}$ in ${\mathbb{L}}_{\omega}{\mathcal{L}}$, $\bigvee\psi\leq_{\mathcal{L}}\bigvee\psi^{\prime}$.

For a given formula $a$, the above remark allows us to define its finite poset of subformulas and its modal depth inductively.

{defi}

[Subformulas and modal depth]

Given a formula $a$ in ${\mathcal{L}}$, the (finite) subobject ${\mathsf{Sf}}(a)$ of ${\mathcal{L}}$ is called the subobject of subformulas of $a$, and is defined inductively as follows. Simultaneously we define the modal depth $d(a)$.

1. (1)

For $a$ in ${\mathsf{At}}$, put {\mathsf{Sf}}(a)=\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 8.9207pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\crcr}}}\ignorespaces{\hbox{\kern-8.9207pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 1.0pt\raise 0.0pt\hbox{\textstyle{a:{\mathbb{1}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 7.4207pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\hbox{{}{\hbox{\kern 3.0pt\hbox{\ignorespaces\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}}}}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 24.52074pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 24.52074pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 1.0pt\raise 0.0pt\hbox{\textstyle{\mathcal{L}}}}}}}}}\ignorespaces}}}}\ignorespaces and $d(a)=0$. 2. (2)

For $a$ of the form $\bigwedge\varphi$, put

[TABLE] 3. (3)

For $a$ of the form $\bigvee\psi$, put

[TABLE] 4. (4)

For $a$ of the form $\nabla\alpha$, put

[TABLE]

Above, all the unions are taken in the lattice of subobjects, see Remark 3.

{exa}

Let us describe the syntax of the logic for the functor $T=A\times{\mathit{Id}}$, where as $A$ we take the poset ${\mathbb{2}}=\{0<1\}$. If we are given a poset ${\mathsf{At}}$ of atomic propositions, the syntax is defined inductively as follows:

[TABLE]

In the above, $p$ is any atomic proposition, $\varphi={\uparrow}\{a_{1},\dots,a_{k}\}$ is a finitely generated upperset and $\psi={\downarrow}\{a_{1},\dots,a_{k}\}$ is a finitely generated lowerset of formulas, and the $n$ in $\nabla_{T^{\partial}_{\omega}}(n,a)$ is an element of ${\mathbb{2}}$. Observe that $\nabla$ is monotone with respect to the first argument.

Hence the more relaxed description of the syntax can be given by

[TABLE]

5.B. The semantics of the coalgebraic language

The above language ${\mathcal{L}}$ will be interpreted in coalgebras for the functor $T$. More precisely, given a coalgebra $c:X\longrightarrow TX$, the semantics will be given by a monotone relation

\textstyle{\Vdash_{0}:{\mathsf{At}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X^{\mathit{op}}}

called a monotone valuation of propositional atoms. The valuation being monotone, $x\leq y$ and $x\Vdash_{0}p$ implies $y\Vdash_{0}p$, and $p\leq_{\mathcal{L}}q$ and $x\Vdash_{0}p$ implies $x\Vdash_{0}q$.

We extend $\Vdash_{0}$ to obtain the semantics

\textstyle{\Vdash:{\mathcal{L}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X^{\mathit{op}}}

of an arbitrary formula $a$ by induction on $a$ as follows:

[TABLE]

Remark 14**.**

The semantics for conjunction and disjunction is standard. The semantics for the modal formula $\nabla_{T^{\partial}_{\omega}}\alpha$ in a state $x$ is given by checking whether the $T^{\partial}$-lifted $\Vdash$ relation contains $c(x)$ and $\alpha$: for type-checking reasons, this is achieved by composing the lifted $\Vdash$ relation with the graph of the natural inclusion of $T^{\partial}_{\omega}$ in $T^{\partial}$, i.e. $(\nu^{T^{\partial}}_{{\mathcal{L}}})_{\diamond}$:

[TABLE]

We can also equivalently write it like this:

[TABLE]

The semantics of nabla is indeed well defined: in the inductive process of defining the relation $\Vdash$ we use the fact that relation lifting commutes with restrictions (see Definition 4 and Example 4). In particular, to compute the lifted relation it is enough to have $\Vdash$ restricted to the base of $\alpha$, whose semantics has been defined previously. Unravelling this yields the following simplification, using the lifted restricted relation ${\Vdash}(-,{\mathsf{base}}(\alpha)-)$: Let \textstyle{{\mathsf{base}}(\alpha):Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{L}} and $z\in Z$ be the unique element with $T^{\partial}{\mathsf{base}}(\alpha)(z)=\alpha$.

[TABLE]

Remark 15**.**

Recall from Remark 13 that ${\mathcal{L}}$ is a poset. The above semantics allows us to define a monotone relation

\textstyle{\sqsubseteq:{\mathcal{L}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{L}}

by putting:

[TABLE]

The relation $\sqsubseteq$ is reflexive (i.e., the relation ${\leq_{\mathcal{L}}}$ is smaller than ${\sqsubseteq}$) and transitive (i.e., the composite relation ${\sqsubseteq}\cdot{\sqsubseteq}$ is smaller than ${\sqsubseteq}$). Therefore $\sqsubseteq$ allows us to define an order-quotient ${\mathcal{Q}}={\mathcal{L}}/{\sqsubseteq}$ of ${\mathcal{L}}$. The elements of the poset $\mathcal{Q}$ are equivalence classes $[a]_{\equiv}$ where

[TABLE]

and $\leq_{\mathcal{Q}}$ is the least order such that $a\sqsubseteq b$ entails $[a]_{\equiv}\leq_{\mathcal{Q}}[b]_{\equiv}$.

The quotient $\mathcal{Q}$ carries an algebra structure for ${\mathbb{U}}_{\omega}+{\mathbb{L}}_{\omega}+T^{\partial}_{\omega}$ that is derived from the algebra structure on ${\mathcal{L}}$.

{exa}

1. (1)

Nabla for the functor $T=A\times{\mathit{Id}}$. Observe that, $T=T_{\omega}$, and the functor dual to $T_{\omega}$ is:

[TABLE]

If we fix a coalgebra $c=\langle out,next\rangle:X\longrightarrow A\times X$, then it holds that

[TABLE]

since the lifting of the semantics relation

\textstyle{\Vdash:{\mathcal{L}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X^{\mathit{op}}}

is the relation

[TABLE]

The monotonicity of $\Vdash$ says that

1. (a)

If $x\leq_{X}x^{\prime}$ and $x\Vdash\nabla_{T^{\partial}_{\omega}}(a,b)$, then $x^{\prime}\Vdash\nabla_{T^{\partial}_{\omega}}(a,b)$, and 2. (b)

if $a\geq_{A}a^{\prime}$ and $b\leq_{\mathcal{L}}b^{\prime}$, then $x\Vdash\nabla_{T^{\partial}_{\omega}}(a,b)$ implies that $x\Vdash\nabla_{T^{\partial}_{\omega}}(a^{\prime},b^{\prime})$. 2. (2)

Nabla for the functor $T={\mathbb{L}}^{A}\times{\mathbb{2}}$. Observe that the arity of nabla is:

[TABLE]

By definition, $x\Vdash\nabla_{T^{\partial}_{\omega}}\alpha$ holds if and only if $c(x)(\mathrel{\overline{T^{\partial}}{\Vdash}\cdot(\nu^{T^{\partial}}_{{\mathcal{L}}})_{\diamond}})\alpha$ holds. Suppose $c(x)$ is a tuple $(l,i)$ and $\alpha$ is a tuple $(o,j)$. Then this is the case if and only if

[TABLE]

We can again use the monotonicity of the semantics relation $\Vdash$ to weaken the above condition: $c(x)(\mathrel{\overline{T^{\partial}}{\Vdash}\cdot(\nu^{T^{\partial}}_{{\mathcal{L}}})_{\diamond}})\alpha$ holds if and only if

[TABLE]

Here $g(l(a))$ and $g(o(a))$ are, again, the generators for the lowerset $l(a)$ in $X$ and upperset $o(a)$ in ${\mathcal{L}}$, respectively. 3. (3)

Recall from Example 2.B that a frame for positive modal logic is a poset $X$ equipped with a monotone relation

\textstyle{R:X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}

that gives rise to two coalgebras

[TABLE]

defined by $c(x)=\{y\ |\ R(x,y)\}$ and $d(x)=\{y\ |\ R(y,x)\}$. The modalities $\Box$ and $\blacklozenge$ defined by the equivalences

[TABLE]

are adjoint in the sense that $a\sqsubseteq\Box b$ holds if and only if $\blacklozenge a\sqsubseteq b$ holds, where $\sqsubseteq$ is the semantic preorder as defined in (5.9).

Now, using the definition of the modalities $\nabla_{{\mathbb{L}}_{\omega}}$ and $\nabla_{{\mathbb{U}}_{\omega}}$ and the corresponding liftings of the semantics $\Vdash$, we see that

[TABLE]

Therefore

[TABLE]

and also conversely

[TABLE] 4. (4)

Let $T={\mathbb{P}}^{c}$, and $T^{\partial}_{\omega}={\mathbb{P}}^{c}_{\omega}$. Recall from Example 2.B that ${\mathbb{P}}^{c}$ coalgebras can be used as semantics for positive modal logic. For a coalgebra $c:X\longrightarrow{\mathbb{P}}^{c}X$ and a monotone valuation, we have

[TABLE]

By the definition of the semantics for $\nabla_{{\mathbb{P}}^{c}_{\omega}}$ and the relation lifting, we see that for $\alpha$ in ${\mathbb{P}}^{c}_{\omega}{\mathcal{L}}$

[TABLE]

As $\alpha$ is a finitely generated convex subset of formulas, we can create a finitely generated upperset of formulas ${\uparrow}\alpha$, and a finitely generated lowerset of formulas ${\downarrow}\alpha$. Then

[TABLE]

and also conversely

[TABLE]

just the same way as it is in the classical finitary Moss’ logic [KKV12b]. 5. (5)

Recall the semantics of small description logic EL from Example 2.B The syntax consists of a poset $N^{c}$ of concept names ordered by concept subsumptions of the form $A\sqsubseteq B$, a poset $N^{r}$ of role names ordered by role subsumptions of the form $r\sqsubseteq s$, and the following grammar of concepts:

[TABLE]

This results in a poset ${\mathcal{L}}$ of concept expressions. The semantics is based on a discrete poset (i.e. a set) $\Delta$ together with: (ii) interpretations $C^{I}$ of concept names by lowersets of $\Delta$ (i.e. subsets of $\Delta$) respecting their order: $C\sqsubseteq D$ implies $C^{I}\subseteq D^{I}$, (ii) interpretations $r^{I}$ of role names by binary relations on $\Delta$, again respecting their order: $r\sqsubseteq s$ implies $r^{I}\subseteq s^{I}$. We can see each structure of this kind as a coalgebra

[TABLE]

which, for each $d\in\Delta$, assigns: for each role name $r$ the lowerset (i.e. subset) $\{e\ |\ (d,e)\in r^{I}\}$, and for each concept name $C$ the value $1$ if $d\in C^{I}$, and the value [math] otherwise. Both assignments are monotone.

For the sake of this example, we shall extract the $v:\Delta\longrightarrow{\mathbb{2}}^{N^{c}}$ part of the coalgebra structure and treat it as a monotone valuation of concept names

\textstyle{\Vdash:N^{c}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\Delta^{\mathit{op}}}

instead. The relation extends inductively to all concept expressions as follows:

[TABLE]

The monotonicity of $\Vdash$ entails that if $C\sqsubseteq_{\mathcal{L}}D$ and $d\Vdash C$, than also $d\Vdash D$.

Each $\beta\in({\mathbb{U}}_{\omega}{\mathcal{L}})^{N^{r}}$ can be seen as a monotone assignment of uppersets of concepts to role names. Unravelling the semantics of the modality $\nabla_{({\mathbb{U}}_{\omega})^{N^{r}}}$ on a coalgebra $c:\Delta\longrightarrow({\mathbb{L}}\Delta)^{N^{r}}$, we see that

[TABLE]

Therefore

[TABLE]

and also conversely

[TABLE]

where $\beta\in({\mathbb{U}}_{\omega}{\mathcal{L}})^{N^{r}}$ is a monotone assignment of uppersets of concepts to role names such that $\beta(r)=C{\uparrow}$ and $\beta(s)=\top$ for all $s\neq r$. 6. (6)

Recall frames for distributive substructural logics from Example 2.B. We restrict ourselves to ternary relations $R$ that generate coalgebras of the form $c_{\otimes}:X\longrightarrow{\mathbb{L}}(X\times X)$.

The polynomial coalgebra functor $T={\mathbb{L}}({\mathit{Id}}\times{\mathit{Id}})$ is locally monotone and satisfies BCC. Its relation lifting is easy to compute, using the properties listed in Example 4. The semantics of the nabla modality with the arity $T_{\omega}^{\partial}={\mathbb{U}}_{\omega}({\mathit{Id}}\times{\mathit{Id}})$, works as follows:

[TABLE]

Therefore

[TABLE]

and conversely

[TABLE]

5.C. Hennessy-Milner property

We now turn to proving that the finitary language defined in Subsection 5.A is adequate and, in the finitary case $T$=$T_{\omega}$, also expressive for the following notion of similarity, which is defined in terms of relation lifting.

{defi}

We fix two pointed models $(c,\Vdash_{c},x_{0})$ and $(d,\Vdash_{d},y_{0})$, i.e., we fix coalgebras $c:X\longrightarrow TX$ and $d:Y\longrightarrow TY$, valuations $\Vdash_{c}$ and $\Vdash_{d}$, and $x_{0}\in X$ and $y_{0}\in Y$.

1. (1)

A relation

\textstyle{S:Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}

is called a $T$-simulation (from $(d,\Vdash_{d},y_{0})$ to $(c,\Vdash_{c},x_{0})$), if the following three conditions are satisfied:

1. (a)

$S(x_{0},y_{0})$ holds. 2. (b)

For any $x\in X$ and $y\in Y$, $S(x,y)$ implies $\overline{T}S(c(x),d(y))$. 3. (c)

If $S(x,y)$ holds, then $x\Vdash_{c}p$ implies $y\Vdash_{d}p$, for each atom $p$ in ${\mathsf{At}}$.

And we say that $(d,\Vdash_{d},y_{0})$ simulates $(c,\Vdash_{c},x_{0})$, if there is a simulation

\textstyle{S:Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}

from $(d,\Vdash_{d},y_{0})$ to $(c,\Vdash_{c},x_{0})$. 2. (2)

We say that $(d,\Vdash_{d},y_{0})$ is modally stronger than $(c,\Vdash_{c},x_{0})$, if $x_{0}\Vdash_{c}a$ implies $y_{0}\Vdash_{d}a$, for each formula $a$.

Remark 16**.**

The notion of simulation given by the monotone relation lifting coincides with the one given by Worrell in [Wor00] in the enriched setting of ${\mathscr{V}}$-categories (of which preorders, hence also posets, are a special case for ${\mathscr{V}}={\mathbb{2}}$). It is also shown in [Wor00] that similarity coincides with the preorder on the final coalgebra, whenever the final coalgebra exists.

{exa}

Fix the empty poset ${\mathsf{At}}$ of atomic propositions. Taking two coalgebras $c:X\longrightarrow A\times X$ and $d:Y\longrightarrow A\times Y$ with two distinguished states $x_{0}\in X$ and $y_{0}\in Y$, the notion of simulation yields that $(d,\Vdash,y_{0})$ simulates $(c,\Vdash,x_{0})$ if the infinite stream $\gamma$ obtained as the behaviour of $x_{0}$ is pointwise smaller than the infinite stream $\delta$ obtained as the behaviour of $y_{0}$.

Proposition 17**.**

Assume $T$ complies with the Assumption 5, and ${\mathcal{L}}$ is defined as in Definition 12.

1. (1)

The language ${\mathcal{L}}$ is adequate for $T$-coalgebras: if $(d,\Vdash_{d},y_{0})$ simulates $(c,\Vdash_{c},x_{0})$, then $(d,\Vdash_{d},y_{0})$ is modally stronger than $(c,\Vdash_{c},x_{0})$.

and

1. (2)

The language ${\mathcal{L}}$ is expressive for $T_{\omega}$-coalgebras: if $(d,\Vdash_{d},y_{0})$ is modally stronger than $(c,\Vdash_{c},x_{0})$, then $(d,\Vdash_{d},y_{0})$ simulates $(c,\Vdash_{c},x_{0})$. Moreover, the relation “being modally stronger” is a $T_{\omega}$-simulation.

Proof 5.1**.**

(1) Let us assume that $(d,\Vdash_{d},y_{0})$ simulates $(c,\Vdash_{c},x_{0})$ via a simulation

\textstyle{S:Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X} . We need to prove that $x_{0}\Vdash_{c}a$ implies $y_{0}\Vdash_{y}a$ for every formula $a$. The adequacy is proved by induction on the complexity of a given formula $a$.

The case when $a$ is an atom is immediate from $S$ being a simulation, the cases of conjunction and disjunction are easy. For the induction step for $a=\nabla\alpha$, let us assume that $x_{0}\Vdash_{c}\nabla\alpha$ holds. The induction hypothesis states that for every $x\in X$, $y\in Y$ and $z\in{\mathsf{base}}(\alpha)$ the following implication holds:

[TABLE]

The induction hypothesis can equivalently be described as a lax triangle

[TABLE]

denoting the base of

\textstyle{\alpha:Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{T^{\partial}_{\omega}{\mathcal{L}}}

by

\textstyle{{\mathsf{base}}(\alpha):\widetilde{Z}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{L}} .

We shall prove that for any $x$ in $X$, $y$ in $Y$, and $w\in T^{\partial}_{\omega}{\mathsf{base}}(\alpha)$, the following implication holds:

[TABLE]

The relation $\overline{T}S(c(x_{0}),d(y_{0}))$ holds since $S$ is a simulation. Moreover, $c(x_{0})(\mathrel{\overline{T^{\partial}}{\Vdash_{c}}\cdot(\nu^{T^{\partial}}_{{\mathcal{L}}})_{\diamond}})\alpha$ holds since $x_{0}\Vdash_{c}\nabla\alpha$ holds. Since $\alpha\in T^{\partial}{\mathsf{base}}(\alpha)$ (to be precise, $\alpha\in T^{\partial}_{\omega}{\mathsf{base}}(\alpha)$, but the base is a finite poset and therefore $T^{\partial}$ and $T^{\partial}_{\omega}$ coincide on it), we could instantiate the implication to get that $d(y_{0})(\mathrel{\overline{T^{\partial}}{\Vdash_{d}}\cdot(\nu^{T^{\partial}}_{{\mathcal{L}}})_{\diamond}})\alpha$ holds, and this would yield $y_{0}\Vdash_{d}\nabla\alpha$ as we wanted.

However, the implication (5.14) can be expressed by the following diagram. The lax triangle is simply the image under $\overline{T^{\partial}}$ of (5.13), and we formally pre-compose it with graph of the natural inclusion $(\nu^{T^{\partial}}_{{\mathcal{L}}})_{\diamond}$ (which, by $\widetilde{Z}$ being finite, is the identity):

[TABLE]

(2) For this part, we assume $T=T_{\omega}$ (i.e., the coalgebra functor is finitary). As both the coalgebra functor $T_{\omega}$ and the arity functor $T^{\partial}_{\omega}$ are finitary, we can simplify the semantic clause for $x\Vdash\nabla_{T^{\partial}_{\omega}}\alpha$ to

[TABLE]

Expressivity boils down to proving that “being modally stronger” is a $T_{\omega}$-simulation. For the purpose of the proof, write

[TABLE]

to denote that $(d,\Vdash_{d},y)$ is modally stronger than $(c,\Vdash_{c},x)$.

Hence the following implication holds for any formula $a$:

[TABLE]

It is clear that $S$ verifies the properties (a) and (c) of $T_{\omega}$-simulations from Definition 5.C. It remains to be proved that $S$ satisfies the property (b):

[TABLE]

Assume therefore that $S(x,y)$ holds and denote the corresponding bases of $c(x)$ and $d(y)$ by

[TABLE]

We first construct a monotone map $f:X^{\mathit{op}}\longrightarrow{\mathcal{L}}$ such that for any $x^{\prime}\in X$ and $w\in{\mathsf{base}}(d(y))$ the following two requirements hold:

[TABLE]

Fix $x^{\prime}$ in $X$, and for each $w\in{\mathsf{base}}(d(y))$ such that

[TABLE]

pick a formula $b_{(x^{\prime},w)}$ for which $x^{\prime}\Vdash_{c}b_{(x^{\prime},w)}$ but $w\not\Vdash_{d}b_{(x^{\prime},w)}$, which is possible by $\neg S(x^{\prime},w)$ and (5.15). Define

[TABLE]

The above conjunction is finitary since $W$ is a finite poset. In case the conjunction is empty, we set $f(x^{\prime})=\top$. Moreover, $f$ is a monotone map (with $x^{\prime\prime}\geq x^{\prime}$ the number of conjuncts in the definition of $f(x^{\prime\prime})$ decreases), and the properties (5.17) and (5.18) hold. In particular, given any $u\in{\mathsf{base}}(c(x))$, the implication

[TABLE]

holds.

The latter implication can be expressed as a 2-cell

[TABLE]

in ${\mathsf{Rel}}$. We apply the functor $\overline{T^{\partial}_{\omega}}$ to it and use the properties of relation lifting to obtain a 2-cell

[TABLE]

By the unit property of ${\mathsf{base}}$, we know that

[TABLE]

holds. Therefore we can use (5.19) and the definition of the converse of a relation to observe that $\overline{T_{\omega}}S(c(x),d(y))$ holds whenever $d(y)\mathrel{\overline{T_{\omega}^{\partial}}{\Vdash_{d}}}(T_{\omega}^{\partial}f)c(x)$ holds.

The relation $d(y)\mathrel{\overline{T_{\omega}^{\partial}}{\Vdash_{d}}}(T_{\omega}^{\partial}f)c(x)$ holds iff $y\Vdash_{d}\nabla((T_{\omega}^{\partial}f)c(x))$ holds. Since we assume that $S(x,y)$ holds, it is enough to prove that $x\Vdash_{c}\nabla((T_{\omega}^{\partial}f)c(x))$ holds, and $y\Vdash_{d}\nabla((T_{\omega}^{\partial}f)c(x))$ will follow.

By (5.17) we know that $x^{\prime}\Vdash_{c}f(x^{\prime})$ holds for every $x^{\prime}$. Thus we get the inequality ${\mathit{id}}_{X}\leq{\Vdash_{c}}(-,f-)$, and by applying the functor $\overline{T_{\omega}^{\partial}}$ to it, we obtain the inequality ${\mathit{id}}_{T_{\omega}^{\partial}X}\leq\overline{T_{\omega}^{\partial}}{\Vdash_{c}}(-,T_{\omega}^{\partial}f-)$. Hence $c(x)\mathrel{\overline{T_{\omega}^{\partial}}{\Vdash_{c}}}(T_{\omega}^{\partial}f)c(x)$ holds, and therefore $x\Vdash_{c}\nabla((T_{\omega}^{\partial}f)c(x))$ holds as required.

5.D. A dual modality $\Delta$

In the preceding paragraphs we proved that the coalgebraic language ${\mathcal{L}}$ with a single nabla modality is adequate, and in the finitary case also expressive. Nevertheless, we introduce another modality $\Delta$ in this subsection. The semantics of this modality will show that $\Delta$ is, in a sense, dual to $\nabla$. Why would we want to extend the language with a new modality, knowing that the language with nabla as the only modality is already expressive? It will turn out that the dual modality is crucial in designing a cut-free two-sided sequent calculus which is sound and complete for the logic of $T$-coalgebras.

The definition of semantics of $\Delta$ below is a straightforward adaptation of a similar modality studied in [KV09] in the context of complementation of coalgebraic automata in the case of ${\mathsf{Set}}$ and classical Moss’ logic, where $\Delta$ is the boolean dual of $\nabla$. For the classical Moss’ logic in ${\mathsf{Set}}$, the dual modality $\Delta$, and its mutual definability with the modality $\nabla$, played a crucial role in the formulation of a cut-free two-sided sequent calculus as shown in [BPV14]. Without the boolean negation, a one-sided sequent calculus is not available in our case already for the propositional part of the language ${\mathcal{L}}$. For that reason we aim at a two-sided calculus, and therefore it is convenient to have a modality dual to nabla in the language.

We extend the language ${\mathcal{L}}$ with a monotone modality

[TABLE]

Given a coalgebra $c:X\longrightarrow TX$ and a monotone valuation

\textstyle{\Vdash:{\mathcal{L}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X^{\mathit{op}}} , the semantics of $\Delta_{T^{\partial}}$ is defined negatively by the relation lifting of the negated relation

\textstyle{\nVdash:{\mathcal{L}}^{\mathit{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}

as follows:

[TABLE]

Before we discuss the mutual relation of the two modalities $\nabla$ and $\Delta$, we illustrate the semantics of $\Delta$ on the running examples:

{exa}

1. (1)

Delta for the functor $T=A\times{\mathit{Id}}$. Let us fix a coalgebra $c=\langle out,next\rangle:X\longrightarrow A\times X$. The semantics of the modality $\Delta$ is then given as follows:

[TABLE] 2. (2)

Delta for the functor $T=({\mathit{Id}})^{A}\times{\mathbb{2}}$. Fix a coalgebra $c:X\longrightarrow X^{A}\times{\mathbb{2}}$. If for some state $x\in X$ we denote by $c(x)=(f,i)$ the successors and output of $x$, the semantics of the modality $\Delta$ in the state $x$ is given as follows:

[TABLE] 3. (3)

Delta for the functor $T=({\mathbb{L}})^{A}\times{\mathbb{2}}$. For a coalgebra $c:X\longrightarrow({\mathbb{L}}X)^{A}\times{\mathbb{2}}$ and for its state $x$ with $c(x)=(l,i)$, we have that $x\Vdash\Delta(p,j)$ holds if and only if

[TABLE] 4. (4)

Consider again frames for modal logic with adjoint modalities (see Example 2.B). We only consider coalgebras of the form $c:X\longrightarrow{\mathbb{U}}X$ for this example. The semantics of $\Delta_{{\mathbb{L}}_{\omega}}$ works as follows:

[TABLE]

Therefore

[TABLE]

Recall from Example 5.B that

[TABLE]

We see that in this particular example $\Delta$ is definable by $\nabla$ as follows:

[TABLE]

Since the arity functor ${\mathbb{L}}_{\omega}$ is finitary, the above expression is a well-formed formula. 5. (5)

Consider ${\mathbb{P}}^{c}$ coalgebras for positive modal logic (see Example 2.B). The semantics of $\Delta_{{\mathbb{P}}^{c}_{\omega}}$ works as follows

[TABLE]

Therefore

[TABLE]

Recall from Example 5.B that

[TABLE]

Thus $\Delta_{{\mathbb{P}}^{c}_{\omega}}\beta$ can be expressed as a disjunction of $\nabla_{{\mathbb{P}}^{c}_{\omega}}$-formulas as follows:

[TABLE]

The above example suggests that the modality $\Delta$ might always be expressible by a certain disjunction of $\nabla$ formulas. This is indeed true, but the disjunction need not in general be finitely generated: for some coalgebra functors the disjunction of the $\nabla$ formulas needed in the expression is inherently infinite and thus $\Delta$ is not definable by a well-formed formula of the finitary language. The mutual definability of the two modalities becomes important when formulating rules of the sequent calculus.

To explain the relationship between the modalities $\nabla$ and $\Delta$, we need to unravel the combinatorial principle underlying their mutual translations. It will not be as simple as the previous example suggests, but let us have a glimpse at it first. Take an upperset ${\uparrow}{b}$ for some b\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}\beta, and generate a lowerset from it in ${\mathbb{L}}_{\omega}{\mathbb{U}}_{\omega}{\mathcal{L}}$. Call it $\Phi_{b}$. It has the following property: \Phi_{b}\neg\overline{{\mathbb{U}}_{\omega}}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}}\beta. Moreover, applying the ${\mathbb{L}}_{\omega}\bigwedge$ map to $\Phi_{b}$ yields an element in ${\mathbb{L}}_{\omega}{\mathcal{L}}$, namely, the lowerset of conjunctions of uppersets containing $b$. It is generated by $\bigwedge{\uparrow}{b}$. We may apply $\nabla_{{\mathbb{L}}_{\omega}}$ to it. The above example suggests, that one of the formulas $\nabla_{{\mathbb{L}}_{\omega}}\bigwedge{\uparrow}{b}$ will be true whenever $\Delta_{{\mathbb{L}}_{\omega}}\beta$ is true.

The underlying operations suggested by the above are in particular the lifted relations \neg\overline{T}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}} and \neg\overline{T}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}}. We describe them first, as they will play a crucial role in the mutual definitions. We provide an inductive definition of these relations for the case of $T$ being a Kripke-polynomial functor.

{exa}

We state explicit formulas for the relation

\textstyle{\neg\overline{T}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}}:T^{\partial}{\mathbb{L}}_{\omega}X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{T^{\partial}X}

when $T$ is a Kripke-polynomial functor.

1. (1)

$T={\mathit{const}}_{E}$: The relation

\textstyle{\neg\overline{E}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}}:E^{\mathit{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{E^{\mathit{op}}}

is the relation

\textstyle{\not\leq_{E}:E^{\mathit{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{E^{\mathit{op}}} . 2. (2)

$T={\mathit{Id}}$: The relation

\textstyle{\neg\overline{{\mathit{Id}}}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}}:{\mathbb{L}}_{\omega}X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X}

is the relation

\textstyle{\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}:{\mathbb{L}}_{\omega}X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X} . 3. (3)

$T=T_{1}+T_{2}$: Let $\alpha$ be in $T_{i}^{\partial}X$ and $\Phi$ be in $T_{j}^{\partial}{\mathbb{L}}_{\omega}X$ for some $i,j$ in $\{1,2\}$. The relation \alpha\mathrel{\neg(\overline{T_{1}+T_{2}}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}})}\Phi holds iff $i\neq j$ or \alpha\mathrel{\neg\overline{T_{i}}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}}}\Phi with $i=j$. 4. (4)

$T=T_{1}\times T_{2}$: The relation (\alpha_{1},\alpha_{2})\mathrel{\neg(\overline{T_{1}\times T_{2}}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}})}(\Phi_{1},\Phi_{2}) holds iff \alpha_{1}\mathrel{\neg\overline{T_{1}}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}}}\Phi_{1} or \alpha_{2}\mathrel{\neg\overline{T_{2}}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}}}\Phi_{2} holds. 5. (5)

$T=T_{1}^{E}$: Generalising the case (4), the relation \alpha\mathrel{\neg\overline{T_{1}^{E}}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}}}\Phi holds iff there is some $e$ from $E$ such that \alpha(e)\mathrel{\neg\overline{T_{1}}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}}}\Phi(e) holds. 6. (6)

$T={\mathbb{L}}_{\omega}T_{1}$: The relation v\mathrel{\neg\overline{{\mathbb{L}}_{\omega}T_{1}}{\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}}}u holds iff the following condition is satisfied:

[TABLE]

The formulas for the relation

\textstyle{\neg\overline{T}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}}:T^{\partial}{\mathbb{L}}_{\omega}X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{T^{\partial}X}

are easy to obtain by dual reasoning. For example, the relation u\mathrel{\neg\overline{{\mathbb{L}}_{\omega}T_{1}}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}}}v holds if and only if the following condition is satisfied:

[TABLE]

Next we define collections $R_{\alpha}$ and $L_{\beta}$, parametric in $\alpha\in T^{\partial}_{\omega}{\mathcal{L}}$ and $\beta\in T^{\partial}_{\omega}{\mathcal{L}}$ respectively. $R_{\alpha}$ contains all $\Psi\in T^{\partial}_{\omega}{\mathbb{L}}_{\omega}{\mathsf{base}}(\alpha)$ of which $\alpha$ is not a lifted non-member. Similarly, $L_{\beta}$ contains all $\Phi\in T^{\partial}_{\omega}{\mathbb{U}}_{\omega}{\mathsf{base}}(\beta)$ of which $\beta$ is not a lifted non-member. The collection $R_{\alpha}$ will be explicitly used to rewrite a formula $\nabla_{T^{\partial}_{\omega}}\alpha$ as a conjunction of delta-formulas by the right rule $\nabla$-r in the calculus in the next section (hence the notation). Similarly, $L_{\beta}$ will be used in rewriting a formula $\Delta_{T^{\partial}_{\omega}}\beta$ as a disjunction of nabla-formulas by the left rule $\Delta$-l in the calculus.

{defi}

Let us fix elements $\alpha\in T^{\partial}_{\omega}{\mathcal{L}}$ and $\beta\in T^{\partial}_{\omega}{\mathcal{L}}$. We define the collections $R_{\alpha}$ and $L_{\beta}$ as follows:

1. (1)

$R_{\alpha}$ is the collection of all elements $\Psi\in T^{\partial}_{\omega}{\mathbb{L}}_{\omega}{\mathsf{base}}(\alpha)$ with

[TABLE] 2. (2)

$L_{\beta}$ is the collection of all elements $\Phi\in T^{\partial}_{\omega}{\mathbb{U}}_{\omega}{\mathsf{base}}(\beta)$ with

[TABLE]

{exa}

To illustrate the above definition we give two simple examples:

1. (1)

Consider $T^{\partial}_{\omega}={\mathbb{L}}_{\omega}$, thus $T_{\omega}={\mathbb{U}}_{\omega}$. Note that \alpha\neg\overline{{\mathbb{U}}_{\omega}}\not\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}\Psi holds iff

[TABLE]

For $\alpha=\{\bot\}$, the collection $R_{\{\bot\}}$ consists of those elements $\Psi$ of ${\mathbb{L}}_{\omega}{\mathbb{L}}_{\omega}\{\bot\}$, where some \psi\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}\Psi contains $\bot$. The only such lowerset $\Psi$ is $\{\emptyset,\{\bot\}\}$. Thus $R_{\{\bot\}}$ equals $\{\{\emptyset,\{\bot\}\}\}$. 2. (2)

Consider $T^{\partial}=\mathbb{N}^{\mathit{op}}\times{\mathit{Id}}$ where $\mathbb{N}$ is the poset of natural numbers with their natural order, and $T=\mathbb{N}\times{\mathit{Id}}$. For $\alpha=(5,b\wedge c)$, the collection $R_{(5,b\wedge c)}$ consists of elements $(n,\psi)$ of $N^{\mathit{op}}\times{\mathbb{L}}_{\omega}{\mathsf{base}}(5,b\wedge c)$ where $5\nleq n$ or b\wedge c\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}\psi. Note that ${\mathbb{L}}_{\omega}{\mathsf{base}}(5,b\wedge c)=\{\emptyset,\{b\wedge c\}\}$. Therefore $R_{(5,b\wedge c)}=\{(n,\emptyset)\ |\ 5\nleq n\}\cup\{(n,\{b\wedge c\})\ |\ n\in N\}$.

To compare the current setting with the classical Moss’ logic: It was shown in [KV09] that the two modalities $\nabla$ and $\Delta$ are mutually definable already in the positive fragment of the classical Moss’ logic. Their mutual definability was used in [BPV14] in designing a two-sided sequent proof system for the logic. We will state a similar fact in the poset-setting in the following two propositions. They will be applied in the next section, when we define a sequent proof system.

Proposition 18**.**

For each coalgebra $c:X\longrightarrow TX$ and every semantics relation $\Vdash_{c}$, the relations

[TABLE]

and

[TABLE]

are equal.

In other words, for each $x$ in $X$, and each $\beta$ in $T^{\partial}_{\omega}{\mathcal{L}}$, we have that $x\Vdash_{c}\Delta\beta$ holds if and only if there is a $\Phi_{x}$ in $T^{\partial}_{\omega}{\mathbb{U}}_{\omega}{\mathcal{L}}$ such that

[TABLE]

Whenever $L_{\beta}$ is finite, we have the following semantic equivalence:

[TABLE]

Proof 5.2**.**

The guiding ideas in the proof are quite simple, however, much of the work is due to type-checking reasons. We divide the proof into several parts:

1. (1)

The inequality {\Vdash_{c}}(-,\Delta-)\cdot(\nu^{T^{\partial}}_{{\mathcal{L}}})_{\diamond}\leq{\Vdash_{c}}(-,\nabla T^{\partial}_{\omega}\bigwedge-)\cdot\neg(\overline{T_{\omega}}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}}).

Suppose that $x\Vdash\Delta\beta$ holds. We will construct an element $\Phi$ in $(T^{\partial}_{\omega}{\mathbb{U}}_{\omega}{\mathcal{L}})^{\mathit{op}}$ such that

[TABLE]

The main idea for this part of the proof is to simply consider the monotone map assigning to a state $x$ the finitely generated upperset of formulas from ${\mathsf{base}}(\beta)$ it satisfies:

[TABLE]

Most of what follows concerns restricting along ${\mathsf{base}}(\beta)$. Using the

\textstyle{{\mathsf{base}}(\beta):W\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{L}} with $W$ finite, we can factorise $f^{\sharp}$ as follows:

[TABLE]

The mapping $f$ with a finite range is then defined as

[TABLE]

Therefore, applying the functor $T$ to $f$ yields an element $(Tf)c(x)$ in $(T^{\partial}{\mathbb{U}}_{\omega}W)^{\mathit{op}}$. Observe first that because $W$ (and therefore ${\mathbb{U}}_{\omega}W$) is a finite poset, we have that $T^{\partial}({\mathbb{U}}_{\omega}W)^{\mathit{op}}=T^{\partial}_{\omega}({\mathbb{U}}_{\omega}W)^{\mathit{op}}$ (i.e., the corresponding natural inclusion $\nu^{T^{\partial}}_{{\mathbb{U}}_{\omega}W}$ is the identity). We may therefore define the element $\Phi_{x}$ in $(T^{\partial}_{\omega}{\mathbb{U}}_{\omega}W)^{\mathit{op}}$ to be the unique one with

[TABLE]

As $({\mathbb{U}}_{\omega}W)^{\mathit{op}}$ is included in $({\mathbb{U}}_{\omega}{\mathcal{L}})^{\mathit{op}}$ via a mono morphism $({\mathbb{U}}_{\omega}{\mathsf{base}}(\beta))^{\mathit{op}}$, we may put

[TABLE]

and see that it is indeed an element of $(T^{\partial}_{\omega}{\mathbb{U}}_{\omega}{\mathcal{L}})^{\mathit{op}}$. Relaxing the typing, we could say that $\Phi,\Phi_{x}$, and $(Tf)c(x)$ are the same thing. The situation is depicted in the following naturality square:

[TABLE]

Let

\textstyle{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}^{\prime}:W^{\mathit{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{({\mathbb{U}}_{\omega}W)^{\mathit{op}}}

be the restriction of the relation

\textstyle{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}:{\mathcal{L}}^{\mathit{op}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{({\mathbb{U}}_{\omega}{\mathcal{L}})^{\mathit{op}}}

along ${\mathsf{base}}(\beta)$, i.e. \not\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}^{\prime}\ =\ \not\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}({\mathbb{U}}_{\omega}{\mathsf{base}}(\beta)-,{\mathsf{base}}(\beta)-). We obtain that $\Phi$ is related with $\beta$ via the lifted \not\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}} relation, i.e. \Phi\mathrel{{\overline{T_{\omega}}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}}}}\beta, if and only if $\Phi_{x}$ and $\beta$ relate in the lifted \not\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}^{\prime} relation restricted along ${\mathsf{base}}(\beta)$, i.e. \Phi_{x}\mathrel{{\overline{T_{\omega}}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}^{\prime}}}}\beta This will concern the point (a) below.

Similarly, let

\textstyle{\Vdash_{c}^{\prime}:W\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X^{\mathit{op}}}

be the restriction of the relation

\textstyle{\Vdash_{c}:{\mathcal{L}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X^{\mathit{op}}}

along ${\mathsf{base}}(\beta)$, i.e. $\Vdash_{c}^{\prime}\ =\ \Vdash_{c}(-,{\mathsf{base}}(\beta)-)$. We obtain that $c(x)$ and $\nu_{\mathcal{L}}^{T^{\partial}}(\beta)$ are related via the lifted $\nVdash_{c}$ relation, i.e. $c(x)(\mathrel{{\overline{T}{\nVdash_{c}}}})\nu_{\mathcal{L}}^{T^{\partial}}(\beta)$, if and only if $c(x)$ and $\beta$ are related via the lifted restricted $\nVdash_{c}^{\prime}$ relation as follows: $c(x)(\mathrel{{\overline{T}{\nVdash_{c}^{\prime}}}})\beta$. This will concern the point (a) below.

For the conjunction map (restricted to ${\mathsf{base}}(\beta)$) $\bigwedge:{\mathbb{U}}_{\omega}W\longrightarrow{\mathcal{L}},$ the restricted relation $\Vdash_{c}(-,\bigwedge-)$ of “satisfying conjunctions of formulas from ${\mathsf{base}}(\beta)$” will be considered in the point (b) below. We obtain that $c(x)$ and $\nu_{\mathcal{L}}^{T^{\partial}}((T^{\partial}_{\omega}\bigwedge)\Phi)$ are related via the lifted $\Vdash_{c}$ relation, i.e. $c(x)(\mathrel{{\overline{T^{\partial}}{\Vdash_{c}}}})\nu_{\mathcal{L}}^{T^{\partial}}((T^{\partial}_{\omega}\bigwedge)\Phi)$, if and only if $c(x)$ and $\Phi_{x}$ are related via the $T^{\partial}$ lifted restricted $\Vdash_{c}(-,\bigwedge-)$ relation. These observations simplify a bit the remaining proof.

1. (a)

To prove that \Phi_{x}\mathrel{\neg{\overline{T_{\omega}}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}^{\prime}}}}\beta holds, it suffices to prove that

[TABLE]

We reason by contraposition and we assume that \Phi_{x}\mathrel{\overline{T_{\omega}}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}^{\prime}}}\beta to show that then $c(x)\mathrel{\overline{T}{\nVdash^{\prime}}}\beta$, contradicting the original assumption that $x\Vdash\Delta\beta$.

By the definition of $f^{\sharp}$, observe that for any $w\in{\mathsf{base}}(\beta)$ we have an implication

[TABLE]

By contraposition, fx\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}^{\prime}w implies $x\not\Vdash_{c}w$. Write this implication as the following diagram:

[TABLE]

The image under $\overline{T}$ of the above diagram yields

[TABLE]

We read the diagram for $\beta$ in $(T^{\partial}W)^{\mathit{op}}$ and $c(x)$ in $TX$ (this is correct because $W$ is finite, and $(T^{\partial}W)^{\mathit{op}}=(T^{\partial}_{\omega}W)^{\mathit{op}}$). The lower part says that (Tf)(c(x))\mathrel{\overline{T}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}^{\prime}}}\beta: By assumption, \Phi_{x}\mathrel{\overline{T_{\omega}}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}^{\prime}}}\beta holds, and since $\Phi_{x}=(Tf)c(x)$, we deduce that (Tf)(c(x))\mathrel{\overline{T}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}^{\prime}}}\beta holds.

For the upper part, we first recall that, by the unit property of base, $\beta\in T_{\omega}^{\partial}{\mathsf{base}}(\beta)$. Together with ${\mathsf{base}}(\beta)$ being finite, this entails that $\beta\in T^{\partial}{\mathsf{base}}(\beta)$. Hence we have $c(x)\mathrel{\overline{T}{\nVdash^{\prime}}}\beta$ by using the above diagram. This is a contradiction with $x\Vdash_{c}\Delta\beta$. 2. (b)

We prove that $x\Vdash_{c}\nabla(T^{\partial}_{\omega}\bigwedge)\Phi_{x}$ holds by proving $c(x)\mathrel{\overline{T^{\partial}}{\Vdash(-,\bigwedge-)}}\Phi_{x}$.

By the definition of $f$ we have that $x\Vdash_{c}\bigwedge f(x)$ holds. The monotonicity of $\Vdash_{c}$ together with the definition of conjunction says that for any other $\varphi\in{\mathbb{U}}_{\omega}W$ with $f(x)\leq\varphi$ we can deduce $x\Vdash_{c}\bigwedge\varphi$. This observation yields a diagram in ${\mathsf{Rel}}$ of the form

[TABLE]

By applying $\overline{T^{\partial}}$ to the above diagram we obtain

[TABLE]

We instantiate the diagram for $c(x)$ in $(TX)^{\mathit{op}}$, and $\Phi_{x}$ in $T^{\partial}{\mathbb{U}}_{\omega}W$. Since

[TABLE]

we have in particular the inequality $(Tf)^{\mathit{op}}c(x)\leq\Phi_{x}$ in $T^{\partial}{\mathbb{U}}_{\omega}W$. By the above diagram, the relation $c(x)\mathrel{\overline{T^{\partial}}{\Vdash_{c}}}(T^{\partial}\bigwedge)\Phi_{x}$ follows.

We deduce from this that $c(x)\mathrel{\overline{T^{\partial}}{\Vdash_{c}}}\nu^{T^{\partial}}_{\mathcal{L}}((T^{\partial}_{\omega}\bigwedge)\Phi_{x})$, using the following naturality square for the conjunction map:

[TABLE] 2. (2)

The inequality {\Vdash_{c}}(-,\nabla T^{\partial}_{\omega}\bigwedge-)\cdot\neg(\overline{T}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}})\leq{\Vdash_{c}}(-,\Delta-)\cdot(\nu^{T^{\partial}}_{{\mathcal{L}}})_{\diamond}.

Consider $x$, $\Phi$ in $T^{\partial}_{\omega}{\mathbb{U}}_{\omega}{\mathcal{L}}$, and $\beta$ in $T^{\partial}_{\omega}{\mathcal{L}}$, such that

[TABLE]

We need to show that $x\Vdash_{c}\Delta\beta$ holds, so by the definition of the semantics of $\Delta$ we need to prove that $c(x)\mathrel{\neg\overline{T}{\nVdash}}\nu_{\mathcal{L}}^{T^{\partial}}(\beta)$ holds. Reasoning by contraposition, we show that

[TABLE]

contradicting the assumption.

First let us observe that whenever there is an $x_{0}\in X$ such that $x_{0}\not\Vdash_{c}a$ for some $a\in{\mathcal{L}}$, and $x_{0}\Vdash_{c}\bigwedge u$ for an upperset $u\in{\mathbb{U}}_{\omega}{\mathcal{L}}$, then u\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}w follows. This is precisely the information contained in the diagram in ${\mathsf{Rel}}$ of the form

[TABLE]

We apply $\overline{T^{\partial}}$ to the above lax triangle to obtain

[TABLE]

We instantiate the diagram for $c(x)$ in $(TX)^{\mathit{op}}$, $\Phi$ in $T^{\partial}{\mathbb{U}}_{\omega}{\mathcal{L}}$, and $\nu^{T^{\partial}}_{\mathcal{L}}(\beta)$ in $T^{\partial}{\mathcal{L}}$. Using the assumptions $c(x)\mathrel{\overline{T^{\partial}}{\Vdash}}(T^{\partial}\bigwedge)\Phi$ and $c(x)\mathrel{\overline{T}{\nVdash^{\prime}}}\beta$, we conclude that \Phi\mathrel{\overline{T}{\not\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}}}\beta holds.

We have proved the desired equality of the two relations. The last assertion of the proposition trivially follows.

The previous proposition states that under certain conditions, the modality $\Delta$ is semantically equivalent to a disjunction of $\nabla$ formulas. The following proposition deals with the dual statement: the modality $\nabla$ is semantically equivalent to a conjunction of $\Delta$ formulas.

Proposition 19**.**

For each coalgebra $c:X\longrightarrow TX$ and every semantics relation $\Vdash_{c}$, the relations

[TABLE]

and

[TABLE]

are equal.

In other words, for each $x$ in $X$, and each $\alpha$ in $T_{\omega}^{\partial}{\mathcal{L}}$, $x\Vdash_{c}\nabla\beta$ holds iff there is a $\Psi$ in $T_{\omega}^{\partial}{\mathbb{L}}_{\omega}{\mathcal{L}}$ such that

[TABLE]

Whenever $R_{\alpha}$ is finite, we have the following semantic equivalence:

[TABLE]

Proof 5.3**.**

The proof is completely analogous to that of Proposition 18.

6. Proof system and completeness

In this section we define a two-sided sequent calculus ${\mathbf{G}}_{\nabla\Delta}$ for the coalgebraic language ${\mathcal{L}}$ defined in Section 5. We prove that the calculus is complete with respect to the semantics of ${\mathcal{L}}$ given therein. The definition of the calculus as well as the completeness proof is general and parametric in the coalgebra functor $T$.

The calculus we are going to define can be seen as closely related to the two-sided sequent calculus for the finitary Moss’ coalgebraic logic of coalgebras in ${\mathsf{Set}}$ as presented in [BPV14]. We point out a closer connection of the two calculi in Subsection 7.A at the very end of the paper.

6.A. The proof system ${\mathbf{G}}^{T}_{\nabla\Delta}$

The calculus ${\mathbf{G}}^{T}_{\nabla\Delta}$ will manipulate sequents. A sequent is a syntactic object of the form $\varphi\Rightarrow\psi$ where $\varphi$ is a finitely generated upperset of formulas, i.e. $\varphi$ is in ${\mathbb{U}}_{\omega}{\mathcal{L}}$, and $\psi$ is a finitely generated lowerset of formulas, i.e., $\psi$ is in ${\mathbb{L}}_{\omega}{\mathcal{L}}$. Sequents can be seen as objects in $({\mathbb{U}}_{\omega}{\mathcal{L}})^{\mathit{op}}\times{\mathbb{L}}_{\omega}{\mathcal{L}}$, and therefore they carry an order and form a poset which we denote $\mathcal{S}$ (this order on sequents is a natural one as becomes clear from their semantics).

Given a coalgebra $c:X\longrightarrow TX$ equipped with a monotone valuation $\Vdash_{c}$ and a state $x_{0}$, we say that sequent $\varphi\Rightarrow\psi$ is refuted in $x_{0}$ if $x_{0}\Vdash_{c}\bigwedge\varphi$ while $x_{0}\nVdash_{c}\bigvee\psi$. Otherwise, the sequent is valid in $x_{0}$. Observe that the validity is monotone w.r.t. the order on $\mathcal{S}$. A sequent that is valid in all states of all $T$-coalgebras under all valuations is simply called a valid sequent, otherwise it is called a refutable sequent.

A rule is a scheme written in the form

[TABLE]

where $\mathcal{A}$ is a poset of sequents (namely, $\mathcal{A}$ is in ${\mathsf{Sub}}_{{\mathcal{M}}}\mathcal{S}$) forming the assumptions of the rule, and the sequent $S$ is the conclusion of the rule.

Notice that as defined, the number of assumptions of a rule need not be finite. It is because, for some functors, we will need infinitary modal rules to form a complete calculus. However, if the functor $T^{\partial}_{\omega}$ preserves finite posets, all the rules will be finitary.

A rule is said to be sound if, whenever all the assumptions are valid sequents, the conclusion is also a valid sequent. A rule is called invertible if whenever the conclusion is valid, then all the assumptions are valid as well. A rule has a subformula property if all the assumptions consist of subformulas of the conclusion only. A rule with the empty set of assumptions is called an axiom.

A proof in the calculus ${\mathbf{G}}^{T}_{\nabla\Delta}$ is a well-founded tree labelled by sequents in the following way:

1. (1)

Each leaf is labelled by an instance of an axiom. 2. (2)

Each non-leaf node $n$ is labelled by the conclusion of an instance $I$ of some rule. The children nodes of $n$ are labelled by the assumptions of the instance $I$.

We say that a sequent is provable if there is a proof whose root is labelled by the sequent.

We start the definition of the calculus ${\mathbf{G}}^{T}_{\nabla\Delta}$ by listing the axioms, rules of weakening and standard rules for conjunction and disjunction. If $\varphi$ is an upperset of formulas, by writing $\varphi,a$ we mean the upperset generated by $\varphi\cup\{a\}$, and by $\varphi,\varphi^{\prime}$ we mean the upperset generated by $\varphi\cup\varphi^{\prime}$. Similarly If $\psi$ is a lowerset of formulas, by writing $\psi,a$ we mean the lowerset generated by $\psi\cup\{a\}$, and by $\psi,\psi^{\prime}$ we mean the lowerset generated by $\psi\cup\psi^{\prime}$.

When writing down a sequent, e.g. in examples we provide, we often use a simplified notation and list only the generators of the corresponding lowersets and uppersets to keep the description finite222One can do so systematically by mapping sequents to their bases as follows: observing $({\mathbb{U}}{\mathcal{L}})^{\mathit{op}}={\mathbb{L}}_{\omega}{\mathcal{L}}^{\mathit{op}}$, we can use $({\mathsf{base}}_{{\mathcal{L}}^{\mathit{op}}},{\mathsf{base}}_{\mathcal{L}}):{\mathsf{Sub}}_{{\mathcal{M}}}({\mathbb{L}}_{\omega}{\mathcal{L}}^{\mathit{op}})\times{\mathsf{Sub}}_{{\mathcal{M}}}({\mathbb{L}}_{\omega}{\mathcal{L}})\longrightarrow{\mathsf{Sub}}_{{\mathcal{M}}}{\mathcal{L}}^{\mathit{op}}\times{\mathsf{Sub}}_{{\mathcal{M}}}{\mathcal{L}}$..

{defi}

The propositional part of the calculus ${\mathbf{G}}^{T}_{\nabla\Delta}$ is given in the following table:

[TABLE]

The rules for conjunction and disjunction above are straightforward adaptations of the standard conjunction and disjunction rules to our specific setting. In the axioms, the side condition requires that the inequality $a\leq_{\mathcal{L}}b$ holds in the free algebra of formulas. All the axioms and rules are sound, and the rules for $\bigwedge$ and $\bigvee$ are moreover invertible, which follows immediately from the definition of valid sequents.

Remark 20**.**

One can see the above tabular of rules as an inductive definition of a monotone relation

\textstyle{\Rightarrow:{\mathbb{L}}_{\omega}{\mathcal{L}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\mathbb{U}}_{\omega}{\mathcal{L}}} as the smallest one such that it in a way subsumes $\leq_{\mathcal{L}}$: $a\leq_{\mathcal{L}}b$ implies ${\uparrow}{a}\Rightarrow{\downarrow}{b}$, and is closed under the conjunction and disjunction rules (the weakening rules ensure the monotonicity).

Next we turn to modal rules. The modal part of the calculus will consist of three rule schemes: (1) a rule for introduction of nabla modality to the right-hand side of a sequent, (2) a rule for introduction of delta modality to the left-hand side of a sequent, and (3) a combined nabla-delta rule.

(1) $\nabla$-r and (2) $\Delta$-l.

Let us first cover the cases of introducing nabla to the right-hand and delta to the left-hand side of a sequent. Behind the soundness of following two rules lie the mutual definability of the two modal operators discussed in the previous section. The two rules, when read backwards, say how to reduce a nabla formula on the right-hand side of a sequent to a conjunction of delta formulas, and dually how to reduce a delta formula on the right-hand side of a sequent to a disjunction of nabla formulas. The laws that guarantee the soundness and invertibility of these two rules are those of Propositions 18 and 19.

{defi}

[Modal rules for $\nabla$-r and $\Delta$-l]

Consider $\alpha\in T_{\omega}^{\partial}{\mathcal{L}}$ with

\textstyle{{\mathsf{base}}(\alpha):V\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{L}} , and $\beta\in T_{\omega}^{\partial}{\mathcal{L}}$ with

\textstyle{{\mathsf{base}}(\beta):W\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{L}} . The two modal rules are defined as

[TABLE]

The sets of assumptions are indexed by collections $R_{\alpha}$ with each $\Psi$ in $T_{\omega}^{\partial}{\mathbb{L}}_{\omega}{\mathsf{base}}(\alpha)$, and $L_{\beta}$ with each $\Phi$ in $T_{\omega}^{\partial}{\mathbb{U}}_{\omega}{\mathsf{base}}(\beta)$, from Definition 5.D. The collections can in general be infinite, and therefore the above rules become infinitary. However, in case that $T_{\omega}^{\partial}$ preserves finite posets, they will become finitary.

{exa}

We illustrate the above definition with two simple examples of instances of the rule $\nabla$-r. The instances are based on Example 5.D.

1. (1)

Consider $T^{\partial}={\mathbb{L}}_{\omega}$, and $\alpha=\{\bot\}$. By Example 5.D (1), $R_{\alpha}=\{\{\emptyset,\{\bot\}\}\}$. Then for the only element $\{\emptyset,\{\bot\}\}$ of $R_{\alpha}$ we obtain ${\mathbb{L}}_{\omega}\bigvee\{\emptyset,\{\bot\}\}=\{\bot\}$. The following is therefore a correct instance of the rule $\nabla$-r:

[TABLE] 2. (2)

Consider $T^{\partial}=\mathbb{N}^{\mathit{op}}\times{\mathit{Id}}$, and $\alpha=(5,b\wedge c)$. By Example 5.D (2), $R_{(5,b\wedge c)}=\{(n,\emptyset)\ |\ 5>n\}\cup\{(n,\{b\wedge c\})\ |\ n\in\mathbb{N}\}$. Note that ${\mathbb{L}}_{\omega}\bigvee(n,\emptyset)=(n,\bot)$ while ${\mathbb{L}}_{\omega}\bigvee(n,\{b\wedge c\})=(n,b\wedge c)$. The following is therefore a correct instance of the rule $\nabla$-r:

[TABLE]

The rule $\nabla$-r is sound and invertible by Proposition 19, and the rule $\Delta$-l is sound and invertible by Proposition 18. Let us make a syntactic observation on the two rules concerning the subformula property.

Remark 21** (A form of the subformula property).**

Given any $\Psi$ of the type

[TABLE]

we can state the following, weaker kind of the subformula property:

[TABLE]

Since $\Psi\in T_{\omega}^{\partial}{\mathbb{L}}_{\omega}{\mathsf{base}}(\alpha)$ holds, we get the inclusion

[TABLE]

by Definition 3.B of base. The weak subformula property follows from this immediately. We can use the weak subformula property in particular to study the rule $\nabla$-r: It shows that all the assumptions of the rule are built from subformulas of the conclusion, using one additional modality $\nabla$, and the operation $T^{\partial}\bigvee$. Similarly, for any $\Phi\in T^{\partial}{\mathbb{U}}_{\omega}{\mathsf{base}}(\beta)$ we get that

[TABLE]

(3) $\nabla\Delta$ rule.

Let us turn now to introducing the last rule scheme. Observe that the invertible rules of the calculus (the $\bigwedge$ and $\bigvee$ rules and rules $\nabla$-r and $\Delta$-l) are strong enough to reduce any valid sequent $\varphi\Rightarrow\psi$ to a set of sequents in a reduced form by a backwards application of the rules. A sequent is reduced if it is of the form

[TABLE]

with $\pi$ and $\lambda$ being finitely generated upperset and lowerset of atomic formulas (or their respective generators in the simplified notation), $A$ being in ${\mathbb{U}}_{\omega}T_{\omega}^{\partial}{\mathcal{L}}$ and $B$ in ${\mathbb{L}}_{\omega}T_{\omega}^{\partial}{\mathcal{L}}$ (or their respective generators in the simplified notation).

The last missing bit of the calculus ${\mathbf{G}}^{T}_{\nabla\Delta}$ is a rule that decomposes sequents in a reduced form. The rule $\nabla\Delta$, which we will formulate in Definition 6.A below, introduces the nabla modality to the left-hand side and the modality delta to the right-hand side of a sequent simultaneously. It is the only rule whose backwards application reduces the modal depth of a sequent.

The idea behind the rule $\nabla\Delta$ is to express what it means for a sequent in a reduced form to be refuted in a state of a coalgebra. It will describe how validity and refutation of the subformulas of the sequent is “redistributed” in the “successors” of the state. This semantical idea will be made precise in Example 6.A below. To be able to formulate the same idea in a syntactic form of a rule we employ a technical notion of redistribution.

{defi}

Fix a pair $(A,B)$ in $({\mathbb{U}}_{\omega}T_{\omega}^{\partial}{\mathcal{L}}\times{\mathbb{L}}_{\omega}T_{\omega}^{\partial}{\mathcal{L}})$. A redistribution of $(A,B)$ is an element $\Phi$ of $T_{\omega}^{\partial}({\mathbb{U}}_{\omega}{\mathsf{base}}(A)\times{\mathbb{L}}_{\omega}{\mathsf{base}}(B))$ satisfying the following two conditions:

1. (1)

for each $\alpha$ with A\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}\alpha it holds that (T_{\omega}^{\partial}p_{0})\Phi\mathrel{\overline{T_{\omega}^{\partial}}{\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}}}\alpha, 2. (2)

for each $\beta$ with \beta\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}B it holds that \beta\mathrel{\overline{T_{\omega}^{\partial}}{\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}}}(T_{\omega}^{\partial}p_{1})\Phi,

where

\textstyle{{\mathbb{U}}_{\omega}{\mathcal{L}}}$$\textstyle{{\mathbb{U}}_{\omega}{\mathcal{L}}\times{\mathbb{L}}_{\omega}{\mathcal{L}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p_{1}}$$\scriptstyle{p_{0}}$$\textstyle{{\mathbb{L}}_{\omega}{\mathcal{L}}}

are the projection maps.

We denote the collection of all redistributions of the pair $(A,B)$ by ${\mathsf{rd}}(A,B)$.

Remark 22**.**

The notion of redistribution was introduced earlier in work on coalgebra automata [KV08]. The idea of “redistributing the subformulas” has appeared, for the case of sets, e.g. in [KKV12b] and [BPV14] under the name of slim redistribution or separated slim redistribution, respectively. For reasons of simplicity we do not adopt the name slim redistribution, and speak simply about redistributions instead.

We illustrate the notion of redistribution with the following example which arises semantically. It is a crucial example because it relates directly to soundness and a weak form of invertibility of the modal rule we prove later in Proposition 25.

{exa}

Suppose a sequent

[TABLE]

is not valid for some pair $(A,B)$ in ${\mathbb{U}}_{\omega}T^{\partial}_{\omega}{\mathcal{L}}\times{\mathbb{L}}_{\omega}T^{\partial}_{\omega}{\mathcal{L}}$. This means that there is a coalgebra $c:X\longrightarrow TX$ and a valuation

\textstyle{\Vdash:{\mathcal{L}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X^{\mathit{op}}}

such that

[TABLE]

for some $x_{0}$ in $X$. The bases of $A$ and $B$ in ${\mathsf{Sub}}_{{\mathcal{M}}}{\mathcal{L}}$ will be denoted by

[TABLE]

respectively, with $V$ and $W$ being finite posets. In this example we will construct a certain redistribution out of this countermodel.

1. (I)

The construction of a redistribution. Again, the main idea of the proof is rather simple, and most of the hassle is due to keep track of types and restricting to bases to keep the reasoning on the language side finitary.

We start by defining two maps

[TABLE]

by putting

[TABLE]

Similarly as before in proof of Proposition 18, they factor through the bases of $A$ and $B$ to result in the following two maps:

[TABLE]

by putting

[TABLE]

Hence the tupling of $f$ and $g$ is of the form

[TABLE]

and by applying $T^{\partial}$ to it we obtain a map

[TABLE]

Consider the composite

[TABLE]

and define $\Phi_{x_{0}}$ to be its value at $x_{0}$ in $X^{\mathit{op}}$:

[TABLE]

Because ${\mathbb{U}}_{\omega}V\times{\mathbb{L}}_{\omega}W$ is a finite poset, $T^{\partial}$ and $T^{\partial}_{\omega}$ agree on it (the corresponding natural inclusion is the identity). Thus we may see $\Phi_{x_{0}}$ as an element of $T^{\partial}_{\omega}({\mathbb{U}}_{\omega}V\times{\mathbb{L}}_{\omega}W)$. Therefore, using ${\mathsf{base}}(A)$ and ${\mathsf{base}}(B)$ as maps,

[TABLE]

is an element of $T^{\partial}_{\omega}({\mathbb{U}}_{\omega}{\mathsf{base}}(A)\times{\mathbb{L}}_{\omega}{\mathsf{base}}(B))$ as required by the definition or a redistribution.

We claim that $\Phi$ is a redistribution of $(A,B)$. We verify item (1) of Definition 6.A, item (2) is verified by dual reasoning. Therefore, we want to prove that

[TABLE]

holds for every $\alpha$ with A\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}\alpha, where $p_{0}:{\mathbb{U}}_{\omega}{\mathcal{L}}\times{\mathbb{L}}_{\omega}{\mathcal{L}}\longrightarrow{\mathbb{U}}_{\omega}{\mathcal{L}}$ is the product projection. By the definition of $\Phi$, we observe that

[TABLE]

For the following diagrams to work, we however need to keep things restricted to bases on the language side, and therefore we are going to use $f$ rather then $f^{\sharp}$. Consider any $\alpha$ such that A\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}\alpha holds. From the unit property of the base we know that $A\in{\mathbb{U}}_{\omega}T^{\partial}_{\omega}{\mathsf{base}}(A)$. So, there is a (unique) $\alpha^{\prime}$ in $T_{\omega}^{\partial}V$ with $\alpha=T^{\partial}_{\omega}{\mathsf{base}}(A)(\alpha^{\prime})$. To sum up, to prove for

\textstyle{\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}:{\mathcal{L}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\mathbb{U}}_{\omega}{\mathcal{L}}}

that

[TABLE]

means to prove that

[TABLE]

and in turn it suffices to prove, for the restricted

\textstyle{\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}:V\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\mathbb{U}}_{\omega}V,}

that

[TABLE]

This by definition of $\Phi_{x_{0}}$ boils down to proving that

[TABLE]

holds for any $\alpha$ such that A\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}\alpha holds.

Given any $x$ in $X$ and $v\in V$ such that $x\Vdash_{c}{\mathsf{base}}(A)(v)$ holds, we know that f(x)\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}v holds by the definition of $f$. The monotonicity of the membership relation \mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}} entails that for every $\varphi$ in ${\mathbb{U}}_{\omega}V$ with $\varphi\leq f(x)$, the relation \varphi\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}v holds as well. Thus the following lax triangle in ${\mathsf{Rel}}$

[TABLE]

commutes. Its image under $\overline{T^{\partial}}$ is the lax triangle

[TABLE]

We prove (6.24) using (6.25). Consider any $\alpha$ such that A\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}\alpha holds. Recall $\alpha^{\prime}$ in $T^{\partial}V$ is the unique element with $\alpha=T^{\partial}{\mathsf{base}}(A)(\alpha^{\prime})$ (as $V$ is a finite poset, we are allowed to write $T^{\partial}$ in place of $T^{\partial}_{\omega}$ here). We instantiate the diagram for $c^{\mathit{op}}(x_{0})$ in $(T^{\partial}X)^{\mathit{op}}$, and $\alpha^{\prime}$ in $T^{\partial}V$.

We know from assumption that $x_{0}\Vdash_{c}\nabla\alpha$. Let \textstyle{{\mathsf{base}}(\alpha):Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{L}} and $z\in Z$ be the unique element with $T^{\partial}_{\omega}{\mathsf{base}}(\alpha)(z)=\alpha$. By the semantic definition we obtain that

[TABLE]

But observe that ${\mathsf{base}}(\alpha)\sqsubseteq{\mathsf{base}}(A)$. Therefore this is equivalent to

[TABLE]

Applying the diagram we finally obtain that T^{\partial}f(c^{\mathit{op}}(x_{0}))\overline{T^{\partial}}\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}\alpha^{\prime} as required. We consequently use the fact that since $V$ and ${\mathbb{U}}_{\omega}V$ are finite posets, $T^{\partial}$ and $T^{\partial}$ coincide on them, and consequently the lifted relations \overline{T^{\partial}}\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}} and \overline{T^{\partial}_{\omega}}\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}} coincide. 2. (II)

The redistribution $\Phi$ constructed above, has the following additional property: the sequent

[TABLE]

is refutable, for every $z\in{\mathsf{base}}(\Phi)$.

1. (a)

Recall the map $(f^{\sharp},g^{\sharp}):X^{\mathit{op}}\longrightarrow{\mathbb{U}}_{\omega}{\mathcal{L}}\times{\mathbb{L}}_{\omega}{\mathcal{L}}$ and consider its $({\mathcal{E}},{\mathcal{M}})$-factorisation

[TABLE]

We will prove the inclusion

[TABLE]

The diagram

[TABLE]

commutes: the left triangle commutes by the definition of $\Phi$, and the right triangle commutes by the $({\mathcal{E}},{\mathcal{M}})$-factorisation of $(f^{\sharp},g^{\sharp})$. This proves that $\Phi\in T^{\partial}m$ holds. Thus ${\mathsf{base}}(\Phi_{x_{0}})\subseteq m$ holds by the definition of base. 2. (b)

We will show that for every $z\in{\mathsf{base}}(\Phi)$ there is a state $x_{z}\in X$ such that

[TABLE]

is not valid in $x_{z}$.

Since $z\in{\mathsf{base}}(\Phi)$ holds, we know that $z\in m$ holds as well. From this and from the surjectivity of the mapping $e$ we can thus define $x_{z}$ to be any element from $X$ such that

[TABLE]

holds. Then we know by the $({\mathcal{E}},{\mathcal{M}})$-factorisation of $(f^{\sharp},g^{\sharp})$ that

[TABLE]

The sequent $p_{0}(z)\Rightarrow p_{1}(z)$ can therefore be written as

[TABLE]

and this in turn is the sequent

[TABLE]

By the definition of $f^{\sharp}$ and $g^{\sharp}$, all formulas in $f^{\sharp}(x_{z})$ are valid in $x_{z}$, while no formula in $g^{\sharp}(x_{z})$ is valid in $x_{z}$.

Now we can state the main modal rule of the calculus ${\mathbf{G}}^{T}_{\nabla\Delta}$, explain how it reads, and show its main properties. {defi}[The modal $\nabla\Delta$ rule]

We formulate the rule $\nabla\Delta$ as follows:

[TABLE]

where the elements in ${\mathsf{rd}}(A,B)$ are of the form $\Phi\in T^{\partial}_{\omega}({\mathbb{U}}_{\omega}{\mathcal{L}}\times{\mathbb{L}}_{\omega}{\mathcal{L}})$, and

[TABLE]

are the projection maps of the product ${\mathbb{U}}_{\omega}{\mathcal{L}}\times{\mathbb{L}}_{\omega}{\mathcal{L}}$.

Recall from Part II of Example 6.A that choosing an element $z^{\Phi}\in{\mathsf{base}}(\Phi)$, we obtain a finitely generated upperset of formulas $p_{0}(z^{\Phi})$ and a finitely generated lowerset of formulas $p_{1}(z^{\Phi})$, therefore $p_{0}(z^{\Phi})\Rightarrow p_{1}(z^{\Phi})$ is a well-formed sequent. The rule $\nabla\Delta$ says that the conclusion is provable whenever for each redistribution $\Phi$ of $(A,B)$ there exists some $z^{\Phi}\in{\mathsf{base}}(\Phi)$ such that the sequent $p_{0}(z^{\Phi})\Rightarrow p_{1}(z^{\Phi})$ is provable. In other words, it says that if the sequent in the conclusion is refutable, there must be a redistribution $\Phi$ of the pair $(A,B)$ (in fact the one of Example 6.A) such that all the sequents $p_{0}(z^{\Phi})\Rightarrow p_{1}(z^{\Phi})$ are refutable.

{exa}

Continuing on Examples 5.D and 6.A, we illustrate the above definition with two instances of the rule:

1. (1)

Consider $T^{\partial}_{\omega}={\mathbb{L}}_{\omega}$ and let us compute ${\mathsf{rd}}(\{\emptyset\},\{\{\bot\}\})$. Any such redistribution $\Phi$ in ${\mathbb{L}}_{\omega}({\mathbb{U}}_{\omega}{\mathcal{L}}\times{\mathbb{L}}_{\omega}{\mathcal{L}})$ has to satisfy the following:

[TABLE]

The first condition is met by $({\mathbb{L}}_{\omega}p_{0})\Phi=\emptyset$ only, while the second condition requires $({\mathbb{L}}_{\omega}p_{1})\Phi\neq\emptyset$, which together is impossible. The collection of redistributions is therefore empty and the following is a correct instance of the $\nabla\Delta$ rule (in fact an axiom):

$\emptyset$

$\nabla\Delta$

$\nabla\emptyset\Rightarrow\Delta\{\bot\}$

Putting the above observations together with Example 6.A (1) we obtain a simple proof in the simplified notation:

$\emptyset$

$\nabla\Delta$

$\nabla\emptyset\Rightarrow\Delta\{\bot\}$

$\nabla$-r

$\nabla\emptyset\Rightarrow\nabla\{\bot\}$ 2. (2)

Consider $T^{\partial}_{\omega}=\mathbb{N}^{\mathit{op}}\times{\mathit{Id}}$ and let us compute ${\mathsf{rd}}(\{(3,b),(8,c)\},\{(n,\bot)\})$ where $n<5$. Any such redistribution $\Phi$ is an element of $\mathbb{N}^{\mathit{op}}\times({\mathbb{U}}_{\omega}{\mathcal{L}}\times{\mathbb{L}}_{\omega}{\mathcal{L}})$, i.e. of the form $(m,(\varphi,\psi))$ satisfying firstly

[TABLE]

which implies that $m\geq 8$ and \varphi\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}b and \varphi\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}c. Secondly,

[TABLE]

which implies that $n\geq m$. But since $m\geq 8$ and $n<5$, this is clearly impossible. Thus there is no such redistribution and the following is a correct instance of the rule, whenever $n<5$:

$\emptyset$

$\nabla\Delta$

$\nabla(3,b),\nabla(8,c)\Rightarrow\Delta(n,\bot)$

Let us compute ${\mathsf{rd}}(\{(3,b),(8,c)\},\{(n,b\wedge c)\})$ for any $n$. Any such redistribution $\Phi$ is of the form $(m,(\varphi,\psi))$ satisfying, as before, $m\geq 8$ and \varphi\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}b and \varphi\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}c. Moreover, it should satisfy

[TABLE]

which implies that $n\geq m$ and b\wedge c\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}\psi. For $n<8$ the collection of redistributions is again empty. For $n\geq 8$ we know that any redistribution $(m,(\varphi,\psi))$ contains in its base the pair $(\varphi,\psi)$ where $\varphi\Rightarrow\psi$ is a provable sequent (using possibly some weakening inferences). Therefore the following is a correct proof in the simplified notation:

$b\Rightarrow b$         $c\Rightarrow c$

$\bigwedge$-r

$b,c\Rightarrow b\wedge c$

w

$\varphi\Rightarrow\psi$

$\nabla\Delta$

$\nabla(3,b),\nabla(8,c)\Rightarrow\Delta(n,b\wedge c)$

Put together with Example 6.A (2) we obtain the following proof, where the left part of the tree covers cases for $n<8$ and the right part of the tree covers cases for $n\geq 8$ and all the existing redistributions:

$\emptyset$

$\nabla\Delta$

$\nabla(3,b),\nabla(8,c)\Rightarrow\Delta(n,\bot)$

       $\ldots$       

$b\Rightarrow b$         $c\Rightarrow c$

$\bigwedge$-r

$b,c\Rightarrow b\wedge c$

w

$\varphi\Rightarrow\psi$

$\nabla\Delta$

$\nabla(3,b),\nabla(8,c)\Rightarrow\Delta(n,b\wedge c)$

       $\ldots$

$\nabla$-r

$\nabla(3,b),\nabla(8,c)\Rightarrow\nabla(5,b\wedge c)$

The rule $\nabla\Delta$ satisfies the subformula property, similar in spirit to the properties discussed in Remark 21.

Remark 23** (Subformula property).**

Since any redistribution $\Phi$ has the form

[TABLE]

we get by the definition of base the inclusion

[TABLE]

Since the image of ${\mathbb{U}}_{\omega}{\mathsf{base}}(A)\times{\mathbb{L}}_{\omega}{\mathsf{base}}(B)$ are the subformulas of the conclusion of the rule $\nabla\Delta$, this observation tells us that the rule $\nabla\Delta$ satisfies the subformula property.

Remark 24** (One-step nature of the rules).**

Coalgebras naturally capture one-step behaviour. As introduced by [Pat03], both the semantics and syntax of coalgebraic logics can be stratified in layers of transition and modal depth. In particular, proof systems (both Hilbert and Gentzen style) can be presented via one-step axioms with no nesting modalities and rules which concern one layer of modalities only, and their completeness demonstrated by an inductive argument in a one-step manner [KKV12b, KP11]. We do not adopt the one-step formalism systematically in this paper, however, the construction of the language in Subsection 5.A allows for such a treatment, the semantics could be presented in a one-step manner following [KKV12b], and the rules of the sequent calculus allow for a purely one-step reformulation. It is roughly because all the rules except the $\nabla\Delta$ rule operate within the same layer of the language, while the $\nabla\Delta$ rule strips precisely one layer of modalities. Namely, in the proof of the following proposition, constructing the model refuting a sequent

[TABLE]

can be seen as a part of presenting a completeness proof by step-by-step method.

The rule $\nabla\Delta$ is sound, and even invertible in a certain technical sense which we explain and prove in the following proposition.

Proposition 25** (Soundness and invertibility of the $\nabla\Delta$ rule).**

Let $A$, $B$ and their bases be given as in Definition 6.A and let $\pi$ and $\lambda$ consist of atomic formulas. The following are equivalent:

1. (1)

The sequent

[TABLE]

is refutable. 2. (2)

The sequent $\pi\Rightarrow\lambda$ is refutable, and there exists a redistribution $\Phi$ of $(A,B)$ such that for all $z\in{\mathsf{base}}(\Phi)$ the sequents

[TABLE]

are refutable.

Proof 6.1**.**

(1) implies (2). Assume that the sequent

[TABLE]

is refutable. Then there is a coalgebra $c:X\longrightarrow TX$, a monotone valuation $\Vdash$ on $c$ and a state $x_{0}$ in $X$ such that $x_{0}$ refutes the sequent $\pi\Rightarrow\lambda$, and (x\Vdash\bigwedge\limits_{A\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}\alpha}\nabla\alpha) and (x\nVdash\bigvee\limits_{\beta\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}B}\Delta\beta).

Then the redistribution $\Phi$ of $(A,B)$, defined in Example 6.A, has the property that all the sequents $p_{0}(z)\Rightarrow p_{1}(z)$ are refutable, see Part (II) of Example 6.A.

(2) implies (1). Assume a redistribution $\Phi$ in ${\mathsf{rd}}(A,B)$ is given. We moreover assume that for all $z\in{\mathsf{base}}(\Phi)$, the sequent $p_{0}(z)\Rightarrow p_{1}(z)$ is refuted by some valuation $\Vdash_{z}$ on a coalgebra $c_{z}:X_{z}\longrightarrow TX_{z}$ in a state $x_{z}$.

We define a new coalgebra $c:X\longrightarrow TX$, a point $x_{0}$ in $X$, and a valuation $\Vdash$ such that $x_{0}$ will validate $\nabla\alpha$ for all $\alpha$ in $A$, and $x_{0}$ will refute $\Delta\beta$ for all $\beta$ in $B$.

1. (a)

The definition of $c:X\longrightarrow TX$ and $x_{0}$ in $X$. We will denote the base of the redistribution $\Phi$ by

[TABLE]

Therefore, by the properties of base, there is a $w_{\Phi}$ in $T^{\partial}Z$ such that

[TABLE]

(and we are allowed to write here $T^{\partial}$ in place of $T^{\partial}_{\omega}$ because $Z$ is a finite poset). Let $Z_{d}$ denote the discrete underlying poset of $Z$. We denote by $e:Z_{d}\longrightarrow Z$ the obviously monotone mapping that is identity on the elements. The monotone map $h:Z_{d}\longrightarrow X^{\mathit{op}}$ is defined by putting $h(z)=x_{z}$.

Define

[TABLE]

and denote the unique element of ${\mathbb{1}}$ by $x_{0}$. The coalgebra map $c:X\longrightarrow TX$ is defined on the individual components as follows:

[TABLE]

where ${\mathsf{inj}}$ and ${\mathsf{inj}}_{z}$ are the coproduct injections, and $w^{\Phi}$ is the element of $T^{\partial}Z_{d}$ with the property that

[TABLE] 2. (b)

The valuation $\Vdash$ on $c:X\longrightarrow TX$.

In all states from all $X_{z}$ the valuation of atoms remains unchanged, while in $x_{0}$ we satisfy all atoms in $\pi$ and refute all atoms in $\lambda$. This is possible because the sequent $\pi\Rightarrow\lambda$ is refutable by assumption. 3. (c)

We need to prove $x_{0}\Vdash\bigwedge\nabla\alpha$ for each $\alpha$ in $A$, and that $x_{0}\nVdash\Delta\beta$ for each $\beta$ in $B$. Equivalently, we can prove that $c(x_{0})\mathrel{\overline{T^{\partial}}{\Vdash}}\alpha$ for each $\alpha$ in $A$, and $c(x_{0})\mathrel{\overline{T}{\nVdash}}\beta$ for each $\beta$ in $B$. We will prove only $c(x_{0})\mathrel{\overline{T^{\partial}}{\Vdash}}\alpha$ for each $\alpha$ in $A$, the second property is verified by dual reasoning.

We consider \textstyle{{\mathsf{base}}(A):V\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{L}} . We first claim that there the following lax diagram in ${\mathsf{Rel}}$ commutes:

[TABLE]

To see that this is the case, fix a $v\in V$ and a $z$ in $Z_{d}$ such that $v$ and $z$ are related by the first-down-then-right passage of the diagram.

Hence there is some $\varphi$ in ${\mathbb{U}}_{\omega}{\mathcal{L}}$ with \varphi\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}{\mathsf{base}}(A)(v), some $(\varphi^{\prime},\psi^{\prime})$ with $\varphi^{\prime}\supseteq\varphi$ and therefore \varphi^{\prime}\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}{\mathsf{base}}(A)(v), and ${\mathsf{base}}(\Phi)(z)\leq_{{\mathbb{U}}_{\omega}{\mathcal{L}}\times{\mathbb{L}}_{\omega}{\mathcal{L}}}(\varphi^{\prime},\psi^{\prime})$. This entails that p_{0}({\mathsf{base}}(\Phi)(z))\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}{\mathsf{base}}(A)(v), and ${\mathsf{base}}(A)(v)$ is valid in $x_{z}$ by assumption. Therefore the pair $v$ and $z$ are related by the first-right-then-down passage of the diagram.

We will use the image under $\overline{T^{\partial}}$ of the above diagram:

[TABLE]

Consider a fixed $\alpha$ in $A$. Let \textstyle{{\mathsf{base}}(\alpha):U\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{L}} , and let $u\in U$ be the unique element with $T^{\partial}{\mathsf{base}}(\alpha)(u)=\alpha$. Because ${\mathsf{base}}(\alpha)\sqsubseteq{\mathsf{base}}(A)$, there is a unique $\alpha^{\prime}$ in $T^{\partial}V$ with $\alpha=T^{\partial}{\mathsf{base}}(A)(\alpha^{\prime})$.

Apply the diagram to $\alpha^{\prime}$ in $T^{\partial}V$, $(T^{\partial}p_{0})\Phi$ in $T^{\partial}{\mathbb{U}}_{\omega}{\mathcal{L}}$, and the unique $w_{\Phi}$ in $T^{\partial}Z$ such that

[TABLE]

Since $\alpha^{\prime}$ and $w_{\Phi}$ are related by the first-down-then-right passage of the diagram, there exists $\xi$ in $(TX)^{\mathit{op}}$ with $c(x_{0})\leq_{(TX)^{\mathit{op}}}\xi$, and such that

[TABLE]

Therefore $c(x_{0})\geq_{TX}\xi$ and, consequently,

[TABLE]

But this is equivalent to

[TABLE]

and this proves that $x_{0}$ validates $\nabla\alpha$, as required.

We remark that, in the above diagram, that since $V$ (and also ${\mathbb{U}}_{\omega}V$) is a finite poset, $T^{\partial}$ and $T^{\partial}_{\omega}$ coincide on it. Therefore $\alpha$ and $\alpha^{\prime}$ are typed properly. For the same reason, also the lifted relations \overline{T^{\partial}}{\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}} and \overline{T^{\partial}_{\omega}}{\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}} coincide.

6.B. Completeness

Assume a valid sequent $\varphi\Rightarrow\psi$ is given. Recall that in a simplified notation, we can identify the finitely generated lowerset $\psi$ (and the finitely generated upperset $\varphi$) with the finite (discrete) poset of its generators $g(\psi)$ (resp. $g(\varphi)$). We will show by an inductive argument that the sequent is provable in the calculus ${\mathbf{G}}^{T}_{\nabla\Delta}$, using the invertibility of the rules of the calculus. To this end we need to define a measure of syntactic complexity of a sequent in such a way that any backward application of a logical rule of the calculus strictly decreases the defined measure.

{defi}

[Measure on sequents]

For each formula $a$ in ${\mathcal{L}}$, we define its complexity on the left-hand side of a sequent, and on the right-hand side of the sequent simultaneously as follows, counting modal formulas as atoms with a slightly bigger complexity.

[TABLE]

For a sequent $\varphi\Rightarrow\psi$ we define its complexity as

[TABLE]

and its modal depth (recall Definition 13) by

[TABLE]

Finally, we define the measure of the sequent $\varphi\Rightarrow\psi$ to be the pair of natural numbers

[TABLE]

We consider the pairs to be ordered lexicographically. The measure is defined exactly as in [BPV14].

Proposition 26**.**

Fix a sequent $\varphi\Rightarrow\psi$. A backward application of any rule of the calculus, except weakening rules333In a backward application of a weakening inference, the set of generators of the corresponding upperset or lowerset may actually get bigger, even if the actual upperset or lowerset does not., to the sequent yields sequents with strictly smaller measure.

Proof 6.2**.**

In each backward application of one of the propositional rules, $k(\varphi\Rightarrow\psi)$ strictly decreases while modal depth remains unchanged, i.e., the measure of any assumption is strictly smaller then the measure of the conclusion.

We inspect the modal rules. Consider a backward application of the $\Delta$-l rule with the conclusion $\varphi,\Delta\beta\Rightarrow\psi$. Its complexity is

[TABLE]

Complexity of any of the assumptions $\varphi,\nabla(T^{\partial}_{\omega}\bigwedge)\Phi\Rightarrow\psi$ is strictly smaller:

[TABLE]

Since $\Phi\in T^{\partial}_{\omega}{\mathbb{U}}_{\omega}{\mathsf{base}}(\beta)$, from Remark 21 it follows that the modal depth of the sequent remains unchanged. The case of the modal rule $\nabla$-r is similar.

Consider a backward application of the $\nabla\Delta$ rule with the conclusion \{\nabla\alpha\mid A\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}\alpha\}\Rightarrow\{\Delta\beta\mid\beta\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}B\}. From the type of any $\Phi$ in ${\mathsf{rd}}(A,B)$ and from Remark 23 it follows that the measure of each of the sequents $p_{0}(z^{\Phi})\Rightarrow p_{1}(z^{\Phi})$ is strictly smaller because in this case the modal depth of the assumptions is strictly smaller than that of the conclusion.

The basic idea is we can apply the rules of the calculus (except the weakening rules) to a sequent backwards, simplifying it in terms of the measure, and using the invertibility of the rules (or a weak form of invertibility in the case of the modal rule). Reaching an irreducible, atomic, sequent, we check for provability. This can be seen as a backward proof-search in a variant of the calculus with the weakening rules built in the axioms. Now we can finally prove that the calculus ${\mathbf{G}}^{T}_{\nabla\Delta}$ is sound and complete.

Theorem 27** (Soundness and Completeness of the calculus ${\mathbf{G}}^{T}_{\nabla\Delta}$).**

Each sequent $\varphi\Rightarrow\psi$ is valid if and only if it is provable.

Proof 6.3**.**

Soundness of the calculus ${\mathbf{G}}^{T}_{\nabla\Delta}$ can be proved by a routine induction on the depth of a proof in the calculus, using in particular appropriate directions of Propositions 18, 19 and 25 establishing soundness of the modal rules.

The completeness can be proved by induction on the measure. Assume a valid sequent $\varphi\Rightarrow\psi$ is given. If the measure of the sequent is $(0,0)$, it consists of atoms and can only be valid if there are some atoms \varphi\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}p and q\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}\psi with $p\leq_{\mathcal{L}}q$. In that case the sequent is provable from an axiom by weakening rules.

Suppose that $(d(\varphi\Rightarrow\psi),k(\varphi\Rightarrow\psi))>(0,0)$, meaning the sequent contains at least one logical operator. We distinguish two cases:

1. (1)

$\varphi\Rightarrow\psi$ is not of the reduced form. Then some of the propositional rules, or the $\Delta$-l or the $\nabla$-r rule can be applied to it backwards. Any such rule is by Propositions 18 and 19 invertible and therefore such an application preserves validity. Moreover, all the assumptions of such a rule have strictly smaller measure by Proposition 26. We may therefore apply the induction hypothesis and conclude that all the assumptions of such a rule application, being valid, are also provable, and so is, by applying the rule forward, its conclusion. 2. (2)

$\varphi\Rightarrow\psi$ is of the form \pi,\{\nabla\alpha\mid A\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}\alpha\}\Rightarrow\{\Delta\beta\mid\beta\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}B\},\lambda with $\pi$ and $\lambda$ consisting of atomic formulas. Then either $\pi\Rightarrow\lambda$ is valid, and therefore provable as in the basic case. The sequent itself is then provable by weakening rules.

Or, by Proposition 25, for each redistribution there is some $z^{\Phi}\in{\mathsf{base}}(\Phi)$ such that the sequent $p_{0}(z^{\Phi})\Rightarrow p_{1}(z^{\Phi})$ is valid. But any such sequent has strictly smaller measure by Proposition 26 and therefore we may apply the induction hypothesis and conclude that any such sequent, being valid, is therefore also provable. Then the sequent \pi,\{\nabla\alpha\mid A\mathrel{\vphantom{\sqsupset}\text{\ooalign{\sqsupset$\cr$-\cr}}}\alpha\}\Rightarrow\{\Delta\beta\ |\ \beta\mathrel{\vphantom{\sqsubset}\text{\ooalign{\sqsubset$\cr$-\cr}}}B\},\lambda is provable by the rule $\nabla\Delta$, and weakening rules.

7. Concluding remarks

We have shown that a finitary Moss’ logic can be meaningfully defined for coalgebras in the category ${\mathsf{Pos}}$ of posets and monotone maps, and that it is expressive and also complete. All the definitions and proofs are parametric in the coalgebra functor $T$, which is required to be locally monotone, to preserve exact squares, and the syntax functor $T^{\partial}_{\omega}$, which is required to preserve intersections of subobjects.

There is still a lot we do not know about endofunctors of ${\mathsf{Pos}}$. Namely we are interested in the following open problems:

1. (1)

Characterise endofunctors of ${\mathsf{Pos}}$ that preserve exact squares. 2. (2)

Characterise endofunctors of ${\mathsf{Pos}}$ that preserve order embeddings. 3. (3)

Among the endofunctors of ${\mathsf{Pos}}$ that preserve order embeddings, characterise those such endofunctors that moreover preserve finite intersections.

There are two interesting questions regarding the logic introduced in this paper that we have not addressed and leave for potential future study:

1. (1)

Is it the case that for a posetification $T_{\omega}^{\prime}$ (see [BK11]) of a ${\mathsf{Set}}$ endofunctor $T_{\omega}$, the Moss’ logic for $T^{\prime}$-coalgebras as introduced in this paper is the positive fragment of the Moss’ logic for $T$-coalgebras? The corresponding result for the logic of predicate liftings was obtained in [BKV13]. 2. (2)

What is the relation of the Moss’ logic for coalgebras for ${\mathsf{Pos}}$-endofunctors to the logic of all monotone predicate liftings considered in [KKV12a]?

Let us briefly comment on (1). First of all, our definition of the language in Subsection 5.A uses ${\mathbb{L}}_{\omega}$ and ${\mathbb{U}}_{\omega}$ for arities of disjunction and conjunction. We have explained that this makes perfect sense in the poset setting in Remark 12 (it is worth noting that even with a discrete poset of atomic propositions, our construction produces an ordered language). But these functors are not poset extensions or liftings of the finitary powerset functor in ${\mathsf{Set}}$444The functors ${\mathbb{L}},{\mathbb{U}}$ can however be obtained as quotients of certain liftings of the powerset functor to the category of preorders and monotone maps [BK11]., which classical Moss’ logic uses as arity of both the connectives. While we could in principle use the self-dual finitary convex powerset functor ${\mathbb{P}}^{c}_{\omega}$, which is the posetification of the finitary powerset functor in ${\mathsf{Set}}$ [BK11], for the arity of both conjunction and disjunction (and this choice would actually produce a discrete language, starting from a discrete poset of atomic propositions), this seems to us to make sense precisely for the purpose of studying positive fragments of ${\mathsf{Set}}$-based coalgebraic logic (which is not the aim of this paper), and not so much for studying the ${\mathsf{Pos}}$-based coalgebraic logic. Had we done so, it would not be difficult to adjust the rest of the syntactic machinery, including the Definition 5.D of the collections $R_{\alpha}$ and $L_{\beta}$ and Definition 6.A of a redistribution, syntactic shape of sequents, and the formulation of the rules of the calculus accordingly. What is more important, under this modification, all the proofs remain correct. We will outline the resulting formalism in the following subsection.

7.A. Positive fragments

We will see how the machinery described in this paper, modulo one alternation concerning arities, can capture positive (i.e. $\neg$-free) fragments of finitary Moss’ logic in ${\mathsf{Set}}$, as presented in [BPV14]. All functors in this section, including the coalgebra functors, are assumed to be finitary.

{asm}

Solely for the purpose of this subsection, we assume that the arities of the conjunction and disjunction in ${\mathsf{Pos}}$ are given by the finitary convex subset functor ${\mathbb{P}}^{c}_{\omega}$.

Let $D:{\mathsf{Set}}\longrightarrow{\mathsf{Pos}}$ be the discrete functor. We consider a finitary coalgebra ${\mathsf{Pos}}$ functor $T^{\prime}$ to be the canonical extension — the posetification — of a fixed finitary standard ${\mathsf{Set}}$ functor $T$ preserving weak pull-backs. $T^{\prime}$ is defined as a completion w.r.t. ${\mathsf{Pos}}$-enriched colimits [BK11], and it preserves exact squares. $T^{\prime}$ is an extension of $T$, meaning that $T^{\prime}D\cong DT$. In particular, $T^{\prime}$ applied to a discrete poset yields a discrete poset. Observe that posetifications are self-dual on discrete posets:

[TABLE]

Therefore we can use $T^{\prime}$ on the syntax side as the arity of both nabla and delta modalities, as long as the language is discrete.

Language.

We fix a set of propositional atoms ${\mathsf{At}}^{\mathsf{Set}}$. Therefore $D{\mathsf{At}}^{\mathsf{Set}}$ can be used as a discrete poset ${\mathsf{At}}^{{\mathsf{Pos}}}$ of propositional atoms. The definition of the finitary Moss’ language in ${\mathsf{Set}}$ [KKV12b, 5.1], namely its $\neg$-free fragment which we denote ${\mathcal{L}}^{{\mathsf{Set}}}$, can be seen as an algebra for ${\mathbb{P}}_{\omega}+{\mathbb{P}}_{\omega}+T+T$, free on ${\mathsf{At}}^{\mathsf{Set}}$ (computed in ${\mathsf{Set}}$). The four components correspond to arities of conjunction, disjunction, nabla, and the delta modality. We aim at a definition of a discrete language ${\mathcal{L}}^{\mathsf{Pos}}$ so that $D{\mathcal{L}}^{{\mathsf{Set}}}\cong{\mathcal{L}}^{{\mathsf{Pos}}}$. For conjunction $\bigwedge:{\mathbb{P}}_{\omega}{\mathcal{L}}^{\mathsf{Set}}\longrightarrow{\mathcal{L}}^{\mathsf{Set}}$, we aim at its ${\mathsf{Pos}}$ counterpart being $D\bigwedge:{\mathbb{P}}^{c}_{\omega}D{\mathcal{L}}^{\mathsf{Set}}\longrightarrow D{\mathcal{L}}^{\mathsf{Set}}$, similarly for disjunction. For the nabla modality $\nabla_{T}:T{\mathcal{L}}^{\mathsf{Set}}\longrightarrow{\mathcal{L}}^{\mathsf{Set}}$ we aim at its ${\mathsf{Pos}}$ counterpart being $\nabla_{T^{\prime}}=D\nabla_{T}:T^{\prime}D{\mathcal{L}}^{\mathsf{Set}}\longrightarrow D{\mathcal{L}}^{\mathsf{Set}}$, similarly for delta. We therefore define the language ${\mathcal{L}}^{{\mathsf{Pos}}}$ to be an algebra for ${\mathbb{P}}^{c}_{\omega}+{\mathbb{P}}^{c}_{\omega}+T^{\prime}+T^{\prime}$, free on ${\mathsf{At}}^{\mathsf{Pos}}$ in ${\mathsf{Pos}}$. Observe that ${\mathcal{L}}^{{\mathsf{Pos}}}$ is indeed a discrete poset, because for two convex subsets of a discrete poset, $u\leq^{EM}v$ implies $u=v$, and $T^{\prime}$ applied to a discrete poset yields a discrete poset. It follows that indeed $D{\mathcal{L}}^{{\mathsf{Set}}}\cong{\mathcal{L}}^{{\mathsf{Pos}}}$.

Sequents in ${\mathsf{Set}}$ [BPV14] are pairs of finite subsets of ${\mathcal{L}}^{\mathsf{Set}}$ written as $\varphi\Rightarrow\psi$. For the purpose of this subsection only, sequents in ${\mathsf{Pos}}$ are pairs of finite convex subsets of ${\mathcal{L}}^{\mathsf{Pos}}$. Translation of the above sequent will be written as $D\varphi\Rightarrow D\psi$. This notation is justified by the following paragraph:

Elements and bases.

Assume that $\alpha$ is an element of $T{\mathcal{L}}^{\mathsf{Set}}$: \textstyle{\alpha:{\mathsf{1}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{T{\mathcal{L}}^{\mathsf{Set}}} . Applying $D$ to it yields an element of $T^{\prime}{\mathcal{L}}^{\mathsf{Pos}}$: \textstyle{D\alpha:D{\mathsf{1}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{DT{\mathcal{L}}^{\mathsf{Set}}\cong T^{\prime}{\mathcal{L}}^{\mathsf{Pos}}} . Similarly for $\varphi,\psi$ in ${\mathbb{P}}_{\omega}{\mathcal{L}}^{\mathsf{Set}}$ we have $D\varphi,D\psi$ in ${\mathbb{P}}^{c}_{\omega}{\mathcal{L}}^{\mathsf{Pos}}$, and for $\Phi,\Psi$ in ${\mathbb{P}}_{\omega}{\mathbb{P}}_{\omega}{\mathcal{L}}^{\mathsf{Set}}$ we have $D\Phi,D\Psi$ in ${\mathbb{P}}^{c}_{\omega}{\mathbb{P}}^{c}_{\omega}{\mathcal{L}}^{\mathsf{Pos}}$. Here we again abuse the notation slightly and denote by $\alpha$ or $D\alpha$ both the inclusion map and its image. Assume the base of $\alpha$ in $T{\mathcal{L}}^{\mathsf{Set}}$ is given by \textstyle{{\mathsf{base}}^{T}(\alpha):Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\mathcal{L}}^{\mathsf{Set}}} . Then we obtain the base of $D\alpha$ as \textstyle{{\mathsf{base}}^{T^{\prime}}(D\alpha)=D{\mathsf{base}}^{T}(\alpha):DZ\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\mathcal{L}}^{\mathsf{Pos}}} .

Relations and their lifting.

For a relation $R$ in ${\mathsf{Rel}}({\mathsf{Set}})$

[TABLE]

we obtain a monotone relation $DR$ in ${\mathsf{Rel}}({\mathsf{Pos}})$ by applying the functor $D$ to the span corresponding to $R$ to yield:

[TABLE]

The lifting of $R$ by $T$ in ${\mathsf{Rel}}({\mathsf{Set}})$ is given by the composite

[TABLE]

Applying the functor $D$ to its underlying span we obtain the $T^{\prime}$ lifting of $DR$

[TABLE]

From the above diagrams one can conclude the following:

[TABLE]

Coalgebras and valuations.

Given a $T$-coalgebra $c:X\longrightarrow TX$ in ${\mathsf{Set}}$, we can apply the functor $D$ to it to obtain the $T^{\prime}$- coalgebra $Dc:DX\longrightarrow T^{\prime}DX$ in ${\mathsf{Pos}}$. Given a valuation of propositional variables on the coalgebra $c$ [BPV14, Definition 3.5.], we can see it as a relation

\textstyle{\Vdash:{\mathsf{At}}^{\mathsf{Set}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X} , we obtain a corresponding valuation on $Dc$ as

\textstyle{D{\Vdash}:{\mathsf{At}}^{\mathsf{Pos}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{(DX)^{\mathit{op}}} . Observing carefully how the connectives $\bigwedge,\bigvee$ and $\nabla,\Delta$ are interpreted in [BPV14, Definition 3.5.] and in this paper in Subsections 5.B and 5.D, we observe that the correspondence carries out to link \textstyle{\Vdash:{\mathcal{L}}^{\mathsf{Set}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X} and

\textstyle{\mathrel{D{\Vdash}}:{\mathcal{L}}^{\mathsf{Pos}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{(DX)^{\mathit{op}}}

so that we can prove by induction that for each sequent

[TABLE]

(cf. [BPV14, Definition 3.18.], and a definition in Subsection 6.A of a valid sequent.) We spell out the case for the nabla modality (the other cases are simpler or similar):

[TABLE]

Before we go further, we sum up the correspondence between the ${\mathsf{Set}}$-based setting of the finitary Moss’ logic of [BPV14] and the ${\mathsf{Pos}}$-based setting of the finitary Moss’ logic of this paper (with the arities of conjunction and disjunction adjusted) in the following table:

[TABLE]

Redistributions.

First let us cover the syntactic constructions behind the $\nabla$-r and $\Delta$-l rules. By [BPV14, Definition 3.14], the collections $L_{T}(\alpha)$ and $R_{T}(\beta)$ are defined as follows:

[TABLE]

Transferring this to ${\mathsf{Pos}}$, we obtain

[TABLE]

Comparing this with Definition 5.D, using the above table, we see that this provides us with the right definition when the arities of conjunction and disjunction are altered to be ${\mathbb{P}}^{c}_{\omega}$, putting:

[TABLE]

Turning to redistributions, from [BPV14, Definition 3.20.] of slim redistribution, and its generalization for two-sided sequents explained on p. 44 therein, we can extract the following: Let $(A,B)$ be an element of $P_{\omega}T{\mathcal{L}}^{\mathsf{Set}}\times P_{\omega}T{\mathcal{L}}^{\mathsf{Set}}$. A $\Phi$ in $T({\mathbb{P}}_{\omega}{\mathsf{base}}^{T}(A)\times{\mathbb{P}}_{\omega}{\mathsf{base}}^{T}(B))$ is a slim redistribution of $(A,B)$ iff

[TABLE]

where $p_{0},p_{1}$ are the projections of the product ${\mathbb{P}}_{\omega}{\mathsf{base}}^{T}(A)\times{\mathbb{P}}_{\omega}{\mathsf{base}}^{T}(B)$. Transferring to ${\mathsf{Pos}}$ we obtain that for $(DA,DB)$ in $P^{c}_{\omega}T^{\prime}{\mathcal{L}}^{\mathsf{Pos}}\times P^{c}_{\omega}T^{\prime}{\mathcal{L}}^{\mathsf{Pos}}$ and $\Phi$ a slim redistribution as above, $D\Phi$ in $T^{\prime}({\mathbb{P}}^{c}_{\omega}{\mathsf{base}}^{T^{\prime}}(DA)\times{\mathbb{P}}^{c}_{\omega}{\mathsf{base}}^{T^{\prime}}(DB))$ satisfies

[TABLE]

Comparing this with Definition 6.A, using the table above, we see again that this fits with $D\Phi$ being a redistribution of $(DA,DB)$, modulo the arities of conjunction and disjunction being altered to be ${\mathbb{P}}^{c}_{\omega}$:

[TABLE]

Rules of the calculus.

Using the transfer machinery described above, we can translate proofs of positive sequents from the two-sided calculus $G2_{T}$ of [BPV14, Definition 5.1.] to the calculus $G^{T^{\prime}}_{\nabla\Delta}$ of this paper (to be precise, to the calculus we obtain by systematically replacing the arities of conjunctions and disjunctions in $G^{T^{\prime}}_{\nabla\Delta}$ with ${\mathbb{P}}^{c}_{\omega}$). We can do so inductively, rule by rule. We will spell out the cases for the modal rules, and leave the propositional part of the calculus to be verified by the reader (propositional part of $G2_{T}$ can be found in [BPV14, Figure 1.], and that of $G^{T^{\prime}}_{\nabla\Delta}$ in Definition 6.A).

The following two rules of $G2_{T}$ are those of [BPV14, Definition 5.1.], adapted to our current notation:

[TABLE]

[TABLE]

They translate into the following instances of the two rules of the modified (as for the arities of conjunctions and disjunctions) $G^{T^{\prime}}_{\nabla\Delta}$ from Definition 6.A

[TABLE]

[TABLE]

The following rule of $G2_{T}$ is the one of [BPV14, Definition 5.1.], adapted to our current notation (in particular, $p_{0}(z^{\Phi})$ is originally denoted by $A_{L}^{\Phi}$ and $p_{1}(z^{\Phi})$ is denoted by $B_{R}^{\Phi}$ and the notation explained on p. 47 (18).)

[TABLE]

It translates into the following instance of the $T^{\prime}(\nabla\Delta)$ rule of Definition 6.A

[TABLE]

To sum up, using the above, we can state the following theorem

Theorem 28**.**

Let $\varphi,\psi$ be finite subsets of ${\mathcal{L}}^{\mathsf{Set}}$ (i.e., the $\neg$-free fragment of the classical Moss’ coalgebraic language).

[TABLE]

Proof 7.1**.**

The left-right direction is proven by induction on the proof in $G2_{T}$, translating it step-by-step using the discrete functor as described above.

The right-left direction is proven by contraposition, using the completeness of the two calculi. Assume that $\nvdash_{G2_{T}}\varphi\Rightarrow\psi$. Then there is a coalgebra $c:X\longrightarrow TX$, a valuation of ${\mathcal{L}}^{\mathsf{Set}}$, and a state $x$ so that

[TABLE]

Then, by 7.28, the coalgebra $Dc:DX\longrightarrow T^{\prime}DX$, the translated valuation of ${\mathcal{L}}^{\mathsf{Pos}}$, and a state $x$ refute the sequent

[TABLE]

{exa}

Consider the finitary convex powerset functor ${\mathbb{P}}^{c}_{\omega}$ as the coalgebra functor. ${\mathbb{P}}^{c}_{\omega}$ is the posetification of the finitary powerset functor ${\mathbb{P}}_{\omega}$, whose coalgebras in ${\mathsf{Set}}$ correspond to image-finite Kripke frames. Thus, adapting the arities of conjuctions and disjunctions in the calculus $G^{{\mathbb{P}}^{c}_{\omega}}_{\nabla\Delta}$ captures the positive fragment of the finitary Moss’ logic over image-finite Kripke frames (whose complete proof theory is provided by the calculus $G2_{{\mathbb{P}}_{\omega}}$ of [BPV14]).