                         CMCS’04 Preliminary Version

Coalgebras and Modal Expansions of Logics

Alexander Kurz^{a} Alessandra Palmigiano^{b}

a University of Leicester b Universitat de Barcelona

Abstract In this paper we construct a setting in which the question of when a logic supports a classical modal expansion can be made precise. Given a fully selfextensional logic S, we find sufficient conditions under which the Vietoris endofunctor V on Sreferential algebras can be defined and we propose to define the modal expansions of S as the logic that arises from the V-coalgebras. As an example, we also show how the Vietoris endofunctor on referential algebras extends the Vietoris endofunctor on Stone spaces.

From another point of view, we examine when a category of ‘spaces’ (X, 𝔸), ie sets X equipped with an algebra 𝔸 of subsets of X, allows for the definition of powerspaces V (and hence transition systems (X, 𝔸) → V(X, 𝔸)).

1 Introduction

The problem studied in this paper can be explained and motivated from rather distinct perspectives.

The Coalgebraic Motivation We investigate systems whose state space can be described by a set X together with an algebra 𝔸 of subsets of X. We think of the elements of 𝔸 as the admissible predicates over X (or the observations that can be made of states in X). The operations of the algebra reflect the ability to built new observations from given ones using logical connectives. This interpretation, as well as the analogy with topological spaces, suggest to call these structures logical spaces. In algebraic logic they are known as referential algebras.

A transition relation can be considered as a map assigning to a state in X the set of its successors. The coalgebraic perspective suggests that we should look for a functor V on the category of logical spaces that allows us to represent systems as morphisms

(X, 𝔸) → (VX, V𝔸).

VX will be a subset of the full powerset PX. In order to see what the admissible predicates V𝔸 on VX should be, we focus on the following two basic

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

                       URL: www.elsevier.nl/locate/entcs

Kurz and Palmigiano

observations one can make about a subset v ∈ VX using an admissible set a ∈ 𝔸: whether all elements of v are contained in a, and whether there exists an element of v contained in a. This leads us to the following basic admissible predicates on VX:

□ □a = {v ∈ VX | v ⊆ a} and ◇ ◇a = {v ∈ VX | v ∩ a ≠ ∅}.

This choice of basic admissible predicates is well known in topology and domain theory where (VX, V𝔸) is known as the Vietoris space or the Plotkin powerdomain. To see under which circumstances this construction can be generalized from topological spaces is one of the aims of this work.

The construction of VX is well-known and presented in Section 3. The main contribution of this paper consists in giving a construction of V𝔸. This construction is motivated by the logical interpretation of referential algebras as models for selfextensional logics and uses the duality theory for selfextensional logics.

Selfextensional Logics One of the major conceptual achievements in philosophical logic is the Fregean distinction between sense and reference, which is captured in the formal distinction between the intensional and the denotational approaches in defining the semantics of logical languages. In a denotational approach, the semantics of formulas is given by their truth values (denotation). The denotational approach is adequate only for those logics for which the substitutivity principle holds, i.e. those logics such that any two sentences with the same truth value can be substituted for one another without altering the truth value of the result. The substitutivity principle does not hold for intensional logics of which modal logic is perhaps the best known example. In any intensional approach, semantic structures are always based on sets of states, or ‘possible worlds’, X, so that any formula φ takes its denotation (truth value) at every possible world. Then ϕ is interpreted as a predicate by mapping it to the subset of the possible worlds at which it is true. This set is often called the intension of φ. The substitutivity principles holds not for formulas with the same denotation in a given world but for formulas with the same intension, i.e. with the same denotation in every possible world. Kripke structures are perhaps the best known example of intensional semantics.

Compositionality is a basic requirement in both the denotational and the intensional approaches to semantics. As it is well known, the denotational approach accounts for compositionality by endowing the set of truth values with an algebraic structure: The paradigmatic example is the Boolean algebra 2, where the truth value of the compound formula φ ∧ ψ can be computed from the truth values of φ and ψ.

Likewise, accounting for a compositional semantics in any intensional setting means to endow (a selected subset of) P(X) with an algebraic structure, so that the intension of the compound formula φ ∧ ψ can be computed from the intensions of φ and ψ (and more often than not there are further requirements on the definition of the operations: for instance, that the intension of φ ∧ ψ coincides with the intersection of the intensions of φ and ψ, and so on). General frames for modal logic are a typical example: they are defined as triples (X, R, 𝔸), where X is a nonempty set of states, R ⊆ X × X and 𝔸 is a subalgebra of the Boolean algebra P(X).

In algebraic logic, the intensional approach to semantics is treated in a general setting that abstracts away from the particular similarity type of logics: for every algebraic similarity type τ, the semantic structures for τ-logics are referential algebras, i.e. tuples (X, 𝔸) such that X ≠ ∅ and 𝔸 is a τ-algebra of subsets of X (that is not required to be a subalgebra of P(X)). Selfextensional logics where characterized by Wójcicki as the logics that are sound and complete w.r.t. their corresponding class of referential algebras. One of their features is that any two formulas are interderivable if and only if they are mapped to the same subsets in any referential algebra. Thus for selfextensional logics, interderivability captures the identity of meaning (intension), in a compositional way. Since referential algebras, that are the canonical semantic structures for selfextensional logics, can be regarded as abstract versions of general frames, selfextensional logics can be loosely thought of as generalizing modal logics. On the other hand, many logics that are neither modal nor intensional, like classical and intuitionistic propositional logics, are selfextensional as well. This paper is the starting point of a line of investigation that aims at a better understanding of the relation between selfextensional logics and modalities.

