                         CMCS’04 Preliminary Version

Algebraic Semantics for Coalgebraic Logics

Clemens Kupke^{a} Alexander Kurz^{b,1} Dirk Pattinson^{c}

a CWI/Universiteit van Amsterdam b University of Leicester c LMU München

Abstract With coalgebras usually being defined in terms of an endofunctor T on sets, this paper shows that modal logics for T -coalgebras can be naturally described as functors L on boolean algebras. Building on this idea, we study soundness, completeness and expressiveness of coalgebraic logics from the perspective of duality theory. That is, given a logic L for coalgebras of an endofunctor T, we construct an endofunctor L such that L-algebras provide a sound and complete (algebraic) semantics of the logic. We show that if L is dual to T, then soundness and completeness of the algebraic semantics immediately yield the corresponding property of the coalgebraic semantics. We conclude by characterising duality between L and T in terms of the axioms of L. This provides a criterion for proving concretely given logics to be sound, complete and expressive.

1 Introduction

Coalgebras have been recognised as models for a large variety of state based systems (see [18] for an overview). The coalgebraic approach to state based systems calls for a general logical framework, where one can describe and reason about properties of state based systems. This question has been addressed in [14,9,17,12,15]. These investigations are specific to coalgebras on the category of sets and use techniques from modal logic to relate syntactic derivability and semantic validity, notably (variations of) the canonical model construction. The observation that descriptive general frames are in 1-1 correspondence to coalgebras for the Vietoris-functor on the category of Stone spaces (see [11]) opens new (algebraic) ways for showing soundness and completeness for certain modal logics over coalgebras: we set up a duality between coalgebras for an endofunctor on Stone spaces and algebras containing the boolean signature. This is similar in spirit to the work of Goldblatt [6],

1 Partially supported by NWO/British Council.

This is a preliminary version. The final version will be published in Electronic Notes in Theoretical Computer Science

                       URL: www.elsevier.nl/locate/entcs

Kupke and Kurz and Pattinson

where the duality between descriptive general frames and boolean algebras with operators is discussed; as it has been shown in [11] this can also be seen as a duality of functors: Given an endofunctor T (on Stone spaces) and a logic for T -coalgebras, we devise a functor L (on boolean algebras). Viewing formulas of the logic as algebraic terms, the category of L-algebras provides a sound and and complete semantics of the logic.

We give conditions which allow to transfer soundness and completeness of the coalgebraic semantics from the corresponding property of the algebraic semantics. If in particular L is dual to T, it follows that the coalgebraic semantics is both sound and complete, and moreover the logic is strong enough to distinguish non-bisimilar points.

In the second part of the paper, we analyse the duality between L and T in logical terms. Our main result characterises this duality in terms of the axioms and modal operators of the logic: We show that L is dual to T, if the axioms are sound, complete and the modal operators are strong enough to distinguish successor states.

2 Preliminaries and Notation

2.1 Algebras and Propositional Logic

For a signature Σ and a set E of equations, we write Alg(Σ, E) for the category of Σ-algebras which satisfy all equations in E. We abbreviate Alg(Σ, ∅) by Alg(Σ) and write BA = Alg(Σ_{BA}, E_{BA}) for the category of boolean algebras. Boolean operators are denoted by ⊥, ⊤, ¬, ∧, →, ↔ and U : BA → Set is the forgetful functor, with left adjoint F.

Algebras can be represented by generators and relations, or formulas and logical equivalence. For our work, the following notions are convenient.

Definition 2.1 (i) A pre-boolean algebra is a Σ_{BA}-algebra. (ii) A boolean preorder (A, ⊢) is a pre-boolean algebra A and a relation ⊢ on A which is closed under the rules and axioms of propositional logic. A morphism of boolean preorders is an order-preserving Σ_{BA}- algebra morphism. (iii) A boolean congruence (A, ≡) is an algebra A for the signature Σ_{BA} and a congruence relation ≡ on A such that A/≡ is a boolean algebra. A morphism f : (A, ≡_{A}) → (B, ≡_{B}) of boolean congruences is a Σ_{BA}-morphism f : A → B such that f(a) ≡_{B} f(a′) whenever a ≡_{A} a′.

The induced categories of boolean congruences and boolean preorders are denoted by Cong_{BA} and PreOrd_{BA}.

Boolean preorders are essentially the same as boolean congruences. Indeed, given (A, ⊢) define ≡ via a ∧ b ≡ a ⇔ a ⊢ b. Conversely, given a congruence ≡ on a pre-boolean algebra A, define a ⊢_{A} b ⇔ a → b ≡ ⊤.

On morphisms, the correspondence between boolean preorders and boolean congruences is described by the following lemma.

Lemma 2.2 The category of boolean preorders is isomorphic to the category of boolean congruences. The isomorphism restricts to the subcategory of boolean preorders and order reflecting morphisms and the subcategory of boolean congruences and those morphisms f : (A, ≡) → (A′, ≡′) for which f̄: A/≡ → A′/≡′ is injective, where f̄([a]) = [f(a)].

Proof We use the notation of the discussion preceding the lemma and [·] to denote equivalence classes. The first claim is immediate. For the second, suppose f is order preserving and reflecting and f̄([a]) = f̄([b]). Then f(a) ≡′ f(b). Since f is order preserving and reflecting it follows a ≡ b, ie, [a] = [b], showing that f̄ is injective. Conversely, assume f(a) ⊢′ f(b). Then f(a) ∧ f(b) ≡′ f(a), i.e. f̄([a] ∧ [b]) = f̄([a]). Since f̄ is injective, [a] ∧ [b] = [a] and therefore a ∧ b ≡ a, i.e. a ⊢ b. □

We will need the following corollary in Section 6.

Corollary 2.3 Let (A, ⊢) be a boolean preorder, B a boolean algebra and d : A → B a pre-boolean algebra morphism and let d̄ be the relation given by

A  ^{d} A/≡ _{d̄} B.

Then d̄ is a boolean algebra morphism iff d is order preserving and d̄ is an injective boolean algebra morphism iff d is order preserving and reflecting.

If V is a set (of variables, or constants) and Σ is a signature, then T_{Σ}(V) denotes the set of terms with variables in V. We frequently consider extensions of Σ_{BA} by a set Λ of unary operation symbols; the extended signature is denoted by Σ_{BA}^{Λ}. By an equation, we mean a pair of terms and write s = t for the equation (s, t); this allows us to consider a relation on a set of variables as a set of equations.

Given a set Ax of equations for the signature Σ_{BA}^{Λ}, and two terms s, t ∈ T_{Σ}(V), we write Ax ⊢_{EL}^{V} s = t if s = t can be equationally derived from Ax and the boolean equations E_{BA}. Since we work with languages over different sets of equations in the sequel, we make this distinction explicit in the notation. In case V = ∅, we write ⊢_{EL} instead of ⊢_{EL}^{∅}.

