Topo-Logic as a Dynamic-Epistemic Logic

Abstract

We extend the ‘topologic’ framework [13] with dynamic modalities for ‘topological public announcements’ in the style of Bjorndahl [5]. We give a complete axiomatization for this “Dynamic Topo-Logic”, which is in a sense simpler than the standard axioms of topologic. Our completeness proof is also more direct (making use of a standard canonical model construction). Moreover, we study the relations between this extension and other known logical formalisms, showing in particular that it is co-expressive with the simpler (and older) logic of interior and global modality [1, 4, 10, 14]. This immediately provides an easy decidability proof (both for topologic and for our extension).

A. Özgün—Acknowledges financial support from European Research Council grant EPS 313360.

1 Introduction

The ‘topologic’ formalism, introduced by Moss and Parikh [13], and investigated further by Dabrowski et al. [6], Georgatos [8, 9] and others, presented a single-agent subset space logic (SSL) for the notions of knowledge and effort (where “effort” refers to any type of evidence-gathering—via, e.g., measurement, computation, approximation, experiment or announcement—that can lead to an increase in knowledge). They proposed a bimodal language with modalities K and $\Box$, where $K\varphi$ is read as “the agent knows $\varphi$ (is true)”, and the effort modality $\Box \varphi$ says that “$\varphi$ stays true no matter what further evidence-gathering efforts are made”. So $\Box$ captures a notion of stability under evidence-gathering. The formulas are interpreted on subset spaces, which include the class of topological spaces. In [13] Moss and Parikh gave a sound and complete axiomatization with respect to the class of all subset spaces. The axiomatization for topological spaces has later been studied by Georgatos [8, 9], and Dabrowski et al. [6], who independently provided complete axiomatizations and proved decidability. The completeness proofs involve however rather complicated constructions. Moreover, one of the main axioms (the so-called Union Axiom, capturing closure of the topology under binary unions) is extremely complex and looks rather unintuitive.

A different logical formalism with a topological semantics was proposed by Bjorndahl [5], motivated by developments in dynamic epistemic logic. Namely, he proposed a topological semantics (in the style of subset space semantics) for the syntax of Public Announcement Logic (PAL), that assumes as precondition of learning $\varphi$ the sentence $int (\varphi )$, saying that $\varphi$ is learnable. Topologically, this corresponds to the interior operator of McKinsey and Tarski [12]. He axiomatized this logic, using natural analogues of the standard reduction axioms of PAL, and showed that this formalism is co-expressive with the simpler (and older) logic of interior $int (\varphi )$ and global modality $K\varphi$ (previously investigated by Bennett, Goranko and Passy, Aiello, and Shehtman [1, 4, 10, 14], extending the work of McKinsey and Tarski [12] on interior semantics).

Another recent development is the work of van Ditmarsch et al. [15], who studied the extension of Bjorndahl’s system with a Topological Arbitrary Public Announcement modality (‘Topo-APAL’, for short), that quantifies universally over Bjorndahl-style public announcements (similarly to the way classical APAL modality in [2] quantifies over public announcements). They proved that this is co-expressive with Bjorndahl’s logic.

In this paper, we investigate a natural extension of ‘topologic’, obtained by adding to it Bjorndahl-style dynamic modalities for ‘updates’ (public announcements). The resulting ‘Dynamic Topo-Logic’ can be thought of as a logic of evidence-based knowledge $K\varphi$, knowability $int (\varphi )$, learning of new evidence $[\varphi ]\psi$ and stability $\Box \varphi$ (of some truth $\varphi$) under any such evidence-acquisition. We show that this extension is co-expressive with the above-mentioned three logical formalisms: Topo-APAL [15], Bjorndahl’s logic of topological public announcements [5], and the logic of interior and global modality [1, 4, 10, 14]. This finally elucidates the relationships between topologic and other modal (and dynamic-epistemic) logics for topology: in particular, topologic is directly interpretable in the simplest logic above (of interior and global modality), which immediately provides a simpler decidability proof (both for topologic and for our extension).

We give a complete axiomatization for Dynamic Topo-Logic, which is in a sense simpler than the standard axioms of Topologic: though we have more axioms, each of them is transparent, natural and easily readable, directly reflecting the intuitive meanings of the connectives. Our axiomatization consists of a slightly different version of Bjorndahl’s axioms, together with only two additional proof principles governing the behavior of the topologic “effort” modality $\Box \varphi$ (which we call “stable truth”): an introduction rule and an elimination axiom. Everything to be said about the effort modality is captured by these two simple principles, which together express the fact that $\Box$ quantifies universally over all updates with any new evidence. In particular, the complicated Union Axiom [8, 9] is not needed in our system. Our completeness proof is also simpler than the existing completeness proofs for Topologic, making direct use of a standard canonical topo-model construction. This shows the advantage of adding dynamic modalities: when considered as a fragment of a dynamic-epistemic logic, Topologic becomes a more transparent and natural formalism, with intuitive axioms and canonical behavior.

In its turn, the effort modality helps to simplify and streamline the axiomatization of Topo-APAL. Indeed, although the two are equivalent, note that the axiomatization of this latter operator in [15] was essentially infinitary: it used an inference rule that takes as inputs infinitely many premisses! In contrast, our axiomatization is recursive, being obtained by replacing the infinitary rule with a finitary one, involving the use of “fresh” propositional variables. This rule’s soundness is due to the “pure semantical” character of the effort modality $\Box \varphi$ (whose meaning does not depend on the valuation of variables not occurring in $\varphi$), in contrast to the “syntactical” character of the APAL modality.¹

Due to page-limit constraints, this Proceedings version includes only the shortest proofs. The other relevant proofs can be found in the long version of this paper, available online at https://sites.google.com/site/ozgunaybuke/publications.

2 Dynamic Topo-Logic: Syntax, Semantics and Axiomatization

In this section, we present the language of Dynamic Topo-Logic, which is obtained by extending Bjorndahl’s logic $\mathbf {L}_{!K int }$ [5] with the effort modality from Topologic [13]; or equivalently, by extending Topologic with the Tarki-McKinsey interior operator $int$ [12] and with Bjorndahl’s topological public announcements. As it turns out, interior is in fact definable using topological public announcements (since $int (\varphi ) = \langle \varphi \rangle \top$). So, although we keep the $int$ operator as primitive for technical reasons, in a sense our syntax is essentially given by adding to topologic only the dynamic modalities.

Syntax. Given a countable set of propositional variables $\mathrm {Prop}$, the language $\mathcal {L}$ of Dynamic Topo-Logic is defined recursively by the grammar

$$\begin{aligned} \varphi \, {:}{:}{=}\, p \ | \ \lnot \varphi \ | \ \varphi \wedge \varphi \ | \ K\varphi \ | \ int (\varphi ) \ | \ [\varphi ]\varphi \ | \ \Box \varphi , \end{aligned}$$

