Strongly Complete Logics for Coalgebras

Alexander Kurz^{∗} University of Leicester, UK

Jiří Rosický^{†} Masaryk University, Brno, Czech Republic

19th July 2006

Abstract

Coalgebras for a functor T on a category X model many different types of transition systems in a uniform way. This paper focuses on a uniform account of finitary strongly complete specification languages for Set-based coalgebras.

We show how to associate a finitary logic to any finite-sets preserving functor T and prove the logic to be strongly complete under a mild condition on T. The proof is based on the following result. An endofunctor on a variety has a presentation by operations and equations iff it preserves sifted colimits.

1 Introduction

Coalgebras for a functor T on a category X model many different types of transition systems in a uniform way. Coalgebras are dual to algebras and the logic of algebras is equational logic. But then, what is the logic of coalgebras? Can logics for coalgebras be described in a uniform way, and their properties be established in a uniform manner?

Our approach to these questions is based on Stone duality. We think of Stone duality [15, 2] as relating a category of algebras A representing a propositional logic to a category of topological spaces X representing the state-based models of the logic. The duality is provided by two contravariant functors P and S,

\xymatrix{X \ar[r]^{P} & A . \ar[l]^{S}}  (1)

P maps a space X to a propositional theory and S maps a propositional theory to its ‘canonical model’. Abramsky [1] extended a basic Stone duality as in Diagram 1 by ‘synchronising’ dual constructions on both sides of Diagram 1, thus providing a description of domain theory in logical form. This suggests that the modal logic of a functor T should be given by its dual L on A:

[figure: X; T; P; A; S; L]  (2)

∗Supported by Nuffield Foundation Grant NUF-NAL04.

†Supported by the Ministry of Education of the Czech Republic under the project 1M0545.

Then the category of L-algebras is dual to the category of T -coalgebras and the initial L-algebra provides a propositional theory characterising T -bisimilarity. Moreover, if L can be presented by generators and relations, one inherits a proof system from equational logic which is sound and strongly complete. Thus, logics for T -coalgebras arise from presentations of the dual of T by generators and relations. We characterise those functors L on varieties A that have a finitary presentation.

Whereas the result above gives us logics for coalgebras, our next aim is to prove a strong completeness result for finitary logics for Set-coalgebras. The approach indicated in Diagram 2 can be applied to Set-coalgebras, but as the dual of Set is the category CABA of complete atomic boolean algebras, the corresponding logics are infinitary. Our solution is to consider two Stone dualities:

[figure: Stone; BA; L; Set; T; CABA]  (3)

The upper row is the duality between Stone spaces and Boolean algebras, accounting for (classical finitary) propositional logic. L describes an expansion of propositional logic by modal operators and axioms. The lower row is the duality where our Set-based T -coalgebras live. How can these two worlds be related?

The crucial observation is the following. BA is the Ind-completion of finite Boolean algebras, that is, the completion of finite Boolean algebras under filtered colimits; Set is the Ind-completion of finite sets; and finite sets are dual to finite Booleans algebras. In other words, Set^{op} is the Pro-completion of finite Boolean algebras, that is, the completion of finite Boolean algebras under cofiltered limits.

[figure: BA; L; S; Set^{op}; P; T^{op}; _{BA_{ω} ≅ Set{op \atop ω}}; ˆ (−); ¯ (−)]  (4)

If T preserves finite sets then we can associate a modal logic to T by defining L to be the continuous extension that agrees with T on finite sets. Moreover, we obtain a natural transformation

δ : LP → P T

giving the semantics to the logic by inducing a functor P̃ : Coalg(T) → Alg(L). Similarly, if T weakly preserves cofiltered limits, we obtain

h : SL → T S

giving rise to a map on objects S̃ : Alg(L) → Coalg(T). From this, one obtains strong completeness: We can associate to any L-algebra A the coalgebra S̃A, which provides a counter example for each formula not holding in A.

Summary of Results Our main results are the following:

1. A functor on a variety A has a presentation iff it preserves sifted colimits.

2. Algebras over Ind-completions can be represented via algebras over Pro-completions.

3. To any functor on Stone that is determined by its action on finite Stone spaces, one can associate a finitary strongly complete modal logic that characterises T -bisimilarity.

4. To any functor on Set that preserves finite sets and weakly preserves cofiltered limits, one can associate a finitary strongly complete modal logic.

The first two results are of purely categorical nature and are treated in Sections 4 and 5. The next two results are essentially corollaries of the first two and are described in Sections 7 and 8. The last one generalises a result in modal logic known as bisimilarity-somewhere-else.

Comparison with other approaches In his seminal paper [24], Moss described a coalgebraic logic for any weak pullback preserving functor on sets, which to a large extent, answers our question for a parametric logic for coalgebras. But his solution has some drawbacks. First, the restrictions to sets and to weak-pullback preserving functors are essential to his approach. This prevents generalisations to logics for systems modelled in a domain theoretic (ie topological) setting. And it prevents extensions to situations where the modal law □φ ∧ □ψ → □(φ ∧ ψ) does not hold. This is typically the case in logics for games where one takes □φ to mean that the player can play some move that restricts the opponent to moves after which φ holds. Second, Moss’s logic does not provide modalities to decompose the structure of T, which is needed to allow for a flexible specification language. Related to this, there is no proof system and no completeness result.

To address these issues, attention was focused on special classes of functors given by a restricted number of type constructors for which logics were built in an ad hoc manner [22, 27, 14]. Pattinson [25] showed that these languages with their ad hoc modalities arise from modal operators given by certain natural transformations, called predicate liftings, associated with the functor T. Schröder [29] investigates the logics given by all predicate liftings of finite arity and shows that these logics are expressive for finitary functors T. This restriction to finitary functors excludes traditional transition systems. Moreover, it is not clear how this approach generalises to topological and domain theoretic settings.

Our approach does not suffer any of these drawbacks. On the other hand, for Set-functors, we restrict attention to those that preserve finite sets and weakly preserve cofiltered limits. As we will explain, this is justified by focussing on strong completeness results.

The observation that all logics given by predicate liftings correspond to a functor L on BA was made in [19]. That functors that have a presentation give rise to a logic for coalgebras was noted in [10]. Here we give a characterisation of the functors which have presentations. The process of taking a finite set preserving functor and extending it to BA, and hence to Stone, is related to a construction in Worrell [33] where a Set-functor is lifted to complete ultrametric spaces.

