# Duality for Instantial Neighbourhood Logic via Coalgebra

Nick Bezhanishvili, Sebastian Enqvist, Jim De Groot

► To cite this version:

Nick Bezhanishvili, Sebastian Enqvist, Jim De Groot. Duality for Instantial Neighbourhood Logic via Coalgebra. 15th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2020, Dublin, Ireland. pp.32-54, 10.1007/978-3-030-57201-3_3. hal-03232350

HAL Id: hal-03232350

https://inria.hal.science/hal-03232350

Submitted on 21 May 2021

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Duality for Instantial Neighbourhood Logic via Coalgebra

Nick Bezhanishvili<fnref n="1" />, Sebastian Enqvist<fnref n="2" />, and Jim de Groot<fnref n="3" />

**Abstract.** Instantial Neighbourhood Logic (INL) has been introduced recently as a language for neighbourhood frames where existential information can be given about what kind of worlds occur in a neighbourhood of a current world. Apart from its semantics, its proof theory and bisimulation games have also been studied. However, conspicuously absent from the treatment of INL is the notion of *descriptive* frames. This is the gap that we are closing in this paper. We introduce descriptive frames for INL and we prove that these are dual to boolean algebras with instantial operators (BAIOs), which give the algebraic semantics of INL. Our methods for establishing this duality make essential use of coalgebra: we observe that BAIOs are algebras for a functor on the category of boolean algebras and show that this functor is dual to the double Vietoris functor (i.e. the composition of the Vietoris functor with itself), thus obtaining a dual equivalence between double Vietoris coalgebras and BAIOs. The proof of our main result is then completed by showing that double Vietoris coalgebras correspond precisely to descriptive frames. As a corollary we obtain that every extension of INL is sound and complete with respect to descriptive frames, that descriptive frames enjoy the Hennessy-Milner property, and as a result, that finite neighbourhood frames enjoy the Hennessy-Milner property.

**Keywords:** Duality · Modal logic · Instantial Neighbourhood Logic · Descriptive frames · Coalgebra.

## 1 Introduction

The concept of *duality* arises in many areas of mathematics, logic and computer science. The first duality milestone in algebraic logic was the Stone representation theorem [31], which described the categorical duality between boolean algebras and so-called Stone spaces. Subsequently, many representation and duality theorems have been established, including a representation theorem for Riesz spaces [38], Priestley duality for distributive lattices [28], and Esakia duality for (bi-)Heyting algebras [12,13,14,9].

<footnote n="1">¹ University of Amsterdam, Amsterdam, The Netherlands
n.bezhanishvili@uva.nl</footnote>

<footnote n="2">² Stockholm University, Stockholm, Sweden
sebastian.enqvist@philosophy.su.se</footnote>

<footnote n="3">³ The Australian National University, Canberra, Australia
jim.degroot@anu.edu.au (✉)</footnote>
The first representation theorem in the realm of modal logic was given by Jónsson and Tarski [20]. Although *op. cit.* does not mention modal logic explicitly, it introduces relational semantics and uses the representation theorem to relate algebraic and relational semantics. The full duality between boolean algebras with operators and descriptive general frames was established by Goldblatt [16], and many other dualities ensued [19,8,15,25].

These dualities are useful because they provide two, algebraic and geometric, perspectives on the same object and allow one to translate results from the algebraic language to the geometric one via (descriptive) frames, and vice versa. For example, this was a key ingredient in Sambin and Vaccaro's simplified proof of the celebrated Sahlqvist completeness theorem in modal logic [30].

A novel system of modal logic for reasoning about neighbourhood frames, called *Instantial Neighbourhood Logic* (INL), was recently introduced in [3]. The modalities in INL give existential information about what kind of worlds occur in a neighbourhood of a current world. Motivations for investigating this logic range from topology to games, and from modelling notions of evidence to belief revision. Surprisingly however, a duality result is still absent from the theory of INL, despite an abundance of recent interest in the logic [32,39,2,1,40].

This is the gap we are filling in this paper. We introduce a suitable notion of descriptive frames for INL and prove a (categorical) duality between descriptive INL-frames and boolean algebras with instantial operators (BAIOs). The latter give the algebraic semantics for INL and play the same rôle for INL that boolean algebras with operators play for normal modal logic [7,10] and boolean algebras with monotone operators for monotone modal logic [17,18].

Our main technical tool for establishing this duality is *coalgebra*. Coalgebras arise as the dual notion of *algebras for a functor* and have found many applications in logic and computer science. For example, they are a natural setting for dealing with non-wellfounded data structures such as streams or infinite trees, and, triggered by Moss' paper on coalgebraic logic [26], they have become a widely-used framework for describing semantics for modal logics [29,24,22,21].

A key feature of the coalgebraic perspective on duality is that, in a sense, it isolates the essential part of the duality. In the case of modal logic, the traditional approach of Jónsson-Tarski duality considers modal algebras as boolean algebras with operators, and directly constructs the dual Kripke frames. From the point of view of coalgebra, this turns out to really be a duality between *functors*. Once we identify modal algebras as the algebras for a certain functor on the category of boolean algebras and recognise its dual functor as the Vietoris functor, the duality between algebras and coalgebras for these two functors, which piggy-backs Stone duality, is a trivial consequence. The same approach works well for other variations of modal logic such as monotone modal logic [18] or positive modal logic (which piggy-backs on Priestley duality) [27]. While these examples have been re-cast in this style with hindsight, we believe that this coalgebraic approach serves as a useful blueprint for establishing dualities for new logics. If a logical system and its algebras are given, and a natural candidate for dual "descriptive frames" is suggested, then proceed as follows:
1. Describe the algebras of the logic as algebras for a functor.

2. Find the dual functor T.

3. Show that T-coalgebras are equivalent to descriptive frames.

In the current paper we use this strategy to prove a duality theorem for INL. First, we observe that BAIOs are algebras for a functor on the category of boolean algebras and homomorphisms. Second, we recall that it was observed in [3] that the neighborhood semantics of INL corresponds to coalgebras for the *double covariant powerset functor*. Since Kripke frames are coalgebras for the covariant powerset functor, and modal algebras are dual to Vietoris coalgebras, this suggests that BAIOs should be dual to coalgebras for the *double Vietoris functor*. We verify that this is indeed the case. Lastly, we show that our descriptive frames are precisely the “double Vietoris coalgebras”, in the sense that the categories are isomorphic. Hence, these descriptive frames are dual to BAIOs.

A rather trivial step in this proof is the representation of BAIOs as algebras for a functor $I$; the functor is simply read off from the defining equations of BAIOs. It was observed by Lutz Schröder (private communication) that the logic INL can be translated into the composition of standard modal logic with itself, and vice versa, in a semantics-preserving manner. This suggests that we could optionally have represented BAIOs as algebras for the functor $M \circ M$, where $M$ is the functor whose algebras correspond to modal algebras. Since $M$ is dual to the Vietoris functor, the dual equivalence of $M \circ M$-algebras with double Vietoris coalgebras would follow directly (in fact, as a special case of a more general result in [23]). While this alternative approach has a certain elegance to it, we have opted for a more direct representation of INL-algebras here. The main benefit is that our proof gives a quite standard canonical model construction for INL and its extensions, without a detour via a translation. This makes the duality better suited for dealing with issues like canonicity and Sahlqvist completeness, which we hope to address in future work. We obtain the equivalence of INL-algebras with algebras for $M \circ M$ as a corollary. Our proof also gives a representation of the double Vietoris functor where the topology is described in terms of the INL-modalities, rather than two layers of box and diamond modalities.

As a corollary of our main duality theorem we obtain that every extension of INL is sound and complete with respect to descriptive frames, that descriptive frames enjoy the Hennessy-Milner property, and as a result, that finite INL-frames enjoy the Hennessy-Milner property.

*Outline.* The paper is structured as follows: In Section 2 we recall the definitions of Instantial Neighbourhood Logic and its semantics, algebras and coalgebras, Stone duality, and the Vietoris functor. In Section 3 we define boolean algebras with instantial operators and descriptive INL-frames. The main results of the paper appear in Section 4, where we prove that the category of BAIOs is dually equivalent to the category of coalgebras for the double Vietoris functor, and in Section 5, where we identify coalgebras for the double Vietoris functor with descriptive INL-frames. Finally, we provide some applications of the developed theory in Section 6, and discuss possible direction for future work in Section 7.
Acknowledgements. The authors would like to thank the reviewers of CMCS 2020 for their helpful comments, which improved the presentation of the paper.

# 2 Preliminaries

## 2.1 Instantial neighbourhood logic

We briefly recall the language and semantics of instantial neighbourhood logic from [3]. The language $\mathcal{L}(\text{Prop})$ of instantial neighbourhood logic over some arbitrary but fixed set $\text{Prop}$ of proposition letters is defined recursively by

$$ \varphi ::= \top | p | \neg \varphi | \varphi \wedge \varphi | \Box (\varphi_1, \dots, \varphi_n; \varphi), $$