In the context of boolean congruences, A is typically a set of formulas and ≡ a relation of logical equivalence. We use boolean congruences to present boolean algebras. A presentation q : (Φ, R) → A of a boolean algebra A consists of a boolean congruence (Φ, R) and a surjective Σ_{BA}-morphism q whose kernel is R. Note that every boolean algebra has a presentation, namely the counit ε_{A} : (UF UA, Diag(A)) → A of the adjunction F ⊣ U where Diag(A), the diagram of A, is the kernel of ε_{A}.^{2}

2 UF UA is the set of all boolean terms that can be formed from elements in A; Diag(A) records which of these expressions are equivalent. For example, if A = P({a, b, c}), then ({a} ∧ {b}, ⊥) is in Diag(A).

We will need two facts about presentations. The first states that we can do derivations with representatives of equivalence classes.

Proposition 2.4 Consider a presentation q : (Φ, R) → A. Let φ_{i}, ψ_{j} ∈ Φ and Ax, t = s equations for Σ_{BA}^{Λ}. Then

Ax ∪ R ⊢_{EL}^{Φ} t(φ_{i}) = s(ψ_{j}) ⇔ Ax ∪ Diag(A) ⊢_{EL}^{UA} t(q(φ_{i})) = s(q(ψ_{j})).

The second fact expresses that derivations in presentations are preserved by morphisms and reflected by injective morphisms.

Proposition 2.5 Consider presentations q : (Φ, R) → A, q′ : (Φ′, R′) → A′ and a boolean algebra morphism f : A → A′. Let a_{i}, b_{j} ∈ A and Ax, t = s equations for Σ_{BA}^{Λ}. Then (eliding the maps q, q′)

Ax ∪ R ⊢_{EL}^{UA} t(a_{i}) = s(b_{j}) ⇔ Ax ∪ R′ ⊢_{EL}^{UA′} t(f(a_{i})) = s(f(b_{j})).

2.2 Coalgebras, Terminal Sequence, Behavioural Equivalence

In the whole paper, Set denotes the category of sets and functions, Stone is the category of Stone spaces and continuous maps. Since the development in this paper can be instantiated to both coalgebras over set and coalgebras over Stone spaces, we develop the theory for both cases simultaneously. The essential ingredient is a functor which assigns boolean algebras to objects of the base category. In the case of sets, this is the contravariant power set functor P̌; for stone spaces we use Clp : Stone^{op} → Set, which maps a stone space to the boolean algebra of its clopen (closed and open) subsets. Our assumptions can be summarised as follows: Convention 1 X is a category equipped with a forgetful (i.e. faithful) functor U_{X} : X → Set and P : X^{op} → BA such that P X ⊆ P(U_{X} X) is a subalgebra of the powerset of U_{X} X. We assume that X has a final object 1 which is mapped by P : X^{op} → BA to the initial boolean algebra 𝟚. Finally, T : X → X denotes an endofunctor such that T 1 has a global element.

Note that the above assumptions are satisfies for both Set and Stone, the two categories our approach is principally targeted at. For both Set and Stone the existence of a global element of T 1 means that T is non-trivial, that is, there is an object which is not mapped to the empty set / the trivial space. Assuming that X comes with a forgetful functor to the category of sets essentially says that objects X ∈ X have elements. This is reflected in our notation by writing x ∈ X for x ∈ U_{X} X.

Definition 2.6 A T -coalgebra is a pair (X, ξ), where X ∈ X and ξ : X → T X. Morphisms of coalgebras (X, ξ) to (Y, χ) are maps f : X → Y ∈ X for which χ ∘ f = T f ∘ ξ.

One of the main motivating example of this study is that Kripke models and Kripke frames naturally arise as coalgebras, for a specific endofunctor.

We write P for the covariant powerset functor on the category of sets:

Example 2.7 (i) Kripke Frames are in 1-1 correspondence with P-coalgebras. (ii) The analogue of the powerset functor for Stone spaces is the Vietoris functor V : Stone → Stone mapping X to the set K(X) of closed subsets. The V-coalgebras are known as descriptive general frames in modal logic, see [11]. (iii) Kripke models over a set A of propositions are coalgebras for T X = P(X) × P(A).

Dually to the construction of initial and free algebras as colimits of the initial sequence of the underlying endofunctor, the notion of terminal sequence plays an important role in the coalgebraic framework. For our purposes, it is sufficient to consider the finitary part, that is, the first ω elements of the terminal sequence. For the whole story, and a precise account of how the terminal sequence can be used to construct cofree coalgebras, we refer to Worrell [19]. The finitary part of the terminal sequence (we allow ourselves to drop the words “finitary part of” from now on) consists of

(i) the sequence (T_{n})_{n∈ω} of objects, where T_{0} = 1 and T_{n+1} = T T_{n}, and (ii) the sequence of morphisms (p_{m}^{n})_{m≤n∈ω} where p_{m}^{n} : T_{n} → T_{m} are such that p_{n}^{n} = id_{T_{n}} and p_{k}^{m} ∘ p_{m}^{n} = p_{k}^{n} for all k ≤ m ≤ n ∈ ω.

In a logical context, the object T_{n} corresponds to the behaviour which can be described with a formula of rank n, where the rank of a formula is the maximal nesting depth of modal operators.

The link between the terminal sequence and arbitrary coalgebras is the observation, that every T -coalgebra (X, ξ) appears as a cone (X, (ξ_{n})_{n∈ω}) over the terminal sequence associated with T as follows: take ξ_{0} : X → 1 to be the morphism induced by finality of 1 and put ξ_{n+1} = T ξ_{n} ∘ ξ for n ∈ ω.

Since we have assumed that X is a concrete category (i.e. comes equipped with a forgetful functor to Set), we can speak about points x ∈ X realising some behaviour (element of T_{n}).

Proposition 2.8 For all t in T_{n} there is a T -coalgebra (X, ξ) and x in X such that ξ_{n}(x) = t.

Proof Pick a global element e : 1 → T 1 and put e_{n} = T^{n}(e). Then (T_{n}, e_{n}) realises the behaviours in T_{n}. □

Furthermore, the presence of elements also allows us to speak about behavioural equivalence in the same way as in the category of sets.

Definition 2.9 Suppose (X, ξ) and (Y, ϱ) ∈ Coalg(T) and (x, y) ∈ X × Y.

(i) We say that x and y are behaviourally equivalent (denoted x ≃ y) if there is (Z, ζ) ∈ Coalg(T) and two morphisms f : (X, ξ) → (Z, ζ) and (Y, ϱ) → (Z, ζ) such that U_{X} (f)(x) = U_{X} (f)(y). (ii) We say that x and y are ω-step equivalent (denoted x ≃_{ω} y) if ξ_{n}(x) = ϱ_{n}(y) for all n ∈ ω.