2 Algebras and Coalgebras

Given a functor L on a category A, an L-algebra (notation: (A, α) or just α) is an arrow α : LA → A. A morphism f : α → α′ is an arrow f : A → A′ such that f ∘ α = α′ ∘ Lf.

The category of algebras for a signature Σ and equations E is defined as usual (in particular, carriers are sets) and denoted by Alg(Σ, E). We say that a category A, equipped with a forgetful functor U : A → Set, has a presentation if there exists a signature Σ and equations E such that A is concretely isomorphic to Alg(Σ, E). A (or more precisely U : A → Set) is monadic (over Set) iff A has such a presentation and U : A → Set has a left adjoint.

A functor is finitary if it preserves filtered colimits. An object K of a category K is finitely presentable if its hom-functor hom(K, −) : K → Set is finitary. In Set, the finitely presentable objects are precisely the finite sets and in Alg(Σ, E) they are the algebras described by a finite set of generators and a finite set of relations.

A category monadic over Set is called a variety if it has a set of finitely presentable objects and every object is a filtered colimit of these. This is the case whenever all operations in Σ are of finite arity. We are particularly interested in the variety BA of Boolean algebras and in the variety DL of distributive lattices (with top and bottom elements).

Given a functor T on a category X, a T -coalgebra (notation: (X, ξ) or just ξ) is an arrow ξ : X → T X in X. A morphism f : ξ → ξ′ is an arrow f : X → X′ such that T f ∘ ξ = ξ′ ∘ f.

Throughout the paper it will be the case that X is the category Set or some category of topological spaces. It makes therefore sense to speak of the elements, or states, of some X ∈ X. We say that two states x, x′ of ξ : X → T X and ξ′ : X′ → T X′ are behaviourally equivalent or bisimilar if there are coalgebra morphisms f, f′ with f(x) = f′(x′). This notion of bisimilarity avoids the problems of Aczel and Mendler [4] bisimulations, which do not work properly if T does not preserve weak pullbacks. It goes back to Aczel and Mendler [4], who use it to generalise the final coalgebra theorem of Aczel [3] by removing the assumption of weak-pullback preservation.

3 Sifted Colimits Preserving Functors

Since a variety A can be built from its finitely presentable algebras by using filtered colimits, filtered colimits preserving functors L : A → A are fully determined by their values on finitely presentable algebras. The latter form a small part of K in the sense that, up to an isomorphism, there is only a set of them.

Filtered colimits are precisely those which commute in sets with finite limits. Thus they stem out from the doctrine of finite limits while varieties are given by the doctrine of finite products, see Lawvere [23]. It is therefore natural to consider colimits which commute in sets with finite products. These colimits are called sifted colimits. They were studied in [6] and the main result is that any variety can be built up from its strongly finitely presentable algebras by using sifted colimits. Here, an algebra A is strongly finitely presentable if hom(A, −) : A → Set preserves sifted colimits. These algebras coincide with finitely presentable (regular) projective algebras, ie with retracts of finitely generated free algebras. Any filtered colimit is of course sifted. Another important kind of sifted colimits are reflexive coequalizers (a parallel pair of arrows f, g is reflexive if there is t with ft = gt = id). Reflexive coequalizers include coequalizers of equivalence relations.

Sifted colimits preserving functors L : A → A are fully determined by their values on finitely generated free algebras. Their algebraic character is documented by the next result; recall that for a functor L preserving filtered colimits, Alg(L) is only locally finitely presentable.

Theorem 3.1. Let A be a variety and L : A → A preserve sifted colimits. Then Alg(L) is a variety.

Proof. Analogous to [5, Remark 2.75] using [7, 1.4.19].

The following result is a consequence of the fact that every finitely presentable algebra is a reflexive coequalizer of finitely generated free algebras.

Proposition 3.2. Let A be a variety and L : A → A preserve filtered colimits and reflexive coequalizers. Then L preserves sifted colimits.

Proof. Let A_{fp} be the full subcategory of A consisting of finitely presentable objects and A_{sfp} be the full subcategory of A consisting of strongly finitely presentable objects. Following [6, 2.3.(2)], A_{fp} is the (free) closure of A_{sfp} under reflexive coequalizers. Thus L is uniquely determined by its restriction L_{sfp} on A_{sfp}. Since A is a (free) closure of A_{sfp} under sifted colimits, L_{sfp} has a unique extension L′ : A → A preserving sifted colimits. Since both reflexive coequalizers and filtered colimits are sifted colimits, we have L′ = L. Hence L preserves sifted colimits.

In some very simple but important varieties like sets or linear spaces, every finitely presentable algebra is projective. As a consequence we get the next result which, in particular, implies that Alg(L) is a variety.

Proposition 3.3. Let A be a variety such that every finitely presentable algebra is projective. Then any functor L : A → A preserving filtered colimits preserves sifted colimits.

The previous proposition can be extended to boolean algebras. In fact, the trivial Boolean algebra 𝟙 is the only finitely presentable that is not projective. 𝟙 is the reflexive coequalizer

\xymatrix{F 1 \ar[r]^{i} \ar[r]_{o} & F 0 \ar[r]^{s} & 𝟙}  (5)

where F is the left adjoint to the forgetful functor BA → Set, i maps the generator to the top, and o maps the generator to the bottom. If L : BA → BA preserves filtered colimits and the above coequalizer, then L preserves sifted colimits.

Proposition 3.4. For any filtered colimit preserving functor L : BA → BA there is a sifted colimit preserving functor L′ : BA → BA such that L and L′ are isomorphic when restricted to the full subcategory of BA without 𝟙. Moreover, Alg(L) = Alg(L′).

Proof. Define L′ = L on the full subcategory of BA not containing 𝟙, and L′𝟙 such that L′ preserves the coequalizer s in (5). Since there are no arrows 𝟙 → A other than the identity, we only have to define L′ on arrows h : A → 𝟙, A ≠ 𝟙. Choose an arrow f : A → F 0 and define L′h = L′s ∘ L′f. This does not depend on the choice of f. Indeed, for another arrow g : A → F 0, there is k : A → F 1 such that i ∘ k = f, o ∘ k = g. Finally, the proof that L′ preserves sifted colimits is essentially the same as the one of Proposition 3.2.