The Logical Motivation The general way in which modal logics are investigated from an algebraic perspective is to regard modal operators as expanding an underlying logical signature. We take the converse perspective and ask ‘When does a given selfextensional logic S support modalities?’ Our aim is to set a context in which this question can be made precise, i.e. to define a general theory of modal expansions of selfextensional logics so that the operators of the modal expansions have predetermined semantics and properties. In this paper we are focusing on expanding a logic with modal operators □ and ◇, that are normal and interrelated like in the modal logic K. So we are going to define the modal expansion of a logic as the logic that canonically arises from the semantic structures that we purposely construct to force the required semantics and properties.

We construct these structures as coalgebras for the Vietoris endofunctor V on the category of referential algebras associated with S, the S-referential algebras. In their turn, the V-coalgebras so obtained can be represented as referential algebras of the modally expanded similarity type: indeed, a Vcoalgebra is a set map ρ : X ⟶ VX such that ρ^{−1} ∈ Hom(V𝔸, 𝔸). Then ρ will correspond to the referential algebra (X, 𝔸′), where 𝔸′ is the modal expansion of 𝔸 associated with ρ^{−1} ∈ Hom(V𝔸, 𝔸). The modal expansion of S will be defined as the logic that arises from this class of referential algebras.

We propose to say that a selfextensional logic S supports classical modalities if its modal expansion can be constructed as sketched above.

Duality Theory The main contribution of this paper is the construction of the Vietoris endofunctor on S-referential algebras. One natural question is how this construction is related with the Vietoris endofunctors on certain classes of topological spaces that are known from the literature, like the Vietoris endofunctors on Stone and Priestley spaces. There is a natural way in which this construction extends the known ones, and it is based on the fact that those topological spaces can be represented as referential algebras. Indeed, the categories of those topological spaces are isomorphic to full subcategories of referential algebras, in such a way that the following diagrams commute:

Stn ⟶^{K} Stn
↓  ↓
RA_{S} ⟶^{V} RA_{S}

Pri ⟶^{V} Pri
↓  ↓
RA_{S} ⟶^{V} RA_{S}.

These embeddings are part of a more general picture that is brought about by the duality theory for selfextensional logics, briefly presented in 2.2. This theory consists of two parts: the first part defines a duality between categories of models of the same selfextensional logic S, namely between the atlases, that provide the algebraic semantics for S according to the theory of Abstract Algebraic Logic, and the S-referential algebras. This duality is shaped around logic, for atlases and referential algebras correspond to one another in such a way that their logical content is integrally preserved. The key feature of this duality is that its logical import is in-built it its definition. The second part is about how this duality uniformly extends a wide class of known dualities, which includes the Stone and Priestley ones. The involved categories of algebras and topological spaces are shown to be respectively isomorphic to categories of atlases and referential algebras, in such a way that the duality functors are lifted too, and as the logical import of the duality for atlases and referential algebras is given by definition, this embedding provides a way to make the logical interpretation of the embedded dualities explicit and uniform.

This comes as no surprise: the logical import of dualities has been widely recognized in the literature by showing their systematic connections with soundness and completeness theorems, and dualities have been widely used in the literature to give a logical interpretation to set-based structures such as topological spaces and coalgebras.

The duality theory for selfextensional logics plays a crucial role in the setting that we present here. The novelty is that this duality is not used to give a logical interpretation to independently defined set-based structures: it is used to define the set-based structures from the logic that we want to modally expand, and from the predetermined semantics and properties of the modal expansion.

Related Work This work is set in the context of abstract algebraic logic (AAL) and duality theory. The monograph [FJ96] provides a detailed account of the basics of AAL. The book [Joh82] is the standard reference for the basics of duality theory. The duality theory for selfextensional logics is developed in [Pal02]. The characterization of selfextensional logics in terms of referential algebras appears in [Wój73] and [Wój88]. Coalgebras of Vietoris endofunctors on Stone and Priestley spaces are shown to be adequate semantic structures for the modal logics K and PML respectively in [KKV03] and [Pal03a]. Analogous but partial results for some modal intuitionistic logics can be found in [Pal03b]. The description of VA in Section 4 owes a lot to the Vietoris locale defined in [Joh85]. The theories of Natural Dualities, developed in [CD98] and of Bounded Lattice Expansions [GH01] will be relevant to further developments of this work (see also discussion in Section 6).

Acknowledgements This paper was written during a visiting period of the second author to the Department of Computer Science of the University of Leicester. The second author wishes to thank the research group of Computer Science of the University of Leicester for their hospitality, and for partially funding her stay. We would like to thank Ramon Jansana for reading preliminary versions of this work and for many useful comments.

2 Preliminaries on Selfextensional Logics

Throughout this section, τ is an algebraic similarity type, A is a τ-algebra and A is its carrier, Fm is the free τ-algebra (of formulas) over a given set of variables Var, S = (Fm, ⊢_{S}) is a τ-consequence relation, H = (W, 𝔸) is a τ-referential algebra, X is the domain of H and Q = (A, B) is a τ-atlas.

2.1 Basic Concepts

A τ-consequence relation is a pair S = (Fm, ⊢_{S}), where Fm is the τ-algebra of formulas over a given set of variables and ⊢_{S} ⊆ P(F m) × F m such that for all Γ ∪ {φ} ⊆ F m,

1. If φ ∈ Γ then Γ ⊢_{S} φ.

2. If Γ ⊢_{S} φ and Γ ⊆ Δ then Δ ⊢_{S} φ.

3. If Γ ⊢_{S} φ and for every ψ ∈ Γ Δ ⊢_{S} ψ, then Δ ⊢_{S} φ.