That is to say that two points are behaviourally equivalent if they can be identified by a coalgebra morphism, and ω-step equivalent if their behaviour agrees for all transition sequences of finite length. It is easy to show that ω-step equivalence is a consequence of behavioural equivalence. One aspect of coalgebraic logics is their expressivity, that is, their ability to distinguish non-bisimilar points.

Definition 2.10 Suppose L is a set (of formulas) and ⊧_{(C,γ)}⊆ C × L is a (satisfaction) relation for every (C, γ) ∈ Coalg(T). Write Th(c) = {φ ∈ L | c ⊧_{(C,γ)} φ}.

(i) L is expressive, if x ≃ y whenever Th(x) = Th(y), for all (X, ξ) and (Y, ϱ) ∈ Coalg(T) and (x, y) ∈ X × Y. (ii) L is ω-step expressive, if x ≃_{ω} y whenever Th(x) = Th(y), for all (X, ξ), (Y, ϱ) ∈ Coalg(T) and (x, y) ∈ X × Y.

In general, for formulas of finitary logics, ω-step expressiveness is the best we can hope for (see [13]).

3 Coalgebraic Modal Logic

The logics under consideration in this paper are parametric in a set of modal operators, which are interpreted using predicate liftings. Intuitively, predicate liftings map properties of states to properties of successor states, and hence allow us to make assertions about state transitions. The formal definition is as follows:

Definition 3.1 A predicate lifting for T is a natural transformation λ : UP → UP T.

The functor U appears because we do not require predicate liftings to preserve boolean structure (the □ of modal logic, for example, preserves meets but not joins).

Example 3.2 (i) Consider X = Set and T X = P(X). Then T -coalgebras are Kripke frames. The predicate lifting for the □-operator of modal logic is given by the natural transformation (λ_{□})_{X} : P̌X → P̌T X, a ⊆ X ↦ {b ⊆ X | b ⊆ a}. (ii) Consider X = Stone and let X be a Stone space with topology O(X) and the Vietoris functor V : Stone → Stone from Example 2.7. The predicate lifting for the □-operator is given by (λ_{□})_{X} : UClpX → UClpVX, a ↦ {b ∈ K(X) | b ⊆ a}.

The language of the modal logics we work with is built by adding a unary modal operator for each lifting. The restriction to unary modalities is mainly for convenience; our results easily extend to the case of modalities of arbitrary (finite) arities.

We now turn to the syntax and the semantics of the modal logics we are going to work with.

Definition 3.3 (Syntax and semantics of L(Λ)) Given a set Λ of predicate liftings, the language L(Λ) is given by the grammar

L(Λ) ∋ φ, ψ ::= ff | φ → ψ | [λ]φ

where λ ∈ Λ. For a structure (X, ξ) ∈ Coalg(T), the semantics [[φ]] = [[φ]]_{ξ} ∈ UP X of formulas φ ∈ L(Λ) is given by

[[ff]] =⊥ [[φ → ψ]] = [[φ]] → [[ψ]] [[[λ]φ]] = UP (ξ) ∘ λ_{X}([[φ]]).

We write (X, ξ) ⊧ φ for [[φ]]_{ξ} = ⊤ and Coalg(T) ⊧ φ for (X, ξ) ⊧ φ for all (X, ξ) ∈ Coalg(T).

Note that L(Λ) = T_{Σ_{BA}^{Λ}}, that is, every modal formula φ ∈ L(Λ) is a term without free variables over the signature Σ_{BA}^{Λ}.

Example 3.4 If T is P or V and Λ = {λ_{□}} as in Example 3.2, then L(Λ) gives basic modal logic if we identify [λ_{□}] with □.

Many proofs in modal logic run by induction on the depth of formulas. The semantics of a formula of depth n can be described by a predicate over T_{n}, the n-th element of the terminal sequence.

Definition 3.5 (Lift, Form_{n}, d_{n}) For a given functor T and a set of predicate liftings Λ, let Lift : Set → Set be the operation that maps a set Φ (of formulas) to Lift(Φ) according to the grammar

Lift(Φ) ∋ φ, ψ ::= ff | φ → ψ | [λ]ϱ

where λ ∈ Λ and ϱ ∈ Φ. For maps d : Φ → UP X we put

Lift(d) : Lift(Φ) → UP T X, [λ]ϱ ↦ λ_{X} ∘ d(ϱ)

and extend to the whole of Lift(Φ) inductively. We put Form_{0} = Lift(∅) and Form_{n+1} = Lift(Form_{n}) and call the elements of Form_{n} the formulas of depth n of L(Λ). Their semantics

d_{n} : Form_{n} → UP T_{n}

is given by d_{0} : Form_{0} → UP 1 (giving propositional formulae their usual interpretation in the Boolean algebra UP 1 = 𝟚) and d_{n+1} = Lift(d_{n}). The set ⋃_{n<ω} Form_{n} is denoted by Form_{ω}.

Since we have assumed that all predicate liftings are unary (hence finitary) from the outset, we know that L can be covered by the sets Form_{n}, for n ∈ ω:

Lemma 3.6 L = ⋃_{n∈ω} Form_{n}.

Viewing coalgebras as cones over the terminal sequence associated with T, we can recover the semantics of formulas as follows:

Proposition 3.7 Let φ be a formula of depth n. Then [[φ]]_{ξ} = P (ξ_{n})(d_{n}(φ)).

In order to capture the specific structure of a given functor T, we introduce axiom schemas. Our axioms are pairs (φ, ψ), which we read as φ ↔ ψ in the context of modal logic and as φ = ψ in an equational context. The notion of axiom as a pair enables us to use them in both settings. The key property of axioms is that they are of rank one, that is, they don’t contain nested modalities. This feature enables us to lift the axioms along the terminal sequence. Recall that, given a set V (of variables), UF V is the closure of V under boolean operations.

Definition 3.8 (Axioms) Given a set Λ of predicate liftings for T and a set (of variables) V, an axiom is a pair (φ, ψ) with φ, ψ ∈ Lift(UF V). In the following we will write axioms (φ, ψ) as equations φ = ψ.

The basic calculus for modal logic can be seen as a special example:

Example 3.9 If T is P or V and Λ = {λ_{□}} as in previous examples, then V = {p, q} and Ax = {□⊤ = ⊤, □(p ∧ q) = □p ∧ □q} give the basic calculus for modal logic which is sound and complete for P-coalgebras.

We only consider axioms of such restricted shape because they are enough to describe the functor T (or its dual), or, in other words, the class of all T - coalgebras. Specific subclasses of T -coalgebras can then be specified by adding additional axioms of unrestricted shape (possibly involving fixpoint operators as in the μ-calculus).