The proposition shows that as far as we are concerned with algebras over BA, we can assume any finitary functor to preserve sifted colimits.

4 Presenting Functors on Varieties

We show that sifted colimits preserving functors are precisely those that can be presented by finitary operations and equations in finite sets of variables.

4.1 Presentations of algebras and functors

An algebra A in a variety A with forgetful functor U : A → Set is said to be presented by generators G and relations R ⊆ UF G × UF G if A is the coequalizer

\xymatrix{F R \ar[r]_{π_{2}^{♯}} \ar[r]^{π_{1}^{♯}} & F G \ar[r]^{q} & A.}  (6)

where F is left-adjoint to U and π_{1}^{♯}, π_{2}^{♯} come from the projections from R to UF G. Each algebra A is presented by its canonical presentation which has as set of generators UA and as relations the kernel of the counit ε_{A} : F UA → A.

Following [10], we define analogously the notion of a functor L : A → A having a presentation by operations and equations. The generators GUA of LA are given by a Set-functor GX = ∐_{k<ω} G_{k} × X^{k}. The elements of G_{k} are the k-ary operations. Relations are now induced by equations over finite sets V of variables, which are instantiated using valuations v : V → UA. The point of (7) below is that it generalises (6) in such a way that the generators and relations defining LA depend uniformly on A.

Definition 4.1 ([10]). A finitary presentation by operations and equations of a functor is a pair ⟨G, E⟩ where G : Set → Set, GX = ∐_{k<ω} G_{k} × X^{k} and E = (E_{V})_{V ∈ω}, E_{V} ⊆ (UF GUF V)^{2}. The functor L presented by ⟨G, E⟩ is the joint coequalizer

\xymatrix{F E_{V} \ar[r]^{π_{1}^{♯}} \ar[r]_{π_{2}^{♯}} & F GUF V \ar[r]^{F GUv} & F GUA \ar[r]^{q_{A}} & LA}  (7)

where V ranges over finite cardinals and v over morphisms (valuations of variables) F V → A.

Example 4.2. A modal algebra, or Boolean algebra with operator (BAO), is the algebraic structure required to interpret (classical) modal logic which consists of propositional logic plus a unary modal operator □ preserving finite conjunctions. Modal algebras are therefore algebras for the functor L : BA → BA, where LA is defined by generators □a, a ∈ A, and relations □⊤ = ⊤, □(a ∧ a′) = □a ∧ □a′. That is, GX = X, E_{V} = ∅ for V ≠ 2, E_{2} = {□⊤ = ⊤, □(v_{0} ∧ v_{1}) = □v_{0} ∧ □v_{1}}.

Remark 4.3. 1. That the generators appear now as a functor expresses that the same generators (the □ in the example above) are used for all LA. Similarly, the coequalizer (7) is expressed using equations in variables V, that is, the same relations are used for all LA. In E_{V} ⊆ (UF GUF V)^{2} the inner UF allows for the conjunction in □(v_{0} ∧ v_{1}) whereas the outer UF allows for the conjunction in □v_{0} ∧ □v_{1}. Finally, note that relationship between the operator □ and the boolean operators can not be expressed by a distributive law between L and UF as L is not defined on sets but only on algebras.

2. In the works of [25, 19, 29] ‘modal axioms of rank 1’ play a prominent role. These are exactly those which, considered as equations, are of the form E_{V} ⊆ (UF GUF V)^{2}.

Before we come to the main consequence of the definition, let us point out the useful fact:

Proposition 4.4. Consider a functor L on a variety A. If L has a presentation then L preserves surjective morphisms and injective morphisms.

The main point of the definition is that one obtains a presentation of Alg(L) from a presentation of A and from a presentation of L.

Theorem 4.5 ([10]). Let A ≅ Alg(Σ_{A}, E_{A}) be a variety and ⟨Σ_{L}, E_{L}⟩ a finitary presentation of L : A → A. Then Alg(Σ_{A} + Σ_{L}, E_{A} + E_{L}) is isomorphic to Alg(L), where equations in E_{A} and E_{L} are understood as equations over Σ_{A} + Σ_{L}.

Remark 4.6. 1. The logical significance of theorem is that it ensures that the Lindenbaum algebra for the signature Σ_{A} + Σ_{L} and the equations E_{A} + E_{L} is the initial L-algebra.

2. The special format of the equations is needed to guarantee that, given a presentation of a functor ⟨Σ, E⟩, the algebras for the presented functor satisfy E.

4.2 The characterisation theorem

Before turning to functors on an arbitrary variety we have a look at functors on Set.

It is well known how to present a finitary endofunctor H on Set by operations and equations: Any such H is a quotient

∐_{k<ω} Hk × X^{k} ⟶^{τ_{X}} HX  (8)
( σ , l ) ↦ Hl(σ)  (9)

where k = {0, … k − 1} and l : k → X. σ ∈ Hk is an k-ary operation and the quotient gives the action of σ on a list of arguments l : k → X.

Now consider L : A → A. The idea behind (8) can also be applied to the set-valued functor UL. Since (8) depends on considering arities k as objects in the domain of H, we replace k by the free algebras F k ∈ A. So Hk becomes ULF k and X^{k} = Set(k, X) becomes A(F k, A) ≅ Set(k, UA) = UA^{k}, which leads us to consider

∐_{k<ω} ULF k × UA^{k} ⟶^{ϱ_{A}} ULA  (10)
( σ , l ) ↦ (ULε_{A} ∘ ULF l)(σ)  (11)

This gives us a signature with k-ary operations ULF k, which we describe by the functor

GY = ∐_{k<ω} ULF k × Y^{k}.  (12)

To obtain the equations from (10), since sifted colimit preserving functors are determined by their action on free algebras, it is enough to consider the maps ϱ_{F V}. But the kernel of ϱ_{F V} : GUF V → ULF V determines only the set ULF V and not the algebra LF V. The equations in variables V will therefore be given by the kernel of the adjoint transpose of ϱ

F GUF V ⟶^{ϱ_{F V}^{♯}} LF V.

