Ultrafilter Extensions for Coalgebras

C. Kupke^{1}, A. Kurz^{2}^{⋆}, D. Pattinson^{3}

1 CWI and Universiteit van Amsterdam, Amsterdam, The Netherlands 2 Department of Computer Science, University of Leicester, UK 3 Imperial College, London, UK

Abstract. This paper studies finitary modal logics as specification languages for Set-coalgebras (coalgebras on the category of sets) using Stone duality. It is wellknown that Set-coalgebras are not semantically adequate for finitary modal logics in the sense that bisimilarity does not in general coincide with logical equivalence. Stone-coalgebras (coalgebras over the category of Stone spaces), on the other hand, do provide an adequate semantics for finitary modal logics. This leads us to study the relationship of finitary modal logics and Set-coalgebras by uncovering the relationship between Set-coalgebras and Stone-coalgebras. This builds on a long tradition in modal logic, where one studies canonical extensions of modal algebras and ultrafilter extensions of Kripke frames to account for finitary logics. Our main contributions are the generalisations of two classical theorems in modal logic to coalgebras, namely the Jónsson-Tarski theorem giving a settheoretic representation for each modal algebra and the bisimulation-somewhere-else theorem stating that two states of a coalgebra have the same (finitary modal) theory iff they are bisimilar (or behaviourally equivalent) in the ultrafilter extension of the coalgebra.

1 Introduction

To formalise transition systems as coalgebras for a functor T : Set → Set has many advantages. In particular, the theory of transition systems can be set up parametric in the ‘type’ T of the transition system and a number of techniques for coalgebras (e.g. final semantics, isomorphism theorems, final sequence, co-Birkhoff theorems) can be obtained by dualising the corresponding concepts for algebras (Rutten [18]). Unfortunately, when it comes to specification languages for coalgebras, it is more difficult to achieve results parametric in the functor T.

The idea that (variants of) modal logics are the natural logics for coalgebras goes back to Moss seminal paper [14]. Applying to modal logic dualised algebraic methods, leads to the insight that modal logic for coalgebras is dual to equational logic for algebras [11,13]. But the methods derived from this approach are adequate only for infinitary logics. This can be seen as a consequence of the fact that Set^{op} is equivalent to the category of complete atomic Boolean algebras which correspond to infinitary propositional logic in the same way as Boolean algebras capture finitary propositional logic.

⋆ Partially support by the Nuffield Foundation Grant NUF-NAL04.

Maybe for this reason, the approach towards (more realistic) finitary logics for coalgebras has been somewhat ad hoc. It essentially consisted in giving up parametricity in T and restricting attention to particular classes of functors [12,17,6]. More recently, Pattinson [15,16] has shown how these logic arise uniformly as logics given by predicate liftings. It is one of the aims of this paper to further develop this approach towards a theory of logics for coalgebras that is fully parametric in the functor T.

Another approach to finitary logics for coalgebras is to change the model theory, that is, to replace coalgebras over Set (Set-coalgebras) by coalgebras over Stone spaces (Stone-coalgebras) [10]. Stone-coalgebras generalise the so-called descriptive general frames which are known in modal logic as the standard adequate semantics for finitary modal logics. Here adequate means that the logic is sound and complete and that two states are bisimilar iff they have the same theory. The deeper reason for the adequateness of finitary modal logics and Stone-coalgebras is the duality of Boolean algebras and Stone spaces, see Johnstone [7].

In [9], we have shown that every sound logic L given by predicate liftings induces a functor L on the category BA of Boolean algebras. Using the dual equivalence of BA and the category Stone of Stone spaces, it follows that L has a ‘dual’ L^{∂} on Stone and that L^{∂}-coalgebras provide an adequate semantics for L.

The main issue of this paper can now be explained as follows: If a finitary modal logic for T -coalgebras is given by a functor L on BA, then an adequate semantics for this logic is provided by the Stone-coalgebras for the dual functor L^{∂}. The quest for a model theory of finitary modal logics for coalgebras now boils down to a comparison of T -coalgebras over Set and Stone-coalgebras for L^{∂}. This is the main theme of this paper. By building on the well-developed model theory of modal logics, where this question has been studied for the special case of Kripke frames and Kripke models, our main contribution is the generalisation of two important theorems of modal logic: The Jónsson-Tarski theorem and bisimulation-somewhere-else. The former result provides us with an completeness theorem, and the latter with a model-theoretic characterisation of logical equivalence.

Summary of Techniques: The main ingredients of our approach are depicted in the following non-commuting diagram

\xymatrix{BA \ar[rr]^{S} &  & Stone \ar[dl]^{U} \\  & Set \ar[ul]^{Q}}  (1)

The category BA of Boolean algebras is the main building block of our logics, which are obtained by ‘adding modal operators’ to BA. The category Stone of Stone spaces is our main technical tool. Stone is ‘categorically the same’ as BA in the sense that Stone is dually equivalent to BA. But, as a category of topological spaces, Stone is sufficiently Set-like to be useful in the study of Set-based coalgebras. The functor Q : Set → BA is the contravariant powerset functor mapping a set X to the algebra of predicates over X. The functor S is one part of the dual equivalence between Stone and BA and maps a Boolean algebra A to its space SA of ultrafilters giving a topological representation^{4} of A. Finally, U is the forgetful functor that maps a space to its carrier set. Note that the one traversal of this diagram, starting at BA, produces the perfect [8] or canonical extension QUS(A) for any Boolean algebra A. The traversal starting at Set produces the set of ultrafilters USQ(X) over a set X (see e.g. [3] for more information).