If T ⊆ F m is closed under ⊢_{S}, i.e. if T ⊢_{S} φ then φ ∈ T for every φ ∈ F m, then T is a theory of S, or an S-theory. T h(S) is the set of the S-theories. S is finitary iff for all Γ ∪ {φ} ⊆ F m, if Γ ⊢_{S} φ then Δ ⊢_{S} φ for some finite set Δ ⊆ Γ. S is structural iff for all Γ ∪ {φ} ⊆ F m, for all σ ∈ Hom(Fm, Fm), if Γ ⊢_{S} φ then σ[Γ] ⊢_{S} σ(φ). A sentential logic is a finitary and structural consequence relation. The interderivability relation of S is the equivalence relation ⊣⊢_{S} = {(φ, ψ⟩ ∈ F m×F m | φ ⊢_{S} ψ and ψ ⊢_{S} φ}. S is selfextensional iff ⊣⊢_{S} is a congruence of Fm.

For every τ-algebra A and every F ⊆ A, F is an S-filter iff for every h ∈ Hom(Fm, A) and every S-sequent Γ ⊢_{S} φ, if h[Γ] ⊆ F then h(φ) ∈ F. F i_{S}(A) is the collection of the S-filters of A. F i_{S}(Fm) = T h(S). S is fully selfextensional iff for every algebra A, the Frege relation Λ_{S} = {⟨a, b⟩ | a ∈ F iff b ∈ F for every F ∈ F i_{S}(A)} is a congruence of A. The Frege relation on Fm is ⊣⊢_{S}. If S is fully selfextensional, then A is an S-algebra iff Λ_{S} is the identity relation. For example, if S is classical propositional logic, then Boolean algebras are the S-algebras. For every fully selfextensional logic S and every algebra A, A/Λ_{S} is an S-algebra. Let q : A ⟶ A/Λ_{S} be the associated canonical projection.

Remark 2.1 For every logic S that is fully selfextensional, and every h ∈ Hom(A_{1}, A_{2}), the assignment q_{1}(a) ↦ q_{2}(h(a)) defines a homomorphism qh ∈ Hom(A_{1}/Λ_{S}, A_{2}/Λ_{S}).

Proof. For every h ∈ Hom(A_{1}, A_{2}) and every F ∈ F i_{S}(A_{2}), h^{−1}(F) ∈ F i_{S}(A_{1}). Therefore, ⟨a, b⟩ ∈ Λ_{S}(A_{1}) implies that ⟨h(a), h(b)⟩ ∈ Λ_{S}(A_{2}), and from this it follows that qh is well defined. The rest is routine. □

As a consequence of this remark, Fm/ ⊣⊢_{S} is the free S-algebra.

2.2 Models for Selfextensional Logics and Duality

A τ-referential algebra is a pair H = (X, 𝔸) where X is a nonempty set and 𝔸 is a τ-algebra of subsets of X. H is differentiated iff for every a, b ∈ X, if a ∈ Y iff b ∈ Y for every Y ∈ A, then a = b. The consequence relation induced by H is defined as follows: For every Γ ∪ {φ} ⊆ F m, Γ ⊧_{H} φ iff for every h ∈ Hom(Fm, A), ⋂_{γ∈Γ} h(γ) ⊆ h(φ). H is an S-referential algebra iff ⊢_{S} ⊆ ⊧_{H}. The consequence relation ⊧_{H} is structural and selfextensional by construction. Conversely, if S is selfextensional, then there exists a DRA H such that ⊢_{S} = ⊧_{H}. For every H = (W, 𝔸) and H′ = (X′, 𝔸′), h ∈ Hom(H, H′) iff h ∈ Set(X, X′) and h^{−1} ∈ Hom(𝔸′, 𝔸). h ∈ Hom(H, H′) is strict iff h^{−1} ∈ Hom(𝔸′, 𝔸) is onto.

A τ-atlas is a pair Q = (A, B) such that A is a τ-algebra and B is a collection of subsets of A. The Frege relation of an atlas Q is the equivalence relation Λ_{Q} = {⟨a, b⟩ ∈ A × A | for every B ∈ B, a ∈ B ⇔ b ∈ B}. Q is Fregean iff Λ_{Q} is a congruence of A. Q is Frege-reduced (FRA) iff Λ_{Q} is the identity relation on A. If Q = (A, B) is Fregean then the quotient atlas Q^{∗} = (A^{∗}, B^{∗}), where A^{∗} = A/Λ_{Q}, B^{∗} = {B^{∗} | B ∈ B}, B^{∗} = p[B] and p : A → A^{∗} is the canonical projection, is Frege-reduced. The consequence induced by Q is defined by: For every Γ ∪ {φ} ⊆ F m, Γ ⊧_{Q} φ iff for every h ∈ Hom(Fm, A) and for every B ∈ B, if h[Γ] ⊆ B then h(φ) ∈ B. Q is an S-atlas iff ⊢_{S} ⊆ ⊧_{Q} iff B ⊆ F i_{S}(A).

For all Q and Q′, h ∈ Hom(Q, Q′) iff h ∈ Hom(A, A′) and {h^{−1}(B′) | B′ ∈ B′} ⊆ B. h ∈ Hom(Q, Q′) is strict iff {h^{−1}(B′) | B′ ∈ B′} = B. For example, the canonical projection p ∈ Hom(Q, Q^{∗}) is strict and onto. If h ∈ Hom(Q, Q′) is strict and onto, then ⊧_{Q′} = ⊧_{Q}. In particular, if h ∈ Hom(Q, Q′) is strict and onto and Q is an S-atlas, then Q′ is an S-atlas. Hence, if Q is a Fregean S-atlas, then Q^{∗} is a Frege-reduced S-atlas.

The dual referential algebra of a Fregean atlas Q = (A, B) is Q_{+} = (B, \overline{A}), where \overline{A} = \{\overline{a} | a ∈ A\}, and \overline{a} = \{B ∈ B | a ∈ B\} for every a ∈ A. Since Λ_{Q} is a congruence, for every f ∈ τ we can define the operation f\overline{A} by declaring f\overline{A}(\overline{a_{1}}, …, \overline{a_{n}}) = \overline{f^{A}(a_{1}, …, a_{n})} for every a_{1}, …, a_{n} ∈ A. Q_{+} is a DRA and ⊧_{Q} = ⊧_{Q_{+}}. In particular, if Q is an S-atlas, then Q_{+} is an S-referential algebra. If h ∈ Hom(Q, Q′), then h_{+} := h^{−1} ∈ Hom(Q′_{+}, Q_{+}). If h is onto, then h_{+} is strict, and if h is strict, then h_{+} is onto.

The dual atlas of H = (X, 𝔸) is H^{+} = (𝔸, \overline{X}) where \overline{X} = \{\overline{x} | x ∈ X\} and \overline{x} = \{Y ∈ A | x ∈ Y \} for every x ∈ X. H^{+} is an FRA and ⊧_{H} = ⊧_{H^{+}}. In particular, if H is an S-referential algebra, then H^{+} is an S-atlas. If h ∈ Hom(H, H′) then h^{+} := h^{−1} ∈ Hom(H^{′+}, H^{+}). If h is onto, then h^{+} is strict, and if h is strict, then h^{+} is onto.

These correspondences define a dual equivalence between the categories FRA of Frege-reduced atlases and atlas morphisms and the category DRA of differentiated referential algebras and referential algebra morphisms.

A feature of this duality is that a wide class of dualities for categories of algebras that have a distributive lattice part can be uniformly “embedded” in it. This is the case of the Stone and Priestley dualities, as well as the case of the duality for BAO’s and descriptive general frames. For example, for every Boolean algebra (BA) A, let Q_{A} = (A, Ultr(A)), where Ultr(A) is the set of the ultrafilters of A, and for every Stone space X = (X, Ω), let H_{X} = (X, 𝔸) where 𝔸 is the BA of the clopen subsets of X. These assignments define two covariant, faithful and full functors Q_{...} : BA ⟶ FRA and H_{...} : Stn ⟶ DRA, such that Hom(A, A′) = Hom(Q_{A}, Q_{A′}), Hom(X, X′) = Hom(H_{X}, H_{X′}), and the following diagrams commute:

BA ⟶^{F} Stn
Q_{...}↓  H_{...}↓
FRA ⟶^{()_{+}} DRA

Stn ⟶^{G} BA
H_{...}↓  Q_{...}↓
DRA ⟶^{()^{+}} FRA.

3 Modally Closed Subsets

As mentioned in the introduction, we want to define a functor V on referential algebras such that a V-coalgebra

ξ : (W, 𝔸) ⟶ (VW, V𝔸)

consists of a transition relation ξ : W → VW ⊆ PW and an algebra V𝔸 whose elements interpret formulae that can be built from the predicates in 𝔸 and the classical modal operators □ and ◇. That is, for all U ∈ 𝔸, V𝔸 will contain the sets

□ □U = {X ∈ VW | X ⊆ U} and ◇ ◇U = {X ∈ VW | X ∩ U ≠ ∅}.

Then, given (W, 𝔸), ξ : W → VW and U ∈ 𝔸 we obtain the classical semantics of □ and ◇ via w ⊩ □U ⇔ ξ(w) ∈ □ □U and w ⊩ ◇U ⇔ ξ(w) ∈ ◇ ◇U. From a logical point of view, we expand the signature of 𝔸 with two modal operators with the semantics determined as above.

This section focuses on the definition of VW which is independent of the algebraic signature. We also describe V𝔸 in case of the empty algebraic signature.

For every H, we introduce the set of abstract symbols L_{□}(H) = {□U | U ∈ 𝔸} and L_{◇}(H) = {◇U | U ∈ 𝔸}, and the relation ⊧ given by

X ⊧ □U ⇔ X ⊆ U and X ⊧ ◇U ⇔ X ∩ U ≠ ∅

for X ⊆ W and U ∈ 𝔸. Let Th_{□}(X) = {□U | X ⊧ □U}, and Th_{◇}(X) = {◇U | X ⊧ ◇U}. Th(X) = (Th_{□}(X), Th_{◇}(X)) is the modal theory of X. X, Y ⊆ W are modally equivalent, (X ≡_{Th} Y) iff Th(X) = Th(Y). For Φ ⊆ L_{□}, Ψ ⊆ L_{◇} let [[Φ]]_{□} = ⋂{U | □U ∈ Φ} and [[Ψ]]_{◇} = W \⋃{U | ◇U ∉ Ψ}. The following proposition is immediate.

Proposition 3.1 For all X ⊆ W, Φ ⊆ L_{□}, Ψ ⊆ L_{◇}

(i) X ⊆ [[Φ]]_{□} ⇔ Φ ⊆ Th_{□}(X) (ii) X ⊆ [[Ψ]]_{◇} ⇔ Th_{◇}(X) ⊆ Ψ

Both 1 and 2 above constitute a Galois connection (adjunction) and, writing [[⟨Φ, Ψ⟩]] = [[Φ]]_{□} ∩ [[Ψ]]_{◇}, we can combine them into one Galois connection [[−]] ⊣ ⟨Th_{□}, Th_{◇}⟩

PW^{(·)^{□◇}}  ^{⟨Th_{□} ,Th_{◇} ⟩}  (PL_{□})^{op} × PL_{◇}_{[[·]]}

In particular, (·)^{□◇} = [[·]] ∘ ⟨Th_{□}, Th_{◇}⟩, explicitly given as

X^{□◇} = ⋂\{U ∈ 𝔸 | X ⊧ □U\} ∩ (W \ ⋃\{U ∈ 𝔸 | X \begin{matrix}/ \\ ⊧ \end{matrix} ◇U\})

is a closure operator which maps X to the largest modally equivalent set. We call the sets X^{□◇} the modally closed sets.

Definition 3.2 Let (W, 𝔸) be a referential algebra for the empty signature. VW = {X ⊆ W | X = X^{□◇}}. V𝔸 = {□ □U | U ∈ 𝔸} ∪ {◇ ◇U | U ∈ 𝔸}. For f : (W, 𝔸) → (W′, 𝔸′), we put Vf : VW → VW′, X ↦ f[X]^{□◇}.

It is not difficult to check that (Vf)^{−1}(□ □U′) = □ □f^{−1}(U′), (Vf)^{−1}(◇ ◇U′) = ◇ ◇f^{−1}(U′). Hence (Vf)^{−1} is indeed a map V𝔸′ → V𝔸.

Remark 3.3

(i) The restriction to modally closed subsets in the definition of the Vietoris functor guarantees that differentiated referential algebras are mapped to differentiated ones.

(ii) Since this power construction based on modally closed subsets is standard in topology and domain theory, we would like to mention some relevant topological notions in the context of referential algebras H = (W, 𝔸). The specialization order is given by

w ≤ w′ ⇔ ∀a ∈ 𝔸 . w ∈ a ⇒ w′ ∈ a.

≤ is a preorder. H is differentiated if ≤ is a partial order. Every admissible set (ie every element in 𝔸) is upper.^{1} In fact, ≤ is the largest relation on W such that all admissible sets are upper. Upper sets coincide with the closure of the admissible sets under arbitrary unions and intersections. A set is saturated if it is an intersection of admissible sets; open if it is a union of admissibles; closed if it is a complement of an open. The sets [[Φ]]_{□} coincide with the saturated sets and the sets [[Ψ]]_{◇} with the closed sets. That is, a set is modally closed iff it is the intersection of a saturated and a closed set. In domain theory saturated and upper sets coincide and modally closed sets are rather called convex sets or lenses.

4 The Vietoris Functor for Referential Algebras

In this section, we assume a fully selfextensional logic S. Given an S-referential algebra (W, 𝔸), we will construct the Vietoris referential algebra (VW, V𝔸) in the following steps.

(i) Construct the free S-algebra G generated by {□U | U ∈ 𝔸} ∪ {◇U | U ∈ 𝔸}.

(ii) Define a collection of ‘modal S-filters’ M ≅ VW of G. (iii) Take the quotient (G^{∗}, M^{∗}) of (G, M) w.r.t. the modal S-filters M. (iv) Obtain (VW, V𝔸) as (isomorphic to) the dual (M^{∗}, \overline{G^{∗}}) of (G^{∗}, M^{∗}).

The first step is possible since S is fully selfextensional. For the second step, we assume that we can find a collection M of S-filters of G, called the modal S-filters, such that for every F ∈ VW there is a unique M_{F} ∈ M satisfying

C1. for every U ∈ 𝔸,

□U ∈ M_{F} ⇔ F ⊆ U and ◇U ∈ M_{F} ⇔ F ∩ U ≠ ∅,

and the following properties hold for S-atlases Q = ⟨G, M⟩, Q′ = ⟨G′, M′⟩ (obtained from referential algebras (W, 𝔸), (W′, 𝔸′))

1 Z ⊆ W is upper if x ∈ Z and x ≤ y implies y ∈ Z.

C2. Λ_{Q} is a congruence of G, C3. every ϕ : G → G′ induced by a referential algebra morphism (W′, 𝔸′) →

(W, 𝔸) is an atlas morphism ϕ : Q → Q′.

Roughly speaking C1 guarantees that M_{F} behaves like the modal theory of F, C2 allows us to take the quotient that will be the Vietoris algebra, and C3 takes care that the construction can also be carried out for morphisms.

To complete the second step, we note that, by C1, the map VW → M, F ↦ M_{F} is injective (and hence bijective):

Lemma 4.1 For every F, G ∈ VW, if F ≠ G, then M_{F} ≠ M_{G}.

Proof. If F ≠ G, then we can assume that x ∈ F \ G. Since G is modally closed, there is U ∈ 𝔸 such that either a) x ∉ U and G ⊧ □U or b) x ∈ U and G \begin{matrix}/ \\ ⊧ \end{matrix} ◇U. If a) then, using that if F ⊈ U then □U ∉ M_{F}, one shows that □U ∈ M_{G} \ M_{F}. If b) then, using that if G ∩ U = ∅ then ◇U ∉ M_{G}, one shows that ◇U ∈ M_{F} \ M_{G}. □