where $p\in \mathrm {Prop}$. The update operator $[\varphi ]\psi$ is sometimes denoted by $[!\varphi ]\psi$ in Public Announcement Logic literature; we skip the exclamation sign, but we will use the notation [!] for this modality when we do not want to specify the announcement formula $\varphi$ (so that ! functions as a placeholder for the content of the announcement). We employ the usual abbreviations for propositional connectives $\top , \bot , \vee , \rightarrow , \leftrightarrow$. The dual modalities are defined as $\hat{K}\varphi :=\lnot K\lnot \varphi$, $\Diamond \varphi := \lnot \Box \lnot \varphi$, $\langle \varphi \rangle \psi :=\lnot [\varphi ]\lnot \psi$, and $cl ( \varphi ) := \lnot int \lnot \varphi$.

Several fragments of the language $\mathcal {L}$ are of both technical and conceptual interest. For all the fragments studied in this paper, we use a notational convention listing in subscript all the modalities of the corresponding language. For example, $\mathcal {L}_{ int }$ denotes the fragment of $\mathcal {L}$ having only the modality $int$ (besides propositional connectives); $\mathcal {L}_{K int }$ has only modalities K and $int$ ; $\mathcal {L}_{K\Box }$ has only modalities K and $\Box$, etc.

Topological Semantics: Intuitions and Motivation. The semantics of this language is over topological spaces ² $(X,\tau )$. The points of the space represent “possible worlds” (or states of the world). The open sets in the topology are meant to represent potential evidence, i.e. facts about the world that are in principle knowable, in the sense of being verifiable: whenever (in any world in which) they are true, they can be known. In contrast, closed sets represent facts that are in principle falsifiable (whenever they are false, their falsity can be known). As it was remarked in [11, 16], the closure properties of a topology are intuitively satisfied in this interpretation. First, contradictions ($\emptyset$) and tautologies (X) are in principle verifiable (as well as falsifiable). The conjunction $P\wedge Q$ of two verifiable facts is also verifiable: if $P\wedge Q$ is true, then both P and Q are true, and since both are assumed to be verifiable, they can both be known, and hence $P\wedge Q$ can be known. Finally, if $\{P_i:i\in I\}$ is a (possibly infinite) family of verifiable facts, then their disjunction $\bigvee _{i\in I} P_i$ is verifiable: indeed, if the disjunction is true, then there must exist some $i\in I$ such that $P_i$ is true, and so $P_i$ can be known (since it is verifiable), and as a result the disjunction $\bigvee _{i\in I} P_i$ can also be known (by inference from $P_i$).

Semantics. A subset space is a pair $(X, \mathcal {O})$, where X is a non-empty set and $\mathcal {O}\subseteq \mathcal {P}(X)$ is a non-empty collection of subsets of X. A subset model $\mathcal {M}= (X,\mathcal {O}, V)$ is triple where $(X,\mathcal {O})$ is a subset space and $V : \mathrm {Prop} \rightarrow P(X)$ is a valuation function. A topological model (or, in short, a topo-model) is a subset model $\mathcal {M}=(X, \tau , V)$ where $(X, \tau )$ is a topological space. Following the Subset Space Semantics [13], formulas are interpreted on pairs of the form (x, U) where $x \in U \in \mathcal {O}$. Such pairs are called epistemic scenarios. The set of all epistemic scenarios of a given topo-model $\mathcal {M}$ is denoted by $ES(\mathcal {M})$. Given a topo-model $\mathcal {M}=(X, \tau , V)$ and an epistemic scenario $(x, U)\in ES(\mathcal {M})$, the semantics for the language $\mathcal {L}$ is given by defining a satisfaction relation $(x,U)\,\models _\mathcal {M}\varphi$, as well as a truth set (interpretation) $[\![ \varphi ]\!]^U_\mathcal {M}=:\{ x\in U \ | \ (x, U)\,\models _\mathcal {M}\varphi \}$, for all formulas $\varphi$. We omit the subscript, writing simply $(x,U)\,\models \,\varphi$ and $[\![ \varphi ]\!]^U$, whenever the model $\mathcal {M}$ is fixed. The definition of satisfaction is by recursion on the complexity of formulas $\varphi$:

$$\begin{aligned} \begin{array}{llll} (x, U)\,\models \,p \ \ &{} \text{ iff }\ \ &{} x\in V(p) \,\,\,\,\,\,\,\,\,\,\,\,\,\,\, \text{(for } p\in \mathrm {Prop}\text{) } \\ (x, U)\,\models \,\lnot \varphi \ \ &{} \text{ iff }\ \ &{} (x, U)\,\not \models \,\varphi \\ (x, U)\,\models \,\varphi \wedge \psi \ \ &{} \text{ iff }\ \ &{} (x, U)\,\models \,\varphi \ \text{ and } \ (x, U)\,\models \,\psi \\ (x, U)\,\models \,K\varphi \ \ &{} \text{ iff }\ \ &{} (\forall y \in U) (y, U)\,\models \,\varphi \\ (x, U)\,\models \, int (\varphi ) \ \ &{} \text{ iff }\ \ &{} x\in Int ([\![ \varphi ]\!]^U) \\ (x, U)\,\models \,[\varphi ]\psi \ \ &{} \text{ iff }\ \ &{} (x, U)\,\models \, int (\varphi ) \ \text{ implies } \ (x, Int ([\![ \varphi ]\!]^U) )\,\models \,\psi \\ (x, U)\,\models \,\Box \varphi \ \ &{} \text{ iff }\ \ &{} (\forall O\in \tau )\left( x\in O\subseteq U \ \text{ implies } \ (x, O)\,\models \,\varphi \right) \\ \end{array} \end{aligned}$$

We say that a formula $\varphi$ is valid in a model $\mathcal {M}$, and write $\mathcal {M}\,\models \,\varphi$, if $(x, U)\,\models \,_\mathcal {M}\varphi$ for all scenarios $(x,U)\in ES(\mathcal {M})$. We say $\varphi$ is valid, and write $\models \,\varphi$, if $\mathcal {M}\,\models \, \varphi$ for all $\mathcal {M}$.