Definition 4.7. Let L be an endofunctor on a variety A. The finitary presentation ⟨G, E⟩ of L (Definition 4.1) is given by generators G : Set → Set as in (12) and equations E = (E_{V})_{V ∈ω} where E_{V} is the kernel π_{1}, π_{2} : E_{V} ⟶ UF GUF V of Uϱ_{F V}^{♯}, with ϱ as in (10).

We first show that the functor presented by ⟨G, E⟩ agrees with L on finitely generated free algebras F n.

Lemma 4.8. Consider n ∈ ℕ. Then

\xymatrix{F E_{V} \ar[r] \ar[r] & F GUF V \ar[r]^{F GUv} & F GUF n \ar[r]^{ϱ_{F n}^{♯}} & LF n}  (13)

is a joint coequalizer.

Proof. We start by showing that

\xymatrix{F E_{n} \ar[r]^{π_{1}^{♯}} \ar[r]_{π_{2}^{♯}} & F GUF n \ar[r]^{ϱ_{F n}^{♯}} & LF n}  (14)

is a coequalizer. Let P be the kernel pair of ϱ_{F n}^{♯} in A. UP = E_{n}. Moreover, the U-image of this kernel pair is a split coequalizer. From this, it follows that the U-image of (14) is split, hence (14) is a coequalizer in A. Next we show that the joint coequalizer of (13) agrees with the coequalizer of (14). First, to see that all pairs in the kernel of ϱ_{F n}^{♯} are identified in the joint coequalizer it is enough to choose V = n and v = id_{V}. Conversely, by the definition of E_{V}, a pair (s, t) in F GUF n is identified in the joint coequalizer only if there is V and v : F V → F n such that (s, t) is the image under UF GUv of a pair in the kernel of ϱ_{F V}^{♯}. So we have to show that the kernel of ϱ_{F V}^{♯} is contained in the kernel of ϱ_{F n}^{♯} ∘ F GUv. But this follows from the commutativity of

\xymatrix{F GUF n \ar[r]^{ϱ_{F n}^{♯}} & LF n \\ F GUF V \ar[u]^{F GUv} \ar[r]_{ϱ_{F V}^{♯}} & LF V \ar[u]_{Lv}}

which is due to naturality of ϱ^{♯}.

The characterisation theorem is now proved using that sifted colimits preserving functors are determined by their action on finitely generated free algebras.

Theorem 4.9. An endofunctor on a variety has a finitary presentation by operations and equations if and only if it preserves sifted colimits.

Proof. Suppose first that L has a presentation as in (7). Let c_{i} : A_{i} → A be a sifted colimit. We have to show that Lc_{i} is a sifted colimit. Given a cocone d_{i} : LA_{i} → L′ we have to show that there is a unique k as depicted in

[figure: F E_{V}; π_{1}^{♯}; π_{2}^{♯}; F GUF V; F GUv^{♯}; F GUA_{i}; q_{A_{i}}; F GUc_{i}; LA_{i}; Lc_{i}; d_{i}; F GUA; q_{A}; h; LA; k; L′]

U preserves sifted colimits because A is a variety, G preserves sifted colimits because they commute with finite products, and F preserves all colimits. Therefore we have h with d_{i} ∘ q_{A_{i}} = h ∘ F GUc_{i}. Then k is obtained from the joint coequalizer q_{A} once we show that h∘F GUv^{♯}∘π_{1}^{♯} = h∘F GUv^{♯}∘π_{2}^{♯} for all v : V → UA. For this consider v : V → UA. Since hom(V, −) preserves sifted colimits (V is finite) and U preserves sifted colimits, there is some A_{j} and some w : V → UA_{j} such that v = Uc_{j} ∘ v′. It follows v^{♯} = c_{j} ∘ w^{♯}, hence F GUv^{♯} = F GUc_{j} ∘ F GUw^{♯}.

For the converse, let ⟨G, E⟩ be the presentation of a sifted colimits preserving functor L and denote by L′ the functor presented by ⟨G, E⟩. It follows from Lemma 4.8 that L′F n ≅ LF n on finitely generated free algebras F n. We know from the first part of the proof that L′ preserves sifted colimits. Hence L and L′ are sifted colimits preserving functors which agree on finitely generated free algebras and, therefore, are isomorphic.

The theorem will give rise to finitary logics for functors in Sections 7 and 8. But let us note two immediate corollaries. First sifted colimit preserving functors preserve regular epis in general. Using that they have a presentation, one can also show:

Corollary 4.10. A sifted colimit preserving functor L on a variety preserves monos.

The import of this proposition is the following. If we build the Lindenbaum algebra of a logic using the initial algebra sequence 0 → L0 → L^{2}0 … then the corollary implies that all arrows in the sequence are injective. This means that logical equivalence of formulas of depth n can be decided at level n.

Using that sifted colimits preserving functors are closed under composition one immediately obtains:

Corollary 4.11. Functor having a finitary presentation are closed under composition.

5 Algebras on Ind and Pro Completions

As motivated in the introduction, we study the relation between two completions of a small category C with finite limits and colimits: the completion ˆ (−) : C → IndC by filtered colimits and the completion ¯ (−) : C → ProC by cofiltered limits. Consider

\xymatrix{IndC \ar[rr]_{Σ} &  & ProC \ar[ll]_{Π} \\  & C \ar[ul]^{ˆ (−)} \ar[ur]_{¯ (−)}}  (15)

where Σ is the left Kan-extension of ¯ (−) along ˆ (−), and Π is the right Kan-extension of ˆ (−) along ¯ (−). In particular we have

ΣĈ = C̄  ΠC̄ = Ĉ  (16)

Example 5.1. 1. C = BA_{ω} (finite Boolean algebras = finitely presentable Boolean algebras), IndC = BA, ProC = Set^{op}. ΣA is the set of ultrafilters over A and Π is (contravariant) powerset.

2. C = DL_{ω} (finite distributive lattices = finitely presentable distributive lattices), IndC = DL, ProC = Poset^{op}. ΣA is the set of prime filters over A and Π gives the set of downsets.

Proposition 5.2. Σ is left adjoint to Π.

Proof. IndC is the subcategory of Set^{C^{op}} of finite limit preserving functors, ˆ (−) is the codomain restriction of the Yoneda embedding C → Set^{C^{op}}, and ¯ (−) is the codomain restriction of the dual of the Yoneda embedding C^{op} → Set^{C}. We need a natural isomorphism