For the third step note that, if C2 holds, then we can consider the quotient algebra G^{∗} = G/Λ_{Q} and the canonical projection p : G ⟶ G^{∗}. C3 shows that morphisms G → G′ induce morphisms G^{∗} → G^{′∗}:

Lemma 4.2 For every h ∈ Hom(G, G′),

(i) if ⟨a, b⟩ ∈ Λ_{Q}, then ⟨h(a), h(b)⟩ ∈ Λ_{Q′}; (ii) the assignment h^{∗}(a) ⟼ p′(h(a)) for every a ∈ G defines a morphism

h^{∗} : G^{∗} → G^{′∗}.

Proof. First, for every M′ ∈ M′, if h(a) ∈ M′, then a ∈ h^{−1}(M′) ∈ M, so ⟨a, b⟩ ∈ Λ_{Q} implies that b ∈ h^{−1}(M′), i.e. h(b) ∈ M′. Second, if p(a) = p(b), then ⟨a, b⟩ ∈ Λ_{Q}, so ⟨h(a), h(b)⟩ ∈ Λ_{Q′}, i.e. p′(h(a)) = p′(h(b)). □

Let Q^{∗} = (G^{∗}, M^{∗}) be the quotient atlas, i.e., M^{∗} = {M_{F}^{∗} | F ∈ VW } where M_{F}^{∗} = p[M_{F}] for every F ∈ VW. Since p(a) = p(b) only if a ∈ M_{F} ⇔ b ∈ M_{F}, it holds that p^{−1}(p[M_{F}^{∗}]) = M_{F}^{∗} for every F ∈ VW. Therefore p is a strict and onto morphism between Q and Q^{∗}, and as Q is a fregean S-atlas, then Q^{∗} is a Frege-reduced S-atlas. In particular, M^{∗} is a collection of S-filters of G^{∗} and M^{∗} ≅ M. G^{∗} can be considered as the Vietoris algebra associated with 𝔸.