Intuitive Reading. In an epistemic scenario (x, U), the first component x represents the actual state of the world, while U is the current evidence possessed by the agent; $x\in U$ expresses the factivity of evidence. The operator K captures “knowledge” (in the sense of absolute certainty: “infallible knowledge”): in a scenario (x, U), $K\varphi$ holds iff $\varphi$ is entailed by the agent’s evidence U (hence, the above semantic clause). $int (\varphi )$ means that $\varphi$ is “knowable” in the actual state of the world (though not necessarily knowable in general, in other worlds): there exists some potential evidence (open set containing the actual state) U that entails $\varphi$ (hence, the actual state is in the interior of $\varphi$); the dual closure operator $cl ( \varphi )$ means that $\varphi$ is “unfalsifiable” in the actual state (i.e. it is consistent with all potential evidence at that state). The ‘effort’ modality $\Box \varphi$ is read as “$\varphi$ is stably true” under evidence-acquisition: i.e. $\varphi$ is true, and will stay true no matter further evidence is obtained. Finally, we read the dynamic update modalities $[\varphi ]\psi$ as “$\psi$ will be true after learning $\varphi$”. The difference between these Bjorndahl-style updates and the standard update operators (sometimes called public announcements)³ is that not every truth is automatically “learnable”; so the precondition of updating with $\varphi$ is the proposition $int (\varphi )$ saying that $\varphi$ is knowable in the actual world (i.e. there exists some true evidence supporting $\varphi$).

The above topological semantics for the language $\mathcal {L}$ was in fact previously studied for some of its subfragments. While the semantic clauses for K and $\Box$ were first introduced in [13], the fragment $\mathcal {L}_{!K int }$ examined in [5]. Bjorndahl provided sound and complete aximatizations for the associated dynamic logic $\mathbf {L}_{!K int }$ (see Table 1 for the axiomatizations). Moreover, he proved—via a translation using so-called Reduction Axioms (see Table 1)—that the languages $\mathcal {L}_{K int }$ and $\mathcal {L}_{!K int }$ are equally expressive under the proposed topological semantics:

Theorem 1

[5, Proposition 5]. $\mathcal {L}_{K int }$ and $\mathcal {L}_{!K int }$ are equally expressive with respect to topo-models.⁴

A Close Relative: Topo-APAL. Yet another relevant variation of $\mathcal {L}$ is the language $\mathcal {L}_{APAL}$ obtained by replacing the effort modality $\Box$ with the so-called arbitrary announcement modality $\blacksquare$ that was introduced by Balbiani et al. [2]. Roughly speaking, the arbitrary announcement modality $\blacksquare \varphi$ is read as “$\varphi$ stays true after any epistemic update”. While Balbiani et al. [2] studied this modality on Kripke frames, a topological semantics for $\blacksquare$ was proposed by van Ditmarsch et al. [15]:

$$\begin{aligned} (x, U)\,\models \, \blacksquare \varphi \ \ \text{ iff }\ \ (\forall \psi \in \mathcal {L}_{!K int })((x, U)\,\models \, [\psi ]\varphi ), \end{aligned}$$

where [!] is the dynamic operator for topological updates (in the sense above). So $\blacksquare$ quantifies over all Bjorndahl-style topological public announcements of epistemic formulas. In [15], van Ditmarsch et al. proved that:

Theorem 2

[15, Theorem 19]. $\mathcal {L}_{K int }$ and $\mathcal {L}_{APAL}$ are equally expressive expressive with respect to topo-models.

As stated in the above semantic clause, the arbitrary announcement modality only quantifies over the $\blacksquare$-free formulas, whereas the effort modality quantifies over all open neighborhoods of the actual state x. Intuitively speaking, the effort modality seems stronger than the arbitrary announcement modality. However, quite surprisingly, this is not the case: in this paper, we will show that the effort modality is in fact semantically equivalent to the arbitrary announcement modality.

Axiomatizations. Given a formula $\varphi \in \mathcal {L}$, we denote by $P_\varphi$ the set of all propositional variables occurring in $\varphi$ (we will use the same notation for the necessity and possibility forms defined below). The axiomatization of our Dynamic Topo-Logic $\mathbf {L}$ consists of all axioms and rules in Table 1 below.

Table 1. The axiomatization $\mathbf {L}$ of Dynamic Topo-Logic.

The intuitive nature of these axioms should be obvious. The first six need no explanation. The Replacement of Equivalents rule (RE) says that updates are extensional: learning equivalent sentences gives rise to equivalent updates, while the reduction axiom (R$[\top ]$) says that updating with tautologies is redundant (nothing changes). The other reduction axioms are the natural analogues of the standard reduction laws in Public Announcement Logic, when one takes into account the fact that the precondition of a Bjorndahl-style update with $\varphi$ is that $\varphi$ is (not only true, but also) knowable: i.e. $int (\varphi )$. The only essentially new components of our system are the last two: the elimination axiom ($[!]\Box$-elim) and the introduction rule ($[!]\Box$-intro) for the effort modality. Taken together, they say that $\theta$ is a stable truth after learning $\varphi$ iff $\theta$ is true after learning any stronger evidence $\varphi \wedge \rho$. The left-to-right implication in this statement is directly captured by ($[!]\Box$-elim), while the converse is captured by the rule ($[!]\Box$-intro). The “freshness” of the variable $p\in P$ in this rule ensures that it represents any ‘generic’ further evidence: this is similar to the introduction rule for the universal quantifier. In essence, the effort axiom and rule express the fact that the effort modality is in fact a universal quantifier (over potential evidence).

Simplicity of Our Axioms. One can compare the transparency and simple nature of our axioms with the complexity of the standard axiomatization of topologic, containing among others the intricate and opaque Union Axiom, which in our notation reads as:

$$\begin{aligned} \Diamond \varphi \wedge \hat{K}\Diamond \psi \rightarrow \Diamond (\Diamond \varphi \wedge \hat{K}\Diamond \psi \wedge K\Diamond \hat{K}(\varphi \vee \psi )) \end{aligned}$$

The fragment $\mathcal {L}_{K int }$, having only modalities K and $int$, was first studied in [10] (with a Kripke semantics) and [4] (with the above topological semantics). A complete axiomatization for the topological interpretation was provided by Aiello [1], though a full completeness proof was given later by Shehtman [14]:

Proposition 1

([14]). The system $\mathbf {L}_{K int }$, consisting of the axioms and rules in group (I) of Table 1, is sound and complete for the language $\mathcal {L}_{K int }$.

The fragment $\mathcal {L}_{!K int }$, obtained by extending $\mathcal {L}_{K int }$ with topological update operators (‘public announcement’), was introduced and axiomatized by Bjorndahl [5]:

Proposition 2

([5]). The system $\mathbf {L}_{!K int }$, consisting of all the axioms and rules in groups (I) and (II) of Table 1, is sound and complete for the language $\mathcal {L}_{!K int }$.

Proof

It is easy to see that all the axioms and rules of $\mathbf {L}_{!K int }$ are sound. A proof of completeness is in [5], for a slightly different, but equivalent, axiomatization. Bjorndahl’s system consists of the axioms of $\mathcal {L}_{K int }$ (i.e. group (I) in our Table), together with our reduction axioms (R$_p$), (R$_\lnot$), (R$_K$) and (R$_!$), as well as the additional reduction laws, (R$_\wedge$) and (R$_{ int }$) in the Proposition below.⁵ Since the latter ones are provable in our system $\mathbf {L}_{!K int }$, it follows that $\mathbf {L}_{!K int }$ is complete as well.