\frac{ΣA → X}{A → ΠX}

Since Σ is filtered colimit preserving and Π cofiltered limit preserving, ProC is a (free) completion of C under cofiltered limits and IndC is a (free) cocompletion of C under filtered colimits, it suffices to have natural isomorphisms

\frac{hom(C, −) → hom(D, −)}{hom(−, C) → hom(−, D)}

(because Ĉ = hom(−, C) and C̄ = hom(C, −)). Since the first line is in (Set^{C})^{op}, we need a natural isomorphism

\frac{hom(D, −) → hom(C, −)}{hom(−, C) → hom(−, D)}

where the both lines are in the corresponding functor categories. But this is evident.

We want to present algebras over IndC by algebras over ProC

[figure: IndC; H; Σ; ProC; Π; K]  (17)

where we assume that H and K agree on C, that is,

ΣHĈ = KC̄  ΠKC̄ = HĈ  (18)

The natural transformation δ : HΠ → ΠK. ΠX is a filtered colimit Ĉ_{i} → ΠX. If H preserves filtered colimits we therefore obtain HΠ → ΠK as in

\xymatrix{ΠX & HΠX \ar[r]^{δ_{X}} & ΠKX \\ Ĉ_{i} \ar[u]^{c_{i}} & HĈ_{i} \ar[u]^{Hc_{i}} \ar[r]^{=} & ΠKΣĈ_{i} \ar[u]_{ΠKc_{i}^{♯}}}  (19)

where c_{i}^{♯} : ΣĈ_{i} → X is the transpose of c_{i} : Ĉ_{i} → ΠX. δ allows us to lift Π to a functor

\xymatrix{Alg(H) & Alg(K) \ar[l]_{Π̃}}  (20)

mapping a K-algebra (B, β) to the H-algebra (ΠB, β ∘ δ_{B}).

The transformation h : KΣ → ΣH. h is defined as in the following diagram where the d_{k} are a filtered colimit and we assume that K weakly preserves filtered colimits.

\xymatrix{A & KΣA \ar[r]^{h_{A}} & ΣHA \\ Â_{k} \ar[u]^{d_{k}} & KΣÂ_{k} \ar[u] \ar[r]^{=} & ΣHÂ_{k} \ar[u]}  (21)

h_{A} is not uniquely determined and we do not assume that it is natural. It allows to lift Σ to a map on objects

\xymatrix{Alg(H) \ar[r]_{Σ̃} & Alg(K)}  (22)

Representing H-algebras as Π-images of K-algebras. Denote by ι the unit of the adjunction Σ ⊣ Π. Our next theorem states that for all algebras HA → A the following diagram commutes

\xymatrix{A \ar[d]_{ι_{A}} &  &  & HA \ar[lll] \ar[d]^{Hι_{A}} \\ ΠΣA & ΠΣHA \ar[l] & ΠKΣA \ar[l]_{Πh_{A}} & HΠΣA \ar[l]_{δ_{ΣA}}}  (23)

Theorem 5.3. Assume in Diagram 17 that H preserves filtered colimits, that K weakly preserves filtered colimits, and that H and K agree on C (ie the equations (18) hold). Then for any H-algebra (A, α) it holds that ι_{A} : A → ΠΣA is an H-algebra morphism (A, α) → Π̃(ΣA, α ∘ h_{A}).

Proof. To show that Diagram 23 commutes, we have to show that ι_{A} is an H-algebra morphism. Since ι is natural ι_{HA} = Πh_{A} ∘ δ_{ΣA} ∘ Hι_{A} does suffice, see the upper row of Diagram 24, where

\xymatrix{HA \ar[r]_{Hι_{A}} \ar[rrrrr]^{ι_{HA}} & HΠΣA \ar[rr]_{δ_{ΣA}} &  & ΠKΣA \ar[rr]_{Πh_{A}} &  & ΠΣA \\ HÂ_{k} \ar[u]^{Hd_{k}} \ar[rrrrr]_{ι_{HÂ_{k}}} & HĈ_{i} \ar[u]^{Hc_{i}} \ar[r]^{=} & ΠKΣĈ_{i} \ar[ur]_{ΠKc_{i}^{♯}} &  & ΠKΣÂ_{k} \ar[ul]^{ΠKΣd_{k}} \ar[r]^{=} & ΠΣHÂ_{k} \ar[u]_{ΠΣHd_{k}}} (24)

c_{i} : Ĉ_{i} → ΠΣA and d_{k} : Â_{k} → A are filtered colimits. The left-hand quadrangle is Diagram 19 and the right-hand quadrangle is the Π-image of Diagram 21. The outer quadrangle commutes, hence ι_{HA} is the unique arrow from the colimiting cocone Hd_{k} to the cocone ΠΣHd_{k} ∘ ι_{HÂ_{k}}. We have to show that Πh_{A} ∘ δ_{ΣA} ∘ Hι_{A} is also an arrow between these cocones.

The d_{k} form the colimiting cocone for the diagram ˆ (−)↓A, the c_{i} for ˆ (−)↓ΠΣA. There is a functor l : ˆ (−)↓A → ˆ (−)↓ΠΣA taking k : B → A to l(k) = ι_{A} ∘ k : B → ΠΣA. We have Ĉ_{l(k)} = A_{k} and ι_{A} ∘d_{k} = c_{l(k)}. It follows that the HÂ_{k} = HĈ_{l(k)} form a subdiagram of the HĈ_{i} and that any cocone over the HĈ_{l(k)} induces a cocone over the HÂ_{k}; it is therefore enough to show that Diagram 25 commutes and that the lower line is ι_{HĈ_{l(k)}}. The diagram commutes since the triangle in the middle

[figure: HA; Hι_{A}; HΠΣA; δ_{ΣA}; ΠKΣA; Πh_{A}; ΠΣA; HĈ_{l(k)}; Hd_{k}; Hc_{l(k)}; =; ΠKΣĈ_{l(k)}; ΠKc_{l(k)}^{♯}; id; ΠKΣÂ_{k}; ΠKΣd_{k}; =; ΠΣHÂ_{k}; ΠΣHd_{k}]  (25)

commutes, which follows from