One of our aims is to lift these constructions to T -coalgebras, where T : Set → Set. This will be achieved by first translating a T -coalgebra to an L-algebra, for a suitable L : BA → BA, then to transport this algebra by duality to an L^{∂}-coalgebra over Stone and finally back to a T -coalgebra where we use Q, S, U to map the carriers of the respective structures.

It has been shown in [9] that any logic L for T -coalgebras (as e.g. the logics in [15,16,6,17,12]) given by predicate liftings can be described by a functor L on BA (capturing syntax and proof rules) and a natural transformation δ : LQ → QT (giving the coalgebraic semantics).

[figure: BA; S; L; Stone; U; δ : LQ → QT; Set; Q; T]  (2)

The transformation δ allows to lift Q to a functor Q̃ : Coalg(T) → Alg(L). The semantics of formulas w.r.t. to a coalgebra ξ : X → T X is given by by the unique morphism from the initial L-algebra to Q̃ξ. The initial L-algebra is commonly known as the Lindenbaum algebra of the logic L.

Summary of Results: We will show how to generalise two classic results from modal logic to coalgebras, namely the Jónsson-Tarski theorem and the bisimulation-somewhere-else result for ultrafilter extensions.

Jónsson-Tarski Theorem (Completeness). Given a modal logic described by L and δ, we extend US : BA → Set to a map ŨS̃ : Alg(L) → Coalg(T). Applying

Q̃ŨS̃ : Alg(L) → Coalg(T) → Alg(L)  (3)

to an algebra LA → A, there will be an injective L-algebra morphism

j_{A} : A → QUSA.

This is known in modal logic, in the case of Kripke frames, as the Jónsson-Tarski theorem. As a corollary, completeness of the logic w.r.t. T -coalgebras then follows because the T -coalgebra corresponding to the initial L-algebra provides a counter-model for any non-derivable formula.

4 The elements of A are represented by the clopen (closed and open) subsets of the topological space SA. ∧, ∨, ¬ in A become intersection, union and complement.

Lifting Functors from Set to Stone. We will lift a functor T : Set → Set to a functor T̂ : Stone → Stone in such a way that SQ extends to a functor

S̃Q̃ : Coalg(T) → Coalg(T̂).

T̂ will depend on a choice of logic for T, but there is a canonical such, namely the logic given by all predicate liftings for T. We show that two states in a T -coalgebra have the same theory if and only if they are bisimilar in the corresponding T̂-coalgebra.

Ultrafilter Extensions. Ultrafilter extensions are one of the central notions in the model theory of modal logics. In order to define ultrafilter extensions we need to find, for each coalgebra X → T X a suitable coalgebra USQ(X) → T (USQ(X)) where USQ : Set → Set maps a set X to the set of ultrafilters on X. We determine conditions that allow us to obtain a transformation t : UT̂ → T U, thus completing Diagram (2) to

[figure: BA; S; L; Stone; U; T̂; δ : LQ → QT; t : UT̂ → T U; Set; Q; T]  (4)

The transformation t allows to lift U to Ũ : Coalg(T̂) → Coalg(T). The ultrafilter extension of a coalgebra is then given by the composition

ŨS̃Q̃ : Coalg(T) → Alg(L) → Coalg(T̂) → Coalg(T).  (5)

Under the assumption that the transformation t above is natural, we show that two states in a T -coalgebra (X, ξ) have the same theory if and only if they are bisimilar in the ultrafilter extension ŨS̃Q̃(X, ξ). This provides a model-theoretic characterisation of logical equivalence for finitary logics.

Related Work. The first attempt of formulating a duality which accounts for an algebraic semantics of modal logic, for the special class of Kripke-polynomial functors, goes back to Jacobs [6]. Moreover, Section 5 of loc.cit. contains some material on ultrafilter extensions of coalgebras but fails to give an account of bisimilarity somewhere else, as there the function embedding a coalgebra into its ultrafilter extension is a morphism of coalgebras.

2 Preliminaries and Notation

Stone Duality. Unfortunately we have space only to indicate the most important notions. For a general introduction we refer to [7,2]. We write Set for the category of sets and functions, BA for the category of Boolean algebras and their morphisms and Stone for the category of Stone-spaces and continuous maps. The contravariant functors witnessing the dual equivalence between Set and Stone are denoted by

P : Stone → BA and S : BA → Stone where P 𝕏 is the Boolean algebra of clopen (closed and open) subsets of 𝕏 and SA is the space consisting of ultrafilters over A; on arrows, these functors act as inverse image; for more on this duality see [7]. The forgetful functors are denoted by U : Stone → Set and V : BA → Set throughout, and Q : Set → BA is the contravariant powerset functor, which is assumed to take values in BA. The composition QUS constructs the perfect [8] or canonical extension of a Boolean algebra, and we write

j_{A} : A → QUSA, a ↦ {u ∈ USA | a ∈ u}

for the canonical embedding. The fact that j_{A} : A → QUSA is an injective Boolean algebra morphism is known as Stone’s representation theorem for Boolean algebras: j_{A} represents A as an algebra of subsets where ∧, ∨, ¬ in A become intersection, union and complement. Another map which we will need throughout the paper is the map

η_{X} : X → USQX, x ↦ {Y ⊆ X | x ∈ Y }

embedding a set X into the set of ultrafilters of QX. (In fact, but we will not use this, Q and US are adjoint on the right and j and η are the (co)units of the adjunction.)

The category Stone allows familiar type constructions. For example, whereas Kripke polynomial functors (KPF) [6] on Set are given by the left-hand side below, Vietoris polynomial functors (VPF) [10] on Stone are given by the right-hand side.