Proposition 3

The first six reduction laws below are provable both in $\mathbf {L}_{!K int }$ and $\mathbf {L}$ (for languages $\mathcal {L}_{!K int }$ and $\mathcal {L}$, respectively). The seventh schema and the inference rule below can be derived in our full proof system $\mathbf {L}$:

1.	($\langle !\rangle$)	$\langle \varphi \rangle \psi \leftrightarrow \left( int (\varphi )\wedge [\varphi ]\psi \right)$
2.	(R$_\bot$)	$[\varphi ]\bot \leftrightarrow \lnot int (\varphi )$
3.	(R$_\wedge$)	$[\varphi ] (\psi \wedge \theta ) \leftrightarrow \left( [\varphi ] \psi \wedge [\varphi ] \theta \right)$
4.	(R$_ int$)	$[\varphi ] int (\psi ) \leftrightarrow \left( int (\varphi ) \rightarrow [\varphi ]\psi \right)$
5.	(R$[ int ]$)	$[ int (\varphi ) ]\psi \leftrightarrow [\varphi ]\psi$
6.	(R$_{[p]}$)	$[\varphi ] [p] \psi \leftrightarrow [\varphi \wedge p]\psi$
7.	($\Box$-elim)	$\Box \theta \rightarrow [\rho ]\theta$       ($\rho \in \mathcal {L}$ arbitrary formula)
8.	($\Box$-intro)	From $\vdash \chi \rightarrow [p]\theta$, infer $\vdash \chi \rightarrow \Box \theta$    ($p \not \in P_\chi \cup P_\theta$ atom).

3 Soundness and Expressivity

In this section, we introduce a more general class of models for our language, called pseudo-models: these are a special case of the (even more general) Subset Space Semantics introduced in [13]. Pseudo-models include all topo-models, as well as other subset-space models, but they have the nice property that the interior operator $int$ can still be interpreted in the standard way. These structures, though interesting enough in themselves, are for us only an auxiliary notion, playing an important technical role in our completeness proof. But for now, we will first prove the soundness of our full system $\mathbf {L}$ from Table 1 with respect to pseudo-models (and thus also over topo-models), and we provide several expressivity results concerning the above defined languages with respect to (both topo-models and) pseudo-models.

Definition 1 (Lattice spaces and Pre-models)

A subset space $(X, \mathcal {O})$ is called a lattice space if $\emptyset , X\in \mathcal {O}$, and $\mathcal {O}$ is closed under finite intersections and finite unions. A pre-model $(X, \mathcal {O}, V)$ is a triple where $(X, \mathcal {O})$ is a lattice space and $V: \mathrm {Prop}\rightarrow \mathcal {P}(X)$ is a valuation map.

Although a lattice space $(X, \mathcal {O})$ is not necessarily a topological space, the family $\mathcal {O}$ constitutes a topological basis over X. Therefore, every pre-model $\mathcal {M}=(X, \mathcal {O}, V)$ has an associated topo-model $\mathcal {M}=(X, \tau _\mathcal {O}, V)$, where $\tau _\mathcal {O}$ is the topology generated by $\mathcal {O}$ (i.e., the smallest topology on X such that $\mathcal {O}\subseteq \tau _\mathcal {O}$).

Satisfaction relation in pre-models. Given a pre-model $\mathcal {M}=(X, \mathcal {O}, V)$, the semantics for $\mathcal {L}$ on pre-models can be defined for all pairs of the form (x, Y), where $Y\subseteq X$ is an arbitrary subset such that $x\in Y$. It is important to notice that, for a given evaluation pair (x, Y) on pre-models, the set Y is not necessarily an element of $\mathcal {O}$. The semantic clauses for the modalities in $\mathcal {L}$ are defined similarly as in Sect. 2, except that $\Box$ quantifies over the elements of $\mathcal {O}$, and $int$ is interpreted as the interior operator of the associated topology $\tau _O$. More precisely, given a pre-model $\mathcal {M}=(X, \mathcal {O}, V)$ and (x, Y) with $x\in Y\subseteq X$, we set

$$\begin{aligned} \begin{array}{llll} (x, Y)\,\models \, int (\varphi ) \ \ &{} \text{ iff }\ \ &{} x\in Int ([\![ \varphi ]\!]^Y) \\ (x, Y)\,\models \, [\varphi ]\psi \ \ &{} \text{ iff }\ \ &{} (x, Y)\,\models \, int (\varphi ) \ \text{ implies } \ (x, Int ([\![ \varphi ]\!]^Y) )\,\models \,\psi \\ (x, Y)\,\models \, \Box \varphi \ \ &{} \text{ iff }\ \ &{} (\forall O\in \mathcal {O})(x\in O\subseteq Y \ \text{ implies } \ (x, O)\,\models \, \varphi )\\ \end{array} \end{aligned}$$

where $Int$ is the interior operator of $\tau _\mathcal {O}$.

Validity in pre-models. Although we did not require the neighbourhood Y to be an element of $\mathcal {O}$ in the definition of the satisfaction relation above, the validity on pre-models is defined by restricting to epistemic scenarios (x, U) such that $x\in U\in \mathcal {O}$, as in the case for the topo-models. More precisely, we say that a formula $\varphi$ is valid in a pre-model $\mathcal {M}$, and write $\mathcal {M}\,\models \,\varphi$, iff $(x, U)\,\models _\mathcal {M}\varphi$ for all epistemic scenarios $(x,U)\in ES(\mathcal {M})$. A formula $\varphi$ is valid, denoted by $\models \varphi$, iff $\mathcal {M}\,\models \,\varphi$ for all $\mathcal {M}$.

Definition 2

(Pseudo-models for $\mathcal {L}$ ). A pseudo-model $\mathcal {M}=(X, \mathcal {O}, V)$ is a pre-model such that $[\![ int (\varphi ) ]\!]^U\in \mathcal {O}$, for all $\varphi \in \mathcal {L}$ and $U\in \mathcal {O}$.

It is obvious that the class of pseudo-models includes all topo-models, and that all formulas that are valid on pseudo-models are also valid on topo-models.⁶

Theorem 3

The system $\mathbf {L}$ is sound with respect to the class of all pseudo-models (and hence also with respect to the class of all topo-models).

We first prove that $\mathcal {L}_{!K int }$ and $\mathcal {L}_{K int }$ are equally expressive on pseudo-models:

Lemma 1

$\mathcal {L}_{!K int }$ and $\mathcal {L}_{K int }$ are co-expressive with respect to pseudo-models. In other words, for every formula $\varphi \in \mathcal {L}_{!K int }$ there exists a formula $\psi \in \mathcal {L}_{K int }$ such that $\varphi \leftrightarrow \psi$ is valid in all pseudo-models.