\xymatrix{ΠKΣĈ_{l(k)} \ar[r]^{ΠKΣc_{l(k)}} & ΠKΣΠΣA \ar[r]^{ΠKηΣA} & ΠKΣA \\ ΠKΣÂ_{k} \ar[u]^{id} \ar[r]_{ΠKΣd_{k}} & ΠKΣA \ar[u]_{ΠKΣι_{A}} \ar[ur]_{id}}

where the right-hand triangle is one of the triangle equalities of the adjunction given by ι : Id → ΠΣ and η : Id → ΣΠ and the upper row is ΠKc_{l(k)}^{♯}. Finally, using the other triangle equality and that the units are isos on finite objects, the lower line is (Πη_{KΣĈ_{l(k)}})^{−1} = ι_{ΠKΣĈ_{l(k)}} = ι_{HĈ_{l(k)}}.

This theorem will give rise to completeness of Set-coalgebras in Section 8. To illustrate the power of the theorem we derive some corollaries.

1. (Stone [30]) Choose C = BA_{ω}, H and K to be the identity. Then IndC, ProC, Σ and Π are as in Example 5.1 and we obtain: Every boolean algebra A can be embedded into a powerset, with Boolean operations receiving their set-theoretic interpretation.

2. (Jónsson and Tarski [17]) C = BA_{ω} as above but take H to be the functor L from Example 4.2 and K to be powerset. With this data, our theorem states that every Boolean algebra with operators can be embedded into a complete Boolean algebra whose carrier is a powerset.

3. (Stone [31]) Choose C = DL_{ω}. Then IndC, ProC, Σ and Π are as in Example 5.1 and we obtain: Every distributive lattice A can be embedded into the completely distributive lattice of subsets ΠΣA.

4. (Gehrke and Jónsson [11]) This is the generalisation of (2.) to distributive lattices. For H one takes the Vietoris functor of Johnstone [16], restricted to DL.

6 A Brief Review of Stone Duality

For most of the paper, we need from this subsection only the fact that there is a category Stone of topological spaces which is dually equivalent to BA. The reason for giving a more abstract account, is that we will occasionally mention distributive lattices and want to indicate possible extensions of our results.

To treat different Stone dualities simultaneously, one considers them as arising from the adjunction of topological spaces Top and frames Frm [15]. Frm captures the algebraic properties of a topology, namely, a frame is a distributive lattice with infinite joins that distribute over finite meets. There are contravariant functors

\xymatrix{Top \ar[r]^{P} & Frm \ar[l]^{S}}

P (X, O) = O, P (f) = f^{−1}, and S(A) = Frm(A, 𝟚), where 𝟚 is the two element frame (consisting of ⊥, ⊤). S(f) = λs ∈ S(A) . s ∘ f. The functors P and S are adjoint on the right, that is, there is a bijection, natural in X and A,

Top(X, SA) ≅ Frm(A, P X).

We are interested in subcategories of Top and Frm on which the adjunction restricts to a dual equivalence, or duality for short. P X ≅ A then means that A is an expressive and complete propositional theory for X in the following sense

• for x ≠ y ∈ X there is a ∈ P X separating x and y,

• for a ≰ b ∈ A there is x ∈ SA ≅ X such that x(a) = 1 and x(b) = 0.

We read the second property as: if a does not imply b then there is a counter-example x. These two properties are ultimately responsible for our expressiveness and completeness results.

Two examples of relevant subcategories are the category Stone of Stone spaces, which is dual to BA. And the category Spec of spectral spaces (coherent spaces in [15]), which is dual to DL. For many more examples see Abramsky and Jung [2] and Johnstone [15].

7 Adequate Modal Logics for Coalgebras

In this section we show how we can associate to a functor T a modal logic that is adequate for T coalgebras in the sense that it is sound, complete, and characterises bisimilarity. We do this in two steps.

1. First, abstracting from syntax, we simply consider as propositions of the logic the elements of the initial L algebra, where L is the dual of T. We call this logic the abstract logic of T -coalgebras.

2. Second, we obtain a syntax and a proof system for the abstract logic from a presentation of the functor L. We call these logics the concrete logics of T -coalgebras.

The point of the separation is that the results we prove about the concrete logics do not depend on the chosen presentation and are conducted solely on the level of the abstract logics.

7.1 Abstract modal logics

Consider

[figure: Coalg(T); P̃; Alg(L); S̃; X; T; P; A; S; L; U; Set; Set]  (26)

where we assume that

• the dual equivalence between X and A arises from the adjunction of Top and Frm by restricting to subcategories X and A,

• L is dual to T, that is, there is an isomorphism

δ : LP → P T

• A is a variety (see p.3).

δ allows us to extend the equivalence between X and A to an equivalence between Coalg(T) and Alg(L), where P̃ maps a coalgebra (X, ξ) to (P X, P ξ ∘ δ_{X}). We can therefore consider Alg(L) as providing a logic for Coalg(T):

Definition 7.1. The algebra of propositions in variables V is the free L-algebra Prop(V ) over V . Given a coalgebra (X, ξ), we write [[−]]_{(X,ξ,h)} for the morphism Prop(V ) → P̃(X, ξ) determined by the valuation h : V → UP X. The semantics of a proposition φ is [[φ]]_{(X,ξ,h)} ⊆ X.

We define

Coalg(T) ⊧ (φ ⊢ ψ)

if [[φ]]_{(X,ξ,h)} ⊆ [[ψ]]_{(X,ξ,h)} for all coalgebras and all valuations. For a collection Γ of ‘sequents’ φ_{i} ⊢ ψ_{i}, we write Γ ⊧ (φ ⊢ ψ) if Coalg(T) ⊧ Γ ⇒ Coalg(T) ⊧ (φ ⊢ ψ).

Remark 7.2. Because distributive lattices have no implication, the notation (φ ⊢ ψ) is needed to logically encode the order ≤ of the lattices. This is as in [1].

Proposition 7.3. The logic for T -coalgebras given in the previous definition

1. respects bisimilarity: propositions are invariant under bisimilarity

2. is expressive: any two non-bisimilar states are distinguished by some proposition

3. Γ ⊧ (φ ⊢ ψ) iff φ ≤ ψ in the quotient of Prop(V ) wrt the equations {φ_{i} ∧ ψ_{i} = φ_{i} | (φ_{i} ⊢ ψ_{i}) ∈ Γ}.