Considering Λ as a set of (unary) operation symbols, we may identify formulas of L(Λ) with terms for the signature Σ_{BA}^{Λ} (see Section 2.1). A modal formula φ can then be seen as the equation φ = ⊤ and every equation φ = ψ can be seen as the formula φ ↔ ψ.

In order to relate algebraic and coalgebraic semantics for modal logics, we begin by (defining and) relating the corresponding proof calculi. Note that axioms may contain variables. Since formulas of L(Λ) do not have free variables, we use ground substitutions, i.e. substitutions which assign a variable free formula to every variable. If σ is a substitution, the result of substituting every variable x by σ(x) in a term (or formula) φ is denoted by σ(φ).

Definition 3.10 (Entailment in Modal Logic) Suppose Ax is a set of axioms. We say that φ is modally derivable from Ax (Ax ⊢_{ML} φ), if φ is contained in the least set Φ of formulas which

• contains σ(φ) ↔ σ(ψ) whenever σ is a ground substitution and (φ, ψ) ∈ Ax • is closed under propositional entailment

• contains [λ]φ ↔ [λ]ψ whenever λ ∈ Λ and φ ↔ ψ ∈ Φ.

The following proposition is crucial since it allows us to simulate modal entailment by equational entailment and vice versa. Recall that ⊢_{EL} denotes equational derivability of equations between ground terms.

Proposition 3.11 Suppose Ax is a set of axioms and φ, ψ ∈ L(Λ). Then Ax ⊢_{ML} φ ↔ ψ iff Ax ⊢_{EL} φ = ψ.

Proof By induction, using the respective definitions. Note that the rule φ ↔ ψ ⟹ [λ]φ ↔ [λ]ψ is precisely the congruence rule of equational logic. □

The previous proposition takes care of the syntactical aspect of our goal to explain modal soundness and completeness in terms of the equational counterparts. The semantical part is treated in the next section, where we translate between algebras and coalgebras on the side of models.

The modal entailment relation can be restricted to formulas of finite depth as follows:

Definition 3.12 (Lift(R), ≡_{n}) Consider a set Λ of predicate liftings for T and a set of axioms Ax. For a boolean congruence (Φ, R), put Lift(Φ, R) = (Lift(Φ), Lift(R)) where

Lift(R) = {(t, s) ∈ Lift(Φ) × Lift(Φ) | Ax ∪ R ⊢_{EL} t = s}.

We let ≡_{0} be propositional equivalence on Form_{0} and ≡_{n+1}= Lift(≡_{n}).

In the last definition, elements φ ∈ Φ are treated as atomic formulas. The relationship to the semantics d_{n} of formulas of finite depth is as expected:

Proposition 3.13 For a formula φ of depth n, Ax ⊢ φ ⇔ φ ≡_{n} ⊤.

4 Algebraic Semantics

The goal of the present section is to define a functor L on the category of boolean algebras such that L-algebras provide a sound and complete semantics for L(Λ). In case that the functor L is dual to T (in a sense which we make precise later), this immediately entails soundness and completeness of the coalgebraic semantics.

Definition 4.1 Suppose E is a set of Σ_{BA}^{Λ}-equations. Given A ∈ Alg(Σ_{BA}^{Λ}, E_{BA}∪ E) and two formulas (terms) s, t ∈ T_{Σ_{BA}^{Λ}}(V), possibly involving variables p ∈ V from a set V, we write [[s]]_{A}^{v} for the interpretation of s in A wrt the valuation v : V → A. Furthermore, A ⊧ s = t if [[s]]_{A}^{v} = [[t]]_{A}^{v} for all valuations v : V → A (we omit v if V = ∅), and Alg(Σ_{BA}^{Λ}, E_{BA} ∪ E) ⊧ s = t iff A ⊧ s = t for all A ∈ Alg(Σ_{BA}^{Λ}, E_{BA} ∪ E).

We now come to the central definition of this paper, namely the functor L on boolean algebras associated with a coalgebraic modal logic L(Λ, Ax). The functor L : BA → BA maps a boolean algebra A to the one which is freely generated by all [λ]a, a ∈ A, λ ∈ Λ, and quotiented by the axioms. Recall that F : Set → BA denotes the construction of free algebras.

Definition 4.2 (The functor L) Given a coalgebraic modal logic L(Λ, Ax) for T -coalgebras (i.e. a set Λ of predicate liftings for T and a set Ax of axioms), the corresponding functor L : BA → BA is

A ↦ F {[λ]a | a ∈ A, λ ∈ Λ}/R

where R is the smallest congruence containing the substitution instances of axioms in Ax with variables replaced by elements of A.

This definition bears some similarities to Cirstea’s notion of language constructor [3]: a language constructor describes the linguistic features to specify the behaviour of a system after one transition step. This corresponds to the set F {[λ]a | a ∈ A, λ ∈ Λ} in the above definition. Our definition extends this idea by additionally forming a quotient defined by logical axioms and rules, which results in a faithful logical description of the behaviour observable in one transition step.

Recalling the operator Lift from Definition 3.12 and that A is presented by (UF UA, Diag(A)) the object part of L can also be understood as follows.

Remark 4.3 Let A be a boolean algebra. Then LA is the boolean algebra given by the carrier set Lift(UF UA)/Lift(Diag(A)).

Given a quotient A/≡, we use { · }_{A/≡} to denote equivalence classes.

Proposition 4.4 (i) L is a functor, that is, for a boolean algebra morphism f : A → A′,

Lf : LA ⟶ LA′
{[λ]a}_{LA} ↦ {[λ]f(a)}_{LA′}

defines a boolean algebra morphism. (ii) L preserves injective morphisms and surjective morphisms.

Proof The first claim follows from ‘ ⇒ ’ of Proposition 2.5 whereas ‘ ⇐ ’ yields that Lf is injective if f is. □

Example 4.5 If T is P or V and Λ = {λ_{□}} and Ax as in previous examples, then L-algebras are precisely the modal algebras (also known as boolean algebras with operators). This representation of modal algebras as algebras for a functor was observed by Abramsky [1] and Ghilardi [4].

It is straightforward to interpret terms (formulas) φ ∈ L(Λ) in L-algebras. This is the algebraic semantics of the logic L(Λ).

Definition 4.6 Suppose (A, α) ∈ Alg(L). The algebraic semantics [[φ]] = [[φ]]_{α} of a formula φ ∈ L(Λ) is given inductively by

[[ff]] =⊥ [[φ → ψ]] = [[φ]] → [[ψ]]

[[[λ]φ]] = α({[λ][[φ]]}_{L(A,α)}),