Finally, consider the dual ⟨M^{∗}, \overline{G^{∗}}⟩ of (G^{∗}, M^{∗}) which is an S-DRA (since (G^{∗}, M^{∗}) is an S-FRA) and the bijection θ : VW → M^{∗}, F ↦ M_{F}^{∗}. The inverse image map θ^{−1} : P(M^{∗}_{V}) ⟶ P(VW) restricts to a map Θ : \overline{G^{∗}} ⟶ P(VW). We define V𝔸 to be the image of Θ. The following diagram summarizes the construction.

(W, 𝔸) ^{f} (W′, 𝔸′) (G, M)_{p}  (G′, M′)_{p′}_{ϕ} (G^{∗}, M^{∗})  (G^{′∗}, M^{′∗})_{ϕ^{∗}} (M^{∗}, \overline{G^{∗}}) _{ϕ^{∗}^{−1}} (M′, \overline{G^{′∗}}) (VW, V𝔸) _{Vf}_{θ}  (VW′, V𝔸′)_{θ}

Definition 4.3 (Vietoris referential algebra) For every S-referential algebra H = (W, 𝔸), the Vietoris referential algebra of H is VH = ⟨VW, V𝔸⟩ with VW as in Definition 3.2 and V𝔸 given by the inverse image θ^{−1} as above. For every S-referential algebra morphism f : (W, 𝔸) → (W′, 𝔸′) let ϕ : G′ → G be the algebra morphism induced by f^{−1} : 𝔸′ → 𝔸 and Vf = θ^{−1} ∘ ϕ^{∗}^{−1} ∘ θ.