T ::= Id | K | T^{I} | T +T | T ×T | P∘T T ::= Id | 𝕂 | T^{I} | T +T | T ×T | V∘T

K, 𝕂 denote constant functors, I denotes a set. P is covariant powerset and V the Stone space analogue: V𝕏 is the Stone space of closed subsets of 𝕏; the topology is generated by {{b ⊆ U𝕏 | b closed and b ⊆ a} | a clopen}.

Coalgebraic Modal Logic. (See [9] for more details). Our treatment of coalgebras and modal logic is parametric in an endofunctor Set → Set, which is denoted by T throughout. By an n-ary predicate lifting for T we mean a natural transformation λ : (2^{·})^{n} → 2^{T ·} where 2^{·} : Set → Set is contravariant powerset (note that 2^{·} = V Q). A set Λ of predicate liftings and associated arities gives rise to a functor L_{0} : Set → BA by mapping A ↦ F {[λ](a_{1}, …, a_{n}) | λ n-ary, a_{1}, …, a_{n} ∈ A}; here F : Set → BA is the functor that constructs free Boolean algebras and expressions of the form [λ](a_{1}, …, a_{n}) are understood purely syntactically. To every set of predicate liftings we associate a logic L(Λ) given by

L(Λ) ∋ φ ::= ff | φ → φ | [λ](φ_{1}, …, φ_{n}) (λ ∈ Λ n-ary)

It follows by induction that L(Λ) = ⋃_{n≥0}(UL_{0})^{n}(V F {tt, ff}) where V : BA → Set is the forgetful functor.

A modal axiom is an expression φ ↔ ψ where φ, ψ ∈ L_{0}(F X) for a denumerable set X of variables. We write A ⊢ φ if φ is derivable using propositional reasoning, congruence (if φ_{1} ↔ ψ_{1}, …, φ_{n} ↔ ψ_{n} then [λ](φ_{1}, …, φ_{n}) ↔ [λ](ψ_{1}, …, ψ_{n})) and substitution instances of axioms in A.

Given a set A of modal axioms, we define a functor L : BA → BA by LA = L_{0}UA/ ∼ where ∼ is the least equivalence relation on UL_{0}A that contains all substitution instances of axioms φ ↔ ψ ∈ A. This allows us to view syntax and proof calculus of a logic given by a set of predicate liftings and modal axioms as endofunctor L : BA → BA. Note that the n-fold application of L to the initial Boolean algebra 𝟚 yields the set

L^{n}(Λ, A) = {φ ∈ L(Λ) | rank(φ) ≤ n}/∼

where ∼ is the inter-derivability relation given by A.

For a T -coalgebra (C, γ), the semantics [[φ]]_{γ} ⊆ C of a formula is given by the inductive extension of the assignment

[[[λ](φ_{1}, …, φ_{n})]]_{γ} = γ^{−1} ∘ λ(C)([[φ_{1}]]_{γ}, …, [[φ_{n}]]_{γ})

to the whole of L(Λ). Assuming soundness of the semantics, that is A ⊢ φ ↔ ψ implies [[φ]]_{γ} = [[ψ]]_{γ} for all T -coalgebras (C, γ), we can define a natural transformation

δ_{X} : LQ(X) → QT (X)

by the inductive extension of the assignment ([λ](φ_{1}, …, φ_{n}))_{∼} ↦ λ(X)(φ_{1}, …, φ_{n}) where (·)_{∼} is the equivalence class of · by ∼.

This allows us to recast the coalgebraic semantics of L(Λ) as follows: For φ ∈ V F ({tt, ff}), [[φ]]_{γ} is given canonically; if φ ∈ (UL_{0})^{n+1}(V F ({tt, ff})) we obtain [[φ]]_{γ} = γ^{−1} ∘ δ(π(φ)) where π : L_{0}U → L takes equivalence classes. Assuming that the initial L-algebra exists, we arrive at the following compact characterisation of the coalgebraic semantics. The semantics of formulas w.r.t. to a coalgebra ξ : X → T X is given by by the unique morphism from the initial algebra LI → I

\xymatrix{I \ar[d]_{[[·]]} &  & LI \ar[ll] \ar[d]^{L[[·]]} \\ QX & QT X \ar[l]_{Qξ} & LQX \ar[l]_{δ_{X}}}  (6)

We say that two states x, y in two coalgebras are behaviourally equivalent or bisimilar if they can be identified by some coalgebra morphism. If two states are bisimilar, then they satisfy the same formulae. The converse is not true in general. This failure plays an important role in this paper.

3 Jónsson-Tarski Theorem (Completeness)

Given an algebra α : LA → A, we want to transform it to the Set-coalgebra

ŨS̃(α) = USA →^{USα} USLA →^{h_{A}} T USA.

Thinking of the elements of USLA as ultrafilters over LA, we define

h_{A} : USLA ⟶ T USA  (7)
u ↦ h_{A}(u) ∈ ⋂{δ(Lj_{A}(a)) | a ∈ u}  (8)

that is, h_{A} chooses an element in ⋂{δ(Lj_{A}(a)) | a ∈ u} for each ultrafilter u on LA. This definition is constructed in such a way that ŨS̃ preserves the semantics (compare Diagram(9) below with Diagram (6)). The notation ŨS̃ suggests that both U and S can be lifted seperately (Section 5), which is possible if h_{A} is natural. Here we neither require h_{A} to be natural nor ŨS̃ to be functorial.

Definition 1. We say that h is definable if for all algebras A and all ultrafilters u on LA we have that ⋂{δ(Lj_{A}(a)) | a ∈ u} is non-empty.