where { · } denotes taking equivalence classes. We write (A, α) ⊧ φ = ψ if [[φ]]_{α} = [[ψ]]_{α} and Alg(L) ⊧ φ = ψ iff (A, α) ⊧ φ = ψ for all (A, α) ∈ Alg(L).

The reason to focus on L-algebras instead of the more familiar Σ_{BA}^{Λ}-algebras is that we want to relate, in the next section, algebraic and coalgebraic semantics by relating the functors L and T. In particular, we will show that the logic is sound, complete and expressive if L is dual to T. On the level of structures, L-algebras and Σ_{BA}^{Λ}-algebras satisfying the axioms are isomorphic.

Proposition 4.7 The category of algebras for the functor L, Alg(L), is isomorphic to the variety of those Σ_{BA}^{Λ}-algebras satisfying Ax and E_{BA}.

Proof Define S : Alg(L) → Alg(Σ_{BA}^{Λ}, E_{BA} ∪ Ax) by mapping (A, α) to the algebra with carrier set UA, which interprets the function symbol [λ] as a ↦ [[[λ]a]]_{α}. Then S(A, α) satisfies Ax because the axioms only involve terms of depth 1. Conversely, we map (A, λ^{A}) to the unique map α determined by

ULA ^{α} A ∑_{Λ} A_{η_{A}}  _{l}

where ∑_{Λ} A is the disjoint union of Λ copies of A, η_{A} is the insertion of generators, and l is the co-tupeling of the operations λ^{A}, λ ∈ Λ. □

As in the case of formulas of depth n, we can also view the algebraic semantics as stratification of the semantics of formulas of depth n, where n ranges over finite ordinals. Formally, this is accomplished via the initial algebra sequence.

Definition 4.8 (L_{n}, algebraic semantics of formulas of depth n) Let L_{0} = 𝟚 and L_{n+1} = L(L_{n}). The algebraic semantic of formulas in L(Λ) is given by the map

q_{n} : Form_{n} ⟶ UL_{n}

which is inductively defined via q_{n+1}([λ]φ) = {[λ]q_{n}(φ)}_{L_{n+1}}.

To prove soundness and completeness w.r.t. to the algebraic semantics, we still have to check that the q_{n} above indeed identify precisely those formulas that are logically equivalent according to the given set of axioms Ax. We need that presentations of (A/≡) are lifted to presentations of L(A/≡):

Lemma 4.9 Let (A, ≡) be a boolean congruence and q : A → A/≡ be the corresponding quotient. Then

q̂: Lift(A) ⟶ UL(A/≡)
[λ]a ↦ {[λ]q(a)}_{L(A/≡)}

is the quotient of Lift(A) w.r.t. Lift(≡).

Proof This follows from Proposition 2.4. □

Proposition 4.10 The kernel of q_{n} : Form_{n} → UL_{n} (Definition 4.8) is ≡_{n} (Definition 3.12).

Proof Follows from Lemma 4.9. □

As mentioned at the beginning of the section, the appealing feature of the algebraic semantics is that we get soundness and completeness for free:

Proposition 4.11 The algebraic semantics is sound and complete, that is Alg(L) ⊧ φ = ψ iff Ax ⊢_{EL} φ = ψ for all φ, ψ ∈ L(Λ).

Proof Using the construction of Proposition 4.7, we obtain (A, α) ⊧ s = t iff S(A, α) ⊧ s = t, hence it suffices to show that Alg(Σ_{BA}^{Λ}, E_{BA} ∪ Ax) ⊧ s = t iff Ax ⊢_{EL} s = t. The latter is standard, and can be shown using a Lindenbaum-Tarski construction. □

5 Completeness and Expressiveness for the Coalgebraic Semantics

Since soundness and completeness w.r.t to the algebraic semantics is straight forward, it is attractive to study soundness and completeness for the coalgebraic semantics via the algebraic semantics. We show that the coalgebraic semantics is sound, complete, and expressive if the functor L is dual to the functor T (Theorem 5.8). This result requires that T is a functor on Stone spaces. We isolate the part of the theorem that is responsible for soundness and completeness (Proposition 5.6), which also works for functors T on sets.

The predicate liftings induce a relation between LP and P T:

Definition 5.1 Consider d_{X} = Lift(id) : Lift(UP X) → UP T X. Let δ_{X} be the relation given by (y, z) ∈ δ_{X} iff d_{X}(x) = z for some x ∈ τ^{−1}({y}) as in the diagram below,

Lift(UP X) _{τ_{X}}  ^{d_{X}} ULP X _{δ_{X}} UP T X

where τ_{X} maps φ ∈ Lift(UP X) to its equivalence class {φ}_{LP X}. We say that L is dual to T if all δ_{X} are bijective functions.

For functors F, G : X → Set we call a family ϱ of relations (ϱ_{X} : F X → GX), X ∈ X, a natural relation between F and G iff ϱ_{Y} ∘ Graph(F f) = Graph(Gf) ∘ ϱ_{X} for all arrows f : X → Y where ∘ denotes here relational composition. It follows from the naturality of the predicate liftings that δ is a natural relation. We say that δ is functional if each δ_{X} is the graph of a function. If δ is functional then the δ_{X} are BA-morphisms and δ : LP → P T is a natural transformation.

These observations allow us, for functional δ, to relate the initial algebra sequence and the final coalgebra sequence via morphisms L_{n} → P T_{n}.

Definition 5.2 Let δ be functional. Define δ_{n} : L_{n} → P T_{n} via δ_{0} = id_{P 1} and δ_{n+1} = δ_{T_{n}} ∘ Lδ_{n}.

The following observation is immediate from Proposition 4.4.

Proposition 5.3 δ_{n} is injective or surjective if δ is injective or surjective, respectively.

As expected, the coalgebraic semantics d_{n} : Form_{n} → UP T_{n} (Definition 3.5) and the algebraic semantics q_{n} : Form_{n} → UL_{n} (Definition 4.8) agree:

Lemma 5.4 If δ is functional then

Form_{n} _{q_{n}}  ^{d_{n}} UL_{n} _{Uδ_{n}} UP T_{n}

commutes.

Proof We calculate that

Uδ_{n+1}(q_{n+1}([λ]φ)) = Uδ_{n+1}{[λ]q_{n}(φ)}_{L_{n+1}} = Uδ_{T_{n}} ∘ ULδ_{n}{[λ]q_{n}(φ)}_{L_{n+1}}
= Uδ_{T_{n}}{[λ]δ_{n}(q_{n}(φ))}_{LP T_{n}} = Uδ_{T_{n}}{[λ]d_{n}(φ))}_{LP T_{n}}
= λ_{T_{n}}(d_{n}(φ)) = d_{n+1}([λ]φ).
□

We can now derive soundness, completeness, and expressiveness for the coalgebraic semantics from the corresponding properties of the algebraic semantics provided that the relationship δ : LP → P T between algebraic and coalgebraic semantics satisfies certain properties.