The interpretation of the modal operators is the intended one:

Proposition 4.4 Θ[\overline{p(□U)}] = □ □U and Θ[\overline{p(◇U)}] = ◇ ◇U for all U ∈ 𝔸.

Proof. For every F ∈ VW,

F ∈ Θ(\overline{p(□U)}) iff F ∈ θ^{−1}(\overline{p(□U)}) F ∈ Θ(\overline{p(◇U)}) iff F ∈ θ^{−1}(\overline{p(◇U)})
iff p[M_{F}] ∈ \overline{p(□U)}  iff p[M_{F}] ∈ \overline{p(◇U)}
iff p(□U) ∈ p[M_{F}]  iff p(◇U) ∈ p[M_{F}]
iff □U ∈ M_{F}  iff ◇U ∈ M_{F}
iff F ⊆ U  iff F ∩ U ≠ ∅
iff F ∈ □ □(U)  iff F ∈ ◇ ◇(U).
□

Vf is given by the direct image of f:

Proposition 4.5 Vf(F) = f[F]^{□◇} for all f : (W, 𝔸) → (W′, 𝔸′), F ∈ VW.

Proof. We elide the isomorphism p[·] : M → M^{∗}. For all U′ ∈ 𝔸′ we calculate f[F]^{□◇} ⊆ U′ ⇔ f[F] ⊆ U′ ⇔ F ⊆ f^{−1}(U′) ⇔ □f^{−1}(U′) ∈ M_{F} ⇔ ϕ(□U′) ∈ M_{F} ⇔ □U′ ∈ ϕ^{−1}(M_{F}) and similarly f[F]^{□◇} ∩ U′ ≠ ∅ ⇔ ◇U′ ∈ ϕ^{−1}(M_{F}). Since ϕ^{−1}(M_{F}) in M′, it follows from C1 that ϕ^{−1}(M_{F}) = M′_{f[F]^{□◇}} , that is, θ^{−1} ∘ ϕ^{−1} ∘ θ(F) = f[F]^{□◇}. □

Example 4.6 Let (W, 𝔸) a referential algebra for the empty signature.^{2} G is the set {□U | U ∈ 𝔸} ∪ {◇U | U ∈ 𝔸}. For M we choose the subsets satisfying C1.

C2 is trivially satisfied. For C3, we calculate ϕ^{−1}(M_{F}) = {t′ ∈ M_{F}′ | ϕ(t′) ∈ M_{F} } = {□U′ | □f^{−1}(U′) ∈ M_{F} } ∪ {◇U′ | ◇f^{−1}(U′)} = {□U′ | F ⊆ f^{−1}(U′)}∪{◇U′ | F ∩f^{−1}(U′) ≠ ∅} = {□U′ | f[F] ⊆ U′}∪{◇U′ | f[F]∩U′ ≠ ∅} = M′_{f[F]^{□◇}} . That V𝔸 and Vf agree with the previous Definition 3.2 follows from the two propositions above.

Another example will be considered in the next section.

5 Extended Example: Stone spaces

In this section, we are going to show that we can perform the construction of the Vietoris endofunctor on the referential algebras that correspond to Stone spaces under the embedding described in Section 2.2, and that this construction extends the familiar definition of the Vietoris endofunctor K on Stone spaces, i.e. that the following diagram commutes:

Stn ⟶^{K} Stn
↓  ↓
RA_{S} ⟶^{V} RA_{S}.

In this case, S is the classical propositional calculus, so the free S-algebra is the free Boolean algebra and S-filters are lattice filters. Let X = (X, Ω) be a Stone space, and let H = (X, 𝔸) be its associated referential algebra, i.e. 𝔸 is the Boolean algebra of the clopen subsets of X. As it is well known, the carrier of the Vietoris space K(X) is the set K(X) of the closed subsets of X and the Boolean algebra of clopen subsets of K(X) is generated by

□ □U = {X ∈ VW | X ⊆ U} and ◇ ◇U = {X ∈ VW | X ∩ U ≠ ∅},

for all U ∈ 𝔸. Therefore, Propositions 4.4 and 4.5 will take care of the commutativity of the diagram above, provided that:

(i) the family of the modally closed subsets of H coincides with K(X), (ii) there exists a family M of filters of the free Boolean algebra G generated