The proof (in Appendix B.2 of the on-line long version) goes over standard lines, using the reduction laws to push dynamic modalities inside the formula and then eliminate them. The proof uses induction on a non-standard notion of complexity of formulas <, given by:

Lemma 2

There exists a well-founded strict partial order < on formulas of $\mathcal {L}$ such that

• 1. $\varphi \in Sub (\psi )$ implies $\varphi <\psi$,

• 2. $( int (\varphi ) \rightarrow p )\, < \, ([\varphi ]p)$,

• 3. $( int (\varphi ) \rightarrow \lnot [\varphi ]\psi ) < ([\varphi ]\lnot \psi )$,

• 4. $([\varphi ]\psi \wedge [\varphi ]\chi ) < ([\varphi ](\psi \wedge \chi ) )$,

• 5. $( int (\varphi ) \rightarrow int ([\varphi ]\psi ) ) < ([\varphi ]\psi )$,

• 6. $( int (\varphi ) \rightarrow K [\varphi ]\psi ) < ([\varphi ] K\psi )$,

• 7. $[\langle \varphi \rangle \psi ]\chi < ([\varphi ][\psi ]\chi )$.

• 8. $\varphi \in \mathcal {L}$ implies $int (p) < \Box \varphi$,

• 9. $[p]\varphi < \Box \varphi$,

Next, we prove that $\mathcal {L}$ and $\mathcal {L}_{K int }$ are equally expressive with respect to the pseudo-models. This result will also be useful in the completeness proof of $\mathbf {L}$ for topo-models. Toward proving the co-expressivity of $\mathcal {L}$ and $\mathcal {L}_{K int }$, we follow a similar strategy as in [2, 15] and use normal forms in $\mathcal {L}_{K int }$ as defined in [15, Definition 8].

Definition 3

(Normal form for the language $\mathcal {L}_{K int }$ ). We say a formula $\psi \in \mathcal {L}_{K int }$ is in normal form if it is a disjunction of conjunctions of the form

$$\begin{aligned} \delta := \alpha \wedge K\beta \wedge \hat{K}\gamma _1 \wedge \dots \wedge \hat{K}\gamma _n \end{aligned}$$

where $\alpha , \beta , \gamma _i\in \mathcal {L}_{ int }$ for all $1\le i\le n$.

Proposition 4

For any $\varphi , \varphi _i \in \mathcal {L}_{ int }$, the following is valid in all pseudo-models:

$$\begin{aligned} \Diamond (\varphi \wedge K\varphi _0\wedge \underset{1\le i\le n}{\bigwedge }\hat{K}\varphi _i)\leftrightarrow (\varphi \wedge int ( \varphi _0)\wedge \underset{1\le i\le n}{\bigwedge }\hat{K}( int (\varphi _0) \wedge \varphi _i))\qquad {\mathrm {(NF}_n)} \end{aligned}$$

We now have sufficient machinery to show that $\mathcal {L}$ and $\mathcal {L}_{K int }$ are equally expressive with respect to pseudo-models.

Theorem 4

$\mathcal {L}$ and $\mathcal {L}_{K int }$ are co-expressive with respect to pseudo-models.

The proof (in Appendix B.4 of the on-line version) uses the above proposition, as well as the co-expressivity of $\mathcal {L}_{!K int }$ and $\mathcal {L}_{K int }$, in a similar way to the analogue proofs concerning the arbitrary public announcement logic in [2, 15].

Theorem 4 will be used in the completeness proof of $\mathbf {L}$ for topo-models. Concerning expressivity of $\mathcal {L}$, we also obtain the following result with respect to topo-models.

Theorem 5

$\mathcal {L}$ and $\mathcal {L}_{K int }$ are co-expressive with respect to topo-models.

Theorem 6

$\mathcal {L}_{K\Box }$ and $\mathcal {L}_{K int }$ are also co-expressive with respect to topo-models.

Corollary 1

$\mathcal {L}$, $\mathcal {L}_{!K int }$ and $\mathcal {L}_{K int }$, as well as the language of topologic $\mathcal {L}_{K\Box }$ are all co-expressive with respect to topo-models.

Proof

The proof follows easily from Theorems 5 and 6, since $\mathcal {L}_{K int }\subseteq \mathcal {L}_{!K int }\subseteq \mathcal {L}$ and $\mathcal {L}_{K\Box }\subseteq \mathcal {L}$.

Corollary 2

Dynamic Topo-Logic $\mathcal {L}$ is decidable and has the Finite Model Property (and thus all its fragments, including in particular topologic, have these properties).

Proof

This follows from Corollary 1, together with the fact that $\mathcal {L}_{K int }$ is easily shown to have these properties, by a standard filtration argument. (This is already known, see e.g., [10, 14]).

Moreover, not only that $\mathcal {L}_{APAL}$ and $\mathcal {L}$ are co-expressive for topo-models, but also the effort modality $\Box$ and the topological APAL modality $\blacksquare$ are in fact equivalent, in the following sense.

Theorem 7

Let $t: \mathcal {L}_{APAL}\rightarrow \mathcal {L}$ be the map that replaces each instance of $\blacksquare$ with $\Box$. Then for every $\varphi \in \mathcal {L}_{APAL}$, we have that $\varphi \leftrightarrow t(\varphi )$ is valid in all topo-models.

4 Completeness

In this section we prove the completeness of the proof systems $\mathbf {L}$ with respect to (both pseudo- and) topo-models. The plan of our proof is as follows. We first prove completeness of $\mathbf {L}$ with respect to a canonical pseudo-model, consisting of maximally consistent witnessed theories. Roughly speaking, a theory is witnessed if every $\Diamond \varphi$ (occurring in every “existential context”) in the theory is “witnessed” by some atomic formula p, i.e. $\langle p \rangle \varphi$ occurs (in the same existential context) in the theory. Next, we use the co-expressivity of $\mathcal {L}$ and $\mathcal {L}_{K int }$, as well as the fact that $\mathcal {L}_{K int }$ cannot distinguish between a pseudo-model and its associated topo-model, to show that $\mathbf {L}$ is complete with respect to the canonical topo-model (associated to the canonical pseudo-model).

The appropriate notion of “existential contexts” is represented by possibility forms, in the following sense:

Definition 4

(“Pseudo-modalities”: necessity and possibility forms). For any finite string $s\in (\{\varphi \rightarrow \ | \ \varphi \in \mathcal {L}\}\cup \{K\}\cup \{\psi \ | \ \psi \in \mathcal {L}\})^*=NF$, we define pseudo-modalities [s] and $\langle s\rangle$, that generalize our dynamic modalities $[\psi ]$ and $\langle \psi \rangle$. These pseudo-modalities are functions mapping any formula $\varphi \in \mathcal {L}$ to another formula $[s]\varphi \in \mathcal {L}$ (necessity form), respectively $\langle s\rangle \varphi \in \mathcal {L}$ (possibility form). The definition is by recursion, putting for necessity forms: $[\lambda ] \varphi :=\varphi$, $[\varphi \rightarrow , s]\varphi :=\varphi \rightarrow [s]\varphi$, $[K, s]\varphi :=K[s]\varphi$, $[\psi , s]\varphi := [\psi ][s]\varphi$, where $\lambda$ is the empty string. For possibility forms, we put $\langle s\rangle \varphi :=\lnot [s]\lnot \varphi$.