where $p \in \text{Prop}$ and $n \in \omega$. Observe that we have a countably infinite number of modal operators: one for each $n \in \omega$. Formulas in $\mathcal{L}(\text{Prop})$ can be interpreted in neighbourhood frames, which we shall call INL-frames.

**Definition 2.1.** An INL-frame is a pair $(X, N)$ comprised of a set $X$ and a neighbourhood functor $N : X \to \text{PPX}$, where $\text{P}$ is the (covariant) powerset functor. A neighbourhood model is a tuple $(X, N, V)$ where $(X, N)$ is a neighbourhood frame and $V : \text{Prop} \to \text{PX}$ is a valuation of the proposition letters.

An INL-morphism from $(X, N)$ to $(X', N')$ is a map $f : X \to X'$ such that

$$ N'(f(x)) = \{f[a] \mid a \in N(x)\}, $$

for all $x \in X$. Here $f[a]$ denotes the direct image of $a$ under $f$. An INL-morphisms $(X, N, V) \to (X', N', V')$ between neighbourhood models is an INL-morphism $f$ between the underlying frames which additionally satisfies

$$ x \in V(p) \quad \text{iff} \quad f(x) \in V'(p) $$

for every $p \in \text{Prop}$.

Write INL and INL$^M$ for the categories of neighbourhood frames and neighbourhood models, respectively, with their corresponding notion of morphism.

The interpretation of INL formulas in a neighbourhood model $(X, N, V)$ is defined recursively, where the classical connectives are treated in the standard manner. For the modalities, let $x \Vdash \Box (\varphi_1, \dots, \varphi_n; \psi)$ if there is a neighbourhood $w \in N(x)$ of $x$ such that $y \Vdash \psi$ for all $y \in w$, and for each $\varphi_i$ there is $y_i \in w$ such that $y_i \Vdash \varphi_i$. We write $\llbracket \varphi \rrbracket = \{x \in X \mid x \Vdash \varphi\}$ and say that $x$ satisfies $\varphi$ if $x \in \llbracket \varphi \rrbracket$. Two states are called logically equivalent if they satisfy precisely the same formulas.

The interpretation of the modalities can be conveniently reformulated using the following notion of witnesses.

**Definition 2.2.** Let $X$ be a set and $w, a_1, \dots, a_n, b$ subsets of $X$. We say that $w$ witnesses $(a_1, \dots, a_n; b)$ if and only if $w \cap a_i \neq \emptyset$ for all $i \in \{1, \dots, n\}$ and $w \subseteq b$. We say that $w$ co-witnesses $(a_1, \dots, a_n; b)$ if and only if $w \subseteq a_i$ for some $i \in \{1, \dots, n\}$ or $w \cap b \neq \emptyset$.
It is straightforward to see that in a neighbourhood model $(X, N, V)$ a state $x$ satisfies $\Box(\varphi_1, \dots, \varphi_n; \psi)$ if there is a $w \in N(x)$ witnessing $([\varphi_1]], \dots, [\varphi_n]]; [\psi])$.

**Definition 2.3.** Let $(X, N)$ be a neighbourhood frame. Define the map $m_{\square,n}: (PX)^{n+1} \to PX$ by

$$m_{\square,n}(a_1, \dots, a_n; b) = \{x \in X \mid \exists w \in N(x) \text{ which witnesses } (a_1, \dots, a_n; b)\}.$$

When there is no danger of confusion, we suppress the subscript $n$ from $m_{\square,n}$.

Yet another way to view the interpretation of the modalities in a neighbourhood model is via the equality $[[\Box(\varphi_1, \dots, \varphi_n; \psi)]] = m_{\square}([\varphi_1], \dots, [\varphi_n], [\psi])$.

## 2.2 Stone Duality

Write **BA** for the category of boolean algebras and homomorphisms, and **Stone** for the category of Stone spaces and continuous functions.

The contravariant functor **uf**: **BA** → **Stone** takes a boolean algebra $B$ to the collection **ufB** of ultrafilters of $B$ topologized by the base $\tilde{B} = \{(\lfloor b \rfloor) \mid b \in B\}$, where $(\lfloor b \rfloor) = \{u \in \text{ufB} \mid b \in u\}$. The action of **uf** on a homomorphism $h: B \to B'$ in **BA** is defined by $(\text{ufh})(u') = h^{-1}(u')$. In the converse direction, the contravariant functor **clp**: **Stone** → **BA** takes a Stone space to its boolean algebra of clopens and a continuous function to its inverse. The functors **uf** and **clp** constitute a dual equivalence between **BA** and **Stone**.

## 2.3 Algebra, Coalgebra, and the Vietoris functor

We recall the definitions of algebras, coalgebras, and the Vietoris functor.

**Definition 2.4.** Let $\mathbf{F}$ be an endofunctor on a category $\mathbf{C}$. An $\mathbf{F}$-coalgebra is a pair $(c, \gamma)$ such that $\gamma: c \to \mathbf{F}c$ is a morphism in $\mathbf{C}$. An $\mathbf{F}$-coalgebra morphism $(c, \gamma) \to (c', \gamma')$ is a morphism $f: c \to c'$ in $\mathbf{C}$ satisfying $\gamma' \circ f = \mathbf{F}f \circ \gamma$. The collection of $\mathbf{F}$-coalgebras and $\mathbf{F}$-coalgebra morphisms constitutes the category $\mathbf{Coalg}(\mathbf{F})$.

The dual notion of a coalgebra is that of an algebra: an $\mathbf{F}$-algebra is a morphism $\gamma: \mathbf{F}c \to c$ in $\mathbf{C}$, an $\mathbf{F}$-algebra morphism $(c, \gamma) \to (c', \gamma')$ is a morphism $f: c \to c'$ in $\mathbf{C}$ such that $\gamma' \circ \mathbf{F}f = f \circ \gamma$, and they form the category $\mathbf{Alg}(\mathbf{F})$.

Coalgebras for an endofunctor on **Set** are used to describe systems [29], but can also be used to characterise the frame semantics for a wide variety of modal logics [24]. In particular, as noted in [3, Section 7.5], we have:

**Proposition 2.5.** The category **INL** of INL-frames and INL-morphisms is isomorphic to $\mathbf{Coalg}(\mathbf{PP})$.

In the realm of modal logic a well-known example of a category of algebras is the category **MA** of modal algebras: we have $\mathbf{MA} \cong \mathbf{Alg}(\mathbf{M})$, where $\mathbf{M}$ is an endofunctor on the category **BA** of boolean algebras and homomorphisms defined as follows:
**Definition 2.6.** For a boolean algebra $B$ let $MB$ be the free boolean algebra generated by the set $\{\square a \mid a \in B\}$, modulo the relations $\square a \wedge \square b = \square(a \wedge b)$ and $\square \top = \top$. This assignment extends to an endofunctor on **BA** by defining the action of $M$ on a homomorphism $h : B \to B'$ via $Mh(\square a) = \square h(a)$ and extending this (uniquely) to $MB$.

A prime example of a category of coalgebras for an endofunctor on a category different from **Set** is the category **DGF** of descriptive general frames and appropriate morphisms. This is isomorphic to the category of coalgebras for the *Vietoris functor V* on **Stone**, the category of Stone spaces and continuous functions [23]. We recall the definition of the *Vietoris functor on Top* (originally introduced by Leopold Vietoris for compact Hausdorff spaces [37], see also [19, Section III.4] for a localic perspective), which restricts to the *Vietoris functor V* on **Stone**.

**Definition 2.7.** For a topological space $\mathcal{X}$ let $V'\mathcal{X}$ be the set of compact subsets of $\mathcal{X}$ topologized by

$$ \square a = \{b \in V'\mathcal{X} \mid b \subseteq a\}, \quad \diamond a = \{b \in V'\mathcal{X} \mid b \cap a \neq \emptyset\}, $$

where $a$ ranges over the open sets of $\mathcal{X}$. This is called the *Vietoris topology*. For a continuous function $f : \mathcal{X} \to \mathcal{X}'$ define $V'f : V'\mathcal{X} \to V'\mathcal{X}' : c \mapsto f[c]$, i.e. $V'f$ is the direct image of $f$. Then $V'$ defines a functor on **Top** called the *Vietoris functor*.

It is well known that $V'$ restricts to an endofunctor on **Stone**, which we denote by $V$. Moreover, if $\mathcal{X}$ is a Stone space then the topology on $V\mathcal{X}$ is generated by $\square a, \diamond a$, where $a$ ranges over the *clopen* subsets of $\mathcal{X}$. The fact that $V$ is the (Stone) dual of $M$ then implies

$$ MA \cong Alg(M) \cong^{\mathrm{op}} Coalg(V) \cong \mathrm{DGF}, $$

where we use $\cong$ to indicate an isomorphism of categories and $\cong^{\mathrm{op}}$ for a dual equivalence. For details we refer to [23].

## 3 BAIOs and general frames

In this section we define boolean algebras with instantial operators (BAIOs) and general INL-frames.

A boolean algebra with instantial operators comprises of a boolean algebra $B$ and an $\omega$-indexed family of functions, reflecting the infinite number of modal operators in INL, and provide algebraic semantics for instantial neighbourhood logic. They play the same rôle for INL that modal algebras play for normal modal logic [10,7] and boolean algebras with monotone operators for monotone modal logic [17,18].

A general INL-frame is an INL-frame together with a collection of “admissible subsets” which is closed under certain operations. As usual, these admissible subsets form a BAIO. In the converse direction, we will show that every BAIO gives rise to a general INL-frame.
**Definition 3.1.** A boolean algebra with *instantial operators* is a pair $(B, (f_n)_{n \in \omega})$ consisting of a boolean algebra $B$ and an $\omega$-indexed set of functions $f_n : B^{n+1} \to B$ satisfying the following equations for all $n \in \omega$:

$$ (B_1) \quad f_n(a_1, \dots, a_{n-1}, \perp; b) = \perp; $$

$$ (B_2) \quad f_n(a_1, \dots, a_i, a_{i+1}, \dots, a_n; b) = f_n(a_1, \dots, a_{i+1}, a_i, \dots, a_n; b); $$

$$ (B_3) \quad f_n(a_1, \dots, a_n; b) \le f_n(a_1, \dots, a_n \lor a'_n; b \lor b'); $$

$$ (B_4) \quad f_n(a_1, \dots, a_n; b) \le f_n(a_1, \dots, a_n \land b; b); $$

$$ (B_5) \quad f_n(a_1, \dots, a_n; b) \le f_{n+1}(a_1, \dots, a_n, c; b) \lor f_n(a_1, \dots, a_n; b \land \neg c); $$

$$ (B_6) \quad f_{n+1}(a_1, \dots, a_{n+1}; b) \le f_n(a_1, \dots, a_n; b); $$

$$ (B_7) \quad f_n(a_1, \dots, a_n; b) \le f_{n+1}(a_1, \dots, a_n, a_n; b). $$

A morphism between BAIOs $(B, (f_n)_{n \in \omega})$ and $(B', (f'_n)_{n \in \omega})$ is a boolean algebra homomorphism $h : B \to B'$ which satisfies