Remark 2. A necessary condition for h to be definable is that δ is injective. For suppose otherwise. Then there will be an a ∈ LA such that a ≠⊥ and δ(Lj_{A}(a)) = ∅. As a ≠⊥ we find an ultrafilter u ∈ USLA s.t. a ∈ u. But then ⋂{δ(Lj_{A}(a)) | a ∈ u} = ∅.

The essence of completeness w.r.t. to the coalgebraic semantics is that

j_{A} : A → QUSA

is an injective Alg(L)-morphism. This is known as the Jónsson-Tarski theorem. It is an extension of Stone’s representation theorem from Boolean algebras to modal algebras (ie L-algebras).

To see how completeness follows, assume that φ is not derivable and α : LA → A is the initial algebra. We have α ⊧ φ ≠ ⊤, hence Q̃ŨS̃(α) ⊧ φ ≠ ⊤ by j_{A} being an injective morphism, hence ŨS̃(α) \begin{matrix}/ \\ ⊧ \end{matrix} φ by definition of the coalgebraic semantics (see Diagram (6)), thus providing the countermodel for φ.

From Stone’s theorem, we know that j_{A} is an injective BA-morphism. To see what is needed to make j_{A} an L-algebra morphism we take a look at the following diagram.

\xymatrix{A \ar[d]_{j_{A}} &  &  & LA \ar[lll]_{α} \ar@{-->}[dll]_{j_{LA}} \ar[d]^{Lj_{A}} \\ QUSA & QUSLA \ar[l]^{QUSα} & QT USA \ar[l]^{Qh_{A}=h_{A}^{−1}} & LQUSA \ar[l]^{δ_{USA}}} (9)

The lower part, which is an L-algebra on QUSA, is obtained by transforming (A, α) into a T -coalgebra and back to an L-algebra. From the naturality of j, it follows that j_{A} is an L-algebra morphism if the triangle commutes. This leads us to

Theorem 3. Assuming that h is definable, the logic given by δ is complete w.r.t. the coalgebraic semantics.

Proof. We show that the triangle in the diagram above commutes. For b ∈ LA, let us write b̂ for j_{LA}(b) = {u ∈ USLA | b ∈ u}. Eliding subscripts, we have to show h^{−1}(δ(Lj(b))) = b̂, that is,

h(u) ∈ δ(Lj(b)) ⇔ b ∈ u.

‘⇐’ holds by definition of h. For ‘⇒’ assume b ∉ u. It follows ¬b ∈ u, hence h(u) ∈ δ(Lj(¬b)), hence h(u) ∈ ¬δ(Lj(b)), ie h(u) ∉ δ(Lj(b)).

Remark 4. The completeness proof of Jacobs [6] works essentially this way (his r is our h). Compared to the completeness proof of [9] (which mimicked the induction along the final coalgebra sequence of [15]), the Jónsson-Tarski approach to completeness is simpler as it avoids an induction along the final sequence. On the other hand not all logics admit such a completeness proof: If we take the finite powerset functor together with the standard modal logic, then h is not definable, see Example 23.

4 Lifting Functors from Set to Stone

In this section we are going to use predicate liftings to lift a functor T : Set → Set to a functor T̂ : Stone → Stone. We will give two descriptions of T̂. First, T̂𝕏 is the dual of the Boolean algebra generated by the images of the predicate liftings QU𝕏 → QT U𝕏 (Definition 7). Second, T̂ is the dual of the functor L on BA that describes the complete logic corresponding to the given predicate liftings (Remark 16).

Given a collection S of subsets of X we denote by ⟨S⟩_{BA} the subalgebra of the Boolean algebra P(X) generated by S, i.e. by closing S under taking finite unions, intersections and under complementation. We will use the following technical lemma.

Definition and Lemma 5. Given a functor F : C → Set and a functor G : C^{op} → Set such that there is a natural transformation j : G → V QF^{op}. Then we can define a functor ⟨G⟩_{BA} : C^{op} → BA by letting ⟨G⟩_{BA}X := ⟨j_{X}[GX]⟩_{BA} and ⟨G⟩_{BA}f := V QF^{op}f ↾_{⟨G⟩_{BA}Y} for arbitrary X, Y and f : X → Y ∈ C.

Proof. Using the naturality of j it is easy to show that ⟨G⟩_{BA} is well defined on objects and morphisms. Functoriality of ⟨G⟩_{BA} then follows from the functoriality of V QF^{op}.

Definition 6. Let F, G : C → Set be functors and τ : F → G a natural transformation. Then we define a functor ℑ(τ) : C → Set by ℑ(τ)(X) := τ_{X}[F X] for X ∈ C and by letting ℑ(τ)(f) to be the unique map such that the following diagram commutes