by the set of abstract symbols L(H) = L_{□}(H) ∪ L_{◇}(H), where L_{□}(H) = {□U | U ∈ 𝔸} and L_{◇}(H) = {◇U | U ∈ 𝔸}, that satisfies conditions C1 – C3 of Section 4.

Proposition 5.1 For every Stone space X = (X, Ω), VX = K(X).

Proof. (⊆) Clearly, every modally closed subset F^{□◇} = ⋂{U ∈ 𝔸 | F ⊧ □U\} ∩ (X \ ⋃\{U ∈ 𝔸 | F \begin{matrix}/ \\ ⊧ \end{matrix} ◇U\}) is closed. For the converse inclusion, let

2 The corresponding logic S has sequents Γ ⊢ ϕ ⇔ ϕ ∈ Γ; hence S-filters are just subsets.

F ∈ K(X), and let us show that F = F^{□◇}. ‘⊆’ is clear since (·)^{□◇} is a closure operator. For the converse note that, as X is a Stone space, then the clopen subsets form a base of Ω, hence F = ⋂{U ∈ 𝔸 | F ⊆ U}. □

Let G be the free Boolean algebra generated by L(H). It is a well known fact that the ultrafilters of a Boolean algebra are exactly the inverse homomorphic images of the top element of the two-element Boolean algebra 2. As G is free, then every h ∈ Hom(G, 2) is uniquely determined by its restriction to L(H). For every F ∈ K(X), let us consider h_{F} ∈ Hom(G, 2) defined by the following assignments: For every U ∈ 𝔸, h_{F} (□U) = 1 iff F ⊆ U and h_{F} (◇U) = 1 iff F ∩ U ≠ ∅. Let M_{F} = h_{F}^{−1}(1) be the corresponding ultrafilter of G. By construction it holds that for every F ∈ K(X), M_{F} is the only ultrafilter of G such that for every U ∈ 𝔸,

□U ∈ M_{F} iff F ⊆ U and ◇U ∈ M_{F} iff F ∩ U ≠ ∅.

So the collection M = {M_{F} | F ∈ K(X)} ⊆ Ultr(A) satisfies condition C1 of Section 4. Let us consider the atlas Q = (G, M). It is easy to see that for every collection U of ultrafilters of a Boolean algebra A the relation Λ_{U} on A, defined as aΛ_{U}b iff ∀V ∈ U(a ∈ V ⇔ b ∈ V), is a congruence of A. Hence Λ_{Q} is a congruence of G, so M satisfies condition C2 of Section 4. As for C3, let f : X → X′ be a continuous map, hence f ∈ Hom(H, H′). The following proposition shows that the corresponding homomorphism ϕ ∈ Hom(G′, G) between the associated free Boolean algebras is an atlas morphism ϕ : Q′ → Q.

Proposition 5.2 For every F ∈ K(X), ϕ^{−1}(M_{F}) = M_{f[F]}.

Proof. As M_{F} is an ultrafilter of G, then ϕ^{−1}(M_{F}) is an ultrafilter of G′. For every U ∈ 𝔸′, □U ∈ ϕ^{−1}(M_{F}) iff □f^{−1}(U) = ϕ(□U) ∈ M_{F}, iff F ⊆ f^{−1}(U), iff f[F] ⊆ U, iff □U ∈ M_{f[F]}. Likewise, one shows that ◇U ∈ ϕ^{−1}(M_{F}) iff ◇U ∈ M_{f[F]}. This is enough to prove the statement, for by construction, M_{f[F]} is the unique ultrafilter of G that contains the modal theory of f[F]. □

We finish this section by showing that the ultrafilters of the quotient algebra G^{∗} = G/Λ_{Q} are exactly the modal (ultra)filters M_{F}^{∗} = p[M_{F}], where p : G → G^{∗} is the canonical projection. Thus, G^{∗} is the Vietoris Boolean algebra.

Proposition 5.3 Ultr(G^{∗}) = M^{∗}.

The proof of this proposition uses the following standard fact about Boolean algebras:

Lemma 5.4 For every Boolean algebra A and every congruence Λ on A, the canonical projection p : A → A/Λ induces a bijective correspondence between Ultr(A/Λ) and the set of the ultrafilters V of A such that p^{−1}(p[V]) = V. In particular,

Ultr(A/Λ) = {p[V] | V ∈ Ultr(A) and p^{−1}(p[V]) = V }.

Let us show Proposition 5.3:

Proof. By Lemma 5.4, we have to show that M^{∗} = {p[V] | V ∈ Ultr(G) and p^{−1}(p[V]) = V }. Let us show that for every ultrafilter V of G, if p^{−1}(p[V]) = V, then V = M_{F} for some F ∈ K(X).

Suppose that there exists an ultrafilter V of G such that p^{−1}(p[V]) = V and V ≠ M_{F} for every F ∈ K(X). It is enough to show that there exists a ∈ V such that a ∉ M_{F} for every F ∈ K(X), for if it is so, then p(a) = 0, hence 0 ∈ p^{−1}(p[V]) = V, contradiction.

Let us consider the Stone space X_{G} which is dual to G. By the Stone duality, the points of X_{G} are the ultrafilters of G, and the clopen subsets of X_{G} are exactly the sets \overline{a} = \{U ∈ Ultr(G) | a ∈ U\}.

Let us consider the set M = {M_{F} | F ∈ K(X)} as a subset of X_{G}. We are supposing that V ∉ M. If we show that M is a closed subset of X_{G}, then by a standard compactness argument, V ∈ \overline{a} and \overline{a} ∩ M = ∅ for some clopen subset \overline{a} of X_{G}, i.e. there exists a ∈ V such that a ∉ M_{F} for every F ∈ K(X), which is what we want.