$$ h(f_n(a_1, \dots, a_n; b)) = f'_n(ha_1, \dots, ha_n; hb) $$

for all $a_i, b \in B$ and $n \in \omega$. The collection of BAIOs and BAIO morphisms forms a category (a variety of algebras, in fact) denoted by **BAIO**.

Every INL-frame $(X, N)$ gives rise to a BAIO, namely its complex algebra.

**Example 3.2.** Let $(X, N)$ be an INL-frame. Let $PX$ be the powerset of $X$ viewed as a boolean algebra and define $f_n(a_1, \dots, a_n; b) = m_\square(a_1, \dots, a_n; b)$. Then it is easy to verify that $(PX, (f_n)_{n \in \omega})$ is a BAIO. This is called the *complex algebra* of $(X, N)$.

**Example 3.3.** Recall that Prop is an arbitrary but fixed set of proposition letters and let $\mathcal{L} = \mathcal{L}(\text{Prop})$ be the collection of instantial formulas as defined in Subsection 2.1. Write $\varphi \equiv \psi$ if two formulas are provably equivalent in the axiomatization given in [3, Section 4] and write $[\varphi]$ for the equivalence class of $\varphi$ under $\equiv$. Then $\mathcal{L}/\equiv$ is a BAIO, where $f_n([\varphi_1], \dots, [\varphi_n]; [\psi])$ is defined to be $[\square(\varphi_1, \dots, \varphi_n; \psi)]$. This is of course the free BAIO generated by Prop, and is known as the Lindenbaum-Tarski algebra.

Towards a duality theorem for BAIOs, we define general INL-frames. These are INL-frames together with a subalgebra of their complex algebra.

**Definition 3.4.** A *general INL-frame* is a triple $(X, N, A)$ such that $(X, N)$ is an INL-frame and $A \subseteq PX$ is a collection of admissible sets that is closed under boolean operations and the operation $m_\square : (PX)^{n+1} \to PX$ (see Definition 2.3).

A *general INL-morphism* from $(X, N, A)$ to $(X', N'A')$ is an INL-morphism $f : (X, N) \to (X', N')$ satisfying $f^{-1}(a') \in A$ for all $a' \in A'$. Write **G-INL** for the category of general INL-frames and general INL-morphisms.

Since every algebra is a subalgebra of itself, every INL-frame can be seen as a general INL-frame:

**Example 3.5.** If $(X, N)$ is an INL-frame, then setting $A = PX$ yields a general INL-frame.
**Example 3.6.** For a BAIO $(B, (f_n)_{n \in \omega})$, let $ufB$ be the collection of ultrafilters of $B$ and let $\tilde{B} = \{|a| \mid a \in B\}$, where $|a| = \{u \in ufB \mid a \in u\}$. Define a neighbourhood function $N$ for $ufB$ via

$$N(u) = \{d \subseteq ufB \mid f_n(a_1, \dots, a_n; b) \in u \text{ whenever} \\ \qquad d \text{ witnesses } (|a_1|, \dots, |a_n|; |b|)\}.$$

Then $(ufB, N, \tilde{B})$ is a general INL-frame.

In the converse direction of Example 3.6 we have the functor $F: \mathbf{G-INL} \to \mathbf{BAIO}$ which sends a general INL-frame $(X, N, A)$ to $(A, (m_{\square,n})_{n \in \omega})$.

One can now ask whether **G-INL** can be restricted to a category of descriptive INL-frames such that the restriction of $F$ to these descriptive frames gives rise to a dual equivalence with **BAIO**. This turns out to be the case for the following definition of descriptive INL-frames:

**Definition 3.7.** A general INL-frame $(X, N, A)$ is called:

- *differentiated* if for any two distinct points $x, y \in X$ there is $a \in A$ such that $x \in a$ and $y \notin a$;

- *compact* if $\bigcap A' \neq \emptyset$ for any subset $A'$ of $A$ with the finite intersection property;

- *crowded* if for all $x \in X$ and $d \subseteq X$ such that $d \notin N(x)$ we can find $a_1, \dots, a_n, b$ such that $d$ witnesses $(a_1, \dots, a_n; b)$ while no $d' \in N(x)$ witnesses $(a_1, \dots, a_n; b)$.

A descriptive INL-frame is a general INL-frame that is differentiated, compact and crowded. Denote by **D-INL** the full subcategory of **G-INL** whose objects are descriptive INL-frames.

The notion of crowdedness is the INL analogue of the tightness condition for normal modal logic [7, Definition 5.65]. Intuitively, it states that $N(x)$ is, in a sense, determined by the admissible subsets. In passing, we make the following observation, the proof of which is straightforward.

**Proposition 3.8.** Let $(X, N)$ be an INL-frame and suppose $X$ is finite. Then $A = \mathbf{P}X$ is the unique set of admissible sets making $(X, N, A)$ a descriptive INL-frame.

We aim to prove the following duality result:

**Theorem 3.9.** We have a dual equivalence

$$\mathbf{D-INL} \equiv^{\mathrm{op}} \mathbf{BAIO}.$$

In order to prove this, we adhere to the strategy suggested in the introduction. First we identify **BAIO** with the category of algebras for some functor $\mathbf{|}$ on **BA**,
then we determine the (Stone) dual of $\mathbf{l}$, and finally, we show that descriptive INL-frames are precisely coalgebras for this dual functor. In a diagram:

<figure><img src="image_2.png" /></figure>

Concretely, the dual equivalence from Theorem 3.9 will be given by the construction from Example 3.6 and the subsequent paragraph, see Remark 5.7 below.

# 4 Duality

We show that BAIOs are algebras for the functor $\mathbf{l} : \mathbf{BA} \to \mathbf{BA}$, and that $\mathbf{l}$ is the (Stone) dual of the double Vietoris functor $\mathbf{VV}$ on **Stone**. As a consequence we obtain an algebra/coalgebra duality in Theorem 4.12.

**Definition 4.1.** Let $B$ be a boolean algebra. Abbreviate $(\mathbf{a}; b) = (a_1, \dots, a_n; b)$ for an $(n+1)$-tuple of elements of $B$. Let $\mathbf{l}B$ be the boolean algebra generated by $\square(a_1, \dots, a_n; b)$, where $n \in \omega$ and $a_i, b \in B$, subject to the relations

$$ (I_1) \quad \square(\mathbf{a}, \perp; b) = \perp; $$

$$ (I_2) \quad \square(a_1, \dots, a_i, a_{i+1}, \dots, a_n; b) = \square(a_1, \dots, a_{i+1}, a_i, \dots, a_n; b); $$

$$ (I_3) \quad \square(\mathbf{a}, c; b) \leq \square(\mathbf{a}, c \lor c', b \lor b'); $$

$$ (I_4) \quad \square(\mathbf{a}, c; b) \leq \square(\mathbf{a}, c \land b; b); $$

$$ (I_5) \quad \square(\mathbf{a}; b) \leq \square(\mathbf{a}, c; b) \lor \square(\mathbf{a}; b \land \neg c); $$

$$ (I_6) \quad \square(\mathbf{a}, c; b) \leq \square(\mathbf{a}; b); $$