Proposition 5.5 If δ is functional, then Ax is sound, i.e. Coalg(T) ⊧ φ if Ax ⊢_{ML} φ for all φ ∈ L(Λ).

Proof Suppose Ax ⊢ φ for a formula φ of depth n. Then, by the lemma, φ = ⊤ in L_{n}. This is preserved by δ_{n} which is a morphism. It follows from Proposition 3.7 that Coalg(T) ⊧ φ. □

Proposition 5.6 If δ is functional and injective, then Ax is sound and complete, i.e. Coalg(T) ⊧ φ iff Ax ⊢_{ML} φ for all φ ∈ L(Λ).

Proof Suppose Ax ⊬_{ML} φ for a formula φ of depth n. Then, by the lemma, φ ≠ ⊤ in L_{n}. This is preserved by δ_{n} which is an injective morphism. It follows from Proposition 2.8 that there is x in T_{n} that refutes φ. □

Proposition 5.7 If δ is functional and surjective, then Ax is sound and ωstep expressive (Definition 2.10).

Proof Given two coalgebras (X, ξ), (Y, ν), and two states x ≄_{ω} y, x in X, and y in Y. Then there is n < ω such that ξ_{n}(x) ≠ ν_{n}(y). Hence there are predicates p_{x}, p_{y} ∈ UP T_{n} separating x and y. By surjectivity of δ_{n}, there are also formulas separating x and y. □

Theorem 5.8 Consider T : Stone → Stone, a set of predicate liftings Λ for T and a set of axioms Ax. Let L : BA → BA be the functor given by Ax (Definition 4.2). If L is dual to T (Definition 5.1), then Ax is sound, complete and expressive.

Proof The claim on soundness and completeness is contained in Propositions 5.5 and 5.6 above. Since the language L(Λ) is built from predicate liftings with finite (in the present paper even unary) arity, the initial algebra sequence for L converges after ω steps. Since T is dual to L and because of the duality between Stone and BA, the final sequence of T also converges after ω steps, hence ω-behavioural equivalence is behavioural equivalence. Now expressiveness follows from Proposition 5.7. □

Remark 5.9 (Canonical Model) In modal logic, the canonical model (C, γ) is a particular model whose states are the maximally consistent sets of formulas and whose transition relation γ is chosen in a way such that the so-called truth lemma

(C, γ), Φ ⊧ φ ⇔ φ ∈ Φ

holds. Completeness is then immediate from the existence of a canonical model. Indeed, suppose φ cannot be derived; then ¬φ is consistent, hence there is Φ ∈ C with ¬φ ∈ Φ, hence (C, γ), Φ ⊧ ¬φ, from which \begin{matrix}/ \\ ⊧ \end{matrix} φ follows.

Clearly, the truth lemma depends on the fact that the states of C are sets of formulas, a property which is not invariant under isomorphism. From a categorical point of view, the truth lemma is not a property of some coalgebra but of the morphism δ_{ω} : L_{ω} → P T_{ω} where L_{ω} is the colimit of the initial algebra sequence (L_{n})_{n<ω}. We then have

(T_{ω}, τ), x ⊧ φ ⇔ x ∈ d̄_{ω}([φ]).

6 A Characterisation of Duality

In the previous section we have seen that the logic given by a set of predicate liftings Λ and a set Ax of axioms is sound, complete and expressive if the induced functor L is dual to T. In this section, we investigate conditions under which is the case. Our main result is Theorem 6.13, where we give a characterisation of this duality in terms of Ax and Λ. More specifically, we have that L is dual to T if the axioms induce order-reflecting and preserving functions Lift(f) : Lift(A) → P T X, given an order-preserving and -reflecting f : A → P X (where Lift(A) are formulas of depth 1 over atoms in A) and, additionally, the predicate liftings Λ allow to distinguish all elements of T X. We discuss both aspects, the condition on the axioms and the condition of the predicate liftings, separately.

6.1 Functionality and Injectivity

We start by showing that the canonical natural relation δ is functional and injective iff the axioms induce order-preserving and -reflecting functions, giving rise to a sound and complete logic. The third author gave sufficient conditions for the coalgebraic modal logic of a functor T : Set → Set to be sound and complete in [15]. We will recall these conditions and then show that they are equivalent to the fact that the relation δ as defined in Definition 5.1 is functional and injective. In the following we fix a set Λ of predicate liftings for T. Recall the definition of Lift(h) : Form(A) → UP T X (Definition 3.5).

Definition 6.1 (order-preservation and reflection) Suppose Ax is a set of axioms.

(i) Ax is order-preserving iff for all functions h : (A, ⊢) → UP X, (A, ⊢) ∈ PreOrd_{BA}, we have that Lift(h) preserves order, if h does. (ii) Ax is order-reflecting iff for all functions h : (A, ⊢) → UP X, (A, ⊢) ∈ PreOrd_{BA}, we have that Lift(h) reflects order, if h does.

We briefly comment on the relation between the present definition and those given in [15].

Remark 6.2 The definition of a order-preserving and -reflecting set of axioms given here is not exactly the same as the definition given in [15]: We restrict our attention to maps which have boolean preorders as domain. The proofs and arguments in [15] for proving soundness and completeness of the logic would however also work with our weaker conditions.

Having the notion of order reflection and -preservation at hand, the main result of this section can be formulated as follows:

Theorem 6.3 Given a set of axioms Ax for L(Λ), then Ax is order-preserving and -reflecting iff δ is functional and injective.

We need some preparations in order to be able to prove the theorem, which we split into two parts. The first (and easy) part is the following lemma:

Lemma 6.4 Given a set of axioms Ax for L(Λ), then

(i) If Ax order-preserving, then δ is functional. (ii) If Ax order-preserving and reflecting, then δ is functional and injective.

Proof

(i) Recall that for X ∈ X the relation δ_{X} was defined as the relation ⊆ ULP X × P T X through which the map d_{X} : Form(P X) → P T X mapping generators of the form [λ]a to λ_{X}(a) factors (cf. Definition 5.1). It is easy to see that d_{X} is nothing but Lift(id_{P X}), i.e. the lifting of the identity function id_{P X} : P X → P X as defined as in Definition 3.5. According to our assumption Lift(id) is order-preserving as id is order-preserving. Corollary 2.3 tells us then that Lift(id) factors through a BA-morphism \overline{Lift(id)}. It can be easily seen that \overline{Lift(id)} = δ_{X}, hence δ_{X} is functional and a BA-morphism. (ii) Suppose now that Ax is order-preserving and -reflecting. Then as in the first case we can show that δ_{X} = \overline{Lift(id)} is a BA-morphism. As Lift(id) is now also order-reflecting we obtain, again by using Corollary 2.3, that δ_{X} is injective.