Lemma 3

For every necessity form $s\in NF$, there exist formulas $\theta , \psi \in \mathcal {L}$ such that for all $\varphi \in \mathcal {L}$, we have

$$\begin{aligned} \vdash [s]\varphi \ \text{ iff } \ \vdash \psi \rightarrow [\theta ]\varphi . \end{aligned}$$

Proof

The proof follows similarly as in [2, Lemma 4.8] and [3, Lemma 2.7].

Lemma 4

The following rule is admissible in $\mathbf {L}$:

$$\begin{aligned} \text{ if } \ \vdash [s][p]\varphi \ \text{ then } \ \vdash [s]\Box \varphi , \ \text{ where } \ p\not \in P_s\cup P_\varphi . \end{aligned}$$

Proof

Suppose $\vdash [s][p]\varphi$. Then, by Lemma 3, there exist $\theta , \psi \in \mathcal {L}$ such that $\vdash \psi \rightarrow [\theta ][p]\varphi$. By the auxiliary reduction law (R$_{[p]}$) in Proposition 3, we get $\vdash \psi \rightarrow [\theta \wedge p]\varphi$. By the construction of the formulas $\psi$ and $\theta$, we know that $P_\psi \cup P_\theta \subseteq P_s$, and so $p\not \in P_\psi \cup P_\theta \cup P_\varphi$. Therefore, by ($[!]\Box$-intro)), we have $\vdash \psi \rightarrow [\theta ]\Box \varphi$. Applying again Lemma 3, we obtain $\vdash [s]\Box \varphi$.

Definition 5

For every countable set of propositional variables P, let $\mathcal {L}^P$ be the language of $\mathbf {L}$ based only on the propositional variables in P. Similarly, let $\mathcal {L}_{K int }^P, \mathcal {L}_{!K int }^P$ and $NF^P$ denote the corresponding languages restricted by P. A P-theory is a consistent set of formulas in $\mathcal {L}^P$. Here, “consistent” means consistent with respect to the axiomatization $\mathbf {L}$ formulated for $\mathcal {L}^P$. A maximal P -theory is a P-theory $\varGamma$ that is maximal with respect to $\subseteq$ among all P-theories; in other words, $\varGamma$ cannot be extended to another P-theory. A P -witnessed theory is a P-theory $\varGamma$ such that, for every $s\in NF^P$ and $\varphi \in \mathcal {L}^P$, if $\langle s\rangle \Diamond \varphi$ is consistent with $\varGamma$ then there is $p\in P$ such that $\langle s\rangle \langle p\rangle \varphi$ is consistent with $\varGamma$. A maximal P- witnessed theory $\varGamma$ is a P-witnessed theory that is not a proper subset of any P-witnessed theory.

Lemma 5

(Lindenbaum’s Lemma). Every P-witnessed theory $\varGamma$ can be extended to a maximal P-witnessed theory $T_{\varGamma }$.

Lemma 6

(Extension Lemma). Let P be a set of propositional variables and $P'$ be a countable set of fresh propositional variables, i.e., $P\cap P'=\emptyset$. Let $\overset{\sim }{P}=P\cup P'$. Then, every P-theory $\varGamma$ can be extended to a $\overset{\sim }{P}$-witnessed theory $\overset{\sim }{\varGamma }\supseteq \varGamma$, and hence to a maximal $\overset{\sim }{P}$-witnessed theory $T_\varGamma \supseteq \varGamma$.

We are now ready to build the canonical pseudo-model. For a fixed countable set P, we define an equivalence relation on maximal P-witnessed theories T and S:

$$\begin{aligned} T\sim S \ \text{ iff } \ (\forall \varphi \in \mathcal {L}^P)(K\varphi \in T \Rightarrow \varphi \in S). \end{aligned}$$

Definition 6

(Canonical Pseudo-Model for $T_0$ ). Let $T_0$ be a maximal P-witnessed theory. The canonical pseudo-model for $T_0$ is a tuple $\mathcal {M}^c=(X^c, \mathcal {O}^c, V^c)$ such that

• $X^c=\{T\subseteq \mathcal {L}^P\ | \ T \ \text{ is } \text{ a } \text{ maximal } P\text{-witnessed } \text{ theory } \text{ such } \text{ that } \ T\sim T_0\}$,

• $\mathcal {O}^c=\{\widehat{ int (\varphi ) } \ | \ \ \varphi \in \mathcal {L}^P\}$, where $\hat{\theta }=\{T\in X^c \ | \ \theta \in T\}$ for any $\theta \in \mathcal {L}^P$,

• $V^c(p)=\{T\in X^c \ | \ p\in T\}$.

We let $\tau ^c$ denote the topology generated by $\mathcal {O}^c$. The associated topo-model $\mathcal {M}^c_{\tau }=(X^c, \tau ^c, V^c)$ is called the canonical topo-model for $T_0$.

Clearly $\mathcal {M}^c=(X^c, \mathcal {O}^c, V^c)$ is a pre-model, but in fact we prove more, namely:

Lemma 7

$\mathcal {M}^c=(X^c, \mathcal {O}^c, V^c)$ is a pseudo-model.

Proof

We need to show that (a) $\mathcal {O}^c$ is closed under finite intersections and finite unions, and (b) for all $\varphi , \alpha \in \mathcal {L}^P$ we have $[\![ int (\varphi ) ]\!]^{\widehat{ int (\alpha ) }} \in \mathcal {O}^c$. The last item (b) follows from the Truth Lemma (see Appendix C.3 of the on-line version for the proof). We here sketch the proof for the first item: (a.1) closure under finite intersection follows from the normality of $int$, namely from the fact that $\vdash int (\varphi ) \wedge int (\psi ) \leftrightarrow int (\varphi \wedge \psi )$. (a.2) closure under finite union follows from the fact that $\vdash ( int (\varphi ) \vee int (\psi ) )\leftrightarrow int ( int (\varphi ) \vee int (\psi ) )$, and that $int ( int (\varphi ) \vee int (\psi ) ) \in \mathcal {L}^P$.

Lemma 8

Let $T\in X^c$, $\varphi , \alpha \in \mathcal {L}^P$ such that $int (\alpha ) \in T$ and $K[\alpha ]\varphi \not \in T$. Then, there is $S\in X^c$ with $int (\alpha ) \in S$ and $[\alpha ]\varphi \not \in S$.