The proposition is an immediate consequence of Stone duality.

7.2 Concrete logics

We restrict our attention now to the duality of BA and Stone. In particular, in Diagram 26, P maps a Stone space to its basis of clopens and S maps a Boolean algebra to the set of ultrafilters over A.

We will show that a modal logic enjoying the properties of Proposition 7.3 can be associated to any functor T : Stone → Stone that is determined by its action on finite Stone spaces.

Let L = P T S be the dual of T. That T is determined by its action on finite Stone spaces means that L preserves filtered colimits. By Proposition 3.4, we can assume L to preserve sifted colimits. It follows from Theorem 4.9 that L has a presentation ⟨Σ_{L}, E_{L}⟩ and from Theorem 4.5 that the free L-algebras Prop(V ) are the Lindenbaum algebras of the equational logic (Σ_{BA} + Σ_{L}, E_{BA} + E_{L}).

To translate this equational logic into a modal logic is a standard procedure [9]. Each term in operation symbols from Σ_{BA} + Σ_{L} is considered as a formula. Equations s = t are rendered as s ↔ t. Conversely, any formula s can be read as an equation s = ⊤ where ⊤ ∈ Σ_{BA}. To summarise:

Theorem 7.4. Let T : Stone → Stone be a functor preserving cofiltered limits. Then T has a sound and strongly complete modal logic that characterises bisimilarity.

Example 7.5. 1. Stone coalgebras for functors built according to

T ::= K | Id | T × T | T + T | T^{N} | PT

(K a constant, N a finite constant, P powerspace) were considered in [21]. All these functors preserve cofiltered limits and the above theorem summarises most aspects of that paper.

2. Given a Stone space (X, OX) define H(X, OX) = (HX, HOX) as HX = {h ⊆ P X}. HOX is generated by the sets □ □a = {h ∈ HX | a ∈ h}. Then H is a functor on Stone. Its dual has a simple presentation: One unary operation □ and no equations.

3. Define H^{↑}(X) = {h ⊆ P X | h upward closed }. Then H^{↑} is a functor on Stone. Its dual is presented by a unary operator □ and an equation saying that □ is monotone. H^{↑}-coalgebras were studied in [12].

8 The Finitary Modal Logic of Set-Coalgebras

The aim of this section is to associate a strongly complete modal logic to suitable functors T : Set → Set. As we are interested here in classical propositional logic the logic will be given by a functor L_{T} : BA → BA. That is we are concerned with the following situation

[figure: BA; L_{T}; S; Set; P; T]  (27)

where S maps an algebra to the set of its ultrafilters and P is the contravariant powerset. Note that S and P take a meaning here that differs from the previous section.

Assuming that T preserves finite sets, we define L_{T} to be L_{T} A = P T SA on finite BAs and then extend L_{T} continuously to all of BA. As L_{T} preserves filtered colimits, we can associate a modal logic to it, as explained in Section 7. This logic is sound and strongly complete for Stone-coalgebras for the dual T̄ of L_{T}. Here, we show that strong completeness also holds wrt T -coalgebras.

Note that Diagram 27 is an instance of Diagram 17. From (19) we obtain a natural transformation δ : L_{T} P → P T which in turn yields, as in (20), a functor P̃ : Coalg(T) → Alg(L_{T}). P̃ now induces a semantics exactly as in Definition 7.1. But we cannot use Proposition 7.3 to prove completeness as we do not have a dual equivalence between BA and Set. We proceed as follows:

Suppose Γ ⊬ φ. Let A be the free L_{T} algebra quotiented by Γ. By Theorem 5.3, there is a T -coalgebra on SA such that ι_{A} : A → P SA is an L_{T} -algebra morphism. ι_{A} maps all propositions in Γ to all of SA, but φ only to a proper subset. Therefore there is an element in SA satisfying Γ and refuting φ. We have shown:

Theorem 8.1. Let T : Set → Set preserve finite sets and weakly preserve cofiltered limits. Then T has a sound and strongly complete modal logic.

Remark 8.2. 1. The weak preservation of cofiltered limits means, in particular, that all projections in the final sequence are onto. The only example of a functor we are aware of that does not satisfy this condition is the finite powerset functor, see [33]. And indeed, standard modal logic is strongly complete wrt Kripke frames, but not wrt finitely branching ones.

2. The probability distribution functor [32] does not preserve finite sets. And indeed, modal logics for probabilistic transition systems, see eg [13], are not strongly complete. Similarly for T X = K × X where K is an infinite constant.

3. In contrast, we can extend our result to functors X ↦ (T X)^{K} for infinite K if T preserves finite sets. Indeed, T^{K} is a cofiltered limit of the functors T^{K_{i}} where K_{i} ranges over the finite subsets of K. We can now apply the theorem to obtain logics L_{T^{K_{i}}} and then extend the result to the colimit of the L_{T^{K_{i}}} and the limit of the T^{K_{i}}. This allows us to include functors such as (PX)^{K} ≅ P(K × X), K infinite (which give rise to labelled transition systems).

4. In [20] it was shown that one can have such a theorem if a suitable h as in (21) exists. Here we gave conditions under which this is indeed the case.

Example 8.3. 1. The functors built according to

T ::= N | Id | T × T | T + T | T^{K} | PT

(K a constant, N a finite constant, P powerset) were studied in [26, 14]. Their completeness results are extended here to strong completeness.

2. The double contravariant powerset functor 2^{2^{−}} does not preserve weak pullbacks [28] and therefore cannot be treated by Moss’s coalgebraic logic [24]. But it does satisfy the assumptions of the theorem and L_{2^{2^{−}}} has a particularly simple presentation: one unary operation symbol □ and no equations.

3. Similarly, but more importantly, the subfunctor UpX of 2^{2^{X}}, which takes as values upward closed sets of subsets, does not preserve weak pullbacks [12]. L_{Up} can be presented by one unary operator □ and one equation expressing that □ is monotone. Coalgebras for that functor are also known as monotone predicate transformers. They provide a natural semantics for logics of 2-player games, mentioned in the introduction.

9 Conclusion