$$ (I_7) \quad \square(a_1, \dots, a_n; b) \leq \square(a_1, \dots, a_n, a_n; b). $$

For a homomorphism $f : B \to B'$ define $\mathbf{l}f : \mathbf{l}B \to \mathbf{l}B'$ on generators by

$$ (\mathbf{l}f)(\square(a_1, \dots, a_n; b)) = \square(f(a_1), \dots, f(a_n); f(b)). $$

The assignment $\mathbf{l}$ determines an endofunctor on **BA**, called the *instantial functor*.

Item $I_2$ of Definition 4.1 allows us to put the $a_i$ in any desired order. In $I_4$ equality holds because of $I_3$ and in $I_7$ equality holds because of $I_6$. The proof of the following theorem is standard.

**Theorem 4.2.** BAIO = Alg($\mathbf{l}$).

As stated in the introduction, it seems reasonable to expect that the double Vietoris functor $\mathbf{VV}$ is the dual of $\mathbf{l}$ under the dual equivalence between boolean algebras and Stone spaces. We prove that this is indeed the case. More concretely, we give a natural isomorphism

$$ \mathbf{u}f \circ \mathbf{l} \circ \mathbf{clp} \to \mathbf{VV}. \qquad (2) $$
We first work towards an isomorphism $uf \circ l \circ clp\mathbb{X} \cong VV\mathbb{X}$, where $\mathbb{X}$ is a Stone space. Lemma 4.11 then states that the collection of these isomorphisms is in fact natural. This ultimately proves the duality between (the categories of) l-algebras and VV-coalgebras (Theorem 4.12).

We commence by giving an alternative subbase for the double Vietoris topology, which is tailored to our specific needs.

**Proposition 4.3.** Let $\mathbb{X}$ be a Stone space. The topology on $VV\mathbb{X}$ is generated by the clopen subbase

$$ \Box(a_1, \dots, a_n; b) = \{W \in VV\mathbb{X} \mid \exists w \in W \text{ s.t. } w \text{ witnesses } (a_1, \dots, a_n; b)\}, $$

$$ \Diamond(a_1, \dots, a_n; b) = \{W \in VV\mathbb{X} \mid \forall w \in W \text{ w co-witnesses } (a_1, \dots, a_n; b)\}, $$

where the $a_i, b$ range over the clopen subsets of $\mathbb{X}$.

*Proof.* The given sets are clopen in $VV\mathbb{X}$, because

$$ \Box(a_1, \dots, a_n; b) = \Diamond(\Diamond a_1 \cap \dots \cap \Diamond a_n \cap \Box b) $$

and

$$ \Diamond(a_1, \dots, a_n; b) = \Box(\Box a_1 \cup \dots \cup \Box a_n \cup \Diamond b). $$

In order to show that they are a subbase for the topology on $VV\mathbb{X}$, we must show that $\Box A$ and $\Diamond A$ are boolean combinations of clopens of the form $\Box(a; b)$ and $\Diamond(a; b)$, where $A$ is clopen in $V\mathbb{X}$. Note that $A$ can be written as the finite intersection of finite unions of clopens in $V\mathbb{X}$ of the form $\Box a, \Diamond a$. Moreover, we may assume that there is a single diamond in each finite union because diamonds distribute over unions. So we may write $A = \bigcap_{i=1}^{n} (\Box a_1 \cup \dots \cup \Box a_{m_i} \cup \Diamond b_i)$. This implies

$$ \Box A = \bigcap_{i=1}^{n} \Box (\Box a_1 \cup \dots \cup \Box a_{m_i} \cup \Diamond b_i) = \bigcap_{i=1}^{n} \Diamond (a_1, \dots, a_{m_i}; b_i). $$

Similarly, writing $A$ as a finite union of finite intersections, $\Diamond A$ can be expressed as a finite union of clopens of the form $\Box(a_1, \dots, a_n; b)$. $\Box$

We note that the statement of Proposition 4.3 holds for any topological space $\mathbb{X}$ if we require the $a_i$ and $b$ to be range over the open subsets of $\mathbb{X}$. The proof of this is slightly more involved because it crucially uses compactness of the elements of $V\mathbb{X}$.

**Remark 4.4.** Recall that ultrafilters correspond bijectively to homomorphisms into $\mathbb{Z}$, the two-element boolean algebra. For an ultrafilter $u$ in $B$ let $p: B \to \mathbb{Z}$ be the corresponding homomorphism. Then $p(b) = \top$ iff $b \in u$. We will use these two perspectives interchangeably.

We now define a map $\xi: uf \circ l \circ clp\mathbb{X} \to VV\mathbb{X}$, where $\mathbb{X}$ is a Stone space. These will form the components of the intended natural transformation from
(2). Although such a map can be defined for any Stone space $\mathcal{X}$, and therefore the definition actually yields a **Stone-indexed collection of maps $(\xi_X)_{X \in \text{Stone}}$, we shall refrain from writing this subscript until Theorem 4.11, where we prove that this collection is a natural transformation.

Intuitively, to an ultrafilter $p$ we want to attach a closed subset $W_p$ of $\mathcal{V}\mathcal{X}$ that satisfies $W_p \in \Box(a_1, \dots, a_n; b)$ if and only if $p(\Box(a_1, \dots, a_n; b)) = \top$. In our definition, we guarantee the implication from left to right by “killing the witnesses”: If $p(\Box(a_1, \dots, a_n; b)) = \bot$, then we make sure that none of the witnesses of $(a_1, \dots, a_n; b)$ is in $W_p$. In other words, we stipulate that $W_p$ be disjoint from $\Diamond a_1 \cap \dots \cap \Diamond a_n \cap \Box b$.

**Definition 4.5.** For a Stone space $\mathcal{X}$, define $\xi: \text{uf} \circ \text{l} \circ \text{clp}\mathcal{X} \to \mathcal{V}\mathcal{V}\mathcal{X}$ by sending an ultrafilter $p$ to

$$W_p = \mathcal{V}\mathcal{X} \setminus \bigcup \{\Diamond a_1 \cap \dots \cap \Diamond a_n \cap \Box b \mid p(\Box(a_1, \dots, a_n; b)) = \bot\}.$$

Since $W_p$ is the complement of a union of clopen subsets of $\mathcal{V}\mathcal{X}$, it is closed in $\mathcal{V}\mathcal{X}$, hence an element of $\mathcal{V}\mathcal{V}\mathcal{X}$. Therefore $\xi$ is well defined. For the converse direction we need the following definition.

**Definition 4.6.** For a Stone space $\mathcal{X}$, define

$$\theta: \mathcal{V}\mathcal{V}\mathcal{X} \to \text{uf} \circ \text{l} \circ \text{clp}\mathcal{X} : W \mapsto p_W,$$

where $p_W: \text{l}(\text{clp}\mathcal{X}) \to 2$ is given on generators by

$$p_W: \text{l} \circ \text{clp}\mathcal{X} \to 2: \Box(\boldsymbol{a}; b) \mapsto \begin{cases} \top & \text{if } W \in \Box(\boldsymbol{a}; b) \\ \bot & \text{otherwise} \end{cases}$$

**Lemma 4.7.** *The assignment $\theta$ is well defined.*

*Proof.* In order to show that $\theta$ is well defined, we need to show that $p_W$ is an ultrafilter, that is, a boolean algebra homomorphism $\text{l} \circ \text{clp}\mathcal{X} \to 2$. Since $\text{l}$ is defined by generators and relations it suffices to show that the images of the generators under $p_W$ satisfy the relations $I_1$ through $I_7$. We leave this straightforward verification to the reader. $\square$

The following lemma provides the key ingredient for proving that $\xi$ and $\theta$ are continuous and inverses of each other.

**Lemma 4.8.** Let $\mathcal{X}$ be a Stone space. We have

$$W_p \in \Box(\boldsymbol{a}; b) \quad \text{if and only if} \quad p(\Box(\boldsymbol{a}; b)) = \top.$$

*Proof.* If $p(\Box(\boldsymbol{a}; b)) = \bot$, then by construction $W_p \notin \Box(\boldsymbol{a}; b)$. So suppose $W_p \notin \Box(\boldsymbol{a}, b)$. Then for every witness $w$ of $(\boldsymbol{a}, b)$ there exists $(c_w, d_w)$ which is witnessed by $w$ and is such that $p(\Box(c_w, d_w)) = \bot$.

The collection of witnesses is the set $A = \Diamond a_1 \cap \dots \cap \Diamond a_n \cap \Box b$. This is a closed set of $\mathcal{V}\mathcal{X}$, and it is covered by the collection

$$\{\Diamond c_{w,1} \cap \dots \cap \Diamond c_{w,m_w} \cap \Box d_w \mid w \in A\}.$$
Clearly this set is an open covering of A, so by compactness of $V\mathbb{X}$ there must be a finite subcover of A. That is