Lemma 9

(Truth Lemma). Let $\mathcal {M}^c=(X^c, \mathcal {O}^c, V^c)$ be the canonical pseudo-model for a maximal P-witnessed theory $T_0$ and $\varphi \in \mathcal {L}^P$. Then, for all $\alpha \in \mathcal {L}^P$ we have

$$\begin{aligned}{}[\![ \varphi ]\!]^{\widehat{ int (\alpha ) }} =\widehat{ \langle \alpha \rangle \varphi }. \end{aligned}$$

Proof

The proof is by induction on the well-founded partial order < on formulas introduced in Lemma 2. We assume the following Induction Hypothesis (IH): For $\psi <\varphi$, we have $[\![ \psi ]\!]^{\widehat{ int (\alpha ) }} =\widehat{ \langle \alpha \rangle \psi }$ for all $\alpha \in \mathcal {L}^P$.

Base case $\varphi = p$:

Case $\varphi := \lnot \psi$:

Case $\varphi = \psi \wedge \chi$:

Case $\varphi = K\psi$:

($\Rightarrow$):

Suppose $T\in [\![ K\psi ]\!]^{\widehat{ int (\alpha ) }}$. This implies, by the semantic clause of K, that $T\in \widehat{ int (\alpha ) }$ and $[\![ \psi ]\!]^{\widehat{ int (\alpha ) }}=\widehat{ int (\alpha ) }$. We want to show that . By Proposition 3-($\langle !\rangle$) and the reduction axiom (R$_K$), we obtain $\vdash \langle \alpha \rangle K\psi \leftrightarrow int (\alpha ) \wedge K[\alpha ]\psi$. We therefore only need to show that $T\in \widehat{ int (\alpha ) }$ and . We have the former by the assumption. Suppose toward contradiction that , i.e., $K[\alpha ]\psi \not \in T$. Then, by Lemma 8, there exists $S\in X^c$ such that $int (\alpha ) \in S$ and $[\alpha ]\psi \not \in S$. Since $\vdash \langle \alpha \rangle \psi \rightarrow [\alpha ]\psi$, we obtain $\langle \alpha \rangle \psi \not \in S$. Therefore, by IH, we have $S\not \in [\![ \psi ]\!]^{\widehat{ int (\alpha ) }}$. Thus, since $S\in \widehat{ int (\alpha ) }$, we then conclude $[\![ \psi ]\!]^{\widehat{ int (\alpha ) }}\not =\widehat{ int (\alpha ) }$. By the semantics of K, this means that $[\![ K\psi ]\!]^{\widehat{ int (\alpha ) }} =\emptyset$, contradiction our first assumption. Hence, .

($\Leftarrow$):

Suppose . Then, by the equality $\langle \alpha \rangle K\psi \leftrightarrow int (\alpha ) \wedge K[\alpha ]\psi$, we have $T\in \widehat{ int (\alpha ) }$ and . Let $S\in \widehat{ int (\alpha ) }$. Since $S\sim T$ and , we also have $[\alpha ]\psi \in S$. Therefore, by Proposition 3-($\langle !\rangle$), we obtain $\langle \alpha \rangle \psi \in S$. This implies, by IH, that $S\in [\![ \psi ]\!]^{\widehat{ int (\alpha ) }}$. Since this holds for all $S\in \widehat{ int (\alpha ) }$, we have $[\![ \psi ]\!]^{\widehat{ int (\alpha ) }}=\widehat{ int (\alpha ) }$. Hence, $[\![ K\psi ]\!]^{\widehat{ int (\alpha ) }}=\widehat{ int (\alpha ) }\ni T$.

Case $\varphi = int (\psi )$:

($\Rightarrow$):

Suppose $T\in [\![ int (\psi ) ]\!]^{\widehat{ int (\alpha ) }}$. Then, by the semantics of $int$, there exists $U\in \mathcal {O}^c$ such that $T\in U\subseteq \widehat{ int (\alpha ) }$ and $U\subseteq [\![ \psi ]\!]^{\widehat{ int (\alpha ) }}$ (since $\mathcal {O}^c$ constitutes a basis for $\tau ^c$). Then, by IH, we have $U\subseteq \widehat{\langle \alpha \rangle \psi }$. By the construction of $\mathcal {O}^c$, we know that $U=\widehat{ int (\gamma ) }$ for some $\gamma \in \mathcal {L}^P$. We therefore obtain that $T\in \widehat{ int (\gamma ) }\subseteq \widehat{\langle \alpha \rangle \psi }.$ This means that, for all $S\in \widehat{ int (\gamma ) }$, we have $S\in \widehat{\langle \alpha \rangle \psi }$. Therefore, $\{\theta \in \mathcal {L}^P\ | \ K\theta \in T\}\cup \{\lnot ( int (\gamma ) \rightarrow \langle \alpha \rangle \psi )\}$ is inconsistent. Then there exists a $\chi \in \{\theta \in \mathcal {L}^P\ | \ K\theta \in T\}$ such that $\vdash \chi \rightarrow ( int (\gamma ) \rightarrow \langle \alpha \rangle \psi )$. Thus, by the normality of K, we have $\vdash K\chi \rightarrow K( int (\gamma ) \rightarrow \langle \alpha \rangle \psi )$. As $K\chi \in T$, we obtain $K( int (\gamma ) \rightarrow \langle \alpha \rangle \psi )\in T$. Then by axiom (K-$int$), we have $int ( int (\gamma ) \rightarrow \langle \alpha \rangle \psi ) \in T$. Since $int$ is an S4 modality, we have $int (\gamma ) \rightarrow int (\langle \alpha \rangle \psi ) \in T$. Since $T\in \widehat{ int (\gamma ) }$, we obtain $int (\langle \alpha \rangle \psi ) \in T$. Moreover, we have

$$\begin{aligned} \vdash&int (\langle \alpha \rangle \psi ) \leftrightarrow int ( int (\alpha ) \wedge [\alpha ]\psi ) \qquad \qquad \qquad \qquad \quad ~~{\text {(Proposition}}\,{\text {3-(}}\langle !\rangle \text {))}\\ \vdash&int ( int (\alpha ) \wedge [\alpha ]\psi ) \leftrightarrow ( int (\alpha ) \wedge int ([\alpha ]\psi ) )\\ \vdash&( int (\alpha ) \wedge int ([\alpha ]\psi ) ) \leftrightarrow ( int (\alpha ) \wedge ( int (\alpha ) \rightarrow [\alpha ] int (\psi ))) \quad \quad {\text {(Proposition}}\,\text {3-(R}_ int {\text {))}}\\ \vdash&( int (\alpha ) \wedge ( int (\alpha ) \rightarrow [\alpha ] int (\psi ))) \leftrightarrow ( int (\alpha ) \wedge [\alpha ] int (\psi ))) \\ \vdash&( int (\alpha ) \wedge [\alpha ] int (\psi ))) \leftrightarrow \langle \alpha \rangle int (\psi ) \qquad \qquad \qquad \qquad \qquad \quad ~~{{\text {(Proposition}}\,{\text {3-(}}\langle !\rangle \text {))}} \end{aligned}$$