So let us show that M is a closed subset of X_{G}. Let K(X) be the Vietoris space of X, and let us consider the map ξ : K(X) ⟶ X_{G} defined by the assignment F ⟼ M_{F} for every F ∈ K(X). As K(X) is compact, then it is enough to show that ξ is continuous, i.e. that for every a ∈ G, ξ^{−1}(\overline{a}) is a clopen subset of K(X). By induction on the structure of a: As for the base, □ □U and ◇ ◇U are clopen subsets of K(X) for every clopen subset U of X, and

ξ^{−1}(\overline{□U}) = \{F ∈ K(X) | M_{F} ∈ \overline{□U}\} ξ^{−1}(\overline{◇U}) = \{F ∈ K(X) | M_{F} ∈ \overline{◇U}\}
= {F ∈ K(X) | □U ∈ M_{F} }  = {F ∈ K(X) | ◇U ∈ M_{F} }
= {F ∈ K(X) | F ⊆ U}  = {F ∈ K(X) | F ∩ U ≠ ∅}
= □ □U  = ◇ ◇U.

The inductive step is routine. □

6 Conclusion, Future Work, Open Problems

In this paper we presented a Vietoris space or powerdomain for a general notion of a state space equipped with an algebra of predicates. We expect this to have applications in such areas as the theory of systems, universal coalgebra, algebraic logic, modal logic, and lattice theory. In order to understand the import of this construction, more work will have to be carried out, some of which we sketch below.

Constructive definition of modal S-filters As we mentioned in the introduction, the aim of our research project is to characterize the selfextensional logics that support modalities, and we propose to use the construction of Section 4 for this characterization, namely to say that a selfextensional logic S supports classical modalities if and only if the construction of the Vietoris endofunctor V on the category of the (differentiated) S-referential algebras can be performed: then the V-coalgebras can be represented as referential algebras of the expanded algebraic signature, and the logic they will give rise to will be the classical modal expansion of S. The crucial step of this construction is that, for every S-referential algebra H, there exists the family of the modal S-filters of the free S-algebra over L_{□}(H) ∪ L_{◇}(H). In the case of Stone spaces, this family is constructed thanks to the existence of the schizophrenic object 2 in the category of Boolean algebras. A natural question is whether the existence of a schizophrenic object characterizes the situations in which the family of the modal S-filters can be constructively presented, or it is just a sufficient condition. As we mentioned in Section 2.2, a feature of the duality for selfextensional logics is that it uniformly accounts for a class of dualities that includes the Stone and Priestley dualities (which are induced by a schizophrenic object), as well as the Jónsson-Tarski one (which is not induced by a schizophrenic object). The question on whether the existence of a schizophrenic object is a characterizing condition or a sufficient one for the family of the modal S-filters to be constructively presented can also be relevant for comparing the Clark and Davey theory of natural dualities and the duality theory for selfextensional logics.

Other modal expansions In this paper we focused on expanding the language of S with a modal signature consisting of the normal operators □ and a ◇ that were interrelated like in the modal logic K. A further line of investigation is to extend this setting to modal expansions in which □ and ◇ are no more related like in the modal logic K, but are independent, or rather, they are related to one another like in the intuitionistic modal logic IK [Ser84], and so on. Other interesting modal expansions would include n-ary modal operators, and the list could continue. Each of these cases would correspond to defining an endofunctor on referential algebras. Perhaps extending the definitions of other hyperspace topologies to endofunctors on referential algebras would be a good starting point for a systematic investigation that would hopefully lead to a general methodology for wide classes of modal expansions.

Bounded lattice expansions An interesting line of investigation is about the connections with the Gehrke-Jónsson theory of bounded (distributive) lattice expansions. There is a non trivial interplay between these two settings: on the one hand, non-modal operators, like the strict implication of intuitionistic logic, are also included in the expansions treated there. On the other, in this work, as in the context of Abstract Algebraic Logic to which it belongs, the language of lattices and facts about them are systematically extended to the more general metatheory of logics.

References

[CD98] David M. Clark and Brian A. Davey. Natural Dualities for the Working Algebraist. Cambridge University Press, 1998.

[FJ96] Josep Maria Font and Ramon Jansana. A General Algebraic Semantics for Sentential Logics. Lecture Notes in Logic. Springer, 1996.

[GH01] Mai Gehrke and John Harding. Bounded lattice expansions. Journal of Algebra, 238(1):345 – 371, 2001.

[Joh82] Peter Johnstone. Stone Spaces. Cambridge University Press, 1982.

[Joh85] Peter Johnstone. Vietoris locales and localic semilattices. In R.- E. Hoffmann and K.H. Hofmann, editors, Continuous Lattices and their Applications, volume 101 of Lecture Notes in Pure and Applied Mathematics, pages 155–180. Marcel Dekker, 1985.

[KKV03] Clemens Kupke, Alexander Kurz, and Yde Venema. Stone coalgebras. In H.P. Gumm, editor, Coalgebraic Methods in Computer Science (CMCS’03), ENTCS, 2003.

[Pal02] Alessandra Palmigiano. A walk around selfextensionality. Technical report, University of Barcelona, 2002.

[Pal03a] Alessandra Palmigiano. A coalgebraic semantics for positive modal logic. In H.-P. Gumm, editor, Coalgebraic Methods in Computer Science (CMCS’03), ENTCS, 2003.

[Pal03b] Alessandra Palmigiano. Coalgebraic semantics for some intuitionistic modal logics. 2003.

[Ser84] Gisèle Fischer Servi. Axiomatizations for some intuitionistic modal logics. Rendiconti del Seminario Matematico dell’ Università Politecnica di Torino, 42(3):179 – 194, 1984.

[Wój73] R. Wójcicki. Matrix approach in the methodology of sentential calculus. Studia Logica, 32:7 – 37, 1973.

[Wój88] R. Wójcicki. Theory of Logical Calculi. Basic Theory of Consequence Operations., volume 199. Reidel, Dordrecht, 1988.