□

To prove the second half of the theorem we take a closer look at the definition of Lift.

Definition 6.5 (“syntactic lifting”) Given a function h : (A, ⊢) → P X where (A, ⊢) ∈ PreOrd_{BA}, we define a function

⟨h⟩ : Lift(A) → Lift(P X)

that maps [λ]a to [λ]h(a) for λ ∈ Λ , a ∈ A.

Using ⟨h⟩, we can characterise the action of Lift on functions as follows:

Lemma 6.6 Let h : (A, ⊢) → P X be a function, (A, ⊢) ∈ PreOrd_{BA}. Then (i) Lift(h) = Lift(id_{P X}) ∘ ⟨h⟩. (ii) If δ is functional and h is order-preserving, then Lift(h) is order-preserving. (iii) If δ is functional and injective and h is order-reflecting, then Lift(h) is order-reflecting.

Proof Assume that δ is functional and h is order-preserving. h factors through the quotient Ā of A wrt to the congruence induced by ⊢, giving rise to h̄ : Ā → P X. Consider the diagram

A_{h}  _{q}  Lift(A)  ^{Lift(h)}_{q̂}_{⟨h⟩}  ULĀ_{ULh̄}  UP T X Ā_{h̄} P X  Lift(UP X)  _{Lift(id)}_{τ_{X}} ULP X _{δ_{X}} UP T X_{id}

with ⟨h⟩ as in Definition 6.5 and q̂ as in Lemma 4.9. The lower row is taken from Definition 5.1. The left hand square commutes:

ULh̄(q([λ]a) = ULh̄({[λ]q(a)}_{LĀ}) = {[λ](h̄(q(a)))}_{LP X}
= {[λ]h(a)}_{LP X} = τ_{X}([λ]h(a))) = τ_{X}(⟨h⟩([λ]a)).

This shows that Lift(h) factors through ULĀ and is therefore order-preserving (Corollary 2.3). Assume now that δ is functional and injective and h is order-reflecting. Since Lh̄ is injective (Proposition 4.4) Lift(h) factors through an injective LĀ → P T X and is therefore order-reflecting. □

The proof of the Theorem 6.3 is now complete: Lemma 6.4 proves one direction and Lemma 6.6 the other direction.

6.2 Surjectivity

We now consider a logic for an endofunctor T : Stone → Stone, i.e. X = Stone and P = Clp. Here we will see that requiring that the set of predicate liftings Λ for T is “separating” (a notion taken from [16]) is equivalent to the fact that the canonical map δ is surjective.

Definition 6.7 (Separation) Let X ∈ Stone.

(i) A collection of clopens C ⊆ ClpX is called separating if the map

s_{X} : X → P(ClpX)
x ↦ {U ∈ X | x ∈ U}

is injective. (ii) A set of predicate liftings Λ for T is called separating if for all X ∈ Stone

Im_{Λ}(X) := {λ_{X}(U) | λ ∈ Λ, U ∈ Clp(X)}

is a separating set of clopens of T X.

Intuitively a separating set of predicate liftings makes it possible to characterise points in T X(“successors”) by lifted predicates over X.

As it was shown in [16] a coalgebraic modal logic which has a separating set of predicate liftings is expressive. We will now see that provided we have a sound and complete logic for the functor T the fact that Λ is separating is equivalent to saying that the functor L defining the algebraic semantics of our logic is the dual of T.

Our main theorem states that δ is surjective if and only if the set Λ of predicate liftings is separating. Before we state (and prove) the theorem, we collect some facts on separating sets, which are necessary for the proof of the theorem.

Lemma 6.8 Let X ∈ Stone and let 𝔸 ⊆ ClpX be a subalgebra of ClpX. Then s_{𝔸} is injective iff 𝔸 = ClpX.

Proof The implication from right to left is immediate. To prove the other direction suppose that s_{𝔸} is injective. Then one can easily see that

⋂{U ∈ 𝔸 | x ∈ U} = {x}  (1)

for all x ∈ X. To prove 𝔸 = ClpX it suffices to show that 𝔸 is a basis for the topology on X. Suppose that W ⊆ X is open and let x ∈ W. We have to show that there is a clopen set U ∈ 𝔸 such that x ∈ U ⊆ W. Because of (1) we know that for all y ∈ −W there is some U_{y} ∈ 𝔸 such that x ∉ U_{y} and y ∈ U_{y}. Hence −W ⊆ ∪_{y∈−W} U_{y}. Because of compactness of the topology there are y_{1}, …, y_{n} ∈ −W such that −W ⊆ ∪_{i=1}^{n}U_{y_{i}}. Define V := −(∪_{i=1}^{n}U_{y_{i}}). Then V ∈ 𝔸 and x ∈ V ⊆ W. Therefore 𝔸 is a basis of the topology of X. □

Lemma 6.9 Let X ∈ Stone and let C ⊆ ClpX be a clopen subbasis of the topology of X. Then C is a separating set of clopens.

Proof Let x, y ∈ X and x ≠ y. Then there is a U ∈ ClpX such that x ∈ U and y ∈ −U. As C is a subbasis of the topology there are V_{1}, …, V_{n} ∈ C such that

x ∈ ⋂_{i=1}^{n} V_{i} ⊆ U.

But this means that there is at least one V_{j} ∈ C such that x ∈ V_{j} and y ∉ V_{j}, and therefore s_{C}(x) ≠ s_{C}(y). □

Lemma 6.10 Let C ⊆ ClpX and define −C := {−U | U ∈ C}. Then

s_{C} injective ⇔ s_{C∪−C} injective

Proof The direction from left to right is obvious. For the other direction, suppose s_{C∪−C} is injective and let x, y ∈ X, x ≠ y. Then according to our assumption

s_{C∪−C}(x) ≠ s_{C∪−C}(y).

Therefore we can assume that there is V ∈ C ∪ −C such that x ∈ V and y ∈ −V. We distinguish the following cases: Case V ∈ C. Then clearly s_{C}(x) ≠ s_{C}(y). Case V ∈ −C. Then −V ∈ C and hence −V ∈ s_{C}(y) and −V ∉ s_{C}(x). Since V ∈ C ∪ −C, this finishes the proof. □

Now we are ready to prove the main result of this section:

Theorem 6.11 Let T : Stone → Stone be a functor, and suppose that L(Λ) is a logic for T that has a order-preserving set of axioms Ax. Then Λ is a separating set of predicate liftings iff the canonical δ : L ∘ Clp → Clp ∘ T is surjective.

Proof Given an order-preserving set of axioms we know that the map Lift(id_{ClpX}) : Lift(ClpX) → ClpT X factors through δ_{X} : LClpX → ClpT X ∈ BA. It is therefore obvious that we have the following equivalence:

∀X.δ_{X} surjective ⇔ ∀X.Lift(id_{ClpX}) surjective

We now show that the last property is equivalent to the fact that Λ is a separating set of liftings. Suppose first that for an arbitrary X ∈ Stone the map Lift(id_{ClpX}) is surjective. As the domain of Lift(id) is closed under the boolean operations it can be easily seen that the image of Lift(id) is equal to ⟨Im_{Λ}(X)⟩_{ClpT X}, the subalgebra of ClpT X generated by Im_{Λ}(X). Hence we get

ClpT X = Im(Lift(id_{ClpX})) = ⟨Im_{Λ}(X)⟩_{ClpT X} .

This implies that Im_{Λ}(X) ∪ −Im_{Λ}(X) is a clopen subbasis of the topology of T X, where again −Im_{Λ}(X) := {−U | U ∈ Im_{Λ}(X)}. Using Lemma 6.9 and 6.10 we obtain that the map s_{Im_{Λ}(X)} is injective. As X was arbitrary we can conclude that Λ is separating. Now suppose that Λ is a separating set of liftings and let X ∈ Stone. Then s_{Im_{λ}(X)} is injective which also implies the injectivity of s_{Lift(id_{ClpX})}. As the image of Lift(id) is a subalgebra of ClpT X it follows by Lemma 6.8 that Im(Lift(id_{ClpX})) = ClpT X. □

We note the following immediate consequence, which is the main result of this section:

Corollary 6.12 Let T : Stone → Stone be a functor, and suppose that L(Λ) is a logic for T that has a order-preserving set of axioms Ax. Then L(Λ) is expressive if Λ is separating.

Proof Follows directly from the theorem and Proposition 5.7 □

Summing up, we can now characterise duality between T and L in logical terms as follows:

Theorem 6.13 Let T : Stone → Stone and Ax is a set of axioms. The following are equivalent:

(i) Ax is order-preserving and reflecting, and Λ is separating (ii) L is dual to T.

Proof Follows directly from Theorem 6.3 and from Theorem 6.11. □

Combining the above result with Theorem 5.8, both of the two equivalent conditions above provide us with a sound, complete and expressive logic for T -coalgebras.

7 Conclusions, Related Work

Our results provide an axiomatic account of some aspects of the duality between modal and equational logic. We have developed an algebraic semantics for coalgebraic logic, which allows us to deduce soundness and completeness wrt the coalgebraic semantics directly from the corresponding property of the algebraic semantics. Moreover, we have given a characterisation of the duality between the algebraic and the coalgebraic aspects in terms of the extralogical axioms.

The theory of algebraic logics has a long tradition, see e.g. [2] for applications in a computer science context. Algebraic techniques in modal logic were first employed by Jónsson and Tarski [10]. Our work stands in the tradition of Goldblatt [6,5], where the duality of descriptive general frames and boolean algebras with operators was made explicit. Our results work towards generalising this duality to coalgebras over stone spaces (generalising descriptive general frames, see [11]) and algebras for extensions of the boolean signature.

In a coalgebraic context, Jacobs [8] has set up an adjunction between the category of coalgebras for certain endofunctors and a related category of boolean algebras with operators. The endofunctors treated in loc.cit. are built syntactically, whereas our approach is axiomatic. The same applies to the duality investigated by Goldblatt [7], where definability issues are studied.

In the future, we plan to extend the approach as to incorporate also different dualities (e.g. Heyting algebras and Priestly spaces). Furthermore, we are trying to relax the condition of a duality between functors to a duality between categories, that is, we hope to be able to give an algebraic semantics for coalgebraic logics if we have a duality between coalgebras over Stone and algebras over BA, which extends the basic Stone duality.

References

[1] S. Abramsky. A Cook’s Tour of the Finitary Non-Well-Founded Sets. Invited Lecture at BCTCS 1988.

[2] A. Andréka, A. Kurucz, I. Neméti, and I. Sain. Applying algebraic logic to logic. In M. Nivat, C. Rattray, T. Rus, and G. Scollo, editors, Algebraic Methodology and Software Technology, Workshops in Computing. Springer, 1994.

[3] C. Cîrstea. On expressivity and compositionality in logics for coalgebras. In H.P. Gumm, editor, Coalgebraic Methods in Computer Science (CMCS’03), volume 82.1 of ENTCS, 2003.

[4] S. Ghilardi. An algebraic theory of normal forms. Annals of Pure and Applied Logic, 71:189–245, 1995.

[5] R. Goldblatt. Varieties of complex algebras. Annals of Pure and Applied Logic, 38:173–241, 1989.

[6] R. Goldblatt. Metamathematics of modal logic. In Mathematics of Modality, volume 43 of CSLI Lecture Notes, chapter 1. Center for the Study of Language and Information, Stanford University, 1993.

[7] R. Goldblatt. Duality for some categories of coalgebras. Algebra Universalis, 46:389–416, 2001.

[8] B. Jacobs. Towards a duality result in coalgebraic modal logic. In Horst Reichel, editor, Coalgebraic Methods in Computer Science (CMCS’00), volume 33 of ENTCS, pages 163–198, 2000.

[9] B. Jacobs. Many-sorted coalgebraic modal logic: a model-theoretic study. Theoretical Informatics and Applications, 35(1):31–59, 2001.

[10] B. Jónsson and A. Tarski. Boolean algebras with operators, part 1. American Journal of Mathematics, 73:891–939, 1951.

[11] C. Kupke, A. Kurz, and Y. Venema. Stone coalgebras. In H.P. Gumm, editor, Coalgebraic Methods in Computer Science (CMCS’03), ENTCS, 2003.

[12] A. Kurz. Specifying coalgebras with modal logic. Theoretical Computer Science, 260:119–138, 2001.

[13] A. Kurz and D. Pattinson. Coalgebraic modal logic of finite rank. Mathematical Structure in Computer Science. To appear.

[14] L. Moss. Coalgebraic logic. Annals of Pure and Applied Logic, 96:277–317, 1999.

[15] D. Pattinson. Coalgebraic modal logic: Soundness, completeness and decidability of local consequence. Theoretical Computer Science, 309(1–3):177– 193, 2003.

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

[17] M. Rößiger. Coalgebras and modal logic. In Horst Reichel, editor, Coalgebraic Methods in Computer Science (CMCS’00), volume 33 of ENTCS, pages 299– 320, 2000.

[18] J.J.M.M. Rutten. Universal coalgebra: A theory of systems. Theoretical Computer Science, 249:3–80, 2000.

[19] J. Worrell. Terminal sequences for accessible endofunctors. In B. Jacobs and J. Rutten, editors, Coalgebraic Methods in Computer Science (CMCS’99), volume 19 of ENTCS, pages 39–53, 1999.