Therefore, as T is maximal, we obtain $\langle \alpha \rangle int (\psi ) \in T$, i.e., .

($\Leftarrow$):

Suppose . This implies, by the above derivation, that . By the constraction of $\mathcal {O}^c$, we have . Moreover, by the T-axiom for $int$, we have that . By IH, we also have that . Therefore , i.e., $T\in [\![ int (\psi ) ]\!]^{\widehat{ int (\alpha ) }}$.

Case $\varphi = \langle \chi \rangle \psi$:

Case $\varphi = \Box \psi$:

($\Rightarrow$):

Suppose $T\in [\![ \Box \psi ]\!]^{\widehat{ int (\alpha ) }}$, i.e., $(T, \widehat{ int (\alpha ) })\,\models \,\Box \psi$. This means that for all $U\in \mathcal {O}$ with $T\in U\subseteq \widehat{ int (\alpha ) }$, we have $(T, U)\,\models \,\psi$. This in particular implies that $(T, \widehat{ int (\alpha ) })\,\models \,[p] \psi$ for all $p\in P$. To show, let $p\in P$ and suppose $(T, \widehat{ int (\alpha ) })\,\models \, int (p)$, i.e., $T\in Int ([\![ p]\!]^{\widehat{ int (\alpha ) }}) =[\![ int (p) ]\!]^{\widehat{ int (\alpha ) }}$. Since $int (p) < \Box \psi$ (see Lemma 2.8), we know by IH that . But, as shown in the case for the modality $int$ above, $\vdash \langle \alpha \rangle int (p) \leftrightarrow int (\langle \alpha \rangle p)$, hence, , thus, $[\![ int (p) ]\!]^{\widehat{ int (\alpha ) }}\in \mathcal {O}^c$. Hence, by the first assumption, we obtain $(T, Int ([\![ p]\!]^{\widehat{ int (\alpha ) }}) )\,\models \,\psi$, thus, $(T, \widehat{ int (\alpha ) })\,\models \,[p]\psi$. Therefore, $T\in [\![ [p]\psi ]\!]^{\widehat{ int (\alpha ) }}$ for all $p\in P$. Then, by IH (since $[p] \psi < \Box \psi$, by Lemma 2.9), we have , thus, $\langle \alpha \rangle [p] \psi \in T$. Hence, by Proposition 3-($\langle !\rangle$), $int (\alpha ) \wedge [\alpha ][p]\psi \in T$ for all $p\in P$. Since T is P-witnessed and maximal, we then obtain $int (\alpha ) \wedge [\alpha ]\Box \psi \in T$. Then, by Proposition 3-($\langle !\rangle$), we conclude $\langle \alpha \rangle \Box \psi \in T$.

($\Leftarrow$):

Suppose . This means (by Proposition 3-($\langle !\rangle$)) that , i.e., that $int (\alpha ) \in T$ and $[\alpha ]\Box \psi \in T$. Then, by axiom ($[!]\Box$-elim), we have that $[\alpha \wedge \chi ]\psi \in T$ for all $\chi \in \mathcal {L}^P$. We want to show that $T\in [\![ \Box \psi ]\!]^{\widehat{ int (\alpha ) }}$. Let $U\in \mathcal {O}^c$ such that $T\in U \subseteq \widehat{ int (\alpha ) }$ and show $T\in [\![ \psi ]\!]^U$. By the construction of $\mathcal {O}^c$, we know that $U=\widehat{ int (\gamma ) }$ for some $\gamma \in \mathcal {L}^P$. We therefore have that . Hence, $int (\alpha \wedge \gamma ) \wedge [\alpha \wedge \gamma ]\psi \in T$. Therefore, by Proposition 3-($\langle !\rangle$) and the fact that T is maximal, we obtain $\langle \alpha \wedge \gamma \rangle \psi \in T$. Thus, by IH (since $\psi < \Box \psi$, by Lemma 2.1), , i.e., $T\in [\![ \psi ]\!]^U$.

Lemma 10

Let $\mathcal {M}=(X, \mathcal {O}, V)$ be a pseudo-model and $\mathcal {M}_\tau =(X, \tau _\mathcal {O}, V)$ be the associated topo-model. Then, for all $\varphi \in \mathcal {L}_{K int }$ and $(x, U)\in ES(\mathcal {M})$, we have

$$\begin{aligned} (x, U)\,\models _\mathcal {M}\varphi \ \text{ iff } \ (x, U)\,\models _{\mathcal {M}_\tau } \varphi . \end{aligned}$$

Corollary 3

$\mathbf {L}$ is complete for canonical pseudo-models and canonical topo-models (and so also complete wrt pseudo-models, as well as wrt topo-models).

Proof

Let $\varphi$ be an $\mathbf {L}$-consistent formula, i.e., it is a $P_\varphi$-theory. Then, by Lemma 6, it can be extended to a maximal $\mathrm {Prop}$-witnessed theory T. Then, by axiom (R$[\top ]$), we have $\langle \top \rangle \varphi \in T$, i.e., $T\in \widehat{\langle \top \rangle \varphi }$. Then, by Truth Lemma (Lemma 9), we obtain that $(T, X^c)\,\models _{\mathcal {M}^c} \varphi$, where $\mathcal {M}^c=(X^c, \mathcal {O}^c, V^c)$ is the canonical pseudo-model for T. This proves the first completeness claim. As for the second: by the co-expressivity of $\mathcal {L}_{K int }$ and $\mathcal {L}$ on pseudo-models (Theorem 4), there exists a $\psi \in \mathcal {L}_{K int }$ such that $\varphi \leftrightarrow \psi$ is valid in all pseudo-models. We therefore have $(T, X^c)\,\models _{\mathcal {M}^c} \psi$. By Lemma 10, we obtain $(T, X^c)\,\models _{\mathcal {M}_\tau } \psi$ where $\mathcal {M}_\tau$ is the canonical topo-model. Using again the semantic equivalence of $\varphi$ and $\psi$ (applied to the model $\mathcal {M}_\tau$), we conclude that $(T, X^c)\,\models _{\mathcal {M}_\tau } \varphi$.

5 Conclusions

This paper throws new light on Topologic and Topo-APAL, elucidating their relations with each other and other modal logics for topology. The addition of dynamic modalities is shown to greatly simplify the axiomatization and completeness proof of Topologic. In on-going work we look at doxastic versions of this logic, able to capture learning-theoretic notions; while in future work we plan to investigate multi-agent versions.