APAL with Memory Is Better

Abstract

We introduce Arbitrary Public Announcement Logic with Memory (APALM), obtained by adding to the models a ‘memory’ of the initial states, representing the information before any communication took place (“the prior”), and adding to the syntax operators that can access this memory. We show that APALM is recursively axiomatizable (in contrast to the original Arbitrary Public Announcement Logic, for which the corresponding question is still open). We present a complete recursive axiomatization, that uses a natural finitary rule, we study this logic’s expressivity and the appropriate notion of bisimulation.

1 Introduction

Arbitrary Public Announcement Logic (APAL) and its relatives are natural extensions of Public Announcements Logic (PAL), involving the addition of operators $\square \varphi$ and $\Diamond \varphi$, quantifying over public announcements $[\theta ]\varphi$ of some given type. These logics are of great interest both philosophically and from the point of view of applications. Motivations range from supporting an analysis of Fitch’s paradox [16] by modeling notions of ‘knowability’ (expressible as $\Diamond K\varphi$), to determining the existence of communication protocols that achieve certain goals (cf. the famous Russian Card problem, given at a mathematical Olympiad [17]), and more generally to epistemic planning [9], and to inductive learnability in empirical science [5]. Many such extensions have been investigated, starting with the original APAL [2], and continuing with its variants GAL (Group Announcement Logic) [1], Future Event Logic [20], FAPAL (Fully Arbitrary Public Announcement Logic) [24], APAL$^+$ (Positive Arbitrary Announcement Logic) [19], BAPAL (Boolean Arbitrary Public Announcement Logic) [18], etc.

One problem with the above formalisms, with the exception of BAPAL¹, is that they all use infinitary axiomatizations. It is therefore not guaranteed that the validities of these logics are recursively enumerable.² The seminal paper on APAL [2] proved completeness using an infinitary rule, and then went on to claim that in theorem-proving³ this rule can be replaced by the following finitary rule: from $\chi \rightarrow [\theta ] [p]\varphi$, infer $\chi \rightarrow [\theta ]\square \varphi$, as long as the propositional variable p is “fresh”. This is a natural $\square$-introduction rule, similar to the introduction rule for universal quantifier in FOL, and it is based on the intuition that variables that do not occur in a formula are irrelevant for its truth value, and thus can be taken to stand for any “arbitrary” formula (via some appropriate change of valuation). However, the soundness of this rule was later disproved via a counterexample by Kuijer [11]. Thus, a long-standing open question concerns finding a ‘strong’ version of APAL for which there exists a recursive axiomatization.⁴

In this paper, we solve this open question. Our diagnosis of Kuijer’s counterexample is that it makes an essential use of a known undesirable feature of PAL and APAL, namely their lack of memory: the updated models “forget” the initial states. As a consequence, the expressivity of the APAL $\square$-modality reduces after any update. This is what invalidates the above rule. We fix this problem by adding to the models a memory of the initial epistemic situation $W^0$, representing the information before any non-trivial communication took place (“the prior”). Since communication - gaining more information - deletes possibilities, the set W of currently possible states is a (possibly proper) subset of the set $W^0$ of initial states. On the syntactic side, we add an operator $\varphi ^0$ saying that “$\varphi$ was initially the case” (before all communication). To mark the initial states, we also need a constant 0, stating that “no non-trivial communication has taken place yet”. Therefore, 0 will be true only in the initial epistemic situation. It is convenient, though maybe not absolutely necessary, to add a universal modality $U\varphi$ that quantifies over all currently possible states.⁵ In the resulting Arbitrary Public Announcement Logic with Memory (APALM), the arbitrary announcement operator $\square$ quantifies over updates (not only of epistemic formulas but) of arbitrary formulas that do not contain the operator $\square$ itself.⁶ As a result, the range of $\square$ is wider than in standard APAL, covering announcements that may refer to the initial situation (by the use of the operators 0 and $\varphi ^0$) or to all currently possible states (by the use of $U\varphi$).

We show that the original finitary rule proposed in [2] is sound for APALM and, moreover, it forms the basis of a complete recursive axiomatization.⁷ Besides its technical advantages, APALM is valuable in its own respect. Maintaining a record of the initial situation in our models helps us to formalize updates that refer to the ‘epistemic past’ such as “what you said, I knew already” [15]. This may be useful in treating certain epistemic puzzles involving reference to past information states, e.g. “What you said did not surprise me” [12]. The more recent Cheryl’s Birthday problem also contains an announcement of the form “At first I didn’t know when Cheryl’s birthday is, but now I know” (although in this particular puzzle the past-tense announcement is redundant and plays no role in the solution).⁸ See [15] for more examples.

Note though that the ‘memory’ of APALM is of a very specific kind. Our models do not remember the whole history of communication, but only the initial epistemic situation (before any communication). Correspondingly, in the syntax we do not have a ‘yesterday’ operator $Y\varphi$, referring to the previous state just before the last announcement as in [14], but only the operator $\varphi ^0$ referring to the initial state. We think of this ‘economy’ of memory as a (positive) “feature, not a bug” of our logic: a detailed record of all history is simply not necessary for solving the problem at hand. In fact, keeping all the history and adding a $Y\varphi$ operator would greatly complicate our task by invalidating some of the standard nice properties of PAL (e.g. the composition axiom, stating that any sequence of announcements is equivalent to a single announcement).⁹

So we opt for simplicity, enriching the models and language just enough to recover the full expressivity of $\square$ after updates, and thus establish the soundness of the $\square$-introduction rule. The minimalistic-memory character of our semantics is rather natural and it is similar to the one encountered in Bayesian models¹⁰, with their distinction between ‘prior’ and ‘posterior’ (aka current) probabilities.¹¹

On the technical side, our completeness proof involves an essential detour into an alternative semantics for APALM (‘pseudo-models’), in the style of Subset Space Logics (SSL) [10, 13]. This reveals deep connections between apparently very different formalisms. Moreover, this alternative semantics is of independent interest, giving us a more general setting for modeling knowability and learnability (see, e.g., [5, 7, 8]). Various combinations of PAL or APAL with subset space semantics have been investigated in the literature [4,5,6,7, 21, 22, 25, 26]. Following SSL-style, our pseudo-models come with a given family of admissible sets of worlds, which in our context represent “publicly announceable” (or communicable) propositions.¹² We interpret $\square$ in pseudo-models as the so-called ‘effort’ modality of SSL, which quantifies over updates with announceable propositions (regardless of whether they are syntactically definable or not). The finitary $\square$-introduction rule is obviously sound for the effort modality, because of its more ‘semantic’ character. This observation, together with the fact that APALM models (unlike original APAL models) can be seen as a special case of pseudo-models, lie at the core of our soundness and completeness proof.

Due to the page limit, we skipped some of the proofs. Readers interested to see all the relevant proofs, as well as a other related results, may consult the extended online version of this paper at https://analuciavsblog.wordpress.com/page/.

2 Syntax, Semantics, and Axiomatization

Let Prop be a countable set of propositional variables and $\mathcal {AG}=\{1, \dots , n\}$ be a finite set of agents. The language $\mathcal {L}$ of APALM (Arbitrary Public Announcement Logic with Memory) is recursively defined by the grammar:

$$ \varphi \,\, {:}{:}{=}\,\, \top \ | \ p \ | \ 0 \ | \ \varphi ^0 \ | \ \lnot \varphi \ | \ \varphi \wedge \varphi \ | \ K_i \varphi \ | \ U\varphi \ | \ \langle \theta \rangle \varphi \ | \ \Diamond \varphi , $$

with $p\in Prop$, $i\in \mathcal {AG}$, and $\theta \in \mathcal {L}_{-\Diamond }$ is a formula in the sublanguage $\mathcal {L}_{-\Diamond }$ obtained from $\mathcal {L}$ by removing the $\Diamond$ operator. Given a formula $\varphi \in \mathcal {L}$, we denote by $P_\varphi$ the set of all propositional variables occurring in $\varphi$. We employ the usual abbreviations for $\bot$ and the propositional connectives $\vee , \rightarrow , \leftrightarrow$. The dual modalities are defined as $\hat{K}_i \varphi :=\lnot K_i \lnot \varphi$, $E\varphi :=\lnot U \lnot \varphi$, $\square \varphi := \lnot \Diamond \lnot \varphi$, and $[\theta ]\varphi :=\lnot \langle \theta \rangle \lnot \varphi$.¹³

We read $K_i \varphi$ as “$\varphi$ is known by agent i”; $\langle \theta \rangle \varphi$ as “$\theta$ can be truthfully announced, and after this public announcement $\varphi$ is true”. U and E are the global universal and existential modalities quantifying over all current possibilities: $U\varphi$ says that “$\varphi$ is true in all current alternatives of the actual state”. $\Diamond \varphi$ and $\square \varphi$ are the (existential and universal) arbitrary announcement operators, quantifying over updates with formulas in $\mathcal {L}_{-\Diamond }$. We can read $\square \varphi$ as “$\varphi$ is stably true (under public announcements)”: i.e., $\varphi$ stays true no matter what (true) announcements are made. The constant 0, meaning that “no (non-trivial) announcements took place yet”, holds only at the initial time. Similarly, the formula $\varphi ^0$ means that “initially (prior to all communication), $\varphi$ was true”.