\xymatrix{F X \ar[d]^{F f} \ar@{->>}[r] & ℑ(τ)(X) \ar[d]^{ℑ(τ)(f)} \ar@{^{(}->}[r] & GX \ar[d]^{Gf} \\ F Y \ar@{->>}[r] & ℑ(τ)(Y) \ar@{^{(}->}[r] & GY}

where f : X → Y ∈ C was arbitrary.

We are now ready for the definition of a lifting of a Set-endofunctor to Stone.

Definition 7. Given T : Set → Set and a set Λ of predicate liftings λ : V Q^{n_{λ}} → V QT define

T̂ := S(⟨ℑ(τ^{Λ})⟩_{BA})

where τ^{Λ} := [(λ_{U} ∘ i^{n_{λ}})_{λ∈Λ}] : ∐_{λ∈Λ} V P^{n_{λ}} → V QT denotes the natural transformation obtained by cotupling of all the transformations λ_{U} ∘ i^{n_{λ}} and the maps i_{𝕏}^{n_{λ}} are the embeddings V P^{n_{λ}}𝕏 → V Q^{n_{λ}}U𝕏.

Proposition 8. T̂ is a functor.

Proof. Clearly τ^{Λ} = [(λ_{U} ∘ i^{n_{λ}})_{λ∈Λ}] is a natural transformation from ∐ V P^{n_{λ}} to V QT U. Therefore ℑ(τ) is a functor from Stone^{op} → Set and there is a natural transformation j : ℑ(τ) → V QT U. But then by Lemma 5 ⟨ℑ(τ)⟩_{BA} is a functor from Stone^{op} to BA. Therefore T̂ is a functor from Stone^{op} to Stone^{op} or, equivalently, T̂ : Stone → Stone.

The previous definition pre-supposes a set Λ of predicate liftings to define the lifted functor T̂ : Stone → Stone. The next proposition, which was stated in [19] and which is an instance of the Yoneda lemma, shows that there is a canonical choice for the set of liftings.

Proposition 9. There is a 1-1 correspondence

{n-ary predicate liftings λ_{X} : (2^{n})^{X} → 2^{T X}} ≅ { subsets of T (2^{n})}

given by S ⊆ T (2^{n}) ↦ λ where

λ(C) : (P_{1}, …, P_{n}) ∈ P(C)^{n} ↦ {t ∈ T C | 𝟙_{S} ∘ T ⟨𝟙_{P_{1}}, …, 𝟙_{P_{n}}⟩(t) = 1}

where, for Y ⊆ X, 𝟙_{Y} : X → 2 is the characteristic function of Y.

Given this canonical choice of liftings, it is instructive to look at some concrete examples.

Example 10. 1. Suppose T X = K is constant with some finite set K as its value. Then T̂ ≅ 𝕂 where 𝕂 is the set K with the discrete topology. To see that, note that every lifting is determined by a subset k ⊆ K, which gives rise to the algebra QK of all subsets of K, which in turn induces the lifted functor T̂𝕏 = SQK ≅ 𝕂.

2. For T X = X, i.e. T = Id, we get T̂ ≅ Id. For n = 1, we obtain a unary lifting λ_{S} for every S ⊆ 2; this gives rise to the liftings

λ_{1} = id λ_{2} = ¬ λ_{3} = tt λ_{4} = ff

where λ_{i}(C) : P(C) → P(C). One can show, that all n-ary liftings can be obtained as Boolean combinations of λ_{1}. Hence the generated Boolean algebra ⟨ℑ(τ^{Λ})⟩_{BA}𝕏 is isomorphic to P 𝕏, whence Îd ≅ Id.

3. For T X = P(X), we obtain T̂ ≅ V where V : Stone → Stone denotes the Vietoris functor. Invoking Proposition 9, we obtain 8 unary liftings of type V QC → V QT C, which are generated by Boolean combinations of □ and ◇, where □(C) : 2^{C} → 2^{T C} is given by c ↦ {d ⊆ C | d ⊆ c} and ◇ = ¬∘□∘¬. Similarly, all n-ary liftings can be defined, and one obtains that for the case T X = PX, ⟨ℑ(τ^{Λ})⟩_{BA}𝕏 is the Boolean algebra generated by {□a | a ∈ P 𝕏} ∪ {◇a | a ∈ P 𝕏} quotiented by the axioms of standard modal logic, i.e. □φ ↔ ¬◇¬φ and □(φ_{1}, …, φ_{n}) ↔ (□φ_{1} ∧ ⋯ ∧ □φ_{n}). From this it follows that T̂ ≅ V, see [10] for details.

Remark 11. It is possible to prove that ˆ · commutes with the formation of products, coproducts and the composition of functors, i.e.

{ \atop T_{1} × T_{2}} ≅ T̂_{1} × T̂_{2}, { \atop T_{1} + T_{2}} ≅ T̂_{1} + T̂_{2} and { \atop T_{1} ∘ T_{2}} ≅ T̂_{1} ∘ T̂_{2}.

Combining this fact with the above mentioned examples one can show that for every Kripke polynomial functor T the corresponding Vietoris polynomial functor is isomorphic to the functor T̂.

We will now show that we can extend the functor SQ : Set → Stone to a functor Coalg(T) → Coalg(T̂). As a first step of this construction let us see how we can transform ultrafilter of QT U𝕏 naturally into ultrafilter of ⟨ℑ(τ^{Λ})⟩_{BA}𝕏 by simply forgetting the sets in QT U𝕏 \ ⟨ℑ(τ^{Λ})⟩_{BA}𝕏.

Definition and Lemma 12. The function π̂_{𝕏} defined by

π̂_{𝕏} : SQT U𝕏 → T̂𝕏
u ↦ u ∩ (⟨ℑ(τ^{Λ})⟩_{BA}𝕏)

is well-defined and continuous. The family of functions π̂_{𝕏∈Stone} gives rise to a natural transformation π̂ : SQT U → T̂.

Proof. Let j be the natural embedding of ⟨ℑ(τ^{Λ})⟩_{BA}𝕏 into QT U𝕏. Then it is easy to see that Sj = π̂_{𝕏}. Hence π̂_{𝕏} is well defined and continuous. Naturality of π̂ then follows from the naturality of j.

With the help of π̂ we can turn T -coalgebras into T̂-coalgebras.

Definition 13. Let (X, γ) ∈ Coalg(T). Then we define a function γ̂ : SQX → T̂SQX by letting γ̂ := π̂_{SQX} ∘ SQT η_{X} ∘ SQγ.

\xymatrix{SQX \ar[r]^{SQγ} \ar[rrr]^{γ̂} & SQT X \ar[r]^{SQT η_{X}} & SQT USQX \ar[r]^{π̂_{SQX}} & T̂SQX}

The operation of turning a T -coalgebra into a T̂-coalgebra is functorial.

Proposition 14. The mapping

(X, γ) ∈ Coalg(T) ↦ (SQX, γ̂) ∈ Coalg(T̂)
f ∈ Coalg(T) ↦ SQf ∈ Coalg(T̂)

defines a functor S̃Q̃ : Coalg(T) → Coalg(T̂).

Proof. The claim follows from the fact that η and π̂ are both natural.

The semantics of the logic w.r.t. T̂-coalgebras is given by the following predicate liftings.

Definition 15. A predicate lifting λ : (V Q)^{n} → V QT for T induces a predicate lifting λ̂ : (V P)^{n} → V P T̂ for T̂ via

λ̂_{𝕏} = V k_{⟨ℑ(τ^{Λ})⟩_{BA}𝕏} ∘ λ_{U𝕏} ∘ i_{𝕏}^{n}

where i_{𝕏}^{n} : (V P 𝕏)^{n} → (V QU𝕏)^{n} and k_{⟨ℑ(τ^{Λ})⟩_{BA}𝕏} : ⟨ℑ(τ^{Λ})⟩_{BA}𝕏 → P S⟨ℑ(τ^{Λ})⟩_{BA}𝕏 is the isomorphism given by Stone duality.

Remark 16. T̂ can be described more abstractly. Let δ′ : L′Q → QT describe the semantics of the logic L given as above by predicate liftings (and no axioms). We can define ‘an improved version’ L of L′ ‘with axioms’ by factoring L′A → LQUSA → QT USA through its image as L′A ↠ LA ↪ QT USA. One then shows the following.

1. L is a functor.

2. LQX is obtained by factoring δ′ : L′QX → QT X through its image. The image δ_{X} : LQX → T QX gives the interpretation of L w.r.t. T -coalgebras whereas, intuitively, the quotient L′QX → LQX describes the axioms added to L. That δ is injective corresponds to the completeness of the logic described by L, see [9].

3. L is dual to T̂, that is, there is an isomorphism SL → T̂S, or, equivalently, δ̂ : LP → P T̂. The iso δ̂ gives a T̂-coalgebra semantics to the logic L which agrees with the one from Definition 15.

4. The functor S̃Q̃ : Coalg(T) → Coalg(T̂) can now be described as mapping X →

T X to SQX → SQT X ⟶^{Sδ_{X}} SLQX →^{≅} T̂SQX.

Proposition 17. 1. Consider a state x of a T -coalgebra and the state η_{X}(x) in the

corresponding T̂-coalgebra. x and η_{X}(x) have the same theory.

2. Two states of a T̂-coalgebra are bisimilar iff they have the same theory.

Proof. 1. Let ι : LI → L be the initial L-algebra and φ ∈ I. The semantics of φ w.r.t. a coalgebra X → T X and its ultrafilter extension SQX → T̂SQX is given by the initial algebra maps as in the following diagram (see Remark 16).

\xymatrix{I \ar[d]^{[[·]]_{Set}} \ar[dd]_{[[·]]_{Stone}} &  &  &  & LI \ar[llll]_{ι} \ar[d]_{L[[·]]_{Set}} \ar[dd]^{L[[·]]_{Stone}} \\ QX \ar[d]^{≅} & QT X \ar[l] \ar[d]^{≅} &  &  & LQX \ar[lll]_{δ_{X}} \ar[d]_{≅} \\ P SQX & P SQT X \ar[l] & P SLQX \ar[l]_{P Sδ_{X}} & P T̂SQX \ar[l]_{≅} & LP SQX \ar[l]_{≅}}

The left column means that u ∈ [[φ]]_{Stone} iff [[φ]]_{Set} ∈ u (note the similarity with the truth lemma of the canonical model known in modal logic). This implies the claim.

2. This follows from T̂ being dual to L.

The following corollary reconciles logical equivalence and bisimilarity. Although two logically equivalent states in a Set-coalgebra may fail to be bisimilar, they will be bisimilar in the corresponding Stone-coalgebra:

Theorem 18. Given T : Set → Set and a logic L for T -coalgebras, let T̂ : Stone → Stone be the lifted functor. Then, given (X, γ) ∈ Coalg(T) and x, y ∈ X, we have that x and y have the same theory iff η_{X}(x) is bisimilar to η_{X}(y) in S̃Q̃(X, γ).

5 The Ultrafilter Extension of a Coalgebra

In this section we define Ũ, thus lifting Diagram (1) to algebras and coalgebras^{5}

\xymatrix{Alg(L) \ar[rr]^{S̃} &  & Coalg(T̂) \ar@{-->}[dl]^{Ũ} \\  & Coalg(T) \ar@{-->}[ul]^{Q̃}}  (10)

ŨS̃Q̃(X →^{ξ} T X) will be the ultrafilter extension of ξ. Although SQ is left-adjoint to U, this will not hold in general for the lifted functors. The reason is that the unit η_{X} : X → USQX may fail to be a coalgebra morphism. This is the observation that gives rise to Theorem 27.

We need a transformation t : UT̂ → T U. This can be done if ultrafilters in T̂ have non-empty intersection, that is, if for all Stone spaces 𝕏 and all ultrafilters u ∈ UT̂𝕏 we have ⋂ u ≠ ∅. We then define

t_{𝕏} : UT̂𝕏 → T U𝕏
u ↦ t_{𝕏}(u) ∈ ⋂ u

Remark 19. Using T̂S ≅ SL, we see that t_{𝕏} appeared already as h_{P 𝕏} in (7). Similarly, h_{A} is t_{SA}. Note that naturality was not required in Section 3.

Under the assumption that t is natural, we can now lift U : Stone → Set to a functor

Ũ : Coalg(T̂) → Coalg(T)

mapping ξ : 𝕏 → T̂𝕏 to U𝕏 →^{Uξ} ÛT 𝕏 →^{t_{𝕏}} T U𝕏. In the following proposition we prove two useful properties of t.

Proposition 20. For all 𝕏 ∈ Stone let t_{𝕏} be defined as above. Then

1. t_{𝕏} is injective for all 𝕏.

2. If for all 𝕏 and for all u ∈ UT̂𝕏 we have that ⋂ u is a singleton set, then t is a natural transformation.

Proof. The first item follows from the fact that for two ultrafilters u ≠ u′ we always have ⋂ u ∩ ⋂ u′ = ∅. To prove that t is natural we have to show that T Uf ∘ t_{𝕏} = t_{𝕐} ∘ UT̂f for some arbitrary f : 𝕏 → 𝕐. Let u ∈ UT̂X. Then

t_{𝕐}(UT̂f(u)) = t_{𝕐}((T Uf^{−1})^{−1}(u)) = F
⇔ F ∈ ⋂(T Uf^{−1})^{−1}(u) = (T Uf^{−1})^{−1}(F′)
for the F′such that (⋂ u) = {F′}
⇔ F = T Uf[F′] ⇔ T Uf(t_{𝕏}(u)) = F.

5 S̃(LA → A) = SA → SLA ≅ T̂SA, see Remark 16.3.

Kripke polynomial functors fulfill this criterion, for example:

Example 21. Let T = P and Λ the canonical set of liftings. Then it is easy to see that ⟨ℑ(τ^{Λ})⟩_{BA}𝕏 = P V𝕏 and therefore we have for all u ∈ UT̂𝕏 = S(⟨ℑ(τ^{Λ})⟩_{BA}𝕏) that ⋂ u = {F } for some F ∈ V𝕏 by Stone duality. Therefore t is natural according to Proposition 20. The reader is invited to check that in fact V𝕏 = (ℑ(t)𝕏, τ_{t}) where ℑ(t) is defined as in 6 and τ is the quotient topology induced by t_{𝕏}. Therefore our definition of an ultrafilter extension for P-coalgebras coincides with the one used in modal logic.

Remark 22. The construction sketched in the example works also for other functors: If t is natural, the mapping T̄ : Stone → Stone, 𝕏 ↦ (ℑ(t)𝕏, τ_{t}), can be extended to a functor with the property that T̂ ≅ T̄ and that UT̄𝕏 ⊆ T U𝕏 for all 𝕏. We can then use the inclusion UT̄𝕏 ⊆ T U𝕏 which simply forgets the topology in place of the t-map to define the ultrafilter extension. This works in particular for a KPF T where we get that T̄ is equal to the corresponding VPF.

There are also functors for which we cannot define an ultrafilter extension.

Example 23. Let T = P_{ω} and Λ = {◇} where P_{ω} denotes the finite power set functor and ◇(Y) := {Y′ | Y′ is finite and Y′ ∩ Y ≠ ∅}. Then t cannot be defined in general. For a counterexample consider 𝕏 = (ω ∪ {∗}, τ) where τ is generated by the Boolean set algebra of all finite subsets of ω and all cofinite subsets of ω ∪ {∗} that contain ∗. Then 𝕏 is a Stone space. If we define U := {◇({n}) | n ∈ ω} ⊆ ⟨ℑ(τ^{Λ})⟩_{BA}𝕏 one can easily check that U has the finite intersection property. Therefore we can extend U to an ultrafilter u ∈ UP̂_{ω}𝕏. But obviously ⋂ U = ∅ and hence also ⋂ u = ∅.

Of course, finitely branching Kripke frames, ie coalgebras for P_{ω}, do have ultrafilter extensions. The point of the example above is that these ultrafilter extensions are Pcoalgebras but not P_{ω}-coalgebras.

The important property we need is that t preserves the semantics. The semantics of the logic w.r.t. T̂-coalgebras was given in Definition 15 and Remark 16.3.

Proposition 24. t : UT̂ → T U preserves the semantics. That is, the subsets of U𝕏 determined by interpreting a formula on ξ : 𝕏 → T̂𝕏 and on t_{𝕏} ∘ Uξ : U𝕏 → T U𝕏 are identical.

Proof. The claim is proven by induction on the structure of formulas. We only provide the inductive step for formulas of the form [λ]φ. Let x ∈ X and ψ = [λ]φ, then

x ∈ [[ψ]]_{t_{𝕏}∘Uξ} ⇔ x ∈ (t_{𝕏} ∘ Uξ)^{−1}(λ_{U𝕏}([[φ]]_{t_{𝕏}∘Uξ})) {I.H. \atop ⇔} x ∈ (t_{𝕏} ∘ Uξ)^{−1}(λ_{U𝕏}([[φ]]_{ξ}))
⇔^{(∗)} x ∈ Uξ^{−1} ({u ∈ UT̂𝕏 | ⋂ u ⊆ λ_{U𝕏}([[φ]]_{ξ})})
⇔ x ∈ Uξ^{−1} ({u ∈ UT̂𝕏 | λ_{U𝕏}([[φ]]_{ξ}) ∈ u}) = Uξ^{−1} (λ̂_{𝕏}([[φ]]_{ξ}))
⇔ x ∈ [[ψ]]_{ξ},

where the ⇒-part of (∗) is true because

⋂ u ⊈ λ_{U𝕏}([[φ]]_{ξ}) ⇒ λ_{U𝕏}([[φ]]_{ξ}) ∉ u ⇒ −λ_{U𝕏}([[φ]]_{ξ}) ∈ u ⇒ ⋂ u ⊆ −λ_{U𝕏}([[φ]]_{ξ}).

Remark 25. That t preserves the semantics means that the left-hand column of the diagram

\xymatrix{I \ar[d]^{[[·]]_{ξ}} \ar[dd]_{[[·]]_{t_{𝕏}∘Uξ}} &  &  & LI \ar[lll]_{ι} \ar[d]_{L[[·]]_{ξ}} \ar[dd]^{L([[·]]_{t_{𝕏}∘Uξ)}} \\ P 𝕏 \ar@{^{(}->}[d] & P T̂𝕏 \ar[l] \ar[d] &  & LP 𝕏 \ar[ll]_{δ̂_{𝕏}} \ar[d] \\ QU𝕏 & QUT̂𝕏 \ar[l] & QT U𝕏 \ar[l]_{Qt_{𝕏}} & LQU𝕏 \ar[l]_{δ_{U𝕏}}}

commutes. We can therefore allow as transformation t : UT̂ → T U any transformation making the lower right square commute, or, redrawing it a bit, making the following commute.

\xymatrix{LQU𝕏 \ar[rr]^{δ_{U𝕏}} &  & QT U𝕏 \ar[d]^{Qt_{𝕏}} \\ LP 𝕏 \ar[r]_{≅} \ar[u] & P T̂𝕏 \ar[r] & QUT̂𝕏}  (11)

This diagram appeared already as the upper square of Diagram (9), compare Remark 19.

Proposition 26. Assume that t is natural. Then Stone-bisimilarity equals Set-bisimilarity. That is, two states in ξ : 𝕏 → T̂𝕏 are bisimilar iff they are bisimilar in Ũξ.

Proof. ⊆ follows from t being natural. ⊇: If two states in Ũξ are bisimilar than they have the same theory. Now apply Propositions 24 and 17.2.

We can now improve on the bisimulation-somewhere-else result of Theorem 18. Together with the proposition above, it implies that two states in X → T X that have the same theory are in fact bisimilar in some other Set-coalgebra, namely the ultrafilter extension of X → T X.

Theorem 27. Given T : Set → Set and a logic L for T -coalgebras, let T̂ : Stone → Stone be the lifted functor. Assume that ultrafilters in T̂ have non-empty intersection and that t : UT̂ → T U is natural. Then, given (X, γ) ∈ Coalg(T) and x, y ∈ X, we have that x and y have the same theory iff η_{X}(x) is bisimilar to η_{X}(y) in ŨS̃Q̃(X, γ).

Remark 28. The assumption on T̂ and t is satisfied for all Kripke polynomial functors.

6 Conclusion and Future Work

The focus of this paper was on the relationship between Stone-coalgebras and Setcoalgebras. This is a special instance of a more general phenomenon in computer science where topology-based structures and set-based structures interact. This was observed already in Abramsky [1] where powerdomain-coalgebras and powerset-coalgebras were compared. We believe that the methods used here will generalise to other such situations.

First, we can treat other logics than classical ones by replacing the duality between BA and Stone by one for, e.g. Heyting algebras or distributive lattices. Infinitary logics can be treated as well, see e.g. [4]. Second, we can replace Set by other categories of interest in semantics. Third, we can make algebraic tools available by upgrading the triangle of Diagram (1) to a square where Set is now accompanied by its dual category of complete atomic Boolean algebras. This will enable the use of methods developed in the study of perfect or canonical extensions of Boolean algebras (see e.g. [20, Section 7]).

There are also a number of more immediate open questions. Formulate a finitary definability result for classes of coalgebras in the style of Goldblatt-Thomason [5], based on ultrafilter extensions. If T preserves finite sets than it has a canonical lifting to from Set to Stone; show that then this lifting agrees with T̂. Find nice conditions guaranteeing that ultrafilters in T̂ have non-empty intersection.

References

1. S. Abramsky. A domain equation for bisimulation. Information and Computation, 92, 1991.

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

3. P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. CSLI, 2001.

4. M. Bonsangue and A. Kurz. Duality for logics of transition systems. In V. Sassone, editor, FoSSaCS’05, volume 3441 of LNCS, 2005.

5. R. Goldblatt. Metamathematics of modal logic I. Reports on Mathematical Logic, 6, 1976.

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

7. P. Johnstone. Stone Spaces. Cambridge University Press, 1982.

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

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

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

11. A. Kurz. A co-variety-theorem for modal logic. In Advances in Modal Logic 2. CSLI, 2001. Selected Papers from AiML 2, Uppsala, 1998.

12. A. Kurz. Specifying coalgebras with modal logic. Theoret. Comput. Sci., 260, 2001. Earlier version appeared in the Proceedings of CMCS’98, ENTCS, Vol. 11, 1998.

13. A. Kurz and J. Rosický. Operations and equations for coalgebras. Math. Structures Comput. Sci., 15, 2005.

14. L. Moss. Coalgebraic logic. Annals of Pure and Applied Logic, 96, 1999.

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

16. D. Pattinson. Expressive logics for coalgebras via terminal sequence induction. Notre Dame Journal of Formal Logic, 45, 2004.

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

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

19. L. Schroeder. Expressivity of Coalgebraic Modal Logic: The Limits and Beyond. In V. Sassone, editor, FoSSaCS’05, volume 3441 of LNCS, 2005.

20. Y. Venema. Handbook of Modal Logic, chapter Algebras and Coalgebras. To appear. Electronically available.