Summary The purpose of the paper was to associate a finitary modal logic to a functor T, so that the logic is strongly complete wrt T -coalgebras. We took up the idea, well-established in domain theory [2], that a logic for the solution of a domain equation X ≅ T X is given by a presentation of the dual L of T. We characterised those functors on a variety that have a presentation (Theorem 4.9).

In a second move, we related two pairs of Stone dualities, one for the logic and one for the semantics. Distilling the essence of the algebraic completeness proof of modal logic via the Jónsson-Tarski Theorem, our second main contribution is Theorem 5.3 relating algebras on Ind and Pro-completions. It yields strong completeness for a large class of Set-functors, see Example 8.3.

One of the main aspects of this work is that it makes use of the notion of the presentation of a functor in order to separate syntax and semantics. The syntax is given by the presentation, the semantics in terms of natural transformations between functors. This led to a syntax-independent proof of Theorem 8.1.

An important point is that we do not need the assumption that T is finitary. This assumption is powerful when working with T -algebras, but it is much less so for T -coalgebras. Similarly, we do not need that T preserves weak pullbacks. Each of these assumptions would exclude fundamental examples.

Further, we find it important not to restrict our attention to Set-coalgebras. In all of domain theory, the systems are based on topological spaces. In fact, in any situation where one wants to incorporate a notion of admissible or observable subset, one is quickly led to a topological setting.

Future work Our approach can be extended to cover, on the semantic side, coalgebras over presheaves, and on the algebraic side, many-sorted algebras. This will allow us to obtain results about logics for name-passing calculi.

Can our characterisation theorem be extended to treat infinitary logics?

If Alg(L) is a variety, does L : A → A then preserve sifted colimits (converse of Theorem 3.1)? It is true for A = Set but the proof in [8, III.4.9] does not generalise.

The reason for getting strong completeness is that in a Stone duality any algebra can be represented by a space (see eg Theorem 8.1). For completeness, it is enough if free algebras can be represented. An example for this situation is propositional logic with countable conjunctions where strong completeness fails. Algebraically, this means that only the free countably complete Boolean algebras can be represented as algebras of subsets [18]. It will be interesting to extend our approach to settings like these.

References

[1] S. Abramsky. Domain theory in logical form. Annals of Pure and Applied Logic, 51, 1991.

[2] S. Abramsky and A. Jung. Domain theory. In Handbook of Logic in Computer Science. OUP, 1994.

[3] P. Aczel. Non-Well-Founded Sets. Stanford, 1988.

[4] P. Aczel and N. P. Mendler. A final coalgebra theorem. In Category Theory and Computer Science, volume 389 of LNCS, 1989.

[5] J. Adámek and J. Rosický. Locally Presentable and Accessible Categories. CUP, 1994.

[6] J. Adámek and J. Rosický. On sifted colimits and generalized varieties. Th. Appl. Categ., 8, 2001.

[7] J. Adámek, J. Rosický, and E. M. Vitale. Varieties. Draft available at http://www.math.

    muni.cz/~rosicky.

[8] J. Adámek and V. Trnková. Automata and Algebras in Categories. Kluwer, 1990.

[9] P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. CUP, 2001.

[10] M. Bonsangue and A. Kurz. Presenting functors by operations and equations. In FoSSaCS’06, LNCS, 2006.

[11] M. Gehrke and B. Jónsson. Bounded distributive lattices with operators. Math. Japonica, 40, 1994.

[12] H. Hansen and C. Kupke. A coalgebraic perspective on monotone modal logic. In CMCS’04, ENTCS, 2004.

[13] A. Heifetz and P. Mongin. Probabilistic logic for type spaces. Games and Economic Behavior, 35, 2001.

[14] B. Jacobs. Many-sorted coalgebraic modal logic: a model-theoretic study. Theor. Inform. Appl., 35, 2001.

[15] P. Johnstone. Stone Spaces. CUP, 1982.

[16] P. Johnstone. Vietoris locales and localic semilattices. In Continuous Lattices and their Applications, volume 101 of Lecture Notes in Pure and Applied Mathematics. Marcel Dekker, 1985.

[17] B. Jónsson and A. Tarski. Boolean algebras with operators, part 1. Amer. J. Math., 73, 1951.

[18] C. Karp. Languages with Expressions of Infinite Length. North-Holland, 1964.

[19] C. Kupke, A. Kurz, and D. Pattinson. Algebraic semantics for coalgebraic logics. In CMCS’04, ENTCS, 2004.

[20] C. Kupke, A. Kurz, and D. Pattinson. Ultrafilter extensions of coalgebras. In CALCO 2005, LNCS 3629, 2005.

[21] C. Kupke, A. Kurz, and Y. Venema. Stone coalgebras. Theoret. Comput. Sci., 327, 2004.

[22] A. Kurz. Specifying coalgebras with modal logic. Theoret. Comput. Sci., 260, 2001.

[23] F. W. Lawvere. Functorial Semantics of Algebraic Theories. PhD thesis, Columbia University, 1963.

[24] L. Moss. Coalgebraic logic. Annals of Pure and Applied Logic, 96, 1999.

[25] D. Pattinson. Coalgebraic modal logic: Soundness, completeness and decidability of local consequence. Theoret. Comput. Sci., 309, 2003.

[26] M. Rößiger. Coalgebras and modal logic. In CMCS’00, volume 33 of ENTCS, 2000.

[27] M. Rößiger. From modal logic to terminal coalgebras. Theoret. Comput. Sci., 260, 2001.

[28] J. Rutten. Universal coalgebra: A theory of systems. Theoret. Comput. Sci., 249, 2000.

[29] L. Schröder. Expressivity of Coalgebraic Modal Logic: The Limits and Beyond. In V. Sassone, editor, FoSSaCS’05, volume 3441 of LNCS, 2005.

[30] M. H. Stone. The theory of representations for boolean algebras. Trans. Amer. Math. Soc, 40, 1936.

[31] M. H. Stone. Topological representation of distributive lattices and Brouwerian lattices. Časopis pěst. mat. fys., 67, 1937.

[32] E. Vink and J. Rutten. Bisimulation for probabilistic transition systems: a coalgebraic approach. In Proceedings of ICALP’97, volume 1256 of LNCS, 1997.

[33] J. Worrell. On the final sequence of an finitary set functor. Theoret. Comput. Sci., 338, 2005.