Definition 1

(Model, Initial Model, and Relativized Model)

• A model is a tuple ${\mathcal M}= (W^0, W, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$, where $W\subseteq W^0$ are non-empty sets of states, $\sim _i\subseteq W^0\times W^0$ are equivalence relations labeled by ‘agents’ $i\in \mathcal {AG}$, and $\Vert \cdot \Vert :Prop\rightarrow {\mathcal P}(W^0)$ is a valuation function that maps every propositional atom $p\in Prop$ to a set of states $\Vert p\Vert \subseteq W^0$. $W^0$ is the initial domain, representing the initial informational situation before any communication took place; its elements are called initial states. In contrast, W is the current domain, representing the current information, and its elements are called current states.

• For every model ${\mathcal M}= (W^0, W, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$, we define its initial model ${\mathcal M}^0= (W^0, W^0, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$, whose current and initial domains are both given by the initial domain of the original model ${\mathcal M}$.

• Given a model ${\mathcal M}= (W^0, W, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$ and a set $A\subseteq W$, we define the relativized model ${\mathcal M}|A= (W^0, A, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$.

For states $w\in W$ and agents i, we will use the notation $w_i \,\, :=\,\, \{s\in W: w\sim _i s\}$ to denote the restriction to W of w’s equivalence class modulo $\sim _i$.

Definition 2

(Semantics). Given a model ${\mathcal M}= (W^0, W, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$, we define a truth set $[\![ \varphi ]\!]_\mathcal {M}$ for every formula $\varphi$. When the current model ${\mathcal M}$ is understood, we skip the subscript and simply write $[\![ \varphi ]\!]$. The definition of $[\![ \varphi ]\!]$ is by recursion on $\varphi$:

Observation 1

Note that we have

$$w\in [\![ \square \varphi ]\!] \,\, \,\, \text{ iff } \,\, \,\, w\in [\![ [\theta ]\varphi ]\!] \text{ for } \text{ every } \theta \in \mathcal {L}_{-\Diamond }.$$

In some of our inductive proofs, we will need a complexity measure on formulas different from the standard one¹⁴:

Lemma 1

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

Proposition 1

We have $[\![ \varphi ]\!]\subseteq W$, for all formulas $\varphi \in \mathcal {L}$.

(The proof, in the online version, is by induction on the complexity < from Lemma 1.)

Definition 3

(APALM Models and Validity). An APALM model is a tuple ${\mathcal M}=(W^0, W, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$ such that $W=[\![ \theta ]\!]_{\mathcal {M}^0}$ for some $\theta \in {\mathcal L}_{-\Diamond }$; i.e. $\mathcal {M}$ can be obtained by updating its initial model $\mathcal {M}^0$ with some formula in ${\mathcal L}_{-\Diamond }$. A formula $\varphi$ is valid on APALM models if it is true in all current states $s\in W$ (i.e. $[\![ \varphi ]\!]_{\mathcal {M}}=W$) for every APALM model ${\mathcal M}= (W^0, W, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$.

APALM models are our intended models, in which the current information range comes from updating the initial range with some public announcement.

We arrive now at the main result of our paper.

Theorem 1

(Soundness and Completeness) APALM validities are recursively enumerable. Indeed, the following axiom system $\mathbf {APALM}$ (given in Table 1, where recall that $P_\varphi$ is the set of propositional variables in $\varphi$) is sound and complete wrt APALM models:

Table 1. The axiomatization $\mathbf {APALM}$. (Here, $\varphi ,\psi ,\chi \in \mathcal {L}$, while $\theta , \rho \in \mathcal {L}_{-\Diamond }$.)

Intuitive Reading of the Axioms. Parts (I) and (II) should be obvious. The axiom R$[\top ]$ says that updating with tautologies is redundant. The reduction laws that do not contain $^0$, U or 0 are well-known PAL axioms. R$_U$ is the natural reduction law for the universal modality. The axiom R$^0$ says that the truth value of $\varphi ^0$ formulas stays the same in time (because the superscript $^0$ serves as a time stamp), so they can be treated similarly to atoms. Ax$_0$ says that 0 was initially the case, and R$_0$ says that at any later stage (after any update) 0 can only be true if it was already true before the update and the update was trivial (universally true). Together, these two say that the constant 0 characterizes states where no non-trivial communication has occurred. Axiom 0-U is a sychronicity constraint: if no non-trivial communication has taken place yet, then this is the case in all the currently possible states. Axiom 0-eq says that initially, $\varphi$ is equivalent to its initial correspondent $\varphi ^0$. The Equivalences with $^0$ express that $^0$ distributes over negation and over conjunction. Imp$^0_{\square }$ says that if initially $\varphi$ was stably true (under any further announcements), then $\varphi$ is the case now. Taken together, the elimination axiom $[!]\square$-elim and introduction rule $[!]\square$-intro say that $\varphi$ is a stable truth after an announcement $\theta$ iff $\varphi$ stays true after any more informative announcement (of the form $\theta \wedge \rho$).¹⁵

Proposition 2

The following schemas and inference rules are derivable in $\mathbf {APALM}$, where $\varphi , \psi , \chi \in \mathcal {L}$ and $\theta \in \mathcal {L}_{-\Diamond }$:

Proposition 3

All S4 axioms and inference rules for $\square$ are derivable in $\mathbf {APALM}$.

3 An Analysis of Kuijer’s Counterexample

To understand Kuijer’s counterexample [11] to the soundness of the finitary $\square$-elimination rule for the original APAL, recall that in the APAL $\square$ quantifies only over updates with epistemic formulas. More precisely, the APAL semantics of $\square$ is given by

$$w\in [\![ \square \varphi ]\!] \,\, \,\, \text{ iff } \,\, \,\, w\in [\![ [\theta ]\varphi ]\!] \text{ for } \text{ every } \theta \in \mathcal {L}_{epi},$$

where $\mathcal {L}_{epi}$ is the sublanguage generated from propositional atoms $p\in Prop$ using only the Boolean connectives $\lnot \varphi$ and $\varphi \wedge \psi$ and the epistemic operators $K_i\varphi$.

Kuijer takes the formula $\gamma := p\wedge \hat{K}_b \lnot p \wedge \hat{K}_a K_b p$, and shows that

$$[\hat{K}_b p]\square \lnot \gamma \rightarrow [q]\lnot \gamma .$$

is valid on APAL models. (In fact, it is also valid on APALM models!) But then, by the $[!]\square$-intro rule (or rather, by its weaker consequence in Proposition 2(5)), the formula

$$[\hat{K}_b p]\square \lnot \gamma \rightarrow \square \lnot \gamma $$

should also be valid. But this is contradicted by the model $\mathcal {M}$ in Fig. 1. The premise $[\hat{K}_b p]\square \lnot \gamma$ is true at w in $\mathcal {M}$, since $\square \lnot \gamma$ holds at w in $\mathcal {M}|{[\![ \hat{K}_b p]\!]}$: indeed, the only way to falsify it would be by deleting the lower-right node from Fig. 2a while keeping (all other nodes, and in particular) the upper-right node. But in $\mathcal {M}|{[\![ \hat{K}_b p]\!]}$ the upper and lower right nodes can’t be separated by epistemic sentences: they are bisimilar.

Fig. 1.

An initial model $\mathcal {M}$. Worlds are nodes in the graph, valuation is given by labeling the node with the true atoms, and epistemic relations are given by labeled arrows.

Fig. 2.

Two updates of $\mathcal {M}$.

In contrast, the conclusion $\square \lnot \gamma$ is false at w in $\mathcal {M}$, since in that original model the two mentioned nodes could be separated. Indeed, we could perform an alternative update with the formula $p\vee \hat{K}_a r$, yielding the epistemic model $\mathcal {M}|{[\![ p\vee \hat{K}_a r]\!]}$ shown in Fig. 2b, in which $\gamma$ is true at w (contrary to the assertion that $\square \lnot \gamma$ was true in $\mathcal {M}$).

To see that the counterexample does not apply to APALM, notice that APALM models keep track of the initial states, so technically speaking the updated model $\mathcal {M}|{[\![ \hat{K}_b p]\!]}$ consists now of the initial structure in Fig. 1 together with current set of worlds W in Fig. 2a. But in this model, $\square \lnot \gamma$ is no longer true at w (and so the premise $[\hat{K}_b p]\square \lnot \gamma$ was not true in $\mathcal {M}$ when considered as an APALM model!). Indeed, we can perform a new update of $\mathcal {M}|{[\![ \hat{K}_b p]\!]}$ with the formula $(p\vee \hat{K}_a r)^0$, which yields an updated model whose current set of worlds is given in Fig. 3:

Fig. 3.

The current worlds resulting from updating $\mathcal {M}|{[\![ \hat{K}_b p]\!]}$ with $(p\vee \hat{K}_a r)^0$.

Note that, in this new model, $\gamma$ is the case at w (-thus showing that $\square \lnot \gamma$ was not true at w in $\mathcal {M}|{[\![ \hat{K}_b p]\!]}$). So the counterexample simply does not work for APALM.

Moreover, we can see that the un-soundness of $[!]\square$-intro rule for APAL has to do with its lack of memory, which leads to information loss after updates: while initially (in $\mathcal {M}$) there were epistemic sentences (e.g. $p\vee \hat{K}_a r$) that could separate the two nodes mentioned above, there are no such sentences after the update.

APALM solves this by keeping track of the initial states, and referring back to them, as in $(p\vee \hat{K}_a r)^0$.

4 Soundness, via Pseudo-model Semantics

To start with, note that the even the soundness of our axiomatic system is not a trivial matter. As we saw from Kuijer’s counterexample, the analogue of our finitary $\square$-introduction rule was not sound for APAL. To prove its soundness on APALM models, we need a detour into an equivalent semantics, in the style of Subset Space Logics (SSL) [10, 13]: pseudo-models.¹⁶

We first introduce an auxiliary notion: ‘pre-models’ are just SSL models, coming with a given family $\mathcal {A}$ of “admissible sets” of worlds (which can be thought of as the communicable propositions). We interpret $\square$ in these structures as the so-called “effort modality” of SSL, which quantifies over updates with admissible propositions in $\mathcal {A}$. Our ‘pseudo-models’ are pre-models with additional closure conditions (saying that the family of admissible sets includes the valuations and is closed under complement, intersection and epistemic operators). These conditions imply that every set definable by $\Diamond$-free formulas is admissible, and this ensures the soundness of our $\square$-elimination axiom on pseudo-models. As for the soundness of the long-problematic $\square$-introduction rule on (both pre- and) pseudo-models, this is due to the fact that the effort modality has a more ‘robust’ range than the arbitrary announcement operator: it quantifies over admissible sets, regardless of whether these sets are syntactically definable or not. Soundness with respect to our intended (APALM) models then follows from the observation that they (in contrast to the original APAL models) are in fact equivalent to a special case of pseudo-models: the “standard” ones (in which the admissible sets in $\mathcal {A}$ are exactly the sets definable by $\Diamond$-free formulas).

Definition 4

(Pre-model). A pre-model is a tuple ${\mathcal M}= (W^0, \mathcal {A}, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$, where $W^0$ is the prior domain, $\sim _i$ are equivalence relations on $W^0$, $\Vert \cdot \Vert :Prop\rightarrow {\mathcal P}(W^0)$ is a valuation map, and ${\mathcal A}\subseteq {\mathcal P}(W^0)$ is a family of subsets of the initial domain, called admissible sets (representing the propositions that can be publicly announced).

Given a set $A\subseteq W^0$ and a state $w\in A$, we use the notation $w^A_i \,\, :=\,\, \{s\in A: w\sim _i s\}$ to denote the restriction to A of w’s equivalence class modulo $\sim _i$.

Definition 5

(Pre-model Semantics). Given a pre-model ${\mathcal M}=(W^0, \mathcal {A}, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$, we recursively define a truth set $[\![ \varphi ]\!]_A$ for every formula $\varphi$ and subset $A\subseteq W^0$:

Observation 2

Note that, for all $w\in A$, we have

$$w\in [\![ \square \varphi ]\!]_A \,\, \text{ iff } \,\, \forall B\in {\mathcal A} (w\in B\subseteq A\Rightarrow w\in [\![ \varphi ]\!]_B),$$

which fits with the semantics of the ‘effort’ modality in SSL [10, 13]. Moreover, it is easy to see that $[\![ \varphi ]\!]_A\subseteq A$ for all $A\in \mathcal {A}$ and $\varphi \in \mathcal {L}$.

Definition 6

(Pseudo-models and Validity). A pseudo-model is a pre-model ${\mathcal M}= (W^0, \mathcal {A}, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$, satisfying the following closure conditions:

A formula $\varphi \in \mathcal {L}$ is valid on pseudo-models if it is true in all admissible sets $A\in \mathcal {A}$ of every pseudo-model $\mathcal {M}$, i.e, $[\![ \varphi ]\!]_{A}=A$ for all $A\in \mathcal {A}$ and all $\mathcal {M}$.

Proposition 4

Given a pseudo-model $(W^0, \mathcal {A}, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$, $A\in \mathcal {A}$ and $\theta \in \mathcal {L}_{-\Diamond }$, we have $[\![ \theta ]\!]_A \in \mathcal {A}$.

Proof

The proof is by subformula induction on $\theta$, where we denote by IH the induction hypothesis. The base cases and the inductive cases for the Booleans are immediate (using the conditions in Definition 6).

Case $\theta :=\psi ^0$. By the semantics, $[\![ \psi ^0]\!]_A=[\![ \psi ]\!]_{W^0}\cap A\in {\mathcal A}$, since $[\![ \psi ]\!]_{W^0}\in \mathcal {A}$ (by the fact that $W^0\in \mathcal {A}$ and IH), $A\in \mathcal {A}$ (by assumption), and ${\mathcal A}$ is closed under intersection.

Case $\theta :=K_i\psi$.

Case $\theta :=U\psi$. By definition, $[\![ U\psi ]\!]_A\in \{\emptyset , A\}\subseteq {\mathcal A}$.

Case $\theta :=\langle \varphi \rangle \psi$. Since $A\in {\mathcal A}$, we have $[\![ \varphi ]\!]_A \in {\mathcal A}$ (by IH), and hence $[\![ \langle \varphi \rangle \psi ]\!]_A = [\![ \psi ]\!]_{[\![ \varphi ]\!]_A}\in {\mathcal A}$ (by the semantics and IH again).

Proposition 5

The system $\mathbf {APALM}$ is sound wrt pseudo-models.

To prove Proposition 5, we need the following:

Lemma 2

Let $\mathcal {M}=(W^0, \mathcal {A}, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$ and $\mathcal {M}'=(W^0, \mathcal {A}, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert ')$ be two pseudo-models and $\varphi \in \mathcal {L}$ such that $\mathcal {M}$ and $\mathcal {M}'$ differ only in the valuation of some $p\not \in P_\varphi$. Then, for all $A\in \mathcal {A}$, we have $[\![ \varphi ]\!]^{\mathcal {M}}_{A} =[\![ \varphi ]\!]^{\mathcal {M}'}_{A}$.

Proof

The proof follows by subformula induction on $\varphi$. Let $\mathcal {M}=(W^0, \mathcal {A}, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$ and $\mathcal {M}'=(W^0, \mathcal {A}, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert ')$ be two pseudo-models such that $\mathcal {M}$ and $\mathcal {M}'$ differ only in the valuation of some $p\not \in P_\varphi$ and let $A\in \mathcal {A}$. We want to show that $[\![ \varphi ]\!]^{\mathcal {M}}_{A} =[\![ \varphi ]\!]^{\mathcal {M}'}_{A}$. The base cases $\varphi :=q$, $\varphi :=\top$, $\varphi :=0$, and the inductive cases for Booleans are immediate.

Case $\varphi :=\psi ^0$. Note that $P_{\psi ^0}=P_{\psi }$. Then, by IH, we have that $[\![ \psi ]\!]^{\mathcal {M}'}_{A}=[\![ \psi ]\!]^{\mathcal {M}}_{A}$ for every $A\in \mathcal {A}$, in particular for $W^0 \in \mathcal {A}$. Thus $[\![ \psi ]\!]^{\mathcal {M}'}_{W^0}=[\![ \psi ]\!]^{\mathcal {M}}_{W^0}$. Then, $[\![ \psi ]\!]^{\mathcal {M}'}_{W^0}\cap A=[\![ \psi ]\!]^{\mathcal {M}}_{W^0} \cap A$ for all $A\in \mathcal {A}$. By the semantics of the initial operator on pseudo-models, we obtain $[\![ \psi ^0]\!]^{\mathcal {M}'}_{A}=[\![ \psi ^0]\!]^{\mathcal {M}}_{A}$.

Case $\varphi :=K_i\psi$. Note that $P_{K_i \psi }=P_\psi$. Then, by IH, we have that $[\![ \psi ]\!]^{\mathcal {M}}_{A}=[\![ \psi ]\!]^{\mathcal {M}'}_{A}$. Observe that $[\![ K_i\psi ]\!]_A^{\mathcal {M}}= \{w\in A: w^A_i \subseteq [\![ \psi ]\!]^\mathcal {M}_A\}$ and, similarly, $[\![ K_i\psi ]\!]_A^{\mathcal {M}'}= \{w\in A: w^A_i \subseteq [\![ \psi ]\!]^{\mathcal {M}'}_A\}$. Then, since $[\![ \psi ]\!]^{\mathcal {M}}_{A}=[\![ \psi ]\!]^{\mathcal {M}'}_{A}$, we obtain $[\![ K_i\psi ]\!]_A^{\mathcal {M}}=[\![ K_i\psi ]\!]_A^{\mathcal {M}'}$.

Case $\varphi :=U\psi$. Note that $P_{U \psi }=P_\psi$. Then, by IH, we have that $[\![ \psi ]\!]^{\mathcal {M}'}_{A}=[\![ \psi ]\!]^{\mathcal {M}}_{A}$ for every $A\in \mathcal {A}$. We have two case: (1) If $[\![ \psi ]\!]^{\mathcal {M}'}_{A}=[\![ \psi ]\!]^{\mathcal {M}}_{A}=A$, then $[\![ U\psi ]\!]^{\mathcal {M}'}_{A}=A=[\![ U\psi ]\!]^{\mathcal {M}}_{A}$. (2) If $[\![ \psi ]\!]^{\mathcal {M}'}_{A}=[\![ \psi ]\!]^{\mathcal {M}}_{A}\not =A$, then $[\![ U\psi ]\!]^{\mathcal {M}'}_{A}=[\![ U\psi ]\!]^{\mathcal {M}}_{A}=\emptyset$.

Case $\varphi :=\langle \theta \rangle \psi$. Note that $P_{\langle \theta \rangle \psi }=P_\theta \cup P_\psi$. By IH, we have $[\![ \theta ]\!]^{\mathcal {M}'}_{A}=[\![ \theta ]\!]^{\mathcal {M}}_{A}$ and $[\![ \psi ]\!]^{\mathcal {M}'}_{A}=[\![ \psi ]\!]^{\mathcal {M}}_{A}$ for every $A\in \mathcal {A}$. By Proposition 4, we know that $[\![ \theta ]\!]^{\mathcal {M}}_{A}=[\![ \theta ]\!]^{\mathcal {M}'}_{A}\in \mathcal {A}$. Therefore, in particular, we have $[\![ \psi ]\!]^{\mathcal {M}'}_{[\![ \theta ]\!]^{\mathcal {M}'}_{A}}=[\![ \psi ]\!]^{\mathcal {M}}_{[\![ \theta ]\!]^{\mathcal {M}}_{A}}$. Therefore, by the semantics of $\langle !\rangle$ on pseudo-models, we obtain $[\![ \langle \theta \rangle \psi ]\!]^{\mathcal {M}'}_{A}=[\![ \langle \theta \rangle \psi ]\!]^{\mathcal {M}}_{A}$.

Case $\varphi :=\Diamond \psi$. Note that $P_{\Diamond \psi }=P_{\psi }$. Since the same family of sets $\mathcal {A}$ is carried by both models $\mathcal {M}$ and $\mathcal {M}'$ and since (by IH) $[\![ \psi ]\!]^{\mathcal {M}'}_{A}=[\![ \psi ]\!]^{\mathcal {M}}_{A}$ for all $A\in \mathcal {A}$, we get:

$$[\![ \Diamond \psi ]\!]^{\mathcal {M}'}_{A}= \bigcup \{ [\![ \psi ]\!]^{\mathcal {M}'}_{B}: B\in \mathcal {A}, B\subseteq A\} =\bigcup \{ [\![ \psi ]\!]^{\mathcal {M}}_{B}: B\in \mathcal {A}, B\subseteq A\}= [\![ \Diamond \psi ]\!]^{\mathcal {M}}_{A}.$$

Proof of Proposition 5. The soundness of most of the axioms follows simply by spelling out the semantics. We present here only the soundness of the rule $[!]\square$-intro:

Suppose $\models \chi \rightarrow [\theta \wedge p]\varphi$ and $\not \models \chi \rightarrow [\theta ]\square \varphi$, where $p\notin P_\chi \cup P_\theta \cup P_\varphi$. The latter means that there exists a pseudo model $\mathcal {M}=(W^0, \mathcal {A}, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$ such that for some $A\in \mathcal {A}$ and some $w\in A$, $w\notin [\![ \chi \rightarrow [\theta ]\square \varphi ]\!]^{\mathcal {M}}_{A}$. Therefore $w\in [\![ \chi \wedge \lnot [\theta ]\square \varphi ]\!]^{\mathcal {M}}_{A}$. Thus we have (1) $w\in [\![ \chi ]\!]^{\mathcal {M}}_{A}$ and (2) $w\in [\![ \lnot [\theta ]\square \varphi ]\!]^{\mathcal {M}}_{A}$. Because of (2), $w\in [\![ \langle \theta \rangle \Diamond \lnot \varphi ]\!]^{\mathcal {M}}_{A}$, and, by the semantics, $w\in [\![ \Diamond \lnot \varphi ]\!]^{\mathcal {M}}_{[\![ \theta ]\!]^{\mathcal {M}}_{A}}$. Therefore, applying the semantics, we obtain (3) there exists $B\in \mathcal {A}$ s.t. $w\in B \subseteq [\![ \theta ]\!]^{\mathcal {M}}_{A}\subseteq A$ and $w\in [\![ \lnot \varphi ]\!]^{\mathcal {M}}_{B}$.

Now consider the pre-model $\mathcal {M}'=(W^0, \mathcal {A}, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert ')$ such that $\Vert p \Vert ':=B$ and $\Vert q \Vert '=\Vert q \Vert$ for any $q \ne p \in Prop$. In order to use Lemma 2 we must show that $\mathcal {M}'$ is a pseudo-model. For this we only need to verify that $\mathcal {M}'$ satisfies the closure conditions given in Definition 6. First note that $\Vert p \Vert ':= B\in \mathcal {A}$ by the construction of $\mathcal {M}'$, so $\Vert p\Vert ' \in \mathcal {A}$. For every $q\ne p$, since $\Vert q\Vert '=\Vert q\Vert$ and $\Vert q\Vert \in \mathcal {A}$ we have $\Vert q\Vert '\in \mathcal {A}$. Since $\mathcal {A}$ is the same for both $\mathcal {M}$ and $\mathcal {M}'$, and $\mathcal {M}$ is a pseudo model, the rest of the closure conditions are already satisfied for $\mathcal {M}'$. Therefore $\mathcal {M}'$ is a pseudo model. Now continuing with our soundness proof, note that by Lemma 2 and since $p\notin P_\chi \cup P_\theta \cup P_\varphi$ we obtain $[\![ \chi ]\!]^{\mathcal {M}'}_{A}=[\![ \chi ]\!]^{\mathcal {M}}_{A}$, $[\![ \theta ]\!]^{\mathcal {M}'}_{A}=[\![ \theta ]\!]^{\mathcal {M}}_{A}$ and $[\![ \lnot \varphi ]\!]^{\mathcal {M}'}_{A}=[\![ \lnot \varphi ]\!]^{\mathcal {M}}_{A}$. Since $\Vert p \Vert '=B \subseteq [\![ \theta ]\!]^{\mathcal {M}'}_{A} \subseteq A$ we have $\Vert p \Vert '= [\![ p]\!]^{\mathcal {M}'}_{A}$. Because of (3) we have that $w\in [\![ \theta ]\!]^{\mathcal {M}'}_{A}$ and $w\in [\![ \lnot \varphi ]\!]^{\mathcal {M}'}_{B} =[\![ \lnot \varphi ]\!]^{\mathcal {M}'}_{[\![ p]\!]^{\mathcal {M}'}_{A}} = [\![ \langle p\rangle \lnot \varphi ]\!]^{\mathcal {M}'}_{A}$. Thus $w\in [\![ p]\!]^{\mathcal {M}'}_{A}$, so $w\in [\![ \theta \wedge p]\!]^{\mathcal {M}'}_{A}= [\![ \theta ]\!]^{\mathcal {M}'}_{A}\cap [\![ p]\!]^{\mathcal {M}'}_{A}=[\![ p]\!]^{\mathcal {M}'}_{A}$ simply because $[\![ p]\!]^{\mathcal {M}'}_{A} \subseteq [\![ \theta ]\!]^{\mathcal {M}'}_{A}$. Since $w\in [\![ \lnot \varphi ]\!]^{\mathcal {M}'}_{[\![ p]\!]^{\mathcal {M}'}_{A}}$ we obtain $w\in [\![ \lnot \varphi ]\!]^{\mathcal {M}'}_{[\![ \theta \wedge p]\!]^{\mathcal {M}'}_{A}}$. Putting everything together, $w\in [\![ \theta \wedge p]\!]^{\mathcal {M}'}_{A}$ and $w\in [\![ \lnot \varphi ]\!]^{\mathcal {M}'}_{[\![ \theta \wedge p]\!]^{\mathcal {M}'}_{A}}$, we obtain that $w\in [\![ \langle \theta \wedge p\rangle \lnot \varphi ]\!]^{\mathcal {M}'}_{A}$ and $w\in [\![ \chi ]\!]^{\mathcal {M}'}_{A}$. Therefore $\mathcal {M}', w \models \chi \wedge \langle \theta \wedge p\rangle \lnot \varphi$, which contradicts the validity of $\chi \rightarrow [\theta \wedge p]\varphi$.

Definition 7

(Standard Pre-model). A pre-model $\mathcal {M}= (W^0, \mathcal {A}, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$ is standard if and only if $\mathcal {A}=\{[\![ \theta ]\!]_{W^0} : \theta \in \mathcal {L}_{-\Diamond }\}$.

Proposition 6

Every standard pre-model is a pseudo-model.

Proof

Let $\mathcal {M}=(W^0, \mathcal {A}, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$ be a standard pre-model. This implies that $\mathcal {A}=\{[\![ \theta ]\!]_{W^0} : \theta \in \mathcal {L}_{-\Diamond }\}$. We need to show that $\mathcal {M}$ satisfies the closure conditions given in Definition 6. Conditions (1) and (2) are immediate.

For (3): let $A\in \mathcal {A}$. Since $\mathcal {M}$ is a standard pre-model, we know that $A=[\![ \theta ]\!]_{W^0}$ for some $\theta \in \mathcal {L}_{-\Diamond }$. Since $\theta \in \mathcal {L}_{-\Diamond }$, we have $\lnot \theta \in \mathcal {L}_{-\Diamond }$, thus, $[\![ \lnot \theta ]\!]_{W^0}\in \mathcal {A}$. Observe that $[\![ \lnot \theta ]\!]_{W^0}=W^0-[\![ \theta ]\!]_{W^0}$, thus, we obtain $W^0-A\in \mathcal {A}$.

For (4): let $A, B\in \mathcal {A}$. Since $\mathcal {M}$ is a standard pre-model, $A=[\![ \theta _1]\!]_{W^0}$ and $B=[\![ \theta _2]\!]_{W^0}$ for some $\theta _1, \theta _2\in \mathcal {L}_{-\Diamond }$. Since $\theta _1, \theta _2\in \mathcal {L}_{-\Diamond }$, we have $\theta _1\wedge \theta _2\in \mathcal {L}_{-\Diamond }$, thus, $[\![ \theta _1\wedge \theta _2 ]\!]_{W^0}\in \mathcal {A}$. Observe that $[\![ \theta _1\wedge \theta _2]\!]_{W^0}=[\![ \theta _1]\!]_{W^0}\cap [\![ \theta _2]\!]_{W^0}=A\cap B$, thus, we obtain $A\cap B\in \mathcal {A}$.

For (5): let $A\in \mathcal {A}$. Since $\mathcal {M}$ is a standard pre-model, $A=[\![ \theta ]\!]_{W^0}$ for some $\theta \in \mathcal {L}_{-\Diamond }$. Since $\theta \in \mathcal {L}_{-\Diamond }$, we have $K_i\theta \in \mathcal {L}_{-\Diamond }$, thus, $[\![ K_i\theta ]\!]_{W^0}\in \mathcal {A}$. Observe that $[\![ K_i\theta ]\!]_{W^0}= \{w\in W^0: \forall s\in W^0 (w\sim _i s \Rightarrow s \in [\![ \theta ]\!]_{W^0})\}=K_i[\![ \theta ]\!]_{W^0}$, thus, we obtain $K_iA\in \mathcal {A}$.

Equivalence Between the Standard Pseudo-models and APALM Models. For Proposition 7 only, we use the notation $[\![ \varphi ]\!]^{PS}_A$ to refer to pseudo-model semantics (as in Definition 5) and use $[\![ \varphi ]\!]_\mathcal {M}$ to refer to APALM semantics (as in Definition 1).

Proposition 7

• 1. For every standard pseudo-model $\mathcal {M}=(W^0, \mathcal {A}, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$ and every set $A\in \mathcal {A}$, we denote by $\mathcal {M}_A$ the model $\mathcal {M}_A=(W^0, A, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$. Then:

  • (a) For every $\varphi \in \mathcal {L}$, we have $[\![ \varphi ]\!]_{\mathcal {M}_A}=[\![ \varphi ]\!]^{PS}_{A}$ for all $A\in \mathcal {A}$.

  • (b) $\mathcal {M}_A$ is an APALM model, for all $A\in \mathcal {A}$.

• 2. For every APALM model $\mathcal {M}=(W^0, W,\sim _1, \dots , \sim _n, \Vert \cdot \Vert )$, we denote by $\mathcal {M}'$ the pre-model $\mathcal {M}'=(W^0, \mathcal {A}, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$, where $\mathcal {A}=\{[\![ \theta ]\!]_{\mathcal {M}^0} : \theta \in \mathcal {L}_{-\Diamond }\}$. Then

  • (a) $\mathcal {M}'$ is a standard pseudo-model.

  • (b) For every $\varphi \in \mathcal {L}$, we have $[\![ \varphi ]\!]_{\mathcal {M}}=[\![ \varphi ]\!]^{PS}_{W}$.

The proof of Proposition 7 needs the following lemma.

Lemma 3

Let $\mathcal {M}=(W^0, \mathcal {A}, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$ a standard pseudo-model, $A\in \mathcal {A}$ and $\varphi \in \mathcal {L}$, then the following holds: $[\![ \Diamond \varphi ]\!]_A=\bigcup \{[\![ \langle \theta \rangle \varphi ]\!]_A : \theta \in \mathcal {L}_{-\Diamond }\}$.

Proof

For $(\subseteq )$: Let $w\in [\![ \Diamond \varphi ]\!]_A$. Then, by the semantics of $\Diamond$ in pseudo-models. there exists some $B\in \mathcal {A}$ such that $w\in B\subseteq A$ and $w\in [\![ \varphi ]\!]_B$. Since $\mathcal {M}$ is standard, we know that $A=[\![ \psi ]\!]_{W^0}$ and $B=[\![ \chi ]\!]_{W^0}$ for some $\psi , \chi \in \mathcal {L}_{-\Diamond }$. Moreover, since $B=[\![ \chi ]\!]_{W^0}\subseteq A=[\![ \psi ]\!]_{W^0}$, we have $B=[\![ \chi ]\!]_{W^0}\cap [\![ \psi ]\!]_{W^0}=[\![ \chi ^0]\!]_{[\![ \psi ]\!]_{W^0}}=[\![ \chi ^0]\!]_A$, and so $w\in [\![ \varphi ]\!]_B=[\![ \varphi ]\!]_{[\![ \chi ^0]\!]_A}= [\![ \langle \chi ^0\rangle \varphi ]\!]_A\subseteq \bigcup \{[\![ \langle \theta \rangle \varphi ]\!]_A : \theta \in \mathcal {L}_{-\Diamond }\}$. For $(\supseteq )$: Let $w\in \bigcup \{[\![ \langle \theta \rangle \varphi ]\!]_A : \theta \in \mathcal {L}_{-\Diamond }\}$. Then we have $w\in [\![ \langle \theta \rangle \varphi ]\!]_A= [\![ \varphi ]\!]_{[\![ \theta ]\!]_A}$, for some $\theta \in \mathcal {L}_{-\Diamond }$, and since $[\![ \theta ]\!]_A\in \mathcal {A}$ (by Proposition 4) and $[\![ \theta ]\!]_A\subseteq A$ (by Observation 2), it follows that $w\in [\![ \Diamond \varphi ]\!]_A$ (by the semantics of $\Diamond$ in pseudo-models).

Proof of Proposition 7

• 1. Let $\mathcal {M}=(W^0, \mathcal {A}, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$ be a standard pseudo-model. $A\in \mathcal {A}$ implies $A=[\![ \theta ]\!]^{PS}_{W^0}\subseteq W$ for some $\theta$, hence $\mathcal {M}_A=(W^0, A, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$ is a model.

  • (a) The proof is by induction on the complexity measure < from Lemma 1. The base cases and the inductive cases for Booleans are straightforward.

    Case $\theta :=\psi ^0$. We have $[\![ \psi ]\!]^{PS}_{A}=[\![ \psi ]\!]^{PS}_{W^0} \cap A= [\![ \psi ]\!]_{\mathcal {M}^0_A}\cap A=[\![ \psi ^0]\!]_{\mathcal {M}_A}$ (by Definition 5, IH, and Definition 2).

    Case $\theta :=K_i\psi$. We have $[\![ K_i\psi ]\!]^{PS}_{A}= \{w\in A: w^A_i \subseteq [\![ \psi ]\!]^{PS}_{A} =\{w\in A: w_i \subseteq [\![ \psi ]\!]_{\mathcal {M}_A}\}=[\![ K_i\psi ]\!]_{\mathcal {M}_A}$ (by Definition 5, IH, and Definition 2).

    Case $\theta := U\psi$. By Definitions 2 and 5, we have:

    

    By IH, $[\![ \psi ]\!]^{PS}_A=[\![ \psi ]\!]_{\mathcal {M}_A}$, therefore, $[\![ U\psi ]\!]^{PS}_A=[\![ U\psi ]\!]_{\mathcal {M}_A}$.

    Case $\varphi :=\langle \psi \rangle \chi$. By Definition 2, we know that $[\![ \langle \psi \rangle \chi ]\!]_{\mathcal {M}_A} = [\![ \chi ]\!]_{\mathcal {M}_A|[\![ \psi ]\!]_{\mathcal {M}_A}}$. Now consider the relativized model $\mathcal {M}_A|[\![ \psi ]\!]_{\mathcal {M}_A}=(W^0, [\![\psi ]\!]_{\mathcal {M}_A}, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$. By Lemma 1(1) and IH, we have $[\![ \psi ]\!]_{\mathcal {M}_A}=[\![ \psi ]\!]^{PS}_{A}$. Moreover, by the definition of standard pseudo-models, we know that $A=[\![ \theta ]\!]^{PS}_{W^0}$ for some $\theta \in \mathcal {L}_{-\Diamond }$. Therefore, $[\![ \psi ]\!]_{\mathcal {M}_A}=[\![ \psi ]\!]^{PS}_{A}=[\![ \psi ]\!]^{PS}_{[\![ \theta ]\!]^{PS}_{W^0}}=[\![ \langle \theta \rangle \psi ]\!]^{PS}_{W^0}$. Therefore, $[\![ \psi ]\!]_{\mathcal {M}_A}\in \mathcal {A}$. We then have

    $$[\![ \langle \psi \rangle \chi ]\!]_{\mathcal {M}_A} = [\![ \chi ]\!]_{\mathcal {M}_{[\![ \psi ]\!]_{\mathcal {M}_A}}} = [\![ \chi ]\!]_{\mathcal {M}_{[\![ \psi ]\!]^{PS}_{A}}} = [\![ \chi ]\!]^{PS}_{[\![ \psi ]\!]^{PS}_{A}} =[\![ \langle \psi \rangle \chi ]\!]^{PS}_{A},$$

    by the semantics and IH on $\psi$ and on $\chi$ (since $[\![ \psi ]\!]^{PS}_A\in \mathcal {A}$).

    Case $\varphi :=\Diamond \psi$. We have:

    

  • (b) By part (a), $[\![ \varphi ]\!]_{\mathcal {M}^0_A}=[\![ \varphi ]\!]_{\mathcal {M}_{W^0}}=[\![ \varphi ]\!]^{PS}_{W^0}$ for all $\varphi$. Since $\mathcal {M}$ is standard, we have $A=[\![ \theta ]\!]^{PS}_{W^0}=[\![ \theta ]\!]_{\mathcal {M}^0_A}$ for some $\theta \in \mathcal {L}_{-\Diamond }$, so $\mathcal {M}_A$ is an APALM model.

• 2. Let $\mathcal {M}=(W^0, W, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$ be an APALM model. Since $\mathcal {A}=\{[\![ \theta ]\!]_{\mathcal {M}^0} : \theta \in \mathcal {L}_{-\Diamond }\}\subseteq \mathcal {P}(W^0)$, the model $\mathcal {M}'=(W^0, \mathcal {A}, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$ is a pre-model. Therefore, the semantics given in Definition 5 is defined on $\mathcal {M}'=(W^0, \mathcal {A}, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$.

  • (a) By Proposition 6, it suffices to prove that the pre-model $\mathcal {M}'=(W^0, \mathcal {A}, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$ is standard, i.e. that $\{[\![ \theta ]\!]_{\mathcal {M}^0} : \theta \in \mathcal {L}_{-\Diamond }\}=\{[\![ \theta ]\!]^{PS}_{W^0} : \theta \in \mathcal {L}_{-\Diamond }\}$. For this, we need to show that for every APALM model $\mathcal {M}=(W^0, W, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$, we have $[\![ \theta ]\!]_{\mathcal {M}}=[\![ \theta ]\!]^{PS}_{W}$ for all $\theta \in \mathcal {L}_{-\Diamond }$.

    We prove this by subformula induction on $\theta$. The base cases and the inductive cases for Booleans are straightforward.

    Case $\theta :=\psi ^0$. Then $[\![ \psi ^0]\!]_{\mathcal {M}} = [\![ \psi ]\!]_{\mathcal {M}^0}\cap W = [\![ \psi ]\!]^{PS}_{W^0} \cap W= [\![ \psi ]\!]^{PS}_{W}$ (by Definition 2, IH, and Definition 5).

    Case $\theta :=K_i\psi$. We have $[\![ K_i\psi ]\!]_{\mathcal {M}} =\{w\in W: w_i \subseteq [\![ \psi ]\!]_{\mathcal {M}}\}= \{w\in W: w^W_i \subseteq [\![ \psi ]\!]^{PS}_{W}\} =[\![ K_i\psi ]\!]^{PS}_{W}$ (by Definition 2, IH, and Definition 5).

    Case $\theta := U\psi$. By Definitions 2 and 5, we have:

    

    By IH, $[\![ \psi ]\!]^{PS}_W=[\![ \psi ]\!]_\mathcal {M}$, therefore, $[\![ U\psi ]\!]^{PS}_W=[\![ U\psi ]\!]_{\mathcal {M}}$.

    Case $\theta :=\langle \psi \rangle \chi$. By Definition 2, we know that $[\![ \langle \psi \rangle \chi ]\!]_{\mathcal {M}} = [\![ \chi ]\!]_{\mathcal {M}|{[\![ \psi ]\!]_{\mathcal {M}}}}$. Now consider the relativized model $\mathcal {M}|{[\![ \psi ]\!]_{\mathcal {M}}}=(W^0, [\![\psi ]\!]_{\mathcal {M}_A}, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$. By Lemma 1(1) and IH on $\psi$, we have $[\![ \psi ]\!]_{\mathcal {M}}=[\![ \psi ]\!]^{PS}_{W}$. Moreover, by the definition of APALM models, we know that $W=[\![ \theta ]\!]_{\mathcal {M}^0}$ for some $\theta \in \mathcal {L}_{-\Diamond }$. Therefore, $[\![ \psi ]\!]_{\mathcal {M}}=[\![ \psi ]\!]_{\mathcal {M}^0|[\![ \theta ]\!]_{\mathcal {M}^0}}=[\![ \langle \theta \rangle \psi ]\!]_{\mathcal {M}^0}$. Therefore, since $\langle \theta \rangle \psi \in \mathcal {L}_{-\Diamond }$, the model $\mathcal {M}|{[\![ \psi ]\!]_{\mathcal {M}}}$ is also an APALM model obtained by updating the initial model $\mathcal {M}^0$. We then have

    

  • (b) The proof of this part follows by <-induction on $\varphi$ (where < is as in Lemma 1). All the inductive cases are similar to ones in the above proof, except for the case $\varphi :=\Diamond \psi$, shown below:

    

Corollary 1

Validity on standard pseudo-models coincides with APALM validity.

Proof

This is a straightforward consequence of Proposition 7.

Corollary 2

The system $\mathbf {APALM}$ is sound wrt APALM models.

This follows immediately from Proposition 5 and Corollary 1.

It is important to note that the equivalence between standard pseudo-models and APALM models (given by Proposition 7 above, and underlying our soundness result) is not trivial. It relies in particular on the equivalence between the effort modality and the arbitrary announcement operator $\square$ on standard pseudo-models, which holds only because our models and language retain the memory of the initial situation (see Lemma 3). Hence, a similar equivalence fails for the original APAL.

5 Completeness

In this section we prove the completeness of $\mathbf {APALM}$. First, we show completeness with respect to pseudo-models, via an innovative modification of the standard canonical model construction. This is based on a method previously used in [6], that makes an essential use of the finitary $\square$-introduction rule, by requiring our canonical theories T to be (not only maximally consistent, but also) “witnessed”. Roughly speaking, a theory T is witnessed if every $\Diamond \varphi$ occurring in every “existential context” in T is witnessed by some atomic formula p, meaning that $\langle p \rangle \varphi$ occurs in the same existential context in T. Our canonical pre-model will consist of all initial, maximally consistent, witnessed theories (where a theory is ‘initial’ if it contains the formula 0). A Truth Lemma is proved, as usual. Completeness for (both pseudo-models and) APALM models follows from the observation that our canonical pre-model is standard, hence it is (a standard pseudo-model, and thus) equivalent to a genuine APALM model.

We now proceed with the details. The appropriate notion of “existential context” is represented by possibility forms, in the following sense.

Definition 8

(Necessity forms and possibility forms). For any finite string $s\in (\{\bullet ^0\}\cup \{\varphi {\rightarrow } \ | \ \varphi \in \mathcal {L}\}\cup \{K_i : i\in \mathcal {A}\}\cup \{U\}\cup \{\rho \ | \ \rho \in \mathcal {L}_{-\Diamond }\})^*=NF_{\mathcal {L}}$, we define pseudo-modalities [s] and $\langle s\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 necessity forms are defined recursively as $[\epsilon ] \varphi =\varphi$, $[s, \bullet ^0] \varphi =[s]\varphi ^0$, $[s, \varphi {\rightarrow }]\varphi = [s] (\varphi \rightarrow \varphi )$, $[s, K_i]\varphi =[s]K_i\varphi$, $[s,U]\varphi =[s]U\varphi$, $[s,\rho ]\varphi = [s][\rho ]\varphi$, where $\epsilon$ is the empty string. For possibility forms, we set $\langle s\rangle \varphi :=\lnot [s]\lnot \varphi$.

Example: $[K_i, \bullet ^0, \Diamond p {\rightarrow },0,U]$ is a necessity form s.t. $[K_i, \bullet ^0, \Diamond p{\rightarrow },0,U]\varphi =K_i(\Diamond p\rightarrow [0] U\varphi )^0$.

Definition 9

(Theories: witnessed, initial, maximal). Let $\mathcal {L}^P$ be the language of APALM based only on some countable set P of propositional variables. Similarly, let $NF^P$ denote the corresponding set of strings defined based on $\mathcal {L}^P$. A P-theory is a consistent set of formulas in $\mathcal {L}^P$ (where “consistent” means consistent with respect to the axiomatization of $\mathbf {APALM}$ 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$ (or equivalently: if $\varGamma \vdash [s][p]\lnot \varphi$ for all $p\in P$, then $\varGamma \vdash [s]\square \lnot \varphi$). A P-theory $\varGamma$ is called initial if $0\in \varGamma$. A maximal P-witnessed theory $\varGamma$ is a P-witnessed theory that is not a proper subset of any P-witnessed theory. A maximal P-witnessed initial theory $\varGamma$ is a maximal P-witnessed theory such that $0\in \varGamma$.

The proofs of the following lemmas are in the online version.

Lemma 4

For every necessity form [s], there exist formulas $\theta \in \mathcal {L}_{-\Diamond }$ and $\psi \in \mathcal {L}$ such that for all $\varphi \in \mathcal {L}$, we have

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

Lemma 5

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

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

Lemma 6

For every maximal P-witnessed theory $\varGamma$, and every formula $\varphi , \psi \in \mathcal {L}^P$:

Lemma 7

For every $\varGamma \subseteq \mathcal {L}^P$, if $\varGamma$ is a P-theory and $\varGamma \not \vdash \lnot \varphi$ for some $\varphi \in \mathcal {L}^P$, then $\varGamma \cup \{\varphi \}$ is a P-theory. Moreover, if $\varGamma$ is P-witnessed, then $\varGamma \cup \{\varphi \}$ is also P-witnessed.

Lemma 8

If $\{\varGamma _i\}_{i \in \mathbb {N}}$ is an increasing chain of P-theories such that $\varGamma _i\subseteq \varGamma _{i+1}$, then $\bigcup _{n\in \mathbb {N}}\varGamma _n$ is a P-theory.

Lemma 9

For every maximal P-witnessed theory T, both $\{\theta \in \mathcal {L}^P : K_i\theta \in T\}$ and $\{\theta \in \mathcal {L}^P : U\theta \in T\}$ are P-witnessed theories.

Lemma 10

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

Lemma 11

(Extension Lemma). Let $P$ be a countable 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 initial $P$-theory $\varGamma$ can be extended to an initial $\overset{\sim }{P}$-witnessed theory $\overset{\sim }{\varGamma }\supseteq \varGamma$, and hence to a maximal $\overset{\sim }{P}$-witnessed initial theory $T_\varGamma \supseteq \varGamma$.

To define our canonical pseudo-model, we first put, for all maximal P-witnessed theories T, S:

$$T\sim _U S \,\, \text{ iff } \,\, \forall \varphi \in \mathcal {L}^P\left( U\varphi \in T\, \text{ implies } \, \varphi \in S\right) .$$

Definition 10

(Canonical Pre-Model). Given a maximal $P$-witnessed initial theory $T_0$, the canonical pre-model for $T_0$ is a tuple ${\mathcal M}^c= (W^c, \mathcal {A}^c, \sim _1^c, \ \ldots , \sim _n^c, \Vert \cdot \Vert ^c)$ such that:

• $W^c\,\, =\,\, \{T : \ T \text{ is } \text{ a } \text{ maximal } P\text{-witnessed } \text{ theory } \text{ such } \text{ that } T_0\sim _{U} T\},$

• $\mathcal {A}^c=\{\widehat{{\theta }} \ : \ \theta \in \mathcal {L}^P_{-\Diamond }\}$ where $\widehat{\varphi }=\{T\in W^c \ : \ \varphi \in T\}$ for any $\varphi \in \mathcal {L}^P$,

• for every $T, S\in W^c$ and $i\in \mathcal {AG}$ we define:

  $$T\sim _{i}^c S \,\, \text{ iff } \,\, \forall \varphi \in \mathcal {L}^P\left( K_i\varphi \in T\, \text{ implies } \, \varphi \in S\right) .$$

• $\Vert p \Vert ^c=\{T\in W^c \ : \ p\in T\}=\widehat{p}$.

As usual, it is easy to see (given the S5 axioms for $K_i$ and for U) that $\sim _U$ and $\sim ^c_{i}$ are equivalence relations.

The proofs of the first three results below are online.

Lemma 12

(Existence Lemma for $K_i$). Let T be a maximal P-witnessed theory, $\alpha \in \mathcal {L}_{-\Diamond }^P$, and $\varphi \in \mathcal {L}^P$ such that $\alpha \in T$ and $K_i[\alpha ]\varphi \not \in T$. Then, there is a maximal P-witnessed theory S such that $T\sim _i S$, $\alpha \in S$ and $[\alpha ]\varphi \not \in S$.

Lemma 13

(Existence Lemma for U). Let T be a maximal P-witnessed theory, $\alpha \in \mathcal {L}_{-\Diamond }^P$, and $\varphi \in \mathcal {L}^P$ such that $\alpha \in T$ and $U[\alpha ]\varphi \not \in T$. Then, there is a maximal P-witnessed theory S such that $T\sim _U S$, $\alpha \in S$ and $[\alpha ]\varphi \not \in S$.

Corollary 3

For $\varphi \in \mathcal {L}$, we have $\widehat{{U\varphi }}=W^c$ if $\widehat{\varphi }=W^c$, and $\widehat{{U\varphi }}=\emptyset$ otherwise.

Lemma 14

Every element $T\in W^c$ is an initial theory (i.e. $0\in T$).

Proof

Let $T\in W^c$. By the construction of $W^c$, we have $T_0\sim _U T$. Since $0\rightarrow U0$ is an axiom and $T_0$ is maximal, $(0\rightarrow U0) \in T_0$. Thus, since $0\in T_0$, we obtain $U0\in T_0$ (by Lemma 6(4)). Therefore, by the definition of $\sim _U$ and since $T_0\sim _U T$, we have that $0\in T$.

Corollary 4

For all $\varphi \in \mathcal {L}^P$, we have $\widehat{\varphi }=\widehat{{\varphi ^0}}$.

Proof

Since $0\in T$ for all $T\in W^c$, we obtain by axiom (0-eq) that $\varphi \leftrightarrow \varphi ^0\in T$ for all $T\in W^c$. Therefore, $\widehat{\varphi }=\widehat{{\varphi ^0}}$.

Lemma 15

(Truth Lemma). Let ${\mathcal M}^c= (W^c, \mathcal {A}^c, \sim _1^c, \ \ldots , \sim _n^c, V^c)$ be the canonical pre-model for some $T_0$ and $\varphi \in \mathcal {L}^P$. Then, for all $\alpha \in \mathcal {L}^P_{-\Diamond }$, we have $[\![ \varphi ]\!]_{\widehat{{\alpha }}} =\widehat{ \langle \alpha \rangle \varphi }.$

Proof

The proof is by <-induction on $\varphi$, using the following induction hypothesis (IH): for all $\psi <\varphi$, we have for all $\alpha \in \mathcal {L}_{-\Diamond }$. The cases for the Boolean connectives are straightforward. The cases for $K_i$ and U are standard, using $\vdash \langle \alpha \rangle K_i\psi \leftrightarrow \alpha \wedge K_i[\alpha ]\psi$ and Lemma 12 for $K_i$, and $\vdash \langle \alpha \rangle U\psi \leftrightarrow \alpha \wedge U[\alpha ]\psi$ and Lemma 13 for U.

Base case $\varphi := \top$. Then , by Definition 5 and the fact that $\vdash \alpha \leftrightarrow \langle \alpha \rangle \top$.

Base case $\varphi :=p$. Then , by Definition 5, the defn. of $\Vert \cdot \Vert ^c$, $R_p$, and Proposition 2(3).

Base case $\varphi :=0$. Then $[\![ 0]\!]_{\widehat{\alpha }}= W^c$ if $\widehat{\alpha }=W^c$, and $[\![ 0]\!]_{\widehat{\alpha }}= \emptyset$ otherwise. Also, (by Propositions 2(2) and Lemma14). By Corollary 3, if $\widehat{\alpha }=W^c$, and otherwise. So .

Case $\varphi :=\psi ^0$. Follows easily from $\widehat{\top }=W^c$ and R[$\top$], Corollary 4, and R$^0$.

Case $\varphi :=\langle \chi \rangle \psi$. Straightforward, using the fact that $\vdash \langle \alpha \rangle \langle \chi \rangle \psi \leftrightarrow \langle \langle \alpha \rangle \chi \rangle \psi$ (by R$_{[!]}$).

Case $\varphi :=\Diamond \psi$.

($\Rightarrow$) Suppose $T\in [\![ \Diamond \psi ]\!]_{\widehat{\alpha }}$. This means, by Definition 5, that $\alpha \in T$ and there exists $B\in \mathcal {A}^c$ such that $T\in B\subseteq \widehat{\alpha }$ and $T\in [\![ \psi ]\!]_B$ (see Observation 2). By the construction of $\mathcal {A}^c$, we know that $B=\widehat{\theta }$ for some $\theta \in \mathcal {L}^P_{-\Diamond }$. Therefore, $T\in [\![ \psi ]\!]_B$ means that $T\in [\![ \psi ]\!]_{\widehat{\theta }}$. Moreover, since $\widehat{\theta }\subseteq \widehat{\alpha }$ and, thus, , we obtain . By Lemma 1(1), we have $\psi <\square \psi$. Therefore, by IH, we obtain . Then, by axiom ($[!]\square$-elim) and the fact that T is maximal, we conclude that .

($\Leftarrow$) Suppose , i.e., $\langle \alpha \rangle \Diamond \psi \in T$. Then, since T is a maximal P-witnessed theory, there is $p\in P$ such that $\langle \alpha \rangle \langle p\rangle \psi \in T$. By Lemma 1(2), we know that $\langle p\rangle \psi <\Diamond \psi$. Thus, by IH on $\langle p\rangle \psi$, we obtain that $T\in [\![ \langle p\rangle \psi ]\!]_{\widehat{\alpha }}$. This means, by Definition 5 and Observation 2, that $T\in [\![ \psi ]\!]_{[\![ p]\!]_{\widehat{\alpha }}}\subseteq [\![ p]\!]_{\widehat{\alpha }}$. Since $p< \Diamond \psi$, by IH on p, we obtain that . By the construction of $\mathcal {A}^c$, we moreover have . Therefore, as and , by Definition 5, we conclude that $T\in [\![ \Diamond \psi ]\!]_{\widehat{\alpha }}$.

Corollary 5

The canonical pre-model ${\mathcal M}^c$ is standard (and hence a pseudo-model).

Proof

$\mathcal {A}^c=\{\widehat{{\theta }} : \theta \in \mathcal {L}^P_{-\Diamond }\} = \{\widehat{\langle \top \rangle {\theta }} : \theta \in \mathcal {L}^P_{-\Diamond }\}= \{[\![ \theta ]\!]_{\widehat{\top }} : \theta \in \mathcal {L}^P_{-\Diamond }\}= \{[\![ \theta ]\!]_{W^c} : \theta \in \mathcal {L}^P_{-\Diamond }\}$.

Lemma 16

For every $\varphi \in \mathcal {L}^P$, if $\varphi$ is consistent then $\{0, \Diamond \varphi \}$ is an initial $P_{\varphi }$-theory.

Proof

Let $\varphi \in \mathcal {L}^P$ s.t. $\varphi \not \vdash \bot$. By the Equivalences with $^0$ in Table 1, we have $\vdash \bot ^0 \leftrightarrow (p\wedge \lnot p)^0\leftrightarrow (p^0\wedge \lnot p^0)\leftrightarrow (p\wedge \lnot p)\leftrightarrow \bot$. Therefore, $\vdash \psi \rightarrow \bot ^0$ iff $\vdash \psi \rightarrow \bot$ for all $\psi \in \mathcal {L}^P$. Then, by Proposition 2(12), we obtain $\vdash \varphi \rightarrow \bot$ iff $\vdash (0\wedge \Diamond \varphi )\rightarrow \bot$. Since $\varphi \not \vdash \bot$, we have $0\wedge \Diamond \varphi \not \vdash \bot$, i.e., $\{0, \Diamond \varphi \}$ is a $P_{\varphi }$-theory. By definition, it is an initial one.

Corollary 6

$\mathbf {APALM}$ is complete with respect to standard pseudo models.

Proof

Let $\varphi$ be a consistent formula. By Lemma 16, $\{0,\Diamond \varphi \}$ is an initial $P_{\varphi }$-theory. By Extension and Lindenbaum Lemmas, we can extend $P_{\varphi }$ to some $P\supseteq P_{\varphi }$, and extend $\{0,\Diamond \varphi \}$ to some maximal P-witnessed theory $T_0$ such that $(0\wedge \Diamond \varphi ) \in T_0$. So $T_0$ is initial, and we can construct the canonical pseudo-model ${\mathcal M}^c$ for $T_0$. Since $\Diamond \varphi \in T_0$ and $T_0$ is P-witnessed, there exists $p\in P$ such that $\langle p\rangle \varphi \in T_0$. By Truth Lemma (applied to $\alpha :=p$), we get $T_0\in [\![ \varphi ]\!]_{\widehat{p}}$. Hence, $\varphi$ is satisfied at $T_0$ in the set $\widehat{p}\in \mathcal {A}^c$.

Corollary 7

$\mathbf {APALM}$ is complete with respect to APALM models.

This follows immediately from Corollaries 1 and 6.

6 Expressivity

To compare APALM and its fragments with basic epistemic logic (and its extension with the universal modality), consider the static fragment $\mathcal {L}_{-\Diamond , \langle !\rangle }$, obtained from $\mathcal {L}$ by removing both the $\Diamond$ operator and the dynamic modality $\langle \varphi \rangle \psi$; as well as the present-only fragment $\mathcal {L}_{-\Diamond , \langle !\rangle , 0, \varphi ^0}$, obtained by removing the operators 0 and $\varphi ^0$ from $\mathcal {L}_{-\Diamond , \langle !\rangle }$; and finally the epistemic fragment $\mathcal {L}_{epi}$, obtained by further removing the universal modality U from $\mathcal {L}_{-\Diamond , \langle !\rangle , 0, \varphi ^0}$. For every APALM model ${\mathcal M}= (W^0, W, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$, consider its initial epistemic model $\mathcal {M}^{initial}=(W^0, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$ and its current epistemic model $\mathcal {M}^{current}= (W, \sim _1\cap W\times W, \ldots , \sim _n\cap W\times W, \Vert \cdot \Vert \cap W)$.

Proposition 8

The fragment $\mathcal {L}_{-\Diamond }$ is co-expressive with the static fragment $\mathcal {L}_{-\Diamond , \langle !\rangle }$. In fact, every formula $\varphi \in \mathcal {L}_{-\Diamond }$ is provably equivalent with some formula $\psi \in \mathcal {L}_{-\Diamond , \langle !\rangle }$ (by using $\mathbf {APALM}$ reduction laws to eliminate dynamic modalities, as in standard PAL).

Proposition 9

The static fragment $\mathcal {L}_{-\Diamond , \langle !\rangle }$ (and hence, also $\mathcal {L}_{-\Diamond }$) is strictly more expressive than the present-only fragment $\mathcal {L}_{-\Diamond , \langle !\rangle , 0, \varphi ^0}$, which in turn is more expressive than the epistemic fragment $\mathcal {L}_{epi}$. In fact, each of the operators 0 and $\varphi ^0$ independently increase the logic’s expressivity.

Kuijer’s counterexample shows that the standard epistemic bisimulation is not appropriate for APALM, so we now define a new such notion:

Definition 11

(APALM Bisimulation). An APALM bisimulation between APALM models ${\mathcal M}_1= (W_1^0, W_1, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$ and ${\mathcal M}_2= (W_2^0, W_2, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$ is a total bisimulation B (in the usual sense)¹⁷ between the corresponding initial epistemic models $\mathcal {M}_1^{initial}$ and $\mathcal {M}_2^{initial}$, with the property that: if $s_1 B s_2$, then $s_1\in W_1$ holds iff $s_2\in W_2$ holds. Two current states $s_1\in W_1$ and $s_2\in W_2$ are APALM-bisimilar if there exists an APAL bisimulation B between the underlying APALM models such that $s_1 B s_2$.

Since APALM models are always of the form $\mathcal {M}=(\mathcal {M}^0)|\theta$ for some $\theta \in \mathcal {L}_{-\Diamond }$, we have a characterization of APALM-bisimulation only in terms of the initial models:

Proposition 10

Let ${\mathcal M}_1= (W_1^0, W_1, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$ and ${\mathcal M}_2= (W_2^0, W_2, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$ be APALM models, and let $B\subseteq W_1^0\times W_2^0$. The following are equivalent:

• 1. B is an APALM bisimulation between ${\mathcal M}_1$ and ${\mathcal M}_2$;

• 2. B is a total bisimulation between ${\mathcal M}_1^{initial}$ and ${\mathcal M}_2^{initial}$ (or equivalently, an APALM bisimulation between $\mathcal {M}_1^0$ and $\mathcal {M}_2^0$), and $\mathcal {M}_1=(\mathcal {M}_1^0)|\theta$, $\mathcal {M}_2=(\mathcal {M}_2^0)|\theta$ for some common formula $\theta \in \mathcal {L}_{-\Diamond }$.

So, to check for APALM-bisimilarity, it is enough to check for total bisimilarity between the initial models and for both models being updates with the same formula.

Proposition 11

APALM formulas are invariant under APALM-bisimulation: if $s_1 B s_2$ for some APALM-bisimulation relation between APALM models ${\mathcal M}_1= (W_1^0, W_1, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$ and ${\mathcal M}_2= (W_2^0, W_2, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$, then: $s_1 \in [\![ \varphi ]\!]_{\mathcal {M}_1}$ iff $s_2 \in [\![ \varphi ]\!]_{\mathcal {M}_2}$. The (Hennessy-Milner) converse holds for finite models: if ${\mathcal M}_1= (W_1^0, W_1, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$ and ${\mathcal M}_2= (W_2^0, W_2, \sim _1, \ldots , \sim _n, \Vert \cdot \Vert )$ are APALM models with $W_1^0, W_2^0$ finite, then $s_1\in W_1$ and $s_2\in W_2$ satisfy the same APALM formulas iff they are APALM-bisimilar.

7 Conclusions and Future Work

This paper solves the open question of finding a strong variant of APAL that is recursively axiomatizable. Our system APALM is inspired by our analysis of Kuijer’s counterexample [11], which lead us to add to APAL a ‘memory’ of the initial situation. The soundness and completeness proofs crucially rely on a Subset Space-like semantics and on the equivalence between the effort modality and the arbitrary announcement modality, thus revealing the strong link between these two formalisms.

It seems clear that our method works for other versions of APAL, and in on-going work we are looking at a recursive axiomatization GALM for a memory-enhanced variant of GAL (Group Announcement Logic) [1]. As in GAL, the $\square$ operator quantifies only over announcements that are known by some of the agents, so GALM seems better fit than APALM for treating puzzles involving epistemic dialogues.