$$A \subseteq \bigcup_{w \in A'} (\diamond c_{w,1} \cap \dots \cap \diamond c_{w,m_w} \cap \Box d_w),$$

where $A'$ is some finite subset of A serving as an index. Now it follows from Lemma 4.9 below that $p(\Box(\boldsymbol{a}; b)) = \perp$. $\square$

The following technical result is motivated by the proof of Lemma 4.8.

**Lemma 4.9.** Let $\mathbb{X}$ be a Stone space, $a_i, b, c_j, d \in \mathrm{clp}\mathbb{X}$. Suppose $A = \diamond a_1 \cap \dots \cap \diamond a_n \cap \Box b$ is covered by the finite set $\{C_i = \diamond c_{i,1} \cap \dots \cap \diamond c_{i,n_i} \cap \Box d_i \mid 1 \le i \le m\}$. Suppose $p : \mathbb{I} \circ \mathrm{clp}\mathbb{X} \to 2$ is a point and $p(\Box(c_{i,1}, \dots, c_{i,n_i}; d_i)) = \perp$ for all $C_i$ in the given cover. Then $p(\Box(a_1, \dots, a_n; b)) = \perp$.

*Proof.* If $A = \emptyset$ the lemma is trivial, so henceforth we shall assume $A \neq \emptyset$.

**Part 1.** Since (clearly) $b \in A$ there must be a $C_i$ containing $b$. Call this $C = \diamond c_1 \cap \dots \cap \diamond c_k \cap \Box d$. Now consider $b_j := b \setminus c_j$. This is not in $C$. If it is not in $A$, then we must have $c_j \supseteq a_i$ for some $i$, because clearly $b_j \subseteq b$. If it is in $A$, then it must be in another element of the cover, say, $C_j = \diamond c_{j1} \cap \dots \cap \diamond c_{jn_j} \cap \Box d_j$. Observe that $b_j = b \setminus c_j \subseteq d_j$.

Next, consider $b_{j,k} := b \setminus (c_j \cup c_{jk})$, where $1 \le k \le n_j$. If this is not in $A$, then we must have $a_i \subseteq c_j \cup c_{jk}$ for some $i$. If it is in $A$, then it must be in one of the elements of the cover, say, $C_{jk} = \diamond c_{jk,1} \cap \dots \cap \diamond c_{jk,n_j} \cap \Box d_{jk}$. Note that $b_{j,k}$ is not in $C$ and not in $C_j$ by construction. Again, observe that $b_{j,k} \subseteq d_{jk}$. Continuing this way gives a tree, see the diagram below for intuition.

Each $b_{j_1,j_2,\dots,j_k} = b \setminus (c_{j_1} \cup c_{j_1j_2} \cup \dots \cup c_{j_1j_2\dots j_k})$ is in none of the preceding cover elements. Since we started with a finite cover, this process must terminate, i.e. the branches of our tree must be finite. That is, at some point $b_{j_1,j_2,\dots,j_k}$ is not in $A$, and since clearly $b_{j_1,j_2,\dots,j_k} \subseteq b$, it must be the case that $b_{j_1,j_2,\dots,j_k} \notin \diamond a_i$ for some $a_i$, i.e. we must have $a_i \subseteq (c_{j_1} \cup c_{j_1j_2} \cup \dots \cup c_{j_1j_2\dots j_k})$.

**Part 2.** Now we have set ourselves up for the proof of the proposition. We will use rule $I_5$ finitely many times. The first step is:

$$\Box (\boldsymbol{a}; b) \le \Box (\boldsymbol{a}, c_1; b) \lor \Box (\boldsymbol{a}; b \setminus c_1). \quad (3)$$

We continue using $I_5$ as follows: given an element of the form $\Box(\boldsymbol{a}, \boldsymbol{c}; b_{j_1, j_2, \dots, j_k})$ we verify what is the lowest entry $l$ such that $c_{j_1 j_2 \dots j_k}^l$ is not in $\boldsymbol{c}$, and apply $I_5$ using this. It can be seen that (3) above is also obtained in this way. Thus the first two iterations are:

$$\begin{align*}
\Box(\boldsymbol{a}; b) &\le \Box(\boldsymbol{a}, c_1; b) &\lor \Box(\boldsymbol{a}; b \setminus c_1) \\
&\le \Box(\boldsymbol{a}, c_1, c_2; b) &\lor \Box(\boldsymbol{a}, c_1; b_2) &\lor \Box(\boldsymbol{a}, c_{11}; b_1) &\lor \Box(\boldsymbol{a}; b_{1,11})
\end{align*}$$

For an entry, we cannot proceed if either all $c_{j_1 \dots j_k}^l$ from a $C_{j_1 \dots j_k}$ in the tree already occur in $\boldsymbol{c}$, or if the thing we subtract from $b$, i.e. $c_{j_1} \cup c_{j_1j_2} \cup \dots \cup c_{j_1j_2 \dots j_k}$
<figure><img src="image_3.png" /></figure>

contains one of the $a_i$ (for then $c_{j_1j_2...j_k, \ell}$ is not defined). In the first case, we have

$$ \begin{aligned} & \square(\boldsymbol{a}, \boldsymbol{c}; b \setminus (c_{j_1} \cup c_{j_1j_2} \cup \dots \cup c_{j_1j_2\dots j_k})) \\ & \leq \square(c_{j_1\dots j_k, 1}, \dots, c_{j_1\dots j_k, n_{j_1\dots j_k}}; d_{j_1\dots j_k}). \end{aligned} \quad (4) $$

The inequality follows from using $I_6$ a lot, and applying $I_3$ to the fact that $b_{j_1,j_2,...,j_k} \subseteq d_{j_1...j_k}$. As the right hand side of (4) is one of the elements in the cover, we get

$$ \begin{aligned} & p(\square(\boldsymbol{a}, \boldsymbol{c}; b \setminus (c_{j_1} \cup c_{j_1j_2} \cup \dots \cup c_{j_1j_2\dots j_k}))) \\ & \leq p(\square(c_{j_1\dots j_k, 1}, \dots, c_{j_1\dots j_k, n_{j_1\dots j_k}}; d_{j_1\dots j_k})) = \perp. \end{aligned} $$

In the second case, we get $\perp$ because the intersection of one of the $a_i$ and $b_{j_1j_2...j_k}$ is empty, and we use $I_4$ and $I_1$.

Since this procedure is finite, this yields $\square(\boldsymbol{a}; b) \leq \perp$, as desired. $\square$

As a corollary of Lemma 4.8 we obtain the following lemma.

**Lemma 4.10.** The maps $\theta$ and $\xi$ are continuous and each others inverses. Hence $\xi$ is a homeomorphism.

*Proof.* We first prove continuity. The open subsets of $uf \circ l \circ clpX$ are generated by $\langle\square(\boldsymbol{a}; b)\rangle = \{p \mid p(\square(\boldsymbol{a}; b)) = \top\}$, where $(\boldsymbol{a}; b) = (a_1, \dots, a_n; b)$ is an $(n+1)$-tuple of clopen subsets of $X$. We have

$$ \begin{aligned} \theta^{-1}(\square(\boldsymbol{a}; b)) &= \theta^{-1}(\{p \mid p(\square(\boldsymbol{a}; b)) = \top\}) \\ &= \{W \in \mathcal{W}\mathcal{W}X \mid W \in \Box(\boldsymbol{a}; b)\} = \Box(\boldsymbol{a}; b), \end{aligned} $$

which is clopen in $\mathcal{W}\mathcal{W}X$. Similarly $\xi^{-1}(\Box(\boldsymbol{a}; b)) = \{p \mid W_p \in \Box(\boldsymbol{a}; b)\} = \langle\square(\boldsymbol{a}; b)\rangle$.
We now show prove $\xi \circ \theta$ and $\theta \circ \xi$ are identities. For the former, observe
that Lemma 4.8 implies $p(\square(\boldsymbol{a}; b)) = \top$ iff $W_p \in \square(\boldsymbol{a}; b)$ iff $p_{W_p}(\square(\boldsymbol{a}; b)) = \top$.
So $p$ and $p_W$ coincide on the generators of $l(clp\mathbb{X})$, therefore $p = p_{W_p}$ and hence
$\theta \circ \xi = \mathrm{id}_{uf \circ l \circ clp\mathbb{X}}$.

To see that $\xi \circ \theta = \mathrm{id}_{VV\mathbb{X}}$, note that it suffices to show that $W$ and $W_{pW}$
are in the same generating opens of the topology. Since the diamond is dual to
the box it suffices to show that $W \notin \square(\boldsymbol{a}; b)$ iff $W_{pW} \notin \square(\boldsymbol{a}; b)$.
This is easy: $W \notin \square(\boldsymbol{a}; b)$ iff $p_W(\square(\boldsymbol{a}, b)) = \bot$ iff $W_{pW} \notin \square(\boldsymbol{a}; b)$.
The first “iff” holds by definition of $\theta$, the second by Lemma 4.8. $\square$

Each Stone space $\mathbb{X}$ gives rise to a homeomorphism $\xi$, so we get a transformation $(\xi_X)_{X \in \text{Stone}} : uf \circ l \circ clp \to VV$. This transformation is in fact natural:

**Lemma 4.11.** *The collection $\xi = (\xi_X)_{X \in \text{Stone}} : uf \circ l \circ clp \to VV$ is a natural isomorphism.*

*Proof.* We have already seen that $\xi_X$ is a homeomorphism for every Stone space $\mathbb{X}$ (i.e. an isomorphism in **Stone**), so it is left to show naturality. That is, where $f: \mathbb{X} \to \mathbb{X}'$ is a continuous function we need to show that

$$ \begin{aligned} \text{uf} \circ l \circ clp\mathbb{X} &\xrightarrow{\xi_X} VV\mathbb{X} \\ \text{uf} \circ l \circ clp f &\searrow^{\xi_X} VVf \\ \text{uf} \circ l \circ clp\mathbb{X}' &\xrightarrow{\xi_X} VV\mathbb{X}' \end{aligned} $$

commutes. Since elements of a Stone space are uniquely determined by the clopen
sets in which they are contained, it suffices to show that for all $p \in \mathrm{uf} \circ l \circ clp\mathbb{X}$
and $a_i, b \in clp\mathbb{X}$ we have

$$ VVf(\xi_X(p)) \in \square(\boldsymbol{a}; b) \quad \text{iff} \quad \xi_{X'}(\mathrm{uf} \circ l \circ clp f(p)) \in \square(\boldsymbol{a}; b). $$

This follows from a straightforward computation:

$$ \begin{array}{l@{\qquad}l} \mathrm{VVf}(\xi_X(p)) \in \square(\boldsymbol{a}; b) & \begin{array}{l} \text{iff } \xi_X(p) \in (VVf)^{-1}(\square(\boldsymbol{a}; b)) \\ \text{iff } \xi_X(p) \in \square(f^{-1}\boldsymbol{a}; f^{-1}b) \\ \text{iff } p(\square(f^{-1}\boldsymbol{a}; f^{-1}b)) = \top \\ \text{iff } p(l \circ clpf(\square(\boldsymbol{a}; b))) = \top \\ \text{iff } \mathrm{uf} \circ l \circ clpf(p)(\square(\boldsymbol{a}; b)) = \top \\ \text{iff } \xi_{X'}(\mathrm{uf} \circ l \circ clpf(p)) \in \square(\boldsymbol{a}; b) \end{array} \end{array} $$

We conclude that $(\xi_X)_{X \in \text{Stone}}$ is indeed a natural isomorphism.

$\square$

As an immediate corollary we obtain the main theorem of this section.

**Theorem 4.12.** *We have a dual equivalence*

$$ \mathbf{Alg}(l) \equiv^{\mathrm{op}} \mathbf{Coalg}(VV). $$

As $V$ is dual to the functor $M$ on boolean algebras, we obtain the following
corollary which confirms the intuition that INL is “modal logic taken twice”.

**Corollary 4.13.** *The functor $l$ is naturally isomorphic to the composition $M \circ M$.*
# 5 Descriptive frames as coalgebras

We show that the descriptive frames from Definition 3.7 are precisely coalgebras for the double Vietoris functor $VV$.

**Theorem 5.1.** We have

$$D-INL \cong \mathrm{Coalg}(VV).$$

A helpful tool in the proof of Theorem 5.1 is the notion of the largest representative of a set $d \subseteq X$ in a general INL-frame $(X, N, A)$.

**Definition 5.2.** Let $(X, N, A)$ be a general INL-frame and $d \subseteq X$. Then we define the largest representative of $d$ to be

$$\bar{d} = \bigcap \{a \in A \mid d \subseteq a\}.$$

This is of course the topological closure of $d$ in the topology on $X$ generated by the clopen base $A$. It enjoys the following useful properties.

**Lemma 5.3.** Let $(X, N, A)$ be a general INL-frame, $d \subseteq X$ and $a_1, \dots, a_n, b \in A$. Then $d$ witnesses $(a_1, \dots, a_n; b)$ if and only if $\bar{d}$ does.

*Proof.* We show that $d \cap a_i \neq \emptyset$ iff $\bar{d} \cap a_i \neq \emptyset$ and $d \subseteq b$ iff $\bar{d} \subseteq b$. It is easy to see that this proves the lemma. Suppose $d \cap a_i \neq \emptyset$. Since $d \subseteq \bar{d}$ we also have $\bar{d} \cap a_i \neq \emptyset$. Conversely, if $d \cap a_i = \emptyset$ then $d \subseteq X \setminus a_i$ and since the latter is in $A$ we have $\bar{d} \subseteq X \setminus a_i$. This implies $\bar{d} \cap a_i = \emptyset$. Next suppose $d \subseteq b$, then by definition $\bar{d} \subseteq b$, because $b \in A$. Conversely, if $\bar{d} \subseteq b$ we have $d \subseteq \bar{d} \subseteq b$. $\square$

**Lemma 5.4.** Let $(X, N, A)$ be a descriptive INL-frame, $d \subseteq X$ and $x \in X$. Then $d \in N(x)$ if and only if $\bar{d} \in N(x)$.

*Proof.* This follows directly from the proof of Lemma 5.3. $\square$

The following two lemmas describe the object part of the isomorphism from Theorem 5.1.

**Lemma 5.5.** Let $(X, \gamma)$ be a $VV$-coalgebra. Write $X$ for the space underlying $X$ and let $N_\gamma(x) = \{d \subseteq X \mid \bar{d} \in \gamma(x)\}$. Then $(X, N_\gamma, \mathrm{clp}X)$ is a descriptive INL frame.

*Proof.* We know that $\mathrm{clp}X$ is closed under boolean operations and it follows from continuity of $\gamma$ that $\mathrm{clp}X$ is closed under $m_\square$. Furthermore, $(X, N_\gamma, \mathrm{clp}X)$ is differentiated because $X$ is Hausdorff and compact because $X$ is compact.

Lastly, we show that it is crowded. Suppose $c \notin N_\gamma(x)$. Without loss of generality we may assume $c$ to be closed, hence an element of $VX$, because we know from Lemma 5.3 that $c$ and $\bar{c}$ witness precisely the same tuples. It follows from the definition of $N_\gamma$ that $c \notin \gamma(x)$. Since $\gamma(x)$ is a closed subset of $VX$, there must be a basic clopen $\diamond a_1 \cap \dots \cap \diamond a_n \cap \square b$ containing $c$ and disjoint from $\gamma(x)$. Therefore $c$ witnesses $(a_1, \dots, a_n; b)$ while none of the elements in $\gamma(x)$ witness $(a_1, \dots, a_n; b)$. It then follows from the definition of $N_\gamma$ and Lemma 5.3 that none of the $d \in N_\gamma(x)$ witness $(a_1, \dots, a_n; b)$. Therefore $(X, N_\gamma, \mathrm{clp}X)$ is crowded. $\square$
**Lemma 5.6.** Let $(X, N, A)$ be a descriptive INL-frame, write $\mathcal{X}$ for the set $X$ topologized by the clopen subbase $A$ and let $\gamma_N : \mathcal{X} \to \mathcal{V}\mathcal{V}\mathcal{X} : x \mapsto \{c \in \mathcal{V}\mathcal{X} | c \in N(x)\}$. Then $(\mathcal{X}, \gamma_N)$ is a $\mathcal{V}\mathcal{V}$-coalgebra.

*Proof.* The topological space $\mathcal{X}$ is zero-dimensional because $A$ is closed under complementation (hence is a clopen base). Moreover, $\mathcal{X}$ is compact Hausdorff because $(X, N, A)$ is compact and differentiated, so $\mathcal{X}$ is a Stone space.

In order to show that $\gamma_N$ is well defined, we need to show that $\gamma_N(x)$ is a closed subset of $\mathcal{V}\mathcal{X}$ for every $x \in \mathcal{X}$. Suppose $c \in \mathcal{V}\mathcal{X}$ and $c \notin \gamma_N(x)$. Then $c \notin N(x)$, and because $(X, N, A)$ is crowded we can find $(a_1, \dots, a_n; b)$ which is witnessed by $c$ but by none of the elements in $N(x)$. This implies $c \in \diamond a_1 \cap \dots \cap \diamond a_n \cap \Box b$ and $\diamond a_1 \cap \dots \cap \diamond a_n \cap \Box b$ is disjoint from $\gamma_N(x)$. Thus we have found an open neighbourhood of $c$ disjoint from $\gamma_N(x)$ so $\gamma_N(x)$ is closed in $\mathcal{V}\mathcal{X}$.

For continuity of $\gamma_N$, it suffices to show that $\gamma_N^{-1}(\Box(a_1, \dots, a_n; b))$ is clopen in $\mathcal{X}$ for all $a_1, \dots, a_n, b \in A$. This is a consequence of the fact that $A$ is closed under $m_\Box$, because

$$ \gamma_N^{-1}(\Box(a_1, \dots, a_n; b)) = m_\Box(a_1, \dots, a_n; b). $$

We conclude that $(\mathcal{X}, \gamma_N)$ is a $\mathcal{V}\mathcal{V}$-coalgebra. $\square$

We proceed with the proof of Theorem 5.1.

*Proof of Theorem 5.1.* First we verify that the assignments from Lemmas 5.5 and 5.6 define a bijection between descriptive INL-frames and $\mathcal{V}\mathcal{V}$-coalgebras. Let $(\mathcal{X}, \gamma)$ be a $\mathcal{V}\mathcal{V}$-coalgebra. Lemma 5.5 assigns to this the descriptive INL-frame $(X, N_\gamma, \mathrm{clp}\mathcal{X})$. We know that the topology on $X$ generated by $\mathrm{clp}\mathcal{X}$ yields the topological space $\mathcal{X}$, so applying Lemma 5.6 to $(X, N_\gamma, \mathrm{clp}\mathcal{X})$ yields the $\mathcal{V}\mathcal{V}$-coalgebra $(\mathcal{X}, \gamma_{N_\gamma})$. Furthermore, for a closed set $c \in \mathcal{V}\mathcal{X}$ we have $c \in \gamma_{N_\gamma}(x)$ iff $c \in N_\gamma(x)$ iff $c \in \gamma(x)$, hence $\gamma = \gamma_{N_\gamma}$ and $(\mathcal{X}, \gamma) = (\mathcal{X}, \gamma_{N_\gamma})$.

Conversely, suppose given a descriptive INL-frame $(X, N, A)$. Write $\tau_A$ for the topology on $X$ generated by the (clopen) base $A$ and let $\mathcal{X} = (X, \tau_A)$. Then Lemma 5.6 sends $(X, N, A)$ to $(\mathcal{X}, \gamma_N)$, which is in turn send to $(X, N_{\gamma_N}, \mathrm{clp}\mathcal{X})$ by Lemma 5.5. We know that the clopen sets of $\tau_A$ are precisely the sets in $A$, so $\mathrm{clp}\mathcal{X} = A$. Comparing the neighbourhood functions gives

$$ d \in N(x) \quad \text{iff} \quad \bar{d} \in N(x) \qquad (\text{Lemma 5.4}) $$

$$ \text{iff } \bar{d} \in \gamma_N(x) \qquad (\text{Lemma 5.6}) $$

$$ \text{iff } \bar{d} \in N_{\gamma_N}(x) \qquad (\text{Lemma 5.5}) $$

$$ \text{iff } d \in N_{\gamma_N}(x) \qquad (\text{Lemma 5.4}) $$

and therefore $(X, N, A) = (X, N_{\gamma_N}, \mathrm{clp}\mathcal{X})$. This proves the isomorphism on objects.

Let $(\mathcal{X}, \gamma)$ and $(\mathcal{X}', \gamma')$ be two $\mathcal{V}\mathcal{V}$-coalgebras and $f : X \to X'$ a function. We claim that $f$ is a $\mathcal{V}\mathcal{V}$-coalgebra morphism if and only if it is a general INL-morphism. If $f$ is a general INL-morphism then clearly it is continuous. Since it
follows that BAIOs provide an algebraic semantics for INL. Then the standard argument yields that every extension $L$ of INL is sound and complete with respect to the class of BAIOs validating $L$. Moreover, as a direct corollary of Theorem 3.9, we obtain:

**Theorem 6.1.** Every extension of INL is sound and complete with respect to descriptive INL-frames.

## 6.2 Bisimulations

We briefly discuss bisimulations for INL and derive a Hennessy-Milner property for descriptive INL-frames. We work in a setting without proposition letters, but all results carry over to the setting with proposition letters.

Recall the definition of a bisimulation, in its coalgebraic form:

**Definition 6.2.** Let $(X, N)$ and $(X', N')$ be neighbourhood frames. A relation $B \subseteq X \times X'$ is an INL-bisimulation if there exists a neighbourhood function $M : B \to PPB$ such that

<figure><img src="image_4.png" /></figure>

commutes. Two states are called bisimilar if they are linked by a bisimulation.

Since PP weakly preserves pullbacks, bisimilarity and behavioural equivalence coincide. In particular, if $(X, N) \stackrel{f}{\to} (Z, M) \stackrel{f'}{\leftarrow} (X', N')$ is a cospan in INL (witnessing behavioural equivalence of some states), then the pullback of $f$ and $f'$ in Set is a bisimulation.

Define bisimulations between descriptive frames as follows:

**Definition 6.3.** A descriptive INL-bisimulation between $(\mathcal{X}, \gamma)$ and $(\mathcal{X}', \gamma')$ is a subspace $B \subseteq \mathcal{X} \times \mathcal{X}'$ such that $B$ is a bisimulation between the underlying neighbourhood frames.

In [11] the notion of $\Lambda$-bisimulation is introduced, where $\Lambda$ is a so-called (characteristic) modal signature for an endofunctor on **Stone**. It is straightforward to see that the interpretation of INL in descriptive INL-frames can be translated to the setting used in *op. cit.* Moreover, an easy computation shows that every descriptive INL-bisimulation in the sense of Definition 6.3 is a $\Lambda$-bisimulation. We expect that the converse holds as well but at present do not have a proof of this. We leave it as an interesting open question.

We now prove a Hennessy-Milner property for descriptive INL-frames. This is the INL analogue of [5, Corollary 3.9].
**Theorem 6.4.** Let $(\mathcal{X}, \gamma)$ and $(\mathcal{X}', \gamma')$ be descriptive frames. Then $x \in \mathcal{X}$ and $x' \in \mathcal{X}'$ are logically equivalent iff they are behaviourally equivalent iff they are linked by a descriptive INL-bisimulation.

*Proof.* Logical equivalence implies behavioural equivalence because every two logically equivalent states are identified by the theory map to the canonical model (i.e. the final object in **D-INL**). If $x$ and $x'$ are behaviourally equivalent then there are morphisms in **D-INL** such that $f(x) = f'(x')$. The pullback of $f$ and $f'$ viewed as functions in **Set** is a bisimulation between the underlying neighbourhood frames (by the text following Definition 6.2). Moreover, this pullback is closed in $\mathcal{X} \times \mathcal{X}'$ because pullbacks in **Stone** are computed as in **Set**. Hence behavioural equivalence implies bisimilarity. Lastly, bisimilarity implies logical equivalence by design. □

We can apply this theorem to all INL-frames that carry a descriptive structure, that is, to $(X, N) \in \mathbf{INL}$ such that there exists $A$ making $(X, N, A)$ a descriptive INL-frame.

**Corollary 6.5.** Suppose the INL-frames $(X, N)$ and $(X', N')$ both carry a descriptive structure. Then between these frames, bisimilarity coincides with logical equivalence.

Restricting this corollary entails [3, Theorem 3.1], the Hennessy-Milner property for finite frames, because all finite neighbourhood frames carry a descriptive frame structure (see Proposition 3.8).

**Theorem 6.6.** Let $(X, N)$ and $(X', N')$ be finite neighbourhood frames. Then bisimilarity coincides with logical equivalence.

# 7 Conclusion and future work

In this paper we introduced descriptive frames for the Instantial Neighbourhood Logic (INL) and showed that these frames are dual to BAIOs, the algebras for INL. Coalgebra provided a key for obtaining this duality. We first presented BAIOs as algebras for the functor $\mathbf{l}$ on the category of boolean algebras. We also represented descriptive INL-frames as coalgebras for the double Vietoris functor $\mathbf{VV}$ on the category of Stone spaces. Finally, we showed that the category of $\mathbf{l}$-algebras is dual to the category of $\mathbf{VV}$-coalgebras, leading to the desired duality result. As a corollary we obtained that every extension of INL is sound and complete with respect to descriptive INL-frames. One interesting question for future work is whether one can obtain an analogue of the celebrated Sahlqvist completeness and correspondence result for extensions of INL.

We recall that the Vietoris functor $\mathbf{V}$ is dual to the functor $\mathbf{M}$ on the category of boolean algebras (Section 2). Intuitively $\mathbf{M}$ freely adds one layer of normal modalities to a boolean algebra. We showed in this paper that BAIOs can be represented as algebras for $\mathbf{M} \circ \mathbf{M}$ (Section 4). Therefore, BAIOs can be seen as “modal algebras squared” and INL itself is, in a way, “the basic modal logic”.
squared". This provokes the question of what "modal algebras cubed" looks like, i.e. what logic and algebras correspond to the functor $M \circled{M} \circ M$, and similar questions for the $n$-fold composition of $M$.

Recall that monotone neighbourhood logic EM algebraically corresponds to a functor $N$ on boolean algebras which intuitively adds one layer of monotone modalities to a boolean algebra [17,18]. This generates a question whether NN-algebras and the corresponding logic admit an "INL-style axiomatization".

Another related formalism that would be interesting to investigate is that of positive INL. The algebras for this logic are distributive lattices with instantial operators (DLIOs):

**Definition 7.1.** A distributive lattice with instantial operators (DLIO) is a tuple $(D, (f_n)_{n \in \omega}, (g_n)_{n \in \omega})$ consisting of a distributive lattice $D$ and two collections of $\omega$-indexed maps $f_n, g_n: D^{n+1} \to D$ such that: (1) The $f_n$ satisfy $(B_1)$ to $(B_7)$ from Definition 3.1, where, in absence of negation, we reformulate $(B_5)$ as

$$f_n(a_1, \dots, a_n; b) \le f_{n+1}(a_1, \dots, a_n, c; b) \lor f_n(a_1, \dots, a_n; b \land d),$$

whenever $c \lor d = \top$; (2) The $g_n$ satisfy relations dual to the ones for $f_n$; and (3) The $f_n$ and $g_n$ satisfy the duality axioms

$$\begin{align}
& g_{n+1}(a_1, \dots, a_n, b'; b) \land \bigwedge_{i=1}^{m} g_n(a_1, \dots, a_n; a'_i \lor b) \tag{D1} \\
& \le g_n(a_1, \dots, a_n; b) \lor f_m(a'_1, \dots, a'_m; b') \nonumber
\end{align}$$

and

$$\begin{align}
& f_n(a_1, \dots, a_n; b) \land g_m(a'_1, \dots, a'_m; b') \tag{D2} \\
& \le f_{n+1}(a_1, \dots, a_n, b'; b) \lor \bigvee_{i=1}^{m} f_n(a_1, \dots, a_n; a'_i \land b). \nonumber
\end{align}$$

These are of course algebras for a endofunctor $J$ on the category **DL** of distributive lattices and homomorphisms. In analogy with the results of this paper, one would expect that descriptive frames for positive INL are isomorphic to coalgebras for the double convex Vietoris functor $V_c$ on the category of Priestley spaces, as this is the Priestley space analogue of the Vietoris functor [27,6,33]. We expect the following duality result:

**Conjecture 7.2.** We have a dual equivalence

$$\mathbf{Alg}(J) \cong^{\mathrm{op}} \mathbf{Coalg}(V_c V_c).$$

Finally, related to positive INL, an interesting question is to consider the geometric logic analogue of INL and to verify a slogan of [4], which in the case of INL will read as

$$\text{Geometric INL} = \text{Positive INL} + \text{Scott continuity.}$$

If correct, this may also provide a novel algebraic presentation of the double Vietoris powerlocale studied extensively by Vickers [35,36,34].
References

1. J. van Benthem, N. Bezhanishvili, and S. Enqvist. A new game equivalence, its logic and algebra. *Journal of Philosophical Logic*, 48(4):649–684, 2019.

2. J. van Benthem, N. Bezhanishvili, and S. Enqvist. A propositional dynamic logic for instantial neighbourhood semantics. *Studia Logica*, 107(4):719–751, 2019.

3. J. van Benthem, N. Bezhanishvili, S. Enqvist, and J. Yu. Instantial neighbourhood logic. *Review of Symbolic Logic*, 10(1):116–144, 2017.

4. N. Bezhanishvili, J. de Groot, and Y. Venema. Coalgebraic Geometric Logic. In M. Roggenbach and A. Sokolova, editors, *Proc. CALCO 2019*, pages 7:1–7:18, Dagstuhl, Germany, 2019. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.

5. N. Bezhanishvili, G. Fontaine, and Y. Venema. Vietoris bisimulations. *Journal of Logic and Computation*, 20(5):1017–1040, 2010.

6. N. Bezhanishvili and A. Kurz. Free modal algebras: A coalgebraic perspective. In T. Mossakowski, U. Montanari, and M. Haveraaen, editors, *Proc. CALCO 2007*, pages 143–157, Berlin, Heidelberg, 2007. Springer.

7. P. Blackburn, M. de Rijke, and Y. Venema. *Modal Logic*. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, 2001.

8. S. Celani and R. Jansana. Priestley duality, a Sahlqvist theorem and a Goldblatt-Thomason theorem for positive modal logic. *Logic Journal of the IGPL*, 7:683–715, 12 1999.

9. S.A. Celani and R. Jansana. Easkia duality and its extensions. In G. Bezhanishvili, editor, *Leo Esakia on Duality in Modal and Intuitionistic Logics*, pages 63–98. Springer Netherlands, Dordrecht, 2014.

10. A. Chagrov and M. Zakharyaschev. *Modal Logic*. Oxford University Press, Oxford, 1997.

11. S. Enqvist and S. Sourabh. Bisimulations for coalgebras on Stone spaces. *Journal of Logic and Computation*, 28(6):991–1010, 2018.

12. L.L. Esakia. Topological Kripke models. *Soviet Mathematics Doklady*, 15:147–151, 1974.

13. L.L. Esakia. The problem of dualism in the intuitionistic logic and Browerian lattices. In *V International Congress of Logic, Methodology and Philosophy of Science*, pages 7–8, Canada, 1975.

14. L.L. Esakia. *Heyting Algebras*. Trends in Logic. Springer International Publishing, Springer, 2019. Translated by A. Evseev.

15. R. Furber, D. Kozen, K.G. Larsen, R. Mardare, and P. Panangaden. Unrestricted stone duality for Markov processes. In *Proc. LICS 2017*, pages 1–9, Reykjavík, Iceland, 2017. IEEE Press.

16. R.I. Goldblatt. Metamathematics of modal logic I. *Reports on Mathematical Logic*, 6:41–78, 1976.

17. H.H. Hansen. Monotonic modal logics, 2003. Master's thesis, Institute for Logic, Language and Computation, University of Amsterdam.

18. H.H. Hansen and C. Kupke. A coalgebraic perspective on monotone modal logic. *Electronic Notes in Theoretical Computer Science*, 106:121–143, 2004.

19. P.T. Johnstone. *Stone Spaces*. Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1982.

20. B. Jónsson and A. Tarski. Boolean algebras with operators, Part I. *American Journal of Mathematics*, 73:891–939, 1951.

21. K. Kapulkin, A. Kurz, and J. Velebil. Expressiveness of positive coalgebraic logic. In T. Bolander, T. Braüner, S. Ghilardi, and L.S. Moss, editors, *Proc. AIML 2012*, pages 368–385. College Publications, 2012.
22. C. Kupke, A. Kurz, and D. Pattinson. Algebraic semantics for coalgebraic logics. *Electronic Notes in Theoretical Computer Science*, 106:219–241, 2004. Proceedings of the Workshop on Coalgebraic Methods in Computer Science (CMCS).

23. C. Kupke, A. Kurz, and Y. Venema. Stone coalgebras. *Theoretical Computer Science*, 327(1):109–134, 2004. Selected Papers of CMCS '03.

24. C. Kupke and D. Pattinson. Coalgebraic semantics of modal logics: An overview. *Theoretical Computer Science*, 412(38):5070–5094, 2011. CMCS Tenth Anniversary Meeting.

25. M. Mio, R. Furber, and R. Mardare. Riesz modal logic for markov processes. In *Proc, LICS 2017*, pages 1–12, 06 2017.

26. L.S. Moss. Coalgebraic logic. *Annals of Pure and Applied Logic*, 96(1):277–317, 1999.

27. A. Palmigiano. A coalgebraic view on positive modal logic. *Theoretical Computer Science*, 327:175–195, 10 2004.

28. H.A. Priestley. Representation of distributive lattices by means of ordered Stone spaces. *Bulletin of the London Mathematical Society*, 2(2):186–190, 1970.

29. J.J.M.M. Rutten. Universal coalgebra: a theory of systems. *Theoretical Computer Science*, 249((1)):3–80, 2000.

30. G. Sambin and V. Vaccaro. A new proof of Sahlqvist's theorem on modal definability and completeness. *The Journal of Symbolic Logic*, 54(3):992–999, 1989.

31. M.H. Stone. The theory of representations for boolean algebras. *Transactions of the American Mathematical Society*, 40:37–111, 1936.

32. O. Tuyt. Canonical rules on neighbourhood frames. Master's thesis, ILLC, University of Amsterdam, 2016.

33. Y. Venema and J. Vosmaer. Modal logic and the Vietoris functor. In G. Bezhanishvili, editor, *Leo Esakia on Duality in Modal and Intuitionistic Logics*, pages 119–153, Dordrecht, 2014. Springer Netherlands.

34. S. Vickers. Constructive points of power locales. *Mathematical Proceedings of the Cambridge Philosophical Society*, 122(2):207–222, 1997.

35. S.J. Vickers. The double powerlocale and exponentiation: A case study in geometric logic. *Theory and Applications of Categories*, 12(13):272–422, 2004.

36. S.J. Vickers and C.F. Townsend. A universal characterization of the double powerlocale. *Theoretical Computer Science*, 316(1):297–321, 2004. Recent Developments in Domain Theory: A collection of papers in honour of Dana S. Scott.

37. L. Vietoris. Bereiche zweiter Ordnung. *Monatshefte für Mathematik und Physik*, 32(1):258–280, 1922.

38. K. Yosida. On the representation of vector lattices. *Proceedings of the Imperial Academy*, 18(7):339–342, 1942.

39. J. Yu. A tableau system for instantial neighborhood logic. In *Proc. LFCS 2018*, pages 337–353, 2018.

40. J. Yu. Lyndon interpolation theorem of instantial neighborhood logic - constructively via a sequent calculus. *Annals of Pure and Applied Logic*, 171(1), 2020.