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

HAL
open science

# From Knowledge to Action: Logics of Permitted and Obligatory Announcements

Xu Li, Guillaume Aucher, Dov Gabbay, Réka Markovich

► To cite this version:

Xu Li, Guillaume Aucher, Dov Gabbay, Réka Markovich. From Knowledge to Action: Logics of Permitted and Obligatory Announcements. Journal of Artificial Intelligence Research, 2025, 82, pp.1629-1672. 10.1613/jair.1.17180. hal-05435926

HAL Id: hal-05435926

https://hal.science/hal-05435926v1

Submitted on 31 Dec 2025

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
# From Knowledge to Action: Logics of Permitted and Obligatory Announcements

Xu Li

University of Luxembourg

XU.LI@UNI.LU

Guillaume Aucher

Univ Rennes, CNRS, IRISA, IRMAR

GUILLAUME.AUCHER@UNIV-RENNES.FR

Dov Gabbay

King's College London
University of Luxembourg

DOV.GABBAY@KCL.AC.UK

Réka Markovich

University of Luxembourg

REKA.MARKOVICH@UNI.LU

## Abstract

We formalize the notions of “permitted and obligatory announcements” in the context of information security, such as privacy policy compliance. In a sender-receiver setting, we define the sender’s permitted and obligatory announcements in terms of the receiver’s ideal epistemic states (i.e., the epistemic states that comply with the given security policies). We propose two logics, LPOA and DLPOA, to reason about permitted and obligatory announcements in static and dynamic contexts, respectively. These two logics are completely axiomatized, and we also study generalizations in which the receiver’s knowledge is characterized by non-S5 logics. Our paper makes two main contributions to the formalization of permitted and obligatory announcements: First, we clarify the interplay between the sender’s permitted and obligatory announcements and the receiver’s knowledge. Second, we distinguish between weakly and strongly permitted announcements.

## 1. Introduction

With the development of technology (especially the use of big data and machine learning), information security is becoming increasingly important for individuals and organizations. Imagine an agent, Alice, who wants to buy a plane ticket from Luxembourg to China online. She visits the airline's website and finds that she needs to provide some personal information by filling out a form. Among the items listed in the form, some are mandatory, while others are optional. Assume that there are only four items in the form: Name, Phone Number, Email Address, and Meal Requirement. The passenger's name is mandatory, as well as *either* her phone number *or* Email address (so that the airline can reach her in case of irregularities). In contrast, the meal requirement is optional. In this case, the question arises as to which information is permitted to be sent by Alice to the airline and which is obligatory.

This example may seem simple, but similar scenarios are common in our daily lives (e.g., communications between a database and its users, conversations between a doctor and a patient, etc.), and most of them involve more complex issues. What these scenarios have in common is that agents (e.g., databases, doctors) need to decide which information is
permitted and which is obligatory to be sent or disclosed, according to a given information security policy (e.g., a privacy policy). In many cases, the security policy is specified in terms of the permitted and obligatory knowledge of the recipients (such as database users and patients). To decide which information is permitted to be disclosed, agents then need to derive it from the security policy. However, the security policy is not the only factor that agents need to consider; they must also take into account the recipients' initial knowledge. Consider the following example:

**Example 1.1** (Website example, Aucher et al., 2011). Consider the communication between a server and one of its users — Bob. The lists of websites visited by each user (v) are stored in the server, which are forbidden to be disclosed to Bob according to the security policy. However, since knowing which websites have been visited (w) is valuable information (for example, for the configuration of a firewall), the security policy does not forbid the disclosure of w to Bob. The server then anonymizes the data by replacing each user's name with a number by hashcode (h). Suppose that Bob is informed about and thus knows w. The server is then forbidden to disclose the hash function even if h is not forbidden by the security policy because the distribution of both w and h implies v.

This example illustrates the ineffectivity of anonymization in privacy protection, which has been shown by Sweeney (2002). The reason is that agents can identify the (anonymized) users by combining additional information (or knowledge) they have about the users (e.g., postal code and date of birth). A series of solutions have been proposed in the area of privacy protection (e.g., Sweeney, 2002; Machanavajjhala et al., 2007; Dwork, 2006).

In this paper, we address the problem of how to derive the permitted and obligatory information from a security policy, given the recipients' background knowledge, from a logical point of view. Specifically, we define a couple of operators for "permitted and obligatory announcements" in our formal language. Then we develop a logical framework to reason about the interplay between permitted and obligatory announcements, knowledge, and their dynamics. The logical framework brings together two branches of philosophical logic: dynamic epistemic logic and deontic logic. The well-known public announcement logic (Plaza, 1989; Gerbrandy & Groeneveld, 1997) provides a logic framework to reason about knowledge and the changes in knowledge brought about by truthful announcements. The public announcement operator [·] is treated as an action operator as in dynamic logic. On the other hand, in dynamic deontic logic (Meyer, 1987), the deontic logic of "ought-to-do" statements is reduced to variants of dynamic logic. The core of dynamic deontic logic is to define action permission (and obligation) by the deontic status after the execution of actions. Thus, it is natural to propose logical formalizations of permitted and obligatory announcements by combining ideas from both public announcement logic and dynamic deontic logic. In this paper, we define permitted and obligatory announcements in terms of the deontic status of the recipients' epistemic state after the announcements.

The idea of applying logic to protect privacy or maintain security in databases is far from new, as witnessed by the work of Bonatti et al. (1995), Cuppens and Demolombe (1996), Barth et al. (2006) and Jafari et al. (2014). However, none of them explicitly includes operators for "permitted (or obligatory) messages/announcements" in the objective language. As far as we know, only Aucher et al. (2011) and Balbiani and Seban (2011) have studied the notions of "permitted and obligatory announcements" at an objective level.
A detailed comparison between our paper and theirs can be found in Section 5. Our
contributions can be summarized as follows.

- Compared to Balbiani and Seban's (2011) work, we clarify the interplay between per-
  permitted and obligatory announcements and the the recipients' knowledge. We discover
  a set of new axioms for the interaction between these notions and we find that differ-
  ent choices of the underlying epistemic logic give rise to different logics of permitted
  and obligatory announcements;

- We distinguish between weakly and strongly permitted announcements. We show that this distinction is crucial to explaining certain phenomena, but was not made by Balbiani and Seban (2011) and Aucher et al. (2011).

The paper is structured as follows. In the next section, we develop a static logic of permitted and obligatory announcements (LPOA), including its language, semantics, and axiomatization. In Section 3, we study how public announcements affect the permitted and obligatory announcements. In Section 4, we generalize our framework to cases where the recipients' knowledge is characterized by non-S5 logics. We discuss related literature in Section 5 and conclude in Section 6.

2. A Logic of Permitted and Obligatory Announcements

In this section, we introduce a logic LPOA extending epistemic logic to reason about “per-
mitted and obligatory announcements” in the static case. The scenarios that LPOA intends
to characterize are communications between two agents where the information can only be
transmitted from one agent (the sender) to the other (the receiver). The sender is also sub-
ject to some security policies, such as privacy policies. Examples of such scenarios include
communications between a database or security monitor and its users, and conversations
between a doctor and their patients. We fix the role of the sender making only one of
the agents able to make (truthful) announcements. We assume that the sender is the only
source of information for the receiver.

We aim to develop a formalism that can be used by the sender to derive the permitted
and obligatory information in these scenarios. As suggested by Example 1.1, the receiver's
knowledge plays an equally important role as security policies in the decision process. But,
strictly speaking, it is the sender's knowledge about the receiver's knowledge (rather than
the receiver's knowledge itself) that should be considered, as it is unrealistic to expect
the sender to take responsibility for what they do not know. Thus, these scenarios are
intrinsically multi-agent. In our framework, however, only the receiver's epistemic state is
explicitly represented. We assume that the modeler is the sender<fnref n="1" /> and is not represented in
the formalism. The sender is also assumed to have perfect knowledge of the actual situation.
This aligns with the standard perspective in public announcement logic (consider, e.g., how
the muddy children puzzle is modeled in PAL, see van Ditmarsch et al., 2008), and allows
us to focus on the characterization of permitted and obligatory announcements. We leave
for future work the extension of our framework to the multi-agent case.

<footnote n="1">1. Thus, all components of our framework should be interpreted from the sender's perspective, such as the interpretation of formulas and the explanation of the semantics. However, as in public announcement logic, we will assume this is understood and will not state it explicitly.</footnote>
## 2.1 Formal Language

Let PROP be a countable infinite set of propositional variables (or atoms).

**Definition 2.1 (Language).** The language $\mathcal{L}_{LPOA}$ is given by the following BNF grammar:

$$ \varphi ::= p \mid \neg \varphi \mid (\varphi \rightarrow \varphi) \mid K \varphi \mid \mathcal{O}^{-} \varphi \mid \mathbb{P}^{-} \varphi \mid \mathbb{P}^{+} \varphi $$

where $p \in \text{PROP}$. Other Boolean connectives are defined as usual and $\mathcal{O}^{+} \varphi := (\mathcal{O}^{-} \varphi \wedge \mathbb{P}^{+} \varphi)$. Let $\mathcal{L}_{el}$ be the sublanguage of $\mathcal{L}_{LPOA}$ without the constructs $\mathcal{O}^{-} \varphi$, $\mathbb{P}^{-} \varphi$, and $\mathbb{P}^{+} \varphi$.

As in epistemic logic, the intuitive reading of the operator $K\varphi$ is “the receiver knows $\varphi$”. There are different notions of “permitted announcements” and “obligatory announcements” in $\mathcal{L}_{LPOA}$. The readings of the remaining operators are as follows:

- $\mathbb{P}^{-} \varphi$: “It is weakly permitted for the sender to (truthfully) announce $\varphi$”;

- $\mathbb{P}^{+} \varphi$: “It is strongly permitted for the sender to (truthfully) announce $\varphi$”;

- $\mathcal{O}^{-} \varphi$: “It is obligatory for the sender to (truthfully) announce $\varphi$”;

- $\mathcal{O}^{+} \varphi$: “Announcing $\varphi$ is the least informative (strongly) permitted announcement”.

The operator $\mathcal{O}^{+} \varphi$ can also be interpreted as an operator for “obligatory announcements”.

We distinguish different notions of “permitted announcements” and “obligatory announcements”, which is inspired by the study of deontic necessity and sufficiency done by van Benthem (1979) and Van De Putte (2017). According to Van De Putte (2017), given a normative system, we can identify two types of actions: those that are necessary conditions for the satisfaction of all obligations (prescribed in the normative system) and those that are sufficient conditions for the satisfaction of all obligations. For example, suppose that Bob is contemplating what he will do on Saturday. Since the birthday of Alice, one of his good friends, is on Saturday, he must join the birthday party. However, Saturday is also the deadline for his homework and he must complete it on time. Suppose that these two are the only obligations that Bob needs to fulfill on Saturday. In this case,

- “visit his other friend, say, Carol” is neither deontically necessary nor sufficient,

- “join Alice’s birthday party” is deontically necessary but not sufficient,

- “join Alice’s birthday, complete the homework, and visit Carol” is deontically sufficient but not necessary, and

- “join Alice’s birthday and complete the homework” is both deontically necessary and sufficient.

The analysis of deontic necessity and sufficiency enables us to distinguish between different concepts of obligation and permission in natural language. It is argued by Van De Putte (2017) that there are two notions of obligation and permission, respectively. For obligation, it may refer to either deontic necessity (as in standard deontic logic) or deontic necessity and sufficiency (as in the work of Anglberger et al., 2015). For permission, it also refers to two notions: the dual of deontic necessity (as in standard deontic logic, often called “weak permission”) and deontic sufficiency (as in the work of Anglberger et al., 2015, called “strong permission”).
Following Van De Putte (2017), we also distinguish between two notions of “permitted announcements” and “obligatory announcements”. The formulas $O^{-}\varphi$ and $P^{+}\varphi$ are intended to express that “announcing $\varphi$ is necessary/sufficient for the receiver’s epistemic state to be ideal”, respectively. $P^{-}\varphi$ is intended to express that “announcing $\varphi$ is not forbidden” or, alternatively, “for the receiver’s epistemic state to be ideal, it is not necessary to *not* announce $\varphi$”.<fnref n="2" /> Finally, $O^{+}\varphi$ expresses that “announcing $\varphi$ is both sufficient and necessary for the receiver’s epistemic state to be ideal”. We illustrate their difference by the plane ticket example at the beginning of the paper:

**Example 2.2 (Plane ticket example).** In the plane ticket scenario, the sender is Alice, and the receiver is the airline. Let $n$, $p$, $e$, and $m$ be the propositions that “Alice’s (full) name is ...”, “Alice’s phone number is ...”, “Alice’s email address is ...”, and “Alice’s meal requirements are ...”, respectively. First of all, $n$ and $p \lor e$ are not forbidden information (according to the airline’s policy), so it is weakly permitted (for Alice) to announce them, i.e., $P^{-}n$ and $P^{-}(p \lor e)$. But neither $n$ nor $p \lor e$ is sufficient, so it is not strongly permitted (for Alice) to announce $n$, as well as $p \lor e$ (i.e., $\neg P^{+}n$ and $\neg P^{+}(p \lor e)$). $n \land p$ is sufficient, so it is strongly permitted (for Alice) to announce $n \land p$ (namely, $P^{+}(n \land p)$).

On the other hand, since $n$ is a piece of necessary information, it is obligatory (for Alice) to announce $n$, i.e., $O^{-}n$. Finally, there is no single formula (composed of the atoms $n$, $p$, $e$, and $m$) that is both sufficient and necessary information. Intuitively, we may think that, to satisfy all obligations, it is sufficient and necessary to announce $n \land p$ or to announce $n \land e$. So, if the action choice $\cup$ were added to our language, we could express it as $O^{+}([n \land p] \cup [n \land e])$.<fnref n="3" /> But we do not consider complex announcements in this paper and leave it for future work.

We summarize the meanings of the four deontic operators in LPOA in Table 1. In fact, all four meanings of permitted and obligatory announcements have been noticed in different literature and characterized in different ways, see Section 5. The logic LPOA provides a uniform way of reasoning about them.

<table><caption>Table 1: The interpretations and readings of the deontic operators in $\mathcal{L}_{LPOA}$.</caption><thead><tr><td>Operator</td><td>Interpretation</td><td>Reading</td></tr></thead><tbody><tr><td>$O^{-}\varphi$</td><td>Announcing $\varphi$ is necessary for the receiver's epistemic state to be ideal</td><td>It is obligatory for the sender to (truthfully) announce $\varphi$</td></tr><tr><td>$P^{+}\varphi$</td><td>Announcing $\varphi$ is sufficient for ...</td><td>It is strongly permitted for ...</td></tr><tr><td>$P^{-}\varphi$</td><td>Announcing $\varphi$ is not forbidden</td><td>It is weakly permitted for...</td></tr><tr><td>$O^{+}\varphi$</td><td>Announcing $\varphi$ is both sufficient and necessary for ...</td><td>$\varphi$ is the least informative (strongly) permitted announcement</td></tr></tbody></table>

<footnote n="2">2. Note that the second "not" means action negation or refraining from an action, instead of the Boolean connective $\neg$. Since "not announce $\varphi$" is intuitively different from "announce $\neg\varphi$", the operator $P^{-}\varphi$ can not be defined via $\neg O^{-}\neg\varphi$. This deviates from standard deontic logic as (weak) permission is usually defined as the dual of obligation.</footnote>

<footnote n="3">3. We note that the "non-deterministic choice between announcements" is a well-studied notion in dynamic epistemic logic, see (Baltag & Moss, 2004).</footnote>
As we have seen from the website example in the Introduction, the notion of “permitted announcements” is not solely determined by the security policies, but also dependent on the receiver’s knowledge. In fact, the same holds also for “obligatory announcements”:

**Example 2.3** (Classified information example, Aucher et al., 2011). Suppose that the sender is communicating classified information to the receiver. Since the receiver is entitled to know some information *p*, the only constraint (in the security policy) is that the sender is forbidden to inform the receiver only about *p* while not informing him that it is classified (*c*). Furthermore, suppose that the receiver is informed about *p*, but does not know *c* (*Kp ∧ ¬Kc*). Intuitively, we will agree that in this case, it is obligatory for the sender to announce *c* (*O*⁻*c*) even if it is not prescribed in the policy.

As we shall see, the logic LPOA enables us to derive the permitted and obligatory announcements based on the receiver's knowledge.

**2.2 Semantics**

In this section, we introduce the formal semantics for LPOA.

**Definition 2.4** (Model). A *model* is a tuple $M = (W, N, V)$ such that:

1. $W$ is a non-empty set;

2. $N: W \to \wp(\wp(W))$ is such that for all $w \in W$ and $U \in N(w)$, $w \in U$;

3. $V: \text{PROP} \to \wp(W)$ is a valuation function.

As usual, an element $w \in W$ is called a possible world (or state). For every state $w$, a set $X$ with $w \in X \subseteq W$ represents an “epistemic state” of the receiver at the (factual) state $w$ (i.e., $X$ is the set of states that the receiver cannot distinguish from the state $w$). The neighbourhood function $N$ therefore assigns to each state $w$ a set of the receiver’s epistemic states. The elements of $N(w)$ are understood as “ideal epistemic states” of the receivers at $w$. That is to say, the receiver’s epistemic state represented by each subset $X \in N(w)$ is compliant with the given security policies (specified at the factual state $w$). Note that it is the sender’s duty to maintain the compliance (or ideality) of the receiver’s epistemic state (i.e., to make sure that the receiver’s actual epistemic state is in $N(w)$ by announcing information). Let us illustrate the definition of the model by the plane ticket example:

**Example 2.5** (Plane ticket example continued). The scenario in Example 2.2 can be characterized by the model $M = (W, N, V)$ (as illustrated in Figure 1) where:

- $W = \wp(\{\mathbf{n}, \mathbf{p}, \mathbf{e}, \mathbf{m}\})$ (we denote $\{\mathbf{n}, \mathbf{p}, \mathbf{e}, \mathbf{m}\}$ by npem and similarly for other states);

- $N(w) = \{W\}$ for all $w \neq \text{npem}^4$ and $N(\text{npem}) = \{U \subseteq W \mid \text{npem} \in U \text{ and } (U \subseteq \{\text{npem}, \text{nem}, \text{npe}, \text{ne}\} \text{ or } U \subseteq \{\text{npem}, \text{rpm}, \text{npe}, \text{np}\})\}$;

- for all $w \in W$ and $p \in \{\mathbf{n}, \mathbf{p}, \mathbf{e}, \mathbf{m}\}$, $w \in V(p)$ if $p \in w$.

<footnote n="4">4. In fact, for all $w \neq \text{npem}$, $N(w)$ could be defined arbitrarily as we only intend to model the permitted and obligatory announcements for Alice at the current world nemp.</footnote>
Note that in each epistemic state npem $\in U \subseteq \{npem, nem, npe, ne\}$, the information n and e are "known" (i.e., true at every indistinguishable state). Hence, it is compliant with the Airline's policy as described at the beginning of this paper. The same holds also for npem $\in U \subseteq \{npem, rpm, npe, np\}$ where the information n and p are known.

<figure><img src="image_3.png" /><figcaption>Figure 1: The model $M = (W, N, V)$. Worlds are the subsets of $\{n, p, e, m\}$ and are indicated as npem, npe, rpm, ... The valuation is such that the set of true atoms at each world is exactly the world itself. The neighbourhood $N(npem)$ consists of all subsets that contain npem and are contained in one of the dashed circles, and $N(w) = \{W\}$ for every $w \neq npem$.</figcaption></figure>

The model defined above encodes only the content of the security policies. To give the semantics, we also need information about the receiver's current epistemic state. In our semantics, the formulas are evaluated not at a single state $w$, but with respect to a pair $w, X$ where $w \in X \subseteq W$. The set $X$ represents the current epistemic state of the receiver at $w$. This kind of "two-dimensional" semantics is far from new in epistemic logic, as it can be found in, e.g., subset space logic (Dabrowski, Moss, & Parikh, 1996) and, more recently, Yalcin's (2007) work. We will not discuss the conceptual link between our semantics and theirs because we choose the two-dimensional semantics mainly for technical reasons. Compared to the usual relational semantics for epistemic logic (van Ditmarsch et al., 2008), "epistemic states" become primitive objects in the two-dimensional semantics. Hence, it is more convenient to talk about the quantification or shifting of "epistemic states".

**Definition 2.6 (Semantics).** Given a model $M = (W, N, V)$, for all $\varphi \in \mathcal{L}_{LPOA}$ and $w \in X \subseteq W$, the satisfaction relation $M, w, X \models \varphi$ is inductively defined as follows:

$$
\begin{array}{l@{\qquad}l}
M, w, X \models p & \text{iff } w \in V(p) \\
M, w, X \models \neg \varphi & \text{iff } \text{not } M, w, X \models \varphi \\
M, w, X \models (\varphi \rightarrow \psi) & \text{iff } M, w, X \not\models \varphi \text{ or } M, w, X \models \psi \\
M, w, X \models K\varphi & \text{iff } \text{for all } v \in X, M, v, X \models \varphi \\
M, w, X \models \mathcal{O}^{-}\varphi & \text{iff } M, w, X \models \varphi \text{ and for all } Y \in N(w), Y \subseteq X \text{ implies } Y \subseteq [\varphi]_{M,X} \\
M, w, X \models \mathcal{P}^{-}\varphi & \text{iff } \text{there is } Y \in N(w) \text{ such that } Y \subseteq [\varphi]_{M,X} \\
M, w, X \models \mathcal{P}^{+}\varphi & \text{iff } [\varphi]_{M,X} \in N(w)
\end{array}
$$
where $[[\varphi]]_{M,X} = \{v \in X \mid M, v, X \models \varphi\}$ is the truth set of $\varphi$ in $X$. We will write $[[\varphi]]_X$ when $M$ is clear from the context.

For every set of formulas $\Gamma \cup \{\varphi\}$, we say $\varphi$ is a semantic consequence of $\Gamma$, notation $\Gamma \models \varphi$, if for every model $M = (W, N, V)$, $w \in W$ and $w \in X \subseteq W$: if $M, w, X \models \psi$ for every $\psi \in \Gamma$ then $M, w, X \models \varphi$. A formula $\varphi$ is valid, notation $\models \varphi$, if $\emptyset \models \varphi$.

"$M, w, X \models \varphi$" is to be read as "$\varphi$ is true at $w$ with respect to the receiver's current epistemic state $X$." The semantics for $\mathbb{P}^+\varphi$ reflects the intuition that "it is strongly permitted to announce $\varphi$" iff "the epistemic state after the announcement of $\varphi$ is ideal".<fnref n="5" /> Given two epistemic states $X$ and $Y$, $Y \subseteq X$ means that $Y$ can be achieved from $X$ by some public announcements.<fnref n="6" /> Thus, the truth definition for $\mathcal{O}^-\varphi$ reflects the intuition that "it is obligatory to announce $\varphi$" iff "$\varphi$ is true ($\varphi$ can be truthfully announced) and $\varphi$ is 'known' at all ideal epistemic states achievable by further announcements". Similarly, for $\mathbb{P}^-\varphi$, we have that "it is weakly permitted to announce $\varphi$" iff "$\varphi$ is 'known' at some ideal epistemic state achievable by further announcements".<fnref n="7" /> Note that, in the truth definition for $\mathbb{P}^-\varphi$, $Y$ is implicitly required to be contained in the current epistemic state $X$ as $[[\varphi]]_{M,X} \subseteq X$ and, therefore, $Y$ is "achievable" from $X$. We illustrate the semantics by the previous examples.

**Example 2.7** (Plane ticket example continued). As the reader can check, the following hold in the model $M$ as illustrated in Figure 1:

- $M, \text{npem}, W \models \mathbb{P}^-\text{n}$ and $M, \text{npem}, W \models \mathbb{P}^-(\mathbf{p} \vee \mathbf{e})$;

- $M, \text{npem}, W \not\models \mathbb{P}^+\text{n}$, $M, \text{npem}, W \not\models \mathbb{P}^+(\mathbf{p} \vee \mathbf{e})$, and $M, \text{npem}, W \models \mathbb{P}^+(\mathbf{n} \wedge \mathbf{p})$;

- $M, \text{npem}, W \models \mathcal{O}^-\text{n}$.

**Example 2.8** (Website example continued). The scenario in Example 1.1 can be represented by the following model $M = (W, N, V)$ where:

- $W = \wp(\{w, h, v\})$;

- $N(\text{whv}) = \{Y \subseteq W \mid \text{whv} \in Y \text{ and } Y \not\subseteq \{\text{whv}, \text{wv}, \text{hv}, v\}\}$ and $N(w)$ is arbitrarily defined for all $w \neq \text{whv}$;

- for all $w \in W$ and $p \in \{w, h, v\}$, $w \in V(p)$ if $p \in w$.

We have $M, \text{whv}, \{\text{whv}, \text{wv}, w\} \models K\mathbf{w} \wedge K((\mathbf{w} \wedge \mathbf{h}) \rightarrow \mathbf{v}) \wedge \neg \mathbb{P}^-\mathbf{h}$.

**Example 2.9** (Classified information example continued). The scenario in Example 2.3 can be represented by the following model $M = (W, N, V)$ where:

- $W = \{w, u, v, x\}$;

- $N(w) = \{Y \subseteq W \mid w \in Y \text{ and } Y \neq \{w, u\}\}$ and $N(z)$ is arbitrarily defined for all $z \neq w$;

- $V(p) = \{w, u\}$ and $V(c) = \{w, v\}$.

<footnote n="5">5. The public announcement of $\varphi$ will restrict the current epistemic state to $[[\varphi]]_{M,X}$, see Section 3.</footnote>

<footnote n="6">6. This does not hold in general, see Remark 2 for the explanation.</footnote>

<footnote n="7">7. This should be seen as a simplified explanation only for S5-epistemic logic, see Section 4.</footnote>
In this model $M$, we have $M, w, \{w, u\} \models \mathcal{O}^{-}c$. Note that the choice of the current epistemic state $\{w, u\}$ reflects the fact that the receiver currently knows $p$ and is uncertain about $c$, i.e., $M, w, \{w, u\} \models Kp \wedge \neg Kc$.

**Remark 1.** A question may arise regarding the semantics for $\mathcal{O}^{-}\varphi$ (and similarly for $\mathbb{P}^{-}\varphi$): why do we just consider ideal epistemic states achievable by further announcements instead of all? Technically, one may propose the following alternative semantic definition for $\mathcal{O}^{-}\varphi$:

$$M, w, X \models \mathcal{O}^{-}\varphi \quad \text{iff} \quad M, w, X \models \varphi \quad \text{and for all } Y \in N(w), Y \subseteq [\varphi]_{M,W}. \quad (\dagger)$$

However, in situations like the classified information example, $(\dagger)$ does not work, since it predicts that the sender is not obliged to announce $c$. The reason is that there are also ideal epistemic states of the receiver at $w$ in which the receiver knows neither $p$ nor $c$ (e.g., the whole domain $W$). However, these ideal epistemic states are not achievable by further announcements from the current epistemic state $\{w, u\}$. Likewise, if we propose a similar alternative semantic definition for $\mathbb{P}^{-}\varphi$, then it would not work in the website example.

**Remark 2.** Another question regarding the semantics for $\mathcal{O}^{-}\varphi$ (and $\mathbb{P}^{-}\varphi$) is whether the achievable ideal epistemic states are precisely those $Y \in N(w)$ with $Y \subseteq X$. The inclusion from left to right seems less problematic, whereas the converse is not. Suppose that the current epistemic state $X$ contains two worlds $x, y$ such that no formula in $\mathcal{L}_{LPOA}$ can distinguish the pairs $M, x, X$ and $M, y, X$, and for some $Y \in N(w)$ we have $Y \subseteq X$, $x \in Y$, and $y \notin Y$. Then $Y$ cannot be obtained by any public announcements of formulas in $\mathcal{L}_{LPOA}$. Thus, it seems reasonable to impose the following constraint on models:

$$\text{For all } w \in X \subseteq W \text{ and } Y \in N(w), \text{ if } Y \subseteq X \text{ then } Y = [\varphi]_{M,X} \text{ for some } \varphi \in \mathcal{L}_{LPOA}.$$

However, imposing such a constraint on models does not change the logic (the set of validities). This is because the canonical model we will construct in Definition 3.24 satisfies this constraint, see Remark 7 on page 1655.

## 2.3 Invariance and Semantic Results

In this section, we show that $\mathcal{L}_{LPOA}$ is invariant under a slightly adapted notion of “bounded morphisms” for neighbourhood semantics (Pacuit, 2017). In addition, we give some semantic results.

**Definition 2.10 (Bounded morphism).** Suppose $M_1 = (W_1, N_1, V_1)$ and $M_2 = (W_2, N_2, V_2)$ are two models, $X_1 \subseteq W_1$, and $X_2 \subseteq W_2$. If $f: X_1 \to X_2$ and $Y \subseteq X_2$, then let $f^{-1}(Y) = \{w \in X_1 | f(w) \in Y\}$ be the inverse image of $Y$. A function $f: X_1 \to X_2$ is a *bounded morphism* from $X_1$ to $X_2$ if it satisfies the following conditions:

(M1) $f$ is surjective;

(M2) for all $p \in \text{PROP}$ and $w \in X_1$, $w \in V_1(p)$ iff $f(w) \in V_2(p)$;

(M3) for all $Y \subseteq X_2$ and $w \in X_1$, if $Y \in N_2(f(w))$ then $f^{-1}(Y) \in N_1(w)$;

(M4) for all $Y \subseteq X_1$ and $w \in X_1$, if $Y \in N_1(w)$ then $f(Y) \in N_2(f(w))$.
Roughly speaking, there are two main differences between the above definition and the definition of "bounded morphisms" by Pacuit (2017, Definition 2.7): first, we require that the function $f$ be surjective. This is because, in addition to the neighbourhood operators ($\mathcal{O}^{-}\varphi$, $\mathbb{P}^{-}\varphi$, and $\mathbb{P}^{+}\varphi$), we also have the operator $K\varphi$ which does not have a neighbourhood semantics. Second, $f$ is a function from a subset of $W_1$ to a subset of $W_2$ (instead of a function from $W_1$ to $W_2$). This is more general than Pacuit's definition. We choose to do so because the truth of the formulas in $\mathcal{L}_{LPOA}$ is always evaluated with respect to a subset of the domain.

**Proposition 2.11.** Suppose that $M_1 = (W_1, N_1, V_1)$ and $M_2 = (W_2, N_2, V_2)$ are two models, $X_1 \subseteq W_1$, and $X_2 \subseteq W_2$. Let $f: X_1 \to X_2$ be a bounded morphism from $X_1$ to $X_2$. Then, for all $\varphi \in \mathcal{L}_{LPOA}$ and $w \in X_1$, $M_1, w, X_1 \models \varphi$ iff $M_2, f(w), X_2 \models \varphi$.

*Proof.* The proof is by induction on the structure of $\varphi$. The base and the cases for Boolean connectives are straightforward.

**Case K$\psi$:**

$$M_1, w, X_1 \models K\psi$$

iff for all $v \in X_1$, $M_1, v, X_1 \models \psi$ (semantics)

iff for all $v \in X_1$, $M_2, f(v), X_2 \models \psi$ (IH)

iff for all $v' \in X_2$, $M_2, v', X_2 \models \psi$ ($f$ is a surjective function from $X_1$ to $X_2$)

iff $M_2, f(w), X_2 \models K\psi$ (semantics)

**Case $\mathcal{O}^{-}\psi$:**

$$M_1, w, X_1 \models \mathcal{O}^{-}\psi$$

iff $M_1, w, X_1 \models \psi$ and for all $Y \subseteq X_1$, $Y \in N_1(w)$ implies $Y \subseteq [[\psi]]_{M_1, X_1}$ (semantics)

iff $M_2, f(w), X_2 \models \psi$ and for all $Y \subseteq X_2$, $Y \in N_2(f(w))$ implies $Y \subseteq [[\psi]]_{M_2, X_2}$ (up by (M4) and IH, down by (M3) and IH)

iff $M_2, f(w), X_2 \models \mathcal{O}^{-}\psi$ (semantics)

**Case $\mathbb{P}^{-}\psi$:**

$$M_1, w, X_1 \models \mathbb{P}^{-}\psi$$

iff there is $Y \in N_1(w)$ such that $Y \subseteq [[\psi]]_{M_1, X_1}$ (semantics)

iff there is $Y \in N_2(f(w))$ such that $Y \subseteq [[\psi]]_{M_2, X_2}$ (up by (M3) and IH, down by (M4) and IH)

iff $M_2, f(w), X_2 \models \mathbb{P}^{-}\psi$ (semantics)

**Case $\mathbb{P}^{+}\psi$: (note that $f^{-1}([[\psi]]_{M_2, X_2}) = [[\psi]]_{M_1, X_1}$ and $f([[\psi]]_{M_1, X_1}) = [[\psi]]_{M_2, X_2}$ by the IH.)**

$$M_1, w, X_1 \models \mathbb{P}^{+}\psi$$

iff $[[\psi]]_{M_1, X_1} \in N_1(w)$ (semantics)

iff $[[\psi]]_{M_2, X_2} \in N_2(f(w))$ (up by (M3) and IH, down by (M4) and IH)

iff $M_2, f(w), X_2 \models \mathbb{P}^{+}\psi$ (semantics)

□

Proposition 2.11 shows that the existence of a bounded morphism is sufficient for two models to be $\mathcal{L}_{LPOA}$-equivalent. However, as we will see in Section 3.2, there are $\mathcal{L}_{LPOA}$-equivalent models such that no bounded morphism exists between them. That is to say, bounded morphisms are not necessary conditions for two models to be $\mathcal{L}_{LPOA}$-equivalent.
Finding the right notion characterizing $\mathcal{L}_{LPOA}$-equivalence between two models remains an open problem.

Next, we list some observations of the semantics by applying Proposition 2.11. First, note that, for all models $M_1, M_2$ and the subsets $X_1, X_2$ of their domains, the definition of bounded morphism from $X_1$ to $X_2$ says nothing “outside” $X_1$ and $X_2$. As an immediate consequence, we have the following.

**Proposition 2.12.** For all models $M = (W, N, V)$ and $\emptyset \neq X \subseteq W$, let the restriction of $M$ to $X$ be the model $M_X = (X, N_X, V_X)$ where $N_X(w) = \{U \in N(w) \mid U \subseteq X\}$ for all $w \in X$ and $V_X$ is the restriction of $V$ to $X$. Then for all $w \in X$ and formulas $\varphi$, $M, w, X \models \varphi$ iff $M_X, w, X \models \varphi$.

*Proof.* Note that the identity function on $X$ is a bounded morphism from $X$ to itself. $\square$

When defining our models, the set of ideal epistemic states for a state $w, N(w)$, is not required to be non-empty. This is in contrast with standard deontic logic. Formally, we call a model $M = (W, N, V)$ *standard* if for all $w \in W, N(w) \neq \emptyset$. The next proposition shows that the class of standard models gives the same logic as the class of all models.

**Proposition 2.13.** Let $M = (W, N, V)$ be a model and $w \in X \subseteq W$. Then there is a standard model $M' = (W', N', V')$ and $w' \in X' \subseteq W'$ such that $M, w, X \models \varphi$ iff $M', w', X' \models \varphi$ for all $\varphi \in \mathcal{L}_{LPOA}$.

*Proof.* Let $z \notin W$ be a new element. We construct $M'$ as follows: $W' = W \cup \{z\}$; $N'(x) = N(x) \cup \{\{x, z\}\}$ for all $x \in W$ and $N'(z) = \{\{z\}\}$; and $V'(p) = V(p)$ for all $p \in \text{PROP}$. It is clear that $M'$ is standard. Let $f: X \to X$ be the identity function on $X$. It is easy to see that $f$ is a bounded morphism from $X$ to itself. Thus, $M, w, X \models \varphi$ iff $M', w, X \models \varphi$ for all $\varphi \in \mathcal{L}_{LPOA}$. $\square$

We conclude this subsection by stating some validities of LPOA.

**Proposition 2.14.** The following hold for all formulas $\varphi, \psi \in \mathcal{L}_{LPOA}$:

(1) $\models \mathbb{P}^{-}\varphi \rightarrow \varphi$.

(2) $\models \mathbb{P}^{+}\varphi \rightarrow \mathbb{P}^{-}\varphi$.

(3) $\models K\varphi \rightarrow \mathbb{O}^{-}\varphi$.

(4) $\models \neg \mathbb{P}^{-}\top \rightarrow (\mathbb{O}^{-}\varphi \leftrightarrow \varphi)$.

(5) $\models K(\varphi \leftrightarrow \psi) \rightarrow (\mathbb{P}^{+}\varphi \leftrightarrow \mathbb{P}^{+}\psi)$.

(6) $\models \mathbb{O}^{-}(\varphi \rightarrow \psi) \rightarrow (\mathbb{O}^{-}\varphi \rightarrow \mathbb{O}^{-}\psi)$.

(7) $\models \mathbb{O}^{-}(\varphi \rightarrow \psi) \rightarrow (\mathbb{P}^{-}\varphi \rightarrow \mathbb{P}^{-}\psi)$.

(8) $\models \mathbb{O}^{-}\varphi \rightarrow (\mathbb{P}^{+}\psi \rightarrow K(\psi \rightarrow \varphi))$.

*Proof.* We show only the last one. Let $M = (W, N, V)$ be a model and $w \in X \subseteq W$. Suppose $M, w, X \models \mathbb{O}^{-}\varphi$ and $M, w, X \models \mathbb{P}^{+}\psi$. Suppose, toward a contradiction, that $M, w, X \not\models K(\psi \rightarrow \varphi)$. By semantics, there is $v \in X$ such that $M, v, X \not\models \psi \rightarrow \varphi$. Hence $M, v, X \models \psi$ and $M, v, X \not\models \varphi$. Thus, $[\psi]_X \not\subseteq [\varphi]_X$. Note that we assume $M, w, X \models \mathbb{P}^{+}\psi$. By semantics, we have $[\psi]_X \in N(w)$. Since $[\psi]_X \subseteq X$, it follows that $M, w, X \not\models \mathbb{O}^{-}\varphi$, contradiction! $\square$
## 2.4 Axiomatization

In this section, we propose a Hilbert-style axiom system for LPOA.

**Definition 2.15** (Axiomatization). The axiomatization **LPOA** for $\mathcal{L}_{LPOA}$ is provided in Figure 2. Let the set of **LPOA**-theorems be the least set of formulas in $\mathcal{L}_{LPOA}$ that contains all instances of the axiom schemas and is closed under the inference rules in Figure 2. If a formula $\varphi$ is an **LPOA**-theorem, we write $\vdash \varphi$. Given a set of formulas $\Gamma \cup \{\varphi\}$ in $\mathcal{L}_{LPOA}$, we write $\Gamma \vdash \varphi$ if there are formulas $\psi_1, \dots, \psi_n \in \Gamma$ such that $\vdash (\psi_1 \wedge \dots \wedge \psi_n) \to \varphi$.

<figure><img src="image_4.png" /><figcaption>Figure 2: The axiomatization **LPOA**.</figcaption></figure>

Some theorems and derived rules of **LPOA** are given in the next proposition, which will be used in the completeness proof.

**Proposition 2.16.** The following hold for all $\varphi, \psi \in \mathcal{L}_{LPOA}$:

(1) If $\vdash \varphi$ then $\vdash \mathcal{O}^{-}\varphi$.

(2) $\vdash \mathcal{P}^{-}\varphi \to (\mathcal{O}^{-}\psi \to \mathcal{P}^{-}\psi)$.

(3) $\vdash \mathcal{O}^{-}\varphi \to \varphi$.

*Proof.* It is easy to see that (1) follows from the axiom (A3) and the rules (Nec<sub>K</sub>) and (MP). Below is a proof for (2):

1. $\psi \to (\varphi \to \psi)$ (PL)

2. $\mathcal{O}^{-}(\psi \to (\varphi \to \psi))$ (Item (1))

3. $\mathcal{O}^{-}(\psi \to (\varphi \to \psi)) \to (\mathcal{O}^{-}\psi \to \mathcal{O}^{-}(\varphi \to \psi))$ (A6)

4. $\mathcal{O}^{-}\psi \to \mathcal{O}^{-}(\varphi \to \psi)$ (MP, 2, 3)

5. $\mathcal{O}^{-}(\varphi \to \psi) \to (\mathcal{P}^{-}\varphi \to \mathcal{P}^{-}\psi)$ (A7)

6. $\mathcal{O}^{-}\psi \to (\mathcal{P}^{-}\varphi \to \mathcal{P}^{-}\psi)$ (Propositional calculus, 4, 5)

7. $\mathcal{P}^{-}\varphi \to (\mathcal{O}^{-}\psi \to \mathcal{P}^{-}\psi)$ (Propositional calculus, 6)

For (3), a proof is as follows:
1. $\mathbb{P}^-\top \rightarrow (\mathcal{O}^-\varphi \rightarrow \mathbb{P}^-\varphi)$ (Item (2))

2. $\mathbb{P}^-\varphi \rightarrow \varphi$ (A1)

3. $\mathbb{P}^-\top \rightarrow (\mathcal{O}^-\varphi \rightarrow \varphi)$ (Propositional calculus, 1, 2)

4. $\neg \mathbb{P}^-\top \rightarrow (\mathcal{O}^-\varphi \leftrightarrow \varphi)$ (A4)

5. $\mathcal{O}^-\varphi \rightarrow \varphi$ (Propositional calculus, 3, 4)

☐

We make some remarks about the axioms in LPOA. (A1) says that every (weakly) permitted announcement is true. Note that in our system, announcements are required to be truthful to be executable. Thus, axiom (A1) just asserts that permitted announcements are always executable. (A2) says that strongly permitted announcements are also not forbidden. To understand (A4), note that $\neg \mathbb{P}^-\top$ holds precisely when there is no achievable ideal epistemic state (which can happen when, e.g., the receiver knows something that she is forbidden to know). In this case, the axiom (A4) predicts that the obligatory announcement operator $\mathcal{O}^-\varphi$ collapsed into the truth of $\varphi$. (A6) is the standard (K) axiom (or distribution axiom) for obligation. (A7) states the following: If the sender is obliged to announce $\varphi \rightarrow \psi$, then the permission to announce $\varphi$ implies the permission to announce $\psi$. Note that (A7) is also a theorem of standard deontic logic.

(A3), (A5), and (A8) remain to be considered. We interpret the formula $K(\psi \rightarrow \varphi)$ as saying that "$\psi$ is more informative for the receiver than $\varphi$".<fnref n="8" /> Then the axiom (A5) says that if $\varphi$ and $\psi$ are equivalently informative for the receiver, then the strongly permitted announcement of $\varphi$ implies the strongly permitted announcement of $\psi$ and vice versa. Similarly, (A8) says that a strongly permitted announcement is more informative than any obligatory announcement. This is quite intuitive because strongly permitted announcements are sufficient information (for the receiver's epistemic state to be ideal), while obligatory announcements are necessary information. Finally, (A3) states that the sender is obliged to announce whatever the receiver knows. This seems counter-intuitive. To understand (A3), note that, if $\varphi$ is known by the receiver, the announcement of $\varphi$ is actually less informative than any announcement for the receiver. Thus, from the informational point of view, the announcement of $\varphi$ is "implied" by any announcement (or, alternatively, the information $\varphi$ is implicitly included in every announcement) since we assume that the sender can only make truthful announcements. In this sense, the announcement of $\varphi$ is inevitable or necessary in our system. So, the obligatory announcement of $\varphi$ simply follows from the fact that the announcement of $\varphi$ is necessary.<fnref n="9" />

*Remark 3.* We interpret obligatory announcements as “announcements that are necessary for the receiver’s epistemic state to be ideal”. This follows a tradition in deontic logic that defines obligation as “what is necessary for a good person to do”, which can be traced back to Leibniz (cf. Hilpinen & McNamara, 2013). The axiom (A3) can thus be seen as an analog of the necessitation rule in standard deontic logic.

However, this interpretation of obligation may not match the intuitive meaning of obligation in all contexts. A finer analysis of the meaning of “obligatory announcements”

<footnote n="8">8. We follow Aucher et al. (2011, Definition 9) for the definition of “informativeness” of formulas.</footnote>

<footnote n="9">9. Another way to understand (A3) is as follows. Note that, with the presence of other axioms and rules, (A3) is equivalent to the following axiom and rule: (1) $K(\varphi \rightarrow \psi) \rightarrow (\mathcal{O}^-\varphi \rightarrow \mathcal{O}^-\psi)$; (2) from $\varphi$, infer $\mathcal{O}^-\varphi$. The latter is the familiar necessitation rule, and the former says that if $\varphi$ is more informative than $\psi$ then the obligatory announcement of $\varphi$ implies the obligatory announcement of $\psi$.</footnote>
remains to be done. We only mention that, for readers still against the axiom (A3), an
alternative notion of obligatory announcements is definable in LPOA: $O_a\varphi := \neg K\varphi \wedge O^{-}\varphi$.
The intuition is that in practice, if $\varphi$ is known (or informed), then the sender does not have
the obligation to inform it again. The operator $O_a\varphi$ thus defined is not a normal modality.
It can also be shown that $\vdash \neg O_a K\varphi$ and $\vdash \neg O_a \neg K\varphi$ for arbitrary formula $\varphi$. For example,
by the negative introspection (the axiom 5) for $K$, we have $\vdash \neg(\neg K\varphi \wedge \neg K \neg K\varphi)$. Note that
$\vdash O_a \neg K\varphi \rightarrow \neg K\varphi$ (as $\vdash O^{-}\psi \rightarrow \psi$ by Proposition 2.16(3)) and $\vdash O_a \neg K\varphi \rightarrow \neg K \neg K\varphi$ (by
the definition of $O_a$). Hence $\vdash O_a \neg K\varphi \rightarrow (\neg K\varphi \wedge \neg K \neg K\varphi)$. Hence $\vdash \neg O_a \neg K\varphi$. Similarly,
we have $\vdash \neg O_a K\varphi$. Moreover, it can even be shown that $\vdash \neg O_a\varphi$ for all pure epistemic
formulas $\varphi$. I.e., the sender has no obligation to announce any statement regarding the
receiver's epistemic state.

**2.5 Soundness and Completeness**

The soundness of **LPOA** is obvious in view of Proposition 2.14. To prove the completeness,
we use the usual canonical model method. However, to build the canonical model, we adopt
the so-called “copy-and-merge” technique which was originally developed by Gargov and
Passy (1990) and Passy and Tinchev (1991). Traditionally, the domain of the canonical
model consists of all maximal consistent sets (in the logic we considered). But in the
canonical model we will construct, the domain is obtained by merging two copies of the set
of all maximal consistent sets (i.e., each state in the domain is a maximal consistent set
indexed by the numbers 1 or 2). By doing so, some subsets of the domain (those consisting
exclusively of maximal consistent sets indexed by one of the numbers) will be the truth sets
of no formula. These subsets can then be used in the construction of the neighbourhood
function to provide “witness” to the truth of formulas like $P^{-}\varphi$, without affecting the truth
value of formulas like $P^{+}\varphi$.

The notion of “maximal consistent sets” is defined as usual and the standard properties
of maximal consistent sets are taken for granted. The set of all maximal consistent sets will
be denoted by *MCS*. The well-known Lindenbaum’s lemma claims that, for any consistent
set of formulas Γ, there is a maximal consistent set Σ extending Γ. This also holds for
LPOA.

**Definition 2.17.** $\sim^c$ and $R^c$ are two binary relations on *MCS* such that for all $\Gamma, \Delta \in \mathbf{MCS}$:

- $\Gamma \sim^c \Delta$ if $\{\psi \mid K\psi \in \Gamma\} \subseteq \Delta$, and

- $\Gamma R^c \Delta$ if $\{\psi \mid O^{-}\psi \in \Gamma\} \subseteq \Delta$.

For every $\Gamma \in \mathbf{MCS}$, let $\sim^c(\Gamma) = \{\Delta \in \mathbf{MCS} \mid \Gamma \sim^c \Delta\}$ and $R^c(\Gamma) = \{\Delta \in \mathbf{MCS} \mid \Gamma R^c \Delta\}$.

**Lemma 2.18.** $R^c$ is reflexive.

*Proof.* Immediately from Proposition 2.16(3). □

The next two lemmas can be shown in the standard way (see Blackburn et al., 2001).

**Lemma 2.19.** $\sim^c$ is an equivalence relation.
**Lemma 2.20.** For any $w \in MCS$ and formula $\varphi$, if $K\varphi \notin w$, there must be $u \in MCS$ such that $w \sim^c u$ and $\varphi \notin u$.

In what follows, we fix a maximal consistent set $\Gamma$ and let $\|\varphi\|_{\Gamma} = \{v \in \sim^c(\Gamma) | \varphi \in v\}$ for any formula $\varphi$.

**Definition 2.21 (Canonical model).** The canonical model for $\Gamma$ is a structure $M(\Gamma) = (W, N, V)$ such that:

- $W = (\sim^c(\Gamma) \times \{1,2\})$ (below we denote each $(w, i) \in W$ by $w^i$);

- for each $w^i \in W$, $N(w^i) = N^{\mathbb{P}^+}(w^i) \cup N^{\mathbb{P}^-}(w^i) \cup N^{\mathbb{O}^-}(w^i)$ where:

$$- N^{\mathbb{P}^+}(w^i) = \{\|\varphi\|_{\Gamma} \times \{1,2\} | \mathbb{P}^+\varphi \in w\},$$

$$- N^{\mathbb{P}^-}(w^i) = \{(\|\varphi\|_{\Gamma} \cap R^c(w)) \times \{i\} | \mathbb{P}^-\varphi \in w\},$$

$$- N^{\mathbb{O}^-}(w^i) = \{(\sim^c(\Gamma) \cap R^c(w)) \times \{i\} | \mathbb{P}^-\top \in w\};$$

- $V(p) = \|p\|_{\Gamma} \times \{1,2\}$ for all $p \in \text{PROP}$.

**Proposition 2.22.** $M(\Gamma)$ is a model.

*Proof.* It is obvious that $W$ is non-empty as $\Gamma \in W$ by Lemma 2.19 and $V$ matches the form of valuation. Thus it suffices to show that for all $w^i \in W$ and $U \in N(w^i)$, $w^i \in U$. We consider the following cases:

(1) $U \in N^{\mathbb{P}^+}(w^i)$. Then there is $\mathbb{P}^+\varphi \in w$ such that $U = \|\varphi\|_{\Gamma} \times \{1,2\}$. Note that $\vdash \mathbb{P}^+\varphi \rightarrow \varphi$ by the axioms (A1) and (A2). Therefore $\varphi \in w$ and thus $w \in \|\varphi\|_{\Gamma}$. Hence $w^i \in U$.

(2) $U \in N^{\mathbb{P}^-}(w^i)$. There is $\mathbb{P}^-\varphi \in w$ such that $U = (\|\varphi\|_{\Gamma} \cap R^c(w)) \times \{i\}$. We need to show $w \in [\|\varphi\|_{\Gamma} \cap R^c(w)]$. Since $R^c$ is reflexive by Lemma 2.18, it suffices to show that $w \in [\|\varphi\|_{\Gamma}]$. Note that $\varphi \in w$ by the axiom (A1). Thus $w \in \|\varphi\|_{\Gamma}$.

(3) $U \in N^{\mathbb{O}^-}(w^i)$. Since $w \in \sim^c(\Gamma)$. It suffices to show that $w \in R^c(w)$. This follows immediately from Lemma 2.18. $\square$

**Lemma 2.23.** For all $w \in \sim^c(\Gamma)$ and formulas $\varphi$, $K\varphi \in w$ iff for all $v \in \sim^c(\Gamma)$, $\varphi \in v$.

*Proof.* From left to right. It suffices to show that $w \sim^c v$ for all $v \in \sim^c(\Gamma)$. Note that $\Gamma \sim^c w$, $\Gamma \sim^c v$, and $\sim^c$ is Euclidean by Lemma 2.19. Therefore $w \sim^c v$. From right to left. Suppose $K\varphi \notin w$, by Lemma 2.20 there is $v \in MCS$ such that $w \sim^c v$ and $\varphi \notin v$. Since $\sim^c$ is transitive by Lemma 2.19, $v \in \sim^c(\Gamma)$. $\square$

**Lemma 2.24.** For all $w \in \sim^c(\Gamma)$ and formulas $\varphi$, if $\mathbb{O}^-\varphi \notin w$ then $\exists v \in \sim^c(\Gamma) \cap R^c(w)$ : $\varphi \notin v$.

*Proof.* Suppose $\mathbb{O}^-\varphi \notin w$. Since $\sim^c$ is an equivalence relation (by Lemma 2.19) and $w \in \sim^c(\Gamma)$, $\sim^c(w) = \sim^c(\Gamma)$. Thus it suffices to show that $\exists v \in \sim^c(w) \cap R^c(w) : \varphi \notin v$. Consider the set $\Delta = \{\psi | K\psi \in w\} \cup \{\psi | \mathbb{O}^-\psi \in w\} \cup \{\neg\varphi\}$. We first show that $\Delta$ is consistent. Suppose not, then there must be $K\psi_1, \dots, K\psi_i, \mathbb{O}^-\psi_{i+1}, \dots, \mathbb{O}^-\psi_n \in w$ ($0 \le i \le n$) such that

$$\vdash \psi_1 \wedge \dots \wedge \psi_i \wedge \psi_{i+1} \wedge \dots \wedge \psi_n \rightarrow \varphi.$$
Since $\mathcal{O}^-$ is a normal modality, we have

$$ \vdash \mathcal{O}^{-}\psi_1 \wedge \dots \wedge \mathcal{O}^{-}\psi_i \wedge \mathcal{O}^{-}\psi_{i+1} \wedge \dots \wedge \mathcal{O}^{-}\psi_n \rightarrow \mathcal{O}^{-}\varphi. $$

For every $1 \le j \le i$, since $K\psi_j \in w$, by the axiom (A3) it follows that $\mathcal{O}^{-}\psi_j \in w$. Therefore $\mathcal{O}^{-}\varphi \in w$, contradicting our assumption at the beginning. Hence $\Delta$ is consistent. By the Lindenbaum lemma, there is $v \in \mathcal{MCS}$ with $\Delta \subseteq v$. Note that $v \in \sim^c(w) \cap R^c(w)$ by the definition of $\sim^c$ and $R^c$. $\square$

**Lemma 2.25.** For all $w^i \in W$ and $\varphi \in \mathcal{L}_{LPOA}$, if $\|\varphi\|_{\Gamma} \times \{1,2\} \in N(w^i)$ then $\mathbb{P}^{+}\varphi \in w$.

*Proof.* Suppose $\|\varphi\|_{\Gamma} \times \{1,2\} \in N(w^i)$. We first show that $\|\varphi\|_{\Gamma} \times \{1,2\} \in N^{\mathbb{P}^+}(w^i)$. Suppose, towards a contradiction, that $\|\varphi\|_{\Gamma} \times \{1,2\} \notin N^{\mathbb{P}^+}(w^i)$. Then we consider the following cases:

(1) $\|\varphi\|_{\Gamma} \times \{1,2\} \in N^{\mathbb{P}^{-}}(w^i)$. Then there is $\mathbb{P}^{-}\psi \in w$ such that $\|\varphi\|_{\Gamma} \times \{1,2\} = (\|\psi\|_{\Gamma} \cap R^c(w)) \times \{i\}$. Note that, since $\|\varphi\|_{\Gamma} \times \{1,2\} \in N(w^i)$ and $M(\Gamma)$ is a model by Proposition 2.22, $w^i \in \|\varphi\|_{\Gamma} \times \{1,2\}$. Let $j \in \{1,2\}$ be such that $j \neq i$. Then $w^j \in \|\varphi\|_{\Gamma} \times \{1,2\}$. However $w^j \notin (\|\psi\|_{\Gamma} \cap R^c(w)) \times \{i\}$. Contradiction!

(2) $\|\varphi\|_{\Gamma} \times \{1,2\} \in N^{\mathcal{O}^{-}}(w^i)$. Then $\|\varphi\|_{\Gamma} \times \{1,2\} = (\sim^c(\Gamma) \cap R^c(w)) \times \{i\}$. Note that, since $\|\varphi\|_{\Gamma} \times \{1,2\} \in N(w^i)$ and $M(\Gamma)$ is a model by Proposition 2.22, $w^i \in \|\varphi\|_{\Gamma} \times \{1,2\}$. Let $j \in \{1,2\}$ be such that $j \neq i$. Then $w^j \in \|\varphi\|_{\Gamma} \times \{1,2\}$. However $w^j \notin (\sim^c(\Gamma) \cap R^c(w)) \times \{i\}$. Contradiction!

We then show that $\mathbb{P}^{+}\varphi \in w$. Since $\|\varphi\|_{\Gamma} \times \{1,2\} \in N^{\mathbb{P}^{+}}(w^i)$, there must be $\mathbb{P}^{+}\psi \in w$ such that $\|\varphi\|_{\Gamma} \times \{1,2\} = \|\psi\|_{\Gamma} \times \{1,2\}$. It follows that $\varphi \leftrightarrow \psi \in v$ for all $v \in \sim^c(\Gamma)$. Therefore, by Lemma 2.23, $K(\varphi \leftrightarrow \psi) \in w$. Since $\mathbb{P}^{+}\psi \in w$, by the axiom (A5) it follows that $\mathbb{P}^{+}\varphi \in w$. $\square$

**Lemma 2.26.** For all $w^i \in W$ and $\varphi \in \mathcal{L}_{LPOA}$, if $\exists Y \in N(w^i) : Y \subseteq \|\varphi\|_{\Gamma} \times \{1,2\}$ then $\mathbb{P}^{-}\varphi \in w$.

*Proof.* We consider the following cases:

(1) $Y \in N^{\mathcal{O}^{-}}(w^i)$. Then $\mathbb{P}^{-}\top \in w$ and $Y = (\sim^c(\Gamma) \cap R^c(w)) \times \{i\}$. Therefore, $\sim^c(\Gamma) \cap R^c(w) \subseteq \|\varphi\|_{\Gamma}$. Hence $\mathcal{O}^{-}\varphi \in w$ by Lemma 2.24. Note that, since $\mathbb{P}^{-}\top \in w$ and $\vdash \mathbb{P}^{-}\top \rightarrow (\mathcal{O}^{-}\varphi \rightarrow \mathbb{P}^{-}\varphi)$ (Proposition 2.16(2)), $\mathcal{O}^{-}\varphi \rightarrow \mathbb{P}^{-}\varphi \in w$. Therefore, $\mathbb{P}^{-}\varphi \in w$.

(2) $Y \in N^{\mathbb{P}^{+}}(w^i)$. Then there is $\mathbb{P}^{+}\psi \in w$ such that $Y = \|\psi\|_{\Gamma} \times \{1,2\}$. Therefore, $\|\psi\|_{\Gamma} \subseteq \|\varphi\|_{\Gamma}$. It follows that $\psi \rightarrow \varphi \in v$ for all $v \in \sim^c(\Gamma) \cap R^c(w)$. Hence $\mathcal{O}^{-}(\psi \rightarrow \varphi) \in w$ by Lemma 2.24. Note that $\mathbb{P}^{-}\psi \in w$ by the axiom (A2). Thus, $\mathbb{P}^{-}\varphi \in w$ by the axiom (A7).

(3) $Y \in N^{\mathbb{P}^{-}}(w^i)$. Then there is $\mathbb{P}^{-}\psi \in w$ such that $Y = (\|\psi\|_{\Gamma} \cap R^c(w)) \times \{i\}$. Hence $\|\psi\|_{\Gamma} \cap R^c(w) \subseteq \|\varphi\|_{\Gamma}$. Therefore, $\sim^c(\Gamma) \cap R^c(w) \subseteq \|\psi \rightarrow \varphi\|_{\Gamma}$. Hence $\mathcal{O}^{-}(\psi \rightarrow \varphi) \in w$ by Lemma 2.24. Then it follows that $\mathbb{P}^{-}\varphi \in w$ by the axiom (A7). $\square$

**Lemma 2.27.** For all $w^i \in W$ and $\varphi \in \mathcal{L}_{LPOA}$, if $\mathcal{O}^{-}\varphi \notin w$ and $\varphi \in w$ then $\exists Y \in N(w^i) : Y \not\subseteq \|\varphi\|_{\Gamma} \times \{1,2\}$.

*Proof.* Suppose $\mathcal{O}^{-}\varphi \notin w$ and $\varphi \in w$. Then $\mathbb{P}^{-}\top \in w$ by the axiom (A4). By the definition of $N^{\mathcal{O}^{-}}(w^i)$, $(\sim^c(\Gamma) \cap R^c(w)) \times \{i\} \in N^{\mathcal{O}^{-}}(w^i)$. Note that $\sim^c(\Gamma) \cap R^c(w) \not\subseteq [[\varphi]]_{\Gamma}$ by Lemma 2.24. Thus, we can let $Y = (\sim^c(\Gamma) \cap R^c(w)) \times \{i\}$. $\square$
**Lemma 2.28.** For all $w^i \in W$ and $\varphi \in \mathcal{L}_{LPOA}$, if $\mathcal{O}^-\varphi \in w$ then $\forall Y \in N(w^i) : Y \subseteq \|\varphi\|_{\Gamma} \times \{1, 2\}$.

*Proof.* Suppose $\mathcal{O}^-\varphi \in w$. We consider the following cases:

(1) $Y \in N^{\mathbb{P}^+}(w^i)$. Then there is $\mathbb{P}^+\psi \in w$ such that $Y = \|\psi\|_{\Gamma} \times \{1, 2\}$. Since $\mathcal{O}^-\varphi \in w$ and $\mathbb{P}^+\psi \in w$, $K(\psi \to \varphi) \in w$ by axiom (A8). Hence $\|\psi\|_{\Gamma} \subseteq \|\varphi\|_{\Gamma}$ by Lemma 2.23. Therefore, $Y \subseteq \|\varphi\|_{\Gamma} \times \{1, 2\}$.

(2) $Y \in N^{\mathbb{P}^-}(w^i) \cup N^{\mathcal{O}^-}(w^i)$. Note that $R^c(w) \subseteq \|\varphi\|_{\Gamma}$ since $\mathcal{O}^-\varphi \in w$. Therefore, $Y \subseteq \|\varphi\|_{\Gamma} \times \{1, 2\}$. $\square$

**Lemma 2.29 (Truth).** For all $w^i \in W$ and $\varphi \in \mathcal{L}_{LPOA}$,

$$M(\Gamma), w^i, W \models \varphi \text{ iff } \varphi \in w.$$

*Proof.* Induction on the structure of $\varphi$. The base and the inductive steps for Boolean connectives are trivial.

**Case** $K\varphi$. We have:

$$M(\Gamma), w^i, W \models K\varphi$$

$$\text{iff} \quad \forall v^j \in W : M(\Gamma), v^j, W \models \varphi \quad (\text{semantics})$$

$$\text{iff} \quad \forall v \in \sim^c(\Gamma) : \varphi \in v \quad (\text{IH})$$

$$\text{iff} \quad K\varphi \in w \quad (\text{Lemma 2.23})$$

**Case** $\mathbb{P}^+\varphi$. We have:

$$M(\Gamma), w^i, W \models \mathbb{P}^+\varphi$$

$$\text{iff} \quad [[\varphi]]_{M(\Gamma),W} \in N(w^i) \quad (\text{semantics})$$

$$\text{iff} \quad \|\varphi\|_{\Gamma} \times \{1, 2\} \in N(w^i) \quad (\text{IH})$$

$$\text{iff} \quad \mathbb{P}^+\varphi \in w \quad (\text{up by definition of } N, \text{ down by Lemma 2.25})$$

**Case** $\mathbb{P}^-\varphi$. We have:

$$M(\Gamma), w^i, W \models \mathbb{P}^-\varphi$$

$$\text{iff} \quad \exists Y \in N(w^i) : Y \subseteq [[\varphi]]_{M(\Gamma),W} \quad (\text{semantics})$$

$$\text{iff} \quad \exists Y \in N(w^i) : Y \subseteq \|\varphi\|_{\Gamma} \times \{1, 2\} \quad (\text{IH})$$

$$\text{iff} \quad \mathbb{P}^-\varphi \in w \quad (\text{up by definition of } N, \text{ down by Lemma 2.26})$$

**Case** $\mathcal{O}^-\varphi$. We have:

$$M(\Gamma), w^i, W \models \mathcal{O}^-\varphi$$

$$\text{iff} \quad M(\Gamma), w^i, W \models \varphi \text{ and } \forall Y \in N(w^i) : Y \subseteq [[\varphi]]_{M(\Gamma),W} \quad (\text{semantics})$$

$$\text{iff} \quad \varphi \in w \text{ and } \forall Y \in N(w^i) : Y \subseteq \|\varphi\|_{\Gamma} \times \{1, 2\} \quad (\text{IH})$$

$$\text{iff} \quad \mathcal{O}^-\varphi \in w \quad (\text{up by Lemmas 2.16(3) and 2.28, down by Lemma 2.27}) \quad \square$$

Given the truth lemma, a standard argument leads to the completeness of **LPOA**.

**Theorem 1 (Soundness and completeness).** For any set of formulas $\Gamma \cup \{\varphi\} \subseteq \mathcal{L}_{LPOA}$, $\Gamma \models \varphi \text{ iff } \Gamma \vdash \varphi$.
### 3. The Dynamic Extension

In this section, we investigate how to incorporate public announcements in LPOA. As we have seen in Examples 1.1 and 2.3, the previous information announced by the sender has a critical impact on what is permitted (or obliged) to be announced next. However, the static logic LPOA is only able to characterize the obligatory and permitted information with respect to a given epistemic state of the receiver. There is no mechanism of informational dynamics for the receiver. Extending LPOA with the public announcement operator $[\varphi]\psi$, we are able to express, e.g., “after the announcement of $p$, it becomes obligatory for the sender to announce $c$” ($[p] \mathbb{O}^{-} c$).

#### 3.1 Language and Semantics

**Definition 3.1 (Dynamic language).** The language $\mathcal{L}_{DLPOA}$ is defined by adding the inductive construct $[\varphi]\varphi$ to Definition 2.1. We define $\langle\varphi\rangle\psi$ as an abbreviation for $\neg[\varphi]\neg\psi$.

For all formulas $\varphi \in \mathcal{L}_{DLPOA}$, let $sub(\varphi)$ be the set of subformulas of $\varphi$. For any set of formulas $\Gamma \subseteq \mathcal{L}_{DLPOA}$, we use $PROP(\Gamma)$ to denote the set of propositional variables occurring in at least one formula in $\Gamma$. Given some $A \subseteq PROP$, $\mathcal{L}_{DLPOA}(A)$ is the logical language $\mathcal{L}_{DLPOA}$ restricted to propositional variables in $A$. Next, we define the notion of the complexity of formulas and show some properties. This will be used in the completeness proof.

**Definition 3.2 (Complexity).** For every formula $\alpha \in \mathcal{L}_{DLPOA}$, the complexity of $\alpha$, with the notation $c(\alpha)$, is a positive integer inductively defined as follows:

$$ 
\begin{aligned}
c(p) &= 1 \\
c(\neg\varphi) &= c(K\varphi) = 1 + c(\varphi) \\
c((\varphi \rightarrow \psi)) &= 1 + \max(c(\varphi), c(\psi)) \\
c(\mathbb{P}^{+}\varphi) &= 2 + c(\varphi) \\
c(\mathbb{O}^{-}\varphi) &= c(\mathbb{P}^{-}\varphi) = 5 + c(\varphi) \\
c([\varphi]\psi) &= (5 + c(\varphi)) \cdot c(\psi)
\end{aligned}
$$

**Proposition 3.3.** The following hold for all $\varphi, \psi, \chi \in \mathcal{L}_{DLPOA}$:

(1) $c(\psi) > c(\varphi)$ if $\varphi \in sub(\psi) \setminus \{\psi\}$.

(2) $c(\mathbb{O}^{-}\varphi) > c(\mathbb{P}^{+}p \rightarrow K(p \rightarrow \varphi))$.

(3) $c(\mathbb{P}^{-}\varphi) > c(\mathbb{P}^{+}p \rightarrow \neg K(p \rightarrow \varphi))$.

(4) $c([\varphi]p) > c(\varphi \rightarrow p)$.

(5) $c([\varphi]\neg\psi) > c(\varphi \rightarrow \neg[\varphi]\psi)$.

(6) $c([\varphi](\psi \rightarrow \chi)) > c([\varphi]\psi \rightarrow [\varphi]\chi)$.

(7) $c([\varphi]K\psi) > c(\varphi \rightarrow K[\varphi]\psi)$.

(8) $c([\varphi][\psi]\chi) > c([\langle\varphi\rangle\psi]\chi)$.

(9) $c([\varphi]\mathbb{P}^{+}\psi) > c(\varphi \rightarrow \mathbb{P}^{+}\langle\varphi\rangle\psi)$.
(10) $c([\varphi]\mathbb{P}^{-}\psi) > c(\varphi \to \mathbb{P}^{-}\langle\varphi\rangle\psi)$.

(11) $c([\varphi]\mathbb{O}^{-}\psi) > c([\varphi]\psi)$.

(12) $c([\varphi]\mathbb{O}^{-}\psi) > c([\varphi](\mathbb{P}^{+}p \to K(p \to \psi)))$.

*Proof.* It can be shown by a direct calculus of the complexity of the formulas on both sides. □

**Definition 3.4 (Dynamic semantics).** Given a model $M = (W, N, V)$, for all formulas $\varphi \in \mathcal{L}_{DLPOA}$ and $w \in X \subseteq W$, the satisfaction relation $M, w, X \models \varphi$ is defined by extending Definition 2.6 with the following clause:

$$M, w, X \models [\varphi]\psi \text{ iff } M, w, X \models \varphi \text{ implies } M, w, [[\varphi]]_{M,X} \models \psi$$

The notion of validity is defined as before. We illustrate the dynamic semantics by the plane ticket example:

**Example 3.5 (Plane ticket example continued).** In the model $M$ depicted in Figure 1, we have $M, npem, W \models [e]\mathbb{O}^{+}n$, i.e., $M, npem, W \models [e](\mathbb{O}^{-}n \wedge \mathbb{P}^{+}n)$. It means that, after the announcement of $e$, it is both sufficient and necessary for Alice to announce $n$ (to be compliant with the Airline's policy).

It is easy to see that all the axioms and rules in **LPOA** are still valid (or preserve validity). In addition, we have reduction axioms for formulas of the forms $[\varphi]\mathbb{P}^{-}\psi$ and $[\varphi]\mathbb{P}^{+}\psi$, as shown in Proposition 3.7. To show this proposition, we need the next Lemma.

**Lemma 3.6.** Let $M = (W, N, V)$ be a model and $X \subseteq W$. For all formulas $\varphi$ and $\psi$, $[[\langle\varphi\rangle\psi]]_{X} = [[\psi]]_{[[\varphi]]_{X}}$.

*Proof.* For every $w \in W$, we have

$$ \begin{array}{l@{\qquad}l@{\qquad}l} w \in [[\langle\varphi\rangle\psi]]_{X} & & \\ \text{iff } w \in X \text{ and } M, w, X \models \langle\varphi\rangle\psi & \text{(def. of $[\cdot]$)} & \\ \text{iff } w \in X, M, w, X \models \varphi, \text{ and } M, w, [[\varphi]]_{X} \models \psi & \text{(semantics)} & \\ \text{iff } w \in [[\varphi]]_{X} \text{ and } M, w, [[\varphi]]_{X} \models \psi & \text{(def. of $[\cdot]$)} & \\ \text{iff } w \in [[\psi]]_{[[\varphi]]_{X}} & \text{(def. of $[\cdot]$)} & \square \end{array} $$

**Proposition 3.7.** The following hold for all formulas $\varphi, \psi \in \mathcal{L}_{DLPOA}$:

(1) $\models [\varphi]\mathbb{P}^{-}\psi \leftrightarrow (\varphi \to \mathbb{P}^{-}\langle\varphi\rangle\psi)$.

(2) $\models [\varphi]\mathbb{P}^{+}\psi \leftrightarrow (\varphi \to \mathbb{P}^{+}\langle\varphi\rangle\psi)$.

*Proof.* Immediately from Lemma 3.6 and the semantics. □

However, for formulas of the form $[\varphi]\mathbb{O}^{-}\psi$, the similar reduction axiom is invalid:

**Proposition 3.8.** $\models [\varphi]\mathbb{O}^{-}\psi \leftrightarrow (\varphi \to \mathbb{O}^{-}\langle\varphi\rangle\psi)$ for some formulas $\varphi, \psi \in \mathcal{L}_{DLPOA}$.

*Proof.* It is not hard to see that the direction $\leftarrow$ is valid. But the converse is not, as witnessed by the counter-model $M = (W, N, V)$ where $W = \{w, v\}$, $N(w) = N(v) = \{\{w, v\}\}$, and $V(p) = \{w\}$. It can be seen that $M, w, W \not\models [p]\mathbb{O}^{-}p \to (p \to \mathbb{O}^{-}\langle p \rangle p)$. □
## 3.2 Expressivity

Given the invalidity of the axiom schema in Proposition 3.8, it is still unclear whether there exist other forms of reduction axiom for the formula $[\varphi]\mathcal{O}^{-}\psi$. To answer the question, we need to study the expressive power of $\mathcal{L}_{DLPOA}$ and $\mathcal{L}_{LPOA}$. The next result implies that no reduction axiom exists for the formula $[\varphi]\mathcal{O}^{-}\psi$.

**Theorem 2 (Expressivity).** $\mathcal{L}_{DLPOA}$ is strictly more expressive than $\mathcal{L}_{LPOA}$.

*Proof.* It is clear that $\mathcal{L}_{DLPOA}$ is at least as expressive as $\mathcal{L}_{LPOA}$, since the latter is a sublanguage of the former and they are interpreted over the same class of models. We show that $\mathcal{L}_{LPOA}$ is not as least as expressive as $\mathcal{L}_{DLPOA}$. Consider the formula $[p]\mathcal{O}^{-}q \in \mathcal{L}_{DLPOA}$. We show that there is no $\varphi \in \mathcal{L}_{LPOA}$ such that $\varphi$ is equivalent to $[p]\mathcal{O}^{-}q$.<fnref n="10" /> Let $M = (W, N, V)$ and $M' = (W, N', V)$ be two models where:

- $W = \{-3, -2, -1, 1, 2, 3\}$;

- $N(1) = \{\{1\}, \{1, 2, 3\}\}, N(2) = N(3) = \emptyset, N(-1) = \{-1\}, \{-1, -2, -3\}, N(-2) = N(-3) = \emptyset$;

- $N'(1) = \{\{1\}, \{1, 2\}, \{1, 3\}\}, N'(2) = N'(3) = \emptyset, N'(-1) = \{-1\}, \{-1, -2\}, \{-1, -3\}, N'(-2) = N'(-3) = \emptyset$;

- $V(p) = \{1, 2, -1, -2\}, V(q) = \{1, -1\}$.

It is not hard to see that $M, 1, W \models [p]\mathcal{O}^{-}q$ and $M', 1, W \not\models [p]\mathcal{O}^{-}q$. Next, we show that for all $\varphi \in \mathcal{L}_{LPOA}$ and $x \in W$, $M, x, W \models \varphi$ iff $M', x, W \models \varphi$. To do this, we need the following claim:

*Claim.* For all $w \in W$ and $Y \in N(w)$ ($Y \in N'(w)$, respectively), $Y \neq [[\varphi]]_{M,W}$ ($Y \neq [[\varphi]]_{M',W}$, respectively) for all $\varphi \in \mathcal{L}_{LPOA}$.

*Proof of Claim.* If $w \notin \{1, -1\}$, then the claim holds trivially. Suppose $w \in \{-1, 1\}$ and $Y \in N(w)$. Let $\varphi \in \mathcal{L}_{LPOA}$ be an arbitrary formula. Note that $M, x, W \models \varphi$ iff $M, -x, W \models \varphi$ for all $x \in W$ (since, as the reader can verify, the function $f(x) = -x$ on $W$ is a bounded morphism from $W$ to itself). In particular, $M, 1, W \models \varphi$ iff $M, -1, W \models \varphi$. However, for all choices of $Y$, if $1 \in Y$ then $-1 \notin Y$ and vice versa. Hence, $Y \neq [[\varphi]]_{M,W}$.

The case for $Y \in N'(w)$ can be shown similarly. $\square$

We then show, by induction on the structure of $\varphi$, that $M, x, W \models \varphi$ iff $M', x, W \models \varphi$ for all $\varphi \in \mathcal{L}_{LPOA}$ and $x \in W$ ($\ast$). The base and the cases for Boolean connectives and $K\psi$ are all trivial.

**Case $\mathcal{O}^{-}\psi$:** Note that $\bigcup N(x) = \bigcup N'(x)$. Thus

$$M, x, W \models \mathcal{O}^{-}\psi$$

iff $M, x, W \models \psi$ and $\forall Y \in N(x), Y \subseteq [[\psi]]_{M,W}$ (semantics)

iff $M', x, W \models \psi$ and $\forall Y \in N'(x), Y \subseteq [[\psi]]_{M',W}$ ($\bigcup N(x) = \bigcup N'(x)$, IH)

iff $M', x, W \models \mathcal{O}^{-}\psi$ (semantics)

<footnote n="10">10. Intuitively, this may be understood as follows: if the current epistemic state is the whole domain, the satisfaction of $[p]\mathcal{O}^{-}q$ at world $w$ just says that all subsets in $N(w)$ that are contained in the truth set of $p$, are also contained in the truth set of $q$. However, in the static language $\mathcal{L}_{LPOA}$, no formula can single out subsets in $N(w)$ that consist exclusively of $p$-worlds.</footnote>
**Case P⁻ψ:** If $x \notin \{1, -1\}$, (*) holds trivially because $M, x, W \not\models P⁻ψ$ and $M', x, W \not\models P⁻ψ$. Suppose $x = 1$. Note that for any $Y' \in N'(1)$ there is $Y \in N(1)$ such that $Y \subseteq Y'$ and vice versa. Thus,

$$M, 1, W \models P^{-} \psi$$

$$\text{iff} \quad \exists Y \in N(1), Y \subseteq [\psi]_{M,W} \quad \text{(semantics)}$$

$$\text{iff} \quad \exists Y' \in N'(1), Y' \subseteq [\psi]_{M',W} \quad \text{(IH)}$$

$$\text{iff} \quad M', 1, W \models P^{-} \psi \quad \text{(semantics)}$$

The case where $x = -1$ can be shown in the same way.

**Case P⁺ψ:** Note that, by the claim above, $M, x, W \not\models P⁺ψ$ and $M', x, W \not\models P⁺ψ$. □

Nevertheless, we can show that $\mathcal{L}_{DLPOA}$ is still invariant under bounded morphisms.

**Lemma 3.9.** Suppose that $M_1 = (W_1, N_1, V_1)$ and $M_2 = (W_2, N_2, V_2)$ are two models, $X_1 \subseteq W_1$, and $X_2 \subseteq W_2$. Let $f: X_1 \to X_2$ be a bounded morphism from $X_1$ to $X_2$. Let $\psi$ be a formula such that, for all $w \in X_1$, $M_1, w, X_1 \models \psi$ iff $M_2, f(w), X_2 \models \psi$. Then the restriction of $f$ to $[\psi]_{M_1, X_1}$, $f|_{[\psi]_{M_1, X_1}}$, is a bounded morphism between $[\psi]_{M_1, X_1}$ and $[\psi]_{M_2, X_2}$.

*Proof.* It is not hard to see that $f|_{[\psi]_{M_1, X_1}}$ is a surjective function from $[\psi]_{M_1, X_1}$ to $[\psi]_{M_2, X_2}$. $f|_{[\psi]_{M_1, X_1}}$ also satisfies the condition (M2) as $f$ satisfies (M2). For the condition (M3), let $Y \subseteq [\psi]_{M_2, X_2}$ and $w \in [\psi]_{M_1, X_1}$. We have $(f|_{[\psi]_{M_1, X_1}})^{-1}(Y) = f^{-1}(Y)$ and $f|_{[\psi]_{M_1, X_1}}(w) = f(w)$. If $Y \in N_2(f|_{[\psi]_{M_1, X_1}}(w))$, then $Y \in N_2(f(w))$. Thus, $f^{-1}(Y) \in N_1(w)$ since $f$ satisfies (M3). Therefore $(f|_{[\psi]_{M_1, X_1}})^{-1}(Y) \in N_1(w)$. For the condition (M4), let $Y \subseteq [\psi]_{M_1, X_1}$ and $w \in [\psi]_{M_1, X_1}$. We have $f|_{[\psi]_{M_1, X_1}}(Y) = f(Y)$ and $f(w) = f|_{[\psi]_{M_1, X_1}}(w)$. If $Y \in N_1(w)$, then $f(Y) \in N_2(f(w))$ since $f$ satisfies (M4). Thus $f|_{[\psi]_{M_1, X_1}}(Y) \in N_2(f|_{[\psi]_{M_1, X_1}}(w))$. □

**Proposition 3.10.** Suppose that $M_1 = (W_1, N_1, V_1)$ and $M_2 = (W_2, N_2, V_2)$ are two models, $X_1 \subseteq W_1$, and $X_2 \subseteq W_2$. Let $f: X_1 \to X_2$ be a bounded morphism from $X_1$ to $X_2$. Then, for all $\varphi \in \mathcal{L}_{DLPOA}$ and $w \in X_1$, $M_1, w, X_1 \models \varphi$ iff $M_2, f(w), X_2 \models \varphi$.

*Proof.* Induction on the structure of $\varphi$. We show only the case for $[\psi]\chi$ (the other cases are the same as in the proof of Proposition 2.11):

$$M_1, w, X_1 \models [\psi]\chi$$

$$\text{iff} \quad M_1, w, X_1 \models \psi \text{ implies } M_1, w, [\psi]_{M_1, X_1} \models \chi \quad \text{(semantics)}$$

$$\text{iff} \quad M_2, f(w), X_2 \models \psi \text{ implies } M_1, w, [\psi]_{M_1, X_1} \models \chi \quad \text{(IH)}$$

$$\text{iff} \quad M_2, f(w), X_2 \models \psi \text{ implies } M_2, f(w), [\psi]_{M_2, X_2} \models \chi \quad \text{(IH)}$$

$$\text{iff} \quad M_2, f(w), X_2 \models [\psi]\chi \quad \text{(semantics)}$$

Note that, since $M_1, w, X_1 \models \psi$ iff $M_2, f(w), X_2 \models \psi$ for all $w \in X_1$ by IH, $f|_{[\psi]_{M_1, X_1}}$ is a bounded morphism between $[\psi]_{M_1, X_1}$ and $[\psi]_{M_2, X_2}$ by Lemma 3.9. Thus, the third “iff” holds by applying IH again. □
### 3.3 Axiomatization

The result of the previous section shows that no reductive axiomatization (like that for dynamic epistemic logic) exists for DLPOA. To axiomatize DLPOA, we employ the notion of “necessity forms” which was originally proposed by Goldblatt (1982) and adapted to axiomatize arbitrary public announcement logic by Balbiani et al. (2008).

**Definition 3.11 (Necessity forms).** Let $\#\$ be a special symbol not occurring in $\mathcal{L}_{DLPOA}$. The set of necessity forms is inductively defined as follows:

$$ \xi(\#) ::= \# | (\varphi \rightarrow \xi(\#)) | K\xi(\#) | [\varphi]\xi(\#) $$

where $\varphi \in \mathcal{L}_{DLPOA}$. Given a necessity form $\xi(\#)$ and a formula $\varphi \in \mathcal{L}_{DLPOA}$, $\xi(\varphi)$ will denote the result of replacing the unique occurrence of $\#\$ in $\xi(\#)$ by $\varphi$.

**Definition 3.12 (Axiomatization).** The axiomatization DLPOA for $\mathcal{L}_{DLPOA}$ is provided in Figure 3. Let the set of DLPOA-theorems be the least set of formulas in $\mathcal{L}_{DLPOA}$ that contains all instances of the axiom schemas and is closed under the inference rules in Figure 3. If $\varphi$ is a DLPOA-theorem, we write $\vdash_{DLPOA} \varphi$.

**Axioms:**

<table><tr><td>(PL)</td><td>All propositional tautologies</td><td>(!Atom)</td><td>[φ]p ↔ (φ → p)</td></tr><tr><td>(S5)</td><td>S5 axioms for K</td><td>(!Neg)</td><td>[φ]¬ψ ↔ (φ → ¬[φ]ψ)</td></tr><tr><td>(A5)</td><td>K(φ ↔ ψ) → (P<sup>+</sup>φ ↔ P<sup>+</sup>ψ)</td><td>(!Imp)</td><td>[φ](ψ → χ) ↔ ([φ]ψ → [φ]χ)</td></tr><tr><td>(A8)</td><td>O<sup>-</sup>φ → (P<sup>+</sup>ψ → K(ψ → φ))</td><td>(!K)</td><td>[φ]Kψ ↔ (φ → K[φ]ψ)</td></tr><tr><td>(A9)</td><td>¬P<sup>-</sup>φ → (P<sup>+</sup>ψ → ¬K(ψ → φ))</td><td>(!P<sup>+</sup>)</td><td>[φ]P<sup>+</sup>ψ ↔ (φ → P<sup>+</sup>⟨φ⟩ψ)</td></tr><tr><td>(A10)</td><td>P<sup>+</sup>φ → φ</td><td>(!P<sup>-</sup>)</td><td>[φ]P<sup>-</sup>ψ ↔ (φ → P<sup>-</sup>⟨φ⟩ψ)</td></tr><tr><td>(A11)</td><td>O<sup>-</sup>φ → φ</td><td>(!Comp)</td><td>[φ][ψ]χ ↔ [⟨φ⟩ψ]χ</td></tr></table>

**Rules:**

<table><caption>Figure 3: The axiomatization DLPOA.</caption><tr><td>(MP)</td><td>from φ and φ → ψ, infer ψ</td></tr><tr><td>(Nec<sub>K</sub>)</td><td>from φ, infer Kφ</td></tr><tr><td>(Nec<sub>↓</sub>)</td><td>from φ, infer [ψ]φ</td></tr><tr><td>(R<sub>O<sup>-</sup></sub>)</td><td>from ξ(P<sup>+</sup>p → K(p → φ)), infer ξ(φ → O<sup>-</sup>φ), where p ∉ PROP(ξ(φ))</td></tr><tr><td>(R<sub>P<sup>-</sup></sub>)</td><td>from ξ(P<sup>+</sup>p → ¬K(p → φ)), infer ξ(¬P<sup>-</sup>φ), where p ∉ PROP(ξ(φ))</td></tr><tr><td>(R<sub>P<sup>+</sup></sub>)</td><td>from ξ(P<sup>+</sup>p → ¬K(p ↔ φ)), infer ξ(¬P<sup>+</sup>φ), where p ∉ PROP(ξ(φ))</td></tr></table>

*Remark 4.* The use of the necessity forms in the axiomatization is not indispensable. As showed by Balbiani et al. (2008, Lemma 4.8), every necessity form $\xi(\#)$ can be transformed into an equivalent one of the form $\psi \rightarrow [\chi]_{\#}$, in the sense that $\vdash \xi(\theta)$ iff $\vdash \psi \rightarrow [\chi]_{\theta}$ for all formulas $\theta$. The result also holds for DLPOA. Thus the inference rules $(R_{O-})$, $(R_{P-})$, and $(R_{P+})$ can be replaced safely by the following ones:

$$(R'_{O-}) \text{ from } \psi \rightarrow [\chi](P^{+}p \rightarrow K(p \rightarrow \varphi)), \text{ infer } \psi \rightarrow [\chi](\varphi \rightarrow O^{-}\varphi)$$

$$(R'_{P-}) \text{ from } \psi \rightarrow [\chi](P^{+}p \rightarrow \neg K(p \rightarrow \varphi)), \text{ infer } \psi \rightarrow [\chi] \neg P^{-} \varphi$$
$(R'_{\mathbb{P}^+})$ from $\psi \to [\chi](\mathbb{P}^+p \to \neg K(p \leftrightarrow \varphi))$, infer $\psi \to [\chi]\neg\mathbb{P}^+\varphi$

where $p \notin \text{PROP}(\psi \to [\chi]\varphi)$. The resulting axiomatization is the same as **DLPOA**.

**Remark 5.** **DLPOA** is an extension to **LPOA**. As the reader can verify, all the axioms in Figure 2 can be derived in **DLPOA**. For example, below is a proof for (A3) in **DLPOA**:

1. $K\varphi \to K(p \to \varphi)$ (theorem of epistemic logic S5)

2. $K\varphi \to (\mathbb{P}^+p \to K(p \to \varphi))$ (propositional calculus)

3. $K\varphi \to (\varphi \to \mathbb{O}^{-}\varphi)$ (2, $(R_{\mathbb{O}^-})$)

4. $K\varphi \to \varphi$ ((T) axiom for K)

5. $K\varphi \to \mathbb{O}^{-}\varphi$ (3, 4, propositional calculus)

**3.4 Soundness**

In this subsection, we show the soundness of **DLPOA** with respect to the semantics. We need to show that all the axioms of **DLPOA** are valid and all the inference rules preserve validity. Note that the validity of (!$\mathbb{P}^+$) and (!$\mathbb{P}^-$) has been shown in Proposition 3.7. We only need to show that the axioms (A9) – (A11) are valid and the rules $(R_{\mathbb{O}^-})$ – $(R_{\mathbb{P}^+})$ preserve validity, as the other axioms or rules are inherited from **LPOA** or classical public announcement logic.

**Proposition 3.13.** *The following hold for all formulas $\varphi, \psi \in \mathcal{L}_{\text{DLPOA}}$:*

$$ (1) \quad \models \mathbb{P}^{+}\varphi \to \varphi. $$

$$ (2) \quad \models \mathbb{O}^{-}\varphi \to \varphi. $$

$$ (3) \quad \models \neg\mathbb{P}^{-}\varphi \to (\mathbb{P}^{+}\psi \to \neg K(\psi \to \varphi)). $$

*Proof.* We show only the last. Let $M = (W, N, V)$ be a model and $w \in X \subseteq W$. Suppose $M, w, X \models \neg\mathbb{P}^{-}\varphi$ and $M, w, X \models \mathbb{P}^{+}\psi$. Suppose, towards a contradiction, that $M, w, X \models K(\psi \to \varphi)$. Then $[[\psi]]_X \subseteq [[\varphi]]_X$. Note that, since we assume $M, w, X \models \mathbb{P}^{+}\psi$, $[[\psi]]_X \in N(w)$. It follows that $M, w, X \models \mathbb{P}^{-}\varphi$, contradiction! $\square$

**Remark 6.** All three formulas in the above proposition are actually theorems of **LPOA** (Definition 2.15). Note that (3) can be reformulated as $K(\psi \to \varphi) \to (\mathbb{P}^+\psi \to \mathbb{P}^-\varphi)$, which says that if $\varphi$ is less informative than $\psi$ (for the receiver), then the (strong) permission to announce $\psi$ implies the (weak) permission to announce $\varphi$.

Given two models $M, M'$ and an atom $p$, we say $M'$ is a $p$-variant of $M$ if $M' = M$ or they differ only in the valuation of $p$.

**Lemma 3.14.** Let $M = (W, N, V)$ be a model and $M' = (W, N, V')$ be a $p$-variant of $M$. Then for every formula $\psi \in \mathcal{L}_{\text{DLPOA}}(\text{PROP} \setminus \{p\})$, $X \subseteq W$, and $w \in X$, $M, w, X \models \psi$ iff $M', w, X \models \psi$.

*Proof.* An easy induction on the structure of $\psi$. $\square$

**Lemma 3.15.** For all necessity form $\xi(\#)$, formulas $\varphi \in \mathcal{L}_{\text{DLPOA}}$, and atoms $p \notin \xi(\varphi)$, the following holds:
(1) if $M, w, X \models \xi(\varphi \to \mathbb{O}^{-}\varphi)$, then there is a $p$-variant of $M, M'$, such that $M', w, X \models \xi(\mathbb{P}^{+}p \to K(p \to \varphi))$.

(2) if $M, w, X \models \xi(\neg\mathbb{P}^{-}\varphi)$, then there is a $p$-variant of $M, M'$, such that $M', w, X \models \xi(\mathbb{P}^{+}p \to \neg K(p \to \varphi))$.

(3) if $M, w, X \models \xi(\neg\mathbb{P}^{+}\varphi)$, then there is a $p$-variant of $M, M'$, such that $M', w, X \models \xi(\mathbb{P}^{+}p \to \neg K(p \leftrightarrow \varphi))$.

*Proof.* We show only (1), by induction on the structure of $\xi(\#)$. (2) and (3) can be shown similarly.

Base: Suppose $M, w, X \models \varphi \wedge \neg\mathbb{O}^{-}\varphi$. By the semantics, there is $Y \in N(w)$ with $Y \subseteq X$ and $Y \not\subseteq [[\varphi]]_{M,X}$. Let $M' = (W, N, V')$ be the $p$-variant of $M$ such that $V'(p) = Y$. It is clear that $M', w, X \models \mathbb{P}^{+}p$. To show that $M', w, X \not\models K(p \to \varphi)$, note that, by Lemma 3.14, $[[\varphi]]_{M',X} = [[\varphi]]_{M,X}$. Hence $M', w, X \not\models K(p \to \varphi)$ by the semantics. Therefore $M', w, X \not\models \mathbb{P}^{+}p \to K(p \to \varphi)$.

Case $\psi \to \xi'(\#)$: Suppose $M, w, X \not\models \psi \to \xi'(\varphi \to \mathbb{O}^{-}\varphi)$. By semantics, $M, w, X \models \psi$ and $M, w, X \not\models \xi'(\varphi \to \mathbb{O}^{-}\varphi)$. Note that $p \notin \text{PROP}(\xi'(\varphi))$. Applying the induction hypothesis, there is a $p$-variant of $M, M'$, such that $M', w, X \not\models \xi'(\mathbb{P}^{+}p \to K(p \to \varphi))$. By Lemma 3.14, $M', w, X \models \psi$. Hence $M', w, X \not\models \psi \to \xi'(\mathbb{P}^{+}p \to K(p \to \varphi))$.

Case $K\xi'(\#)$: Suppose $M, w, X \not\models K\xi'(\varphi \to \mathbb{O}^{-}\varphi)$. By semantics, there is $v \in X$ such that $M, v, X \not\models \xi'(\varphi \to \mathbb{O}^{-}\varphi)$. Note that $p \notin \text{PROP}(\xi'(\varphi))$. Applying the induction hypothesis, there is a $p$-variant of $M, M'$, such that $M', v, X \not\models \xi'(\mathbb{P}^{+}p \to K(p \to \varphi))$. Thus $M', w, X \not\models K\xi'(\mathbb{P}^{+}p \to K(p \to \varphi))$.

Case $[\psi]\xi'(\#)$: Suppose $M, w, X \not\models [\psi]\xi'(\varphi \to \mathbb{O}^{-}\varphi)$. By semantics, $M, w, X \models \psi$ and $M, w, [[\psi]]_{M,X} \not\models \xi'(\varphi \to \mathbb{O}^{-}\varphi)$. Note that $p \notin \text{PROP}(\xi'(\varphi))$. Applying the induction hypothesis, there is a $p$-variant of $M, M'$, such that $M', w, [[\psi]]_{M,X} \models \xi'(\mathbb{P}^{+}p \to K(p \to \varphi))$. Note that $M', w, X \models \psi$ and $[[\psi]]_{M,X} = [[\psi]]_{M',X}$ by Lemma 3.14. Thus $M', w, [[\psi]]_{M',X} \not\models \xi'(\mathbb{P}^{+}p \to K(p \to \varphi))$. We conclude that $M', w, X \not\models [\psi]\xi'(\mathbb{P}^{+}p \to K(p \to \varphi))$. $\square$

**Proposition 3.16.** *The inference rules (R<sub>Ø</sub><sup>-</sup> – (R<sub>p+</sub>) preserve validity.*

*Proof.* Immediately from Lemma 3.15. $\square$

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

Since all axioms and rules are valid (or preserve validity), the soundness of **DLPOA** follows from the standard argument of induction on the length of proofs.

**Theorem 3** (Soundness). *For all formulas $\varphi \in \mathcal{L}_{DLPOA}$, if $\vdash_{DLPOA} \varphi$ then $\models \varphi$.*

## 3.5 Completeness

In this section, we prove that the axiomatization **DLPOA** is (weakly) complete with respect to the semantics. This is achieved by making a detour. Let **DLPOA**<sup>ω</sup> be the axiomatization obtained by replacing the rules (R<sub>Ø</sub><sup>-</sup>), (R<sub>p-</sub><sup>-</sup>), and (R<sub>p+</sub><sup>-</sup>) in **DLPOA** with the following rules (R<sub>Ø</sub><sup>ω</sup><sub>-</sub>), (R<sub>p-</sub><sup>ω</sup><sub>-</sub>), and (R<sub>p+</sub><sup>ω</sup><sub>-</sub>):

(R<sub>Ø</sub><sup>ω</sup><sub>-</sub>) from $\xi(\mathbb{P}^{+}p \to K(p \to \varphi))$ for all $p \in \text{PROP}$, infer $\xi(\varphi \to \mathbb{O}^{-}\varphi)$

(R<sub>p-</sub><sup>ω</sup><sub>-</sub>) from $\xi(\mathbb{P}^{+}p \to \neg K(p \to \varphi))$ for all $p \in \text{PROP}$, infer $\xi(\neg\mathbb{P}^{-}\varphi)$
$(R_{\mathbb{P}+}^{\omega})$ from $\xi(\mathbb{P}^{+}p \to \neg K(p \leftrightarrow \varphi))$ for all $p \in \text{PROP}$, infer $\xi(\neg \mathbb{P}^{+}\varphi)$

It is clear that $(R_{\mathbb{O}-}^{\omega})$, $(R_{\mathbb{P}-}^{\omega})$, and $(R_{\mathbb{P}+}^{\omega})$ are admissible in **DLPOA**, i.e., the set of all **DLPOA**<sup>ω</sup>-theorems is a subset of the set of all **DLPOA**-theorems. Thus, the soundness of **DLPOA**<sup>ω</sup> follows from that of **DLPOA**. Conversely, the (weak-)completeness of **DLPOA** follows from that of **DLPOA**<sup>ω</sup>. In what follows, we will focus on the completeness of **DLPOA**<sup>ω</sup>.

The basic idea behind the completeness proof is to construct the canonical model using maximal consistent sets closed under the rules $(R_{\mathbb{O}-}^{\omega}) - (R_{\mathbb{P}+}^{\omega})$ (which we call “maximal consistent theories” in the next definition). In this way, we could “reduce” the truth of formulas like $\mathbb{O}^{-}\varphi$ to the truth of all formulas $\mathbb{P}^{+}p \to K(p \to \varphi)$ with $p \in \text{PROP}$ (note that the rules $(R_{\mathbb{O}-}^{\omega}) - (R_{\mathbb{P}+}^{\omega})$ can roughly be seen as the converse of the axioms (A8), (A9), and (A5), respectively). The function of necessity forms is, roughly speaking, to ensure that this reduction can also be done within the scope of the modal operators.

**Definition 3.17 (Theory).** A set $x$ of formulas in $\mathcal{L}_{\text{DLPOA}}$ is called a theory iff it satisfies the following conditions:

- $x$ contains all **DLPOA**<sup>ω</sup>-theorems;

- $x$ is closed under the inference rules (MP), $(R_{\mathbb{O}-}^{\omega})$, $(R_{\mathbb{P}-}^{\omega})$, and $(R_{\mathbb{P}+}^{\omega})$.

A theory $x$ is *consistent* iff $\perp \notin x$. A set $x$ of formulas is *maximal* iff for all formulas $\varphi$, $\varphi \in x$ or $\neg \varphi \in x$. We will denote the set of all maximal consistent theories by MCT.

**Lemma 3.18.** The following hold for all $x \in \text{MCT}$,

(1) $\neg \varphi \in x$ iff $\varphi \notin x$.

(2) $(\varphi \to \psi) \in x$ iff $\varphi \notin x$ or $\psi \in x$.

**Definition 3.19.** For all sets of formulas $x$ and formulas $\varphi$, let $x + \varphi = \{\psi \mid \varphi \to \psi \in x\}$ and $Kx = \{\psi \mid K\psi \in x\}$.

**Lemma 3.20.** Let $\varphi$ be a formula. For all theories $x$,

(1) $x + \varphi$ is a theory containing $x$ and $\varphi$.

(2) $Kx$ is a theory.

*Proof.* We show only (2). We first show that $Kx$ contains all **DLPOA**<sup>ω</sup>-theorems. Let $\vdash_{\text{DLPOA}^{\omega}} \psi$. Then $\vdash_{\text{DLPOA}^{\omega}} K\psi$ by the rule (Nec<sub>K</sub>). Since $x$ contains all **DLPOA**<sup>ω</sup>-theorems, $K\psi \in x$. Thus, $\psi \in Kx$. We then show that $Kx$ is closed under the rule (MP). Suppose $\psi, \psi \to \chi \in Kx$, it follows that $K\psi, K(\psi \to \chi) \in x$. Note that $\vdash_{\text{DLPOA}^{\omega}} K(\psi \to \chi) \to (K\psi \to K\chi)$, thus $K(\psi \to \chi) \to (K\psi \to K\chi) \in x$ since $x$ is a theory. It then follows that $K\chi \in x$ since $x$ is closed under (MP). Hence $\chi \in x$. To show that $Kx$ is also closed under $(R_{\mathbb{O}-}^{\omega})$, suppose $\xi(\mathbb{P}^{+}p \to K(p \to \varphi)) \in Kx$ for all $p \in \text{PROP}$. Then $K\xi(\mathbb{P}^{+}p \to K(p \to \varphi)) \in x$ for all $p \in \text{PROP}$. Note that $K\xi(\#)$ is a necessity form. Thus, $K\xi(\varphi \to \mathbb{O}^{-}\varphi) \in x$ since $x$ is closed under $(R_{\mathbb{O}-})$. Therefore, $\xi(\varphi \to \mathbb{O}^{-}\varphi) \in Kx$. Similarly, $Kx$ is also closed under $(R_{\mathbb{P}-}^{\omega})$ and $(R_{\mathbb{P}+}^{\omega})$. □
**Lemma 3.21.** The following holds for all theories $x$ and formulas $\varphi$:

(1) $x + \varphi$ is consistent iff $\neg\varphi \notin x$.

(2) if $x$ is a consistent theory, then $x + \varphi$ is consistent or $x + \neg\varphi$ is consistent.

*Proof.* (1) From left to right. If $\neg\varphi \in x$, we have $\perp \in x + \varphi$ since $\vdash_{\mathbf{DLPOA}^\omega} \varphi \to (\neg\varphi \to \perp)$ and $x + \varphi$ is a theory containing $x$ and $\varphi$. Thus, $x + \varphi$ is inconsistent. From right to left. If $x + \varphi$ is inconsistent, we have $\perp \in x + \varphi$. Thus, $\varphi \to \perp \in x$. Hence $\neg\varphi \in x$.

(2) Suppose $x$ is consistent and both $x + \varphi$ and $x + \neg\varphi$ are inconsistent. By (1), we have $\neg\varphi \in x$ and $\neg\neg\varphi \in x$. Thus, $\perp \in x$. Contradiction! $\square$

**Lemma 3.22 (Lindenbaum).** If $x$ is a consistent theory, then there is $y \in \mathbf{MCT}$ such that $x \subseteq y$.

*Proof.* Let $\psi_0, \psi_1, \dots$ be an enumeration of all formulas. We inductively define a sequence $y_0, y_1, \dots$ of consistent theories as follows. First, let $y_0 = x$. Second, suppose that, for some $n \ge 0$, $y_n$ is a consistent theory containing $x$ that has been already defined. By Lemma 3.21(2), $y_n + \psi_n$ is consistent or $y_n + \neg\psi_n$ is consistent. If $y_n + \psi_n$ is consistent, then we define $y_{n+1} = y_n + \psi_n$. Otherwise, $\neg\psi_n \in y_n$ (by Lemma 3.21(1)) and we consider the following two cases.

(1) If $\psi_n$ is not a conclusion of any of $(R_{\mathbb{O}-}^{\omega-})$, $(R_{\mathbb{P}-}^{\omega-})$, and $(R_{\mathbb{P}+}^{\omega-})$, we define $y_{n+1} = y_n$.

(2) Otherwise, $\psi_n$ is a conclusion of $(R_{\mathbb{O}-}^{\omega-})$, $(R_{\mathbb{P}-}^{\omega-})$, or $(R_{\mathbb{P}+}^{\omega-})$. Let $\xi_1(\chi_1), \dots, \xi_k(\chi_k)$ be all the representations of $\psi_n$ as a conclusion of $(R_{\mathbb{O}-}^{\omega-})$, $(R_{\mathbb{P}-}^{\omega-})$ or $(R_{\mathbb{P}+}^{\omega-})$, where each $\chi_i$ is of the forms $\theta \to \mathbb{O}^{-}\theta$, $\neg\mathbb{P}^{-}\theta$, or $\neg\mathbb{P}^{+}\theta$. We define the sequence $y_n^0, \dots, y_n^k$ of consistent theories as follows. First, let $y_n^0 = y_n$. Second, suppose that, for some $i < k$, $y_n^i$ is a consistent theory containing $y_n$ that has been already defined. Then, it contains $\neg\xi_i(\chi_i)$. We consider three subcases:

(a) $\chi_i$ is of the form $\theta \to \mathbb{O}^{-}\theta$. Since $y_n^i$ is closed under $(R_{\mathbb{O}-}^{\omega-})$, then $\exists p \in \mathbf{PROP}$ such that $\xi_i(\mathbb{P}^+p \to K(p \to \chi_i)) \notin y_n^i$. In this case, define $y_n^{i+1} = y_n^i + \neg\xi_i(\mathbb{P}^+p \to K(p \to \chi_i))$.

(b) $\chi_i$ is of the form $\neg\mathbb{P}^{-}\theta$. Since $y_n^i$ is closed under $(R_{\mathbb{P}-}^{\omega-})$, then there is $p \in \mathbf{PROP}$ such that $\xi_i(\mathbb{P}^+p \to \neg K(p \to \chi_i)) \notin y_n^i$. In this case, define $y_n^{i+1} = y_n^i + \neg\xi_i(\mathbb{P}^+p \to \neg K(p \to \chi_i))$.

(c) $\chi_i$ is of the form $\neg\mathbb{P}^{+}\theta$. Since $y_n^i$ is closed under $(R_{\mathbb{P}+}^{\omega-})$, then there is $p \in \mathbf{PROP}$ such that $\xi_i(\mathbb{P}^+p \to \neg K(p \leftrightarrow \chi_i)) \notin y_n^i$. In this case, define $y_n^{i+1} = y_n^i + \neg\xi_i(\mathbb{P}^+p \to \neg K(p \leftrightarrow \chi_i))$.

Now, we put $y_{n+1} = y_n^k$.

Finally, we define $y = y_0 \cup y_1 \cup \dots$. It is not hard to see that $y$ is a theory. $y$ is also consistent (otherwise $\perp \in y$, there must be some $n \ge 0$ such that $\perp \in y_n$, contradicting that $y_n$ is consistent). On the other hand, for all $n \ge 0$, either $y_n + \psi_n$ or $y_n + \neg\psi_n$ is consistent. In the former case, $\psi_n \in y_{n+1} \subseteq y$ by the construction of $y_{n+1}$. In the latter case, $\neg\psi_n \in y_n \subseteq y$. We conclude that $y$ is also maximal. $\square$
Since $K\varphi$ is an S5-modality, the next lemma follows from the standard argument.

**Lemma 3.23.** The following hold for all $x, y, z \in MCT$,

(1) $Kx \subseteq x$.

(2) if $Kx \subseteq y$ and $Ky \subseteq z$, then $Kx \subseteq z$.

(3) if $Kx \subseteq y$ and $Kx \subseteq z$, then $Ky \subseteq z$.

In the sequel, for every formula $\varphi$ and $X \subseteq MCT$, let $\|\varphi\|_X = \{x \in X \mid \varphi \in x\}$. Now we are ready to define the notion of “canonical model”.

**Definition 3.24 (Canonical model).** Given $x \in MCT$, the canonical model for $x$ is a structure $M(x) = (W, N, V)$ where:

- $W = \{y \in MCT \mid Kx \subseteq y\}$;

- $N(w) = \{\|p\|_W \mid \mathbb{P}^+p \in w\}$ for all $w \in W$;

- $V(p) = \|p\|_W$ for all $p \in \text{PROP}$.

**Proposition 3.25.** $M(x)$ is a model.

*Proof.* It is clear that $W$ is non-empty (since $x \in W$ by Lemma 3.23(1)) and $V$ matches the form of valuations. Suppose $Y \in N(w)$ for some $w \in W$, it remains to show that $w \in Y$. By the definition of $N$, $Y = \|p\|_W$ for some $\mathbb{P}^+p \in W$. Since $w$ contains all **DLPOA**$^\omega$-theorems, $\mathbb{P}^+p \to p \in w$ by the axiom (A11). Since $w$ is closed under (MP), $p \in w$. Therefore, $w \in \|p\|_W = Y$. $\square$

*Remark 7.* Two remarks on the canonical model $M(x)$:

1. Note that $M(x)$ satisfies the constraint in Remark 2 on page 1637: for all $w \in X \subseteq W$ and $Y \in N(w)$, if $Y \subseteq X$ then $Y = [p]_{M(x),X}$ for some $p \in \text{PROP}$.

2. To make the completeness proof go through, it is essential to ensure that the elements in $N(w)$ are all truth sets of atoms (see Footnote 11 on page 1657). This is the reason why “maximal consistent theories” are also required to be closed under the rules $(R_{\mathbb{P}^-}^\omega)$ and $(R_{\mathbb{P}^+}^\omega)$ so that the truth of formulas $\mathbb{P}^-\varphi$ and $\mathbb{P}^+\varphi$ is also reduced to the truth of $\mathbb{P}^+p$.

**Lemma 3.26.** For all $w \in W$ and formulas $K\psi$, $K\psi \in w$ iff for all $v \in W$, $\psi \in v$.

*Proof.* From left to right. Suppose $K\psi \in w$. Note that $Kx \subseteq w$ and $Kx \subseteq v$. Thus $Kw \subseteq v$ by Lemma 3.23(3). Hence $\psi \in v$. From right to left. Suppose $K\psi \notin w$. We need to find $v \in W$ such that $\psi \notin v$. Consider the set of formulas $Kw + \neg\psi$, $Kw + \neg\psi$ is a theory by Lemma 3.20. Besides, it is consistent (otherwise $\bot \in Kw + \neg\psi$. Hence $\neg\psi \to \bot \in Kw$ and thus $\psi \in Kw$. Therefore, $K\psi \in w$, contradicting the assumption). By the Lindenbaum lemma, there is $v \in MCT$ such that $Kw + \neg\psi \subseteq v$. We have $\psi \notin v$ and $v \in W$ (since $Kx \subseteq w$ and $Kw \subseteq v$, $Kx \subseteq v$ by Lemma 3.23(2)). $\square$

**Lemma 3.27.** For all $w \in W$ and formulas $\mathbb{P}^+\psi$, $\mathbb{P}^+\psi \in w$ iff there is $p \in \text{PROP}$ such that $\mathbb{P}^+p \to \neg K(p \leftrightarrow \psi) \notin w$.
*Proof.* From left to right. Suppose that for all $p \in \text{PROP}$, $\mathbb{P}^+p \to \neg K(p \leftrightarrow \psi) \in w$. Since $w$ is closed under the rule $(R^\omega_{\mathbb{P}+})$, $\neg \mathbb{P}^+\psi \in w$. Thus $\mathbb{P}^+\psi \notin w$ by Lemma 3.18. From right to left. Suppose $\mathbb{P}^+p \to \neg K(p \leftrightarrow \psi) \notin w$, then $\mathbb{P}^+p \in w$ and $K(p \leftrightarrow \psi) \in w$. By axiom (A5), it implies that $\mathbb{P}^+\psi \in w$. $\square$

**Lemma 3.28.** Let $\mathbb{P}^+\psi$ be a formula and suppose that $[[\psi]]_{M(x),W} = \|\psi\|_W$. For all $w \in W$, $M(x), w, W \models \mathbb{P}^+\psi$ iff there is $p \in \text{PROP}$ such that $\mathbb{P}^+p \to \neg K(p \leftrightarrow \psi) \notin w$.

*Proof.* From left to right. Suppose $M(x), w, W \models \mathbb{P}^+\psi$. By semantics, $[[\psi]]_{M(x),W} \in N(w)$. By the construction of $N$, there is $p \in \text{PROP}$ with $\mathbb{P}^+p \in w$ and $\|p\|_W = [[\psi]]_{M(x),W} = \|\psi\|_W$. From the latter it follows that for all $v \in W$, $p \leftrightarrow \psi \in v$. Thus, by Lemma 3.26, $K(p \leftrightarrow \psi) \in w$. Since $\mathbb{P}^+p \in w$, $\mathbb{P}^+p \to \neg K(p \leftrightarrow \psi) \notin w$.

From right to left. Suppose $\mathbb{P}^+p \to \neg K(p \leftrightarrow \psi) \notin w$. Then $\mathbb{P}^+p \in w$ and $K(p \leftrightarrow \psi) \in w$. From the former, it follows that $\|p\|_W \in N(w)$. From the latter it follows that $\|p\|_W = \|\psi\|_W$ by Lemma 3.26. Note that we assume $[[\psi]]_{M(x),W} = \|\psi\|_W$. Hence $[[\psi]]_{M(x),W} = \|p\|_W \in N(w)$. That is, $M(x), w, W \models \mathbb{P}^+\psi$. $\square$

**Lemma 3.29.** The following hold for all $w \in W$ and formulas $\mathcal{O}^{-}\psi, \chi$:

(1) $\mathcal{O}^{-}\psi \in w$ iff $\psi \in w$ and for all $p \in \text{PROP}$, $\mathbb{P}^{+}p \to K(p \to \psi) \in w$.

(2) $[\chi]\mathcal{O}^{-}\psi \in w$ iff $[\chi]\psi \in w$ and for all $p \in \text{PROP}$, $[\chi](\mathbb{P}^{+}p \to K(p \to \psi)) \in w$.

*Proof.* (1) The direction from left to right follows from the axioms (A11) and (A8). For the converse, suppose $\psi \in w$ and $\mathbb{P}^+p \to K(p \to \psi) \in w$ for all $p \in \text{PROP}$. Since $w$ is closed under the rule $(R^\omega_{\mathcal{O}-})$, $\psi \to \mathcal{O}^{-}\psi \in w$. Since $\psi \in w$, $\mathcal{O}^{-}\psi \in w$.

(2) From left to right. Since $[\chi]$ is a normal modality, by the axioms (A11) and (A8), it is not hard to see that $\vdash_{\text{DLPOA}^\omega}$ $[\chi]\mathcal{O}^{-}\psi \to [\chi]\psi$ and $\vdash_{\text{DLPOA}^\omega}$ $[\chi]\mathcal{O}^{-}\psi \to [\chi](\mathbb{P}^+p \to K(p \to \psi))$. Since $[\chi]\mathcal{O}^{-}\psi \in w$, $[\chi]\psi \in w$ and $[\chi](\mathbb{P}^+p \to K(p \to \psi)) \in w$ for all atoms $p$. From right to left. Note that $[\chi]_\sharp$ is a necessity form. Since $[\chi](\mathbb{P}^+p \to K(p \to \psi)) \in w$ for all $p \in \text{PROP}$ and $w$ is closed under the rule $(R_{\mathcal{O}-})$, $[\chi](\psi \to \mathcal{O}^{-}\psi) \in w$. Since $[\chi]\psi \in w$, $[\chi]\mathcal{O}\psi \in w$. $\square$

**Lemma 3.30.** For all $w \in W$, $\neg \mathbb{P}^{-}\psi \in w$ iff for all $p \in \text{PROP}$, $\mathbb{P}^{+}p \to \neg K(p \to \psi) \in w$.

*Proof.* Similarly to the proof of Lemma 3.29. $\square$

**Lemma 3.31.** The following hold for all $w \in W$:

(1) if $M(x), w, W \models \psi \wedge \neg \mathcal{O}^{-}\psi$ then there is $p \in \text{PROP}$ such that $M(x), w, W \not\models \mathbb{P}^{+}p \to K(p \to \psi)$.

(2) if $M(x), w, W \models [\chi]\psi \wedge \neg[\chi]\mathcal{O}^{-}\psi$ then there is $p \in \text{PROP}$ such that $M(x), w, W \not\models [\chi](\mathbb{P}^{+}p \to K(p \to \psi))$.

*Proof.* (1) Suppose $M(x), w, W \models \psi \wedge \neg \mathcal{O}^{-}\psi$. By the semantics, there is $Y \in N(w)$ such that $Y \not\subseteq [[\psi]]_{M(x),W}$. By the definition of $N$, there is $\mathbb{P}^+p \in w$ such that $V(p) = Y$. Thus, $M(x), w, W \models \mathbb{P}^+p$. Since $V(p) \not\subseteq [[\psi]]_{M(x),W}$, $M(x), w, W \not\models K(p \to \psi)$. Hence $M(x), w, W \not\models \mathbb{P}^+p \to K(p \to \psi)$.

(2) Suppose $M(x), w, W \models [\chi]\psi \wedge \neg[\chi]\mathcal{O}^{-}\psi$. By the semantics, it follows that $M(x), w, W \models$
$\chi$, $M(x), w, [[\chi]]_W \models \psi$, and $M(x), w, [[\chi]]_W \not\models \mathcal{O}^{-}\psi$. From the latter two it follows that there is $Y \in N(w)$ such that $Y \subseteq [[\chi]]_W$ and $Y \not\subseteq [[\psi]]_{[[\chi]]_W}$. By the definition of $N$, there is $p \in \text{PROP}$ such that $Y = V(p)$.

We need to show that $M(x), w, W \not\models [\chi]([\mathbb{P}^+p \to K(p \to \psi)])$. Since $M(x), w, W \models \chi$, it suffices to show that $M(x), w, [[\chi]]_W \not\models \mathbb{P}^+p \to K(p \to \psi)$. Since $V(p) = Y \subseteq [[\chi]]_W$, $[[p]]_{[[\chi]]_W} = V(p) = Y \in N(w)$.<fnref n="11" /> Thus $M(x), w, [[\chi]]_W \models \mathbb{P}^+p$. Since $[[p]]_{[[\chi]]_W} \not\subseteq [[\psi]]_{[[\chi]]_W}$, $M(x), w, [[\chi]]_W \not\models K(p \to \psi)$. □

**Lemma 3.32.** For all $w \in W$, if $M(x), w, W \models \mathbb{P}^{-}\psi$ then there is $p \in \text{PROP}$ such that $M(x), w, W \not\models \mathbb{P}^{+}p \to \neg K(p \to \psi)$.

*Proof.* Similarly to the proof of Lemma 3.31. □

**Lemma 3.33 (Truth).** For all $w \in W$ and $\varphi \in \mathcal{L}_{DLPOA}$, $\varphi \in w$ iff $M(x), w, W \models \varphi$.

*Proof.* Induction on $c(\varphi)$. The following cases cover both the base and inductive steps. The case $p$ is trivial. The cases for $\neg\psi$ and $\psi \to \chi$ follow from Lemma 3.18, the IH, and the semantics.

**Case K$\psi$.** We have

$K\psi \in w$ iff for all $v \in W$, $\psi \in v$ (Lemma 3.26)

iff for all $v \in W$, $M(x), v, W \models \psi$ (IH)

iff $M(x), w, W \models K\psi$ (semantics)

**Case P$^{+}\psi$.** We have

$\mathbb{P}^{+}\psi \in w$ iff $\exists p \in \text{PROP}$ such that $\mathbb{P}^{+}p \to \neg K(p \leftrightarrow \psi) \notin w$ (Lemma 3.27)

iff $M(x), w, W \models \mathbb{P}^{+}\psi$ (Lemma 3.28)

**Case O$^{-}\psi$.** Note that $c(O^{-}\psi) > c(\mathbb{P}^{+}p \to K(p \to \psi))$ by Proposition 3.3. Then

$O^{-}\psi \in w$

iff $\psi \in w$ and $\forall p \in \text{PROP}, \mathbb{P}^{+}p \to K(p \to \psi) \in w$ (Lemma 3.29)

iff $M(x), w, W \models \psi$ and $\forall p \in \text{PROP}, M(x), w, W \models \mathbb{P}^{+}p \to K(p \to \psi)$ (IH)

iff $M(x), w, W \models O^{-}\psi$ (up by the validity of (A11) and (A8), down by Lem. 3.31(1))

**Case P$^{-}\psi$.** Note that $c(P^{-}\psi) > c(\mathbb{P}^{+}p \to \neg K(p \to \psi))$ by Proposition 3.3. Then

$P^{-}\psi \notin w$

iff $\neg P^{-}\psi \in w$ (Lemma 3.18)

iff $\forall p \in \text{PROP}, \mathbb{P}^{+}p \to \neg K(p \to \psi) \in w$ (Lemma 3.30)

iff $\forall p \in \text{PROP}, M(x), w, W \models \mathbb{P}^{+}p \to \neg K(p \to \psi)$ (IH)

iff $M(x), w, W \not\models P^{-}\psi$ (up by the validity of (A9), down by Lemma 3.32)

<footnote n="11">11. If the atom $p$ here were replaced by some non-propositional formulas, then the equivalence would not hold in general. Therefore, we have constructed the canonical model so that all elements in $N(w)$ are truth sets of atoms.</footnote>
The cases for [χ]p, [χ]¬ψ, [χ](ψ → ψ'), [χ]Kψ, [χ]P⁺ψ, [χ]P⁻ψ, and [χ][ψ]ψ' follow from the induction hypothesis, the validity of the axioms (!Atom) – (!Comp), and that w is a consistent theory. The case for [χ]O⁻ψ remains to be considered.

**Case** [χ]O⁻ψ. Note that c([χ]O⁻ψ) > c([χ]ψ) and c([χ]O⁻ψ) > c([χ](P⁺p → K(p → ψ))) by Proposition 3.3. Then

$$[\chi] \mathcal{O}^{-} \psi \in w$$

iff [χ]ψ ∈ w and ∀p ∈ PROP, [χ](P⁺p → K(p → ψ)) ∈ w. (Lemma 3.29)

iff M(x), w, W |= [χ]ψ and ∀p ∈ PROP, M(x), w, W |= [χ](P⁺p → K(p → ψ)) (IH)

iff M(x), w, W |= [χ]O⁻ψ (up by |= [χ]O⁻ψ → [χ](P⁺p → K(p → ψ))) and
|= [χ]O⁻ψ → [χ]ψ, down by Lemma 3.31(2)) □

**Theorem 4.** For all formulas $\varphi \in \mathcal{L}_{DLPOA}$, if $\models \varphi$ then $\vdash_{DLPOA^\omega} \varphi$.

*Proof.* Suppose $\vdash_{DLPOA^\omega} \varphi$, then $\vdash_{DLPOA^\omega} \neg\neg\varphi$. Note that the set of all **DLPOA**<sup>ω</sup>-theorems, *Th(**DLPOA**<sup>ω</sup>), is a theory. By Lemma 3.20, **DLPOA**<sup>ω</sup> +¬φ is a theory containing **DLPOA**<sup>ω</sup> and¬φ. Since¬¬φ /∈ *Th(**DLPOA**<sup>ω</sup>), by Lemma 3.21, *Th(**DLPOA**<sup>ω</sup>) +¬φ is consistent. Thus, there must be x ∈ MCT such that **DLPOA**<sup>ω</sup> +¬φ ⊆ x by Lemma 3.22. From Lemma 3.33, it follows that M(x), x, W |=¬φ. Therefore, != φ. □

**Corollary 3.34.** The axiomatization **DLPOA** is weakly complete with the semantics.

# 4. Generalization

In this section, we study how to generalize LPOA to epistemic logics other than S5. The motivations for considering such a generalization are as follows. First, even if S5 is taken as the logic of knowledge in artificial intelligence and game theory, it is criticized in philosophical literature (e.g., Lenzen, 1978, 1995; Aucher, 2014). It is still not clear whether the choice of the underlying epistemic logic will affect the logic of permitted and obligatory announcements. Second, despite the elegance of the two-dimensional semantics, it is difficult to extend it to the multi-agent case. In contrast, the generalized semantics builds on the usual relational models and thus paves the way to the multi-agent case.

## 4.1 Preliminaries

In order to define our semantics, some preliminary notions are needed. A *Kripke model* is a tuple $M = (W, R, V)$ where $W$ and $V$ are as before and $R$ is a binary relation over $W$. Given two Kripke models $M = (W, R, V)$ and $M' = (W', R', V')$, a non-empty binary relation $Z \subseteq W \times W'$ is a *bisimulation* from $M$ to $M'$ if for all $(w, w') \in Z$:

**atoms** $w \in V(p)$ iff $w' \in V'(p)$ for all $p \in \text{PROP}$.

**forth** If $wRv$ then there is $v'$ (in $W'$) such that $w'R'v'$ and $vZv'$.

**back** If $w'Rv'$ then there is $v$ (in $W$) such that $wRv$ and $vZv'$.

$Z$ is called a *refinement* if it satisfies only the conditions **atoms** and **back**. Let $w$ and $w'$ be two states. If $Z$ is a bisimulation (refinement, respectively) from $M$ to $M'$ with $(w, w') \in Z$, we write $Z : M, w \triangleleftharpoons M'$, $w'$ ($Z : M, w \succeq M'$, $w'$, respectively); if there is a
bisimulation (refinement, respectively) Z such that $Z : M, w \triangleleft M', w' (Z : M, w \succeq M', w'$, respectively), we write $M, w \triangleleft M', w' (M, w \succeq M', w'$, respectively).

Given a Kripke model $M = (W, R, V)$ and a set $U \subseteq W$, the restriction of $M$ to $U$ is a Kripke model $M|_U = (U, R|_U, V|_U)$ such that $R|_U = R \cap (U \times U)$ and $V|_U(p) = V(p) \cap U$ for all $p \in \text{PROP}$. Given two pointed Kripke models $M, w$ and $M', w'$, we write $M, w \geq M', w'$ if there is $U \ni w$ such that $M|_U, w \triangleleft M', w'$. It is easy to see that $M, w \geq M', w'$ implies $M, w \succeq M', w'$ for all pointed Kripke models $M, w$ and $M', w'$.

Intuitively, given two pointed Kripke models $M, w$ and $M', w'$, $M, w \geq M', w'$ means that $M', w'$ can be obtained from $M, w$ by a public announcement;<fnref n="12" /> $M, w \succeq M', w'$ means that the knowledge (rather than ignorance) represented by $M, w$ is contained in $M', w'$; and $M, w \triangleleft M', w'$ captures the intuition that they contain the same set of knowledge, as well as ignorance. The second statement is justified by the next proposition. Let $\Vdash$ be the standard Kripke semantics for $\mathcal{L}_{el}^{13}$ and $\mathcal{L}_{el}^{+}$ the sublanguage of $\mathcal{L}_{el}$ that is defined by the following BNF:

$$ \varphi ::= p \mid \neg p \mid (\varphi \land \varphi) \mid (\varphi \lor \varphi) \mid K\varphi $$

**Proposition 4.1** (Bozzelli et al., 2014, Proposition 8). For any image-finite (every state has only finitely many successors) pointed Kripke models $M, w$ and $M', w'$,

$$ M, w \succeq M', w' \text{ iff, for all formulas } \varphi \in \mathcal{L}_{el}^{+}, M, w \Vdash \varphi \text{ implies } M', w' \Vdash \varphi. $$

In the sequel, we will present some properties of $\triangleleft$, $\succeq$, and $\geq$, which will be used in later proofs. The reader can skip this part for now and come back to it when needed. Given a Kripke model $M = (W, R, V)$, we say

- $M$ is a **4-model** iff $R$ is transitive;

- $M$ is an **S4-model** iff $R$ is reflexive and transitive;

- $M$ is an **S4.4-model** iff $R$ is reflexive, transitive, convergent, and remotely symmetric;<fnref n="14" />

- $M$ is an **S5-model** iff $R$ is an equivalence relation.

**Proposition 4.2.** Let $M = (W, R, V)$ be an S4.4-Kripke-model. For all $w, u, v \in W$ with $wRu$ and $wRv$, if $V(u) = V(v)$ then $M, u \triangleleft M, v$.

*Proof.* It suffices to show that $R(u) \setminus \{u\} = R(v) \setminus \{v\}$ (since, as one can verify, the relation $Z = \{(x, x) \mid x \in R(u) \& x \neq u\} \cup \{(u, v)\}$ is then a bisimulation such that $Z : M, u \triangleleft M, v$). Suppose $uRz$ and $z \neq u$. Since $wRu$ and $uRz$, by the transitivity of $R$, $wRz$. Note that $wRv$. Hence, by the convergence of $R$, there must be $x$ such that $zRx$ and $vRx$. Since $uRz$, $zRx$ and $u \neq z$, by remote symmetry of $R$, $xRz$. Note that $vRx$ and $xRz$. By transitivity, it follows that $vRz$. Hence $R(u) \setminus \{u\} \subseteq R(v) \setminus \{v\}$. By symmetry, we have $R(u) \setminus \{v\} \subseteq R(v) \setminus \{u\}$. Therefore, $R(u) \setminus \{u\} = R(v) \setminus \{v\}$. $\square$

<footnote n="12">12. Of course, even if $M|_U, w \triangleleft M', w'$ for some $U \ni w$, $M', w'$ may not be achievable by a public announcement (since $U$ may be the truth set of no formula). The similar problem has been discussed in Remark 2. In Section 4.4, we will see that this problem does not affect the logic when only S5-models are considered.</footnote>

<footnote n="13">13. That is, in addition to the usual truth definition for atoms and Boolean connectives, we have: $M, w \Vdash K\varphi$ iff $M, v \Vdash \varphi$ for all $v$ such that $wRv$.</footnote>

<footnote n="14">14. A relation $R$ is convergent iff $wRx$ and $wRy$ implies $\exists z : xRz \& yRz$; $R$ is remotely symmetric iff $xRy$ and $yRz$ implies that $zRy$ or $x = y$.</footnote>
Given a Kripke model $M = (W, R, V)$ and $\varphi \in \mathcal{L}_{el}$, let $M|_{\varphi} = M|_{\{w \in W | M, w \models \varphi\}}$.

**Proposition 4.3.** Let $M = (W, R, V)$ be a Kripke-model with $R = W \times W$. Then

(1) for all $U \subseteq W$ and $\varphi \in \mathcal{L}_{el}$, if $M|_{\varphi}, w \supseteq M|_{U}, v$ (for some states $w, v \in W$) then
$U \subseteq \{x \in W \mid M, x \models \varphi\}$.

(2) for all $\varphi, \psi \in \mathcal{L}_{el}$, if $M|_{\varphi}, w \stackrel{\leftrightarrow}{\models} M|_{\psi}, v$ (for some states $w, v \in W$) then, for all $x \in W$, $M, x \models \varphi$ iff $M, x \models \psi$.

*Proof.* We show only (1) as (2) follows from (1). Let $x \in U$. Then $vR|_U x$. Since $M|_{\varphi}, w \supseteq M|_U, v$, there must be $x'$ such that $M, x' \models \varphi$ and $M|_{\varphi}, x' \supseteq M|_U, x$. Then $V(x) = V(x')$. Thus, $M, x \stackrel{\leftrightarrow}{\models} M, x'$ (by Proposition 4.2). Hence $M, x \models \varphi$. $\square$

**4.2 Semantics**

Now we are ready to introduce the semantics. Given that the logic of knowledge is weaker than S5, “epistemic states” can no longer be represented by sets of possible worlds, but by pointed Kripke models.

**Definition 4.4 (Deontic-epistemic-model).** Let $I$ be a non-empty set. An $I$-deontic-epistemic-model (or, simply, deontic-epistemic-model) $\mathcal{M} = (\mathcal{S}, \mathcal{N})$ is a set $\mathcal{S} = \{M_i \mid i \in I\}$ of disjoint Kripke models $M_i = (W_i, R_i, V_i)^{15}$ together with a (total) function $\mathcal{N} : \bigcup_{i \in I} W_i \to \wp(\bigcup_{i \in I} W_i)$ such that for all $j \in I$ and $w_j, v_j \in W_j, v_j \notin \mathcal{N}(w_j)$.

Intuitively, given an $I$-deontic-epistemic-model $\mathcal{M} = (\{M_i \mid i \in I\}, \mathcal{N})$, if a pointed Kripke model $(M_i, w_i)$ represents the current epistemic state of the receiver then the pointed Kripke models $(M_j, w_j)$, for all $w_j \in \mathcal{N}(w_i)$, represent the ideal epistemic states of the receiver according to the given security policy.

**Definition 4.5 (Model class).** Let an $I$-deontic-epistemic-model $\mathcal{M} = (\{M_i \mid i \in I\}, \mathcal{N})$ be given. We say $\mathcal{M}$ is a 4-model (S4-model, S4.4-model, S5-model, respectively) if, for each $i \in I$, $M_i$ is a 4-Kripke-model (S4-Kripke-model, S4.4-Kripke-model, S5-Kripke-model, respectively).

In addition, we say $\mathcal{M}$ is *realistic* if, for all $i \in I$, $w_i \in W_i$, and $w_j \in \mathcal{N}(w_i)$, $M_i, w_i \supseteq M_j, w_j$. That is, all ideal epistemic states are achievable by some public announcements. $\mathcal{M}$ is *standard* if $\mathcal{N}(w_i) \neq \emptyset$ for all $i \in I$ and $w_i \in W_i$.

Note that if there is no knowledge involved (the relations $R_i$ are all empty) then a standard deontic-epistemic-model is isomorphic to a standard deontic model (i.e., a Kripke model where the accessibility relation is serial) and vice versa.

*Remark 8.* For “realistic” models, since each ideal epistemic state $(M_j, w_j)$ is bisimilar to a submodel of $(M_i, w_i)$, we can replace $\mathcal{N}$ by a neighbourhood function $N : \bigcup_{i \in I} W_i \to \wp(\bigcup_{i \in I} W_i)$ such that, for all $i \in I$ and $w_i \in W_i$, $N(w_i) = \{U \subseteq W_i \mid w_i \in U \text{ and } \exists w_j \in N(w_i) : M_i|_U, w_i \stackrel{\leftrightarrow}{\models} M_j, w_j\}$.

<footnote n="15">15. The states in $M_i$ are denoted by $w_i, v_i, \dots$.</footnote>
**Definition 4.6** (General semantics). Let $I$ be a non-empty set. Given an $I$-deontic-epistemic-model $\mathcal{M}$, for all $i \in I$, $w_i \in W_i$, and formulas $\varphi \in \mathcal{L}_{LPOA}$,<fnref n="16" /> the satisfaction relation $\mathcal{M}, w_i \asymp \varphi$ is inductively defined as follows (the truth conditions for atoms and Boolean connectives are as usual and thus omitted):

- $\mathcal{M}, w_i \asymp K\varphi$ iff $\mathcal{M}, w_i \asymp \varphi$ for all $w_i \in W_i$ with $w_i R_i w_i$

- $\mathcal{M}, w_i \asymp \mathbb{P}^+\varphi$ iff $\mathcal{M}, w_i \asymp \varphi$ and there is $w_j \in \mathcal{N}(w_i)$ such that $M_i|_{\varphi}, w_i \stackrel{\leftrightarrow}{\rightleftharpoons} M_j, w_j$

- $\mathcal{M}, w_i \asymp \mathbb{P}^-\varphi$ iff $\mathcal{M}, w_i \asymp \varphi$ and there is $w_j \in \mathcal{N}(w_i)$ such that $M_i, w_i \geq M_j, w_j$ and $M_i|_{\varphi}, w_i \succeq M_j, w_j$

- $\mathcal{M}, w_i \asymp \mathbb{O}^-\varphi$ iff $\mathcal{M}, w_i \asymp \varphi$ and for all $w_j \in \mathcal{N}(w_i)$, if $M_i, w_i \geq M_j, w_j$ then $M_i|_{\varphi}, w_i \succeq M_j, w_j$

where $M_i|_{\varphi} = M_i|_{\llbracket \varphi \rrbracket}^i_{\mathcal{M}}$ and $\llbracket \varphi \rrbracket^i_{\mathcal{M}} = \{v_i \in W_i \mid \mathcal{M}, v_i \asymp \varphi\}$. The notion of validity is defined as usual.

Some remarks about the intuition behind the semantics are in order. The clause for $\mathbb{P}^+\varphi$ reflects the intuition that the sender is strongly permitted to announce $\varphi$ if $\varphi$ is true and the receiver's epistemic state after the announcement of $\varphi$ is ideal. For $\mathbb{P}^-\varphi$, we have that the sender is weakly permitted to announce $\varphi$ if $\varphi$ is true and all the (receiver's) "knowledge" following from the announcement of $\varphi$ is contained in one of the achievable ideal epistemic state. Finally, for $\mathbb{O}^-\varphi$, we have that the sender is obliged to announce $\varphi$ if $\varphi$ is true and all the (receiver's) "knowledge" following from the announcement of $\varphi$ is contained in every achievable ideal epistemic state.

The reader may notice that the truth definitions for $\mathbb{P}^+\varphi$, $\mathbb{P}^-\varphi$, and $\mathbb{O}^-\varphi$ speak only about ideal epistemic states achievable from the actual by some announcements. Thus, removing those unachievable ideal epistemic states would not affect the truth of formulas. The next proposition formally states the observation. It also follows that the class of realistic deontic-epistemic-models gives the same logic as the class of all deontic-epistemic-models.

**Proposition 4.7.** For all $I$-deontic-epistemic-model $\mathcal{M}$, $i \in I$, and $w_i \in W_i$, there is a realistic $J$-deontic-epistemic-model $\mathcal{M}'$, $j \in J$ and $w'_j \in W'_j$ such that $\mathcal{M}, w_i \asymp \varphi$ iff $\mathcal{M}', w'_j \models \varphi$ for all $\varphi \in \mathcal{L}_{LPOA}$.

We can also show that the class of standard deontic-epistemic-models gives the same logic as the class of all deontic-epistemic-models.

**Proposition 4.8.** For all deontic-epistemic-models $\mathcal{M} = (\{M_i \mid i \in I\}, \mathcal{N})$, $i \in I$, and $w_i \in W_i$, there is a standard deontic-epistemic-model $\mathcal{M}' = (\{M'_j \mid j \in J\}, \mathcal{N}')$, $j \in J$ and $w'_j \in W'_j$ such that $\mathcal{M}, w_i \asymp \varphi$ iff $\mathcal{M}', w'_j \models \varphi$ for all $\varphi \in \mathcal{L}_{LPOA}$.

*Proof Sketch.* For each $w_k \in \bigcup_{i \in I} W_i$ with $\mathcal{N}(w_k) = \emptyset$, add a new Kripke model $\mathcal{M}$ into $\mathcal{M}$ consisting of a single isolated state $w$. It is required that the valuation of $w$ is different from

$$ \mathcal{M}, w_i \asymp [\varphi]\psi \text{ iff } \mathcal{M}, w_i \asymp \varphi \text{ implies } \mathcal{M}|_{\varphi}, w_i \asymp \psi $$

where $\mathcal{M}|_{\varphi} = (\{M_i|_{\varphi}, M_j \mid j \in I \setminus \{i\}\}, \mathcal{N}_{\varphi})$ such that $\mathcal{N}_{\varphi}$ is the restriction of $\mathcal{N}$ to $\llbracket \varphi \rrbracket^i_{\mathcal{M}} \cup \bigcup_{j \in I \setminus \{i\}} W_j$.

<footnote n="16">16. One can easily extend the semantics to $\mathcal{L}_{DLPOA}$ by adding the following clause:</footnote>
the valuation of $w_k$ (thus $M_i, w_i \nsubseteq M, w$). Then add $w$ into $\mathcal{N}(w_k)$ and let $\mathcal{N}(w) = \{w_k\}$.
Let the resulting deontic-epistemic-model be $\mathcal{M}'$. By induction on the structure of formulas,
it can be shown that, for all $w_i \in W_i$ and $\varphi \in \mathcal{L}_{LPOA}$, $M, w_i \models \varphi$ iff $\mathcal{M}', w_i \models \varphi$. $\square$

## 4.3 Semantic Results

In this subsection, we explore some (in)validities of the general semantics. As we shall see,
the choice of the underlying epistemic logic has a critical impact on the logic of permitted
and obligatory announcements.

In the following, the notation $\approx_4$ ($\approx_{S4}, \approx_{S4.4}, \approx_{S5}$, respectively) will denote the notion of validity over the class of all 4-models (S4-models, S4.4-models, S5-models, respectively).
For every $\varphi \in \mathcal{L}_{LPOA}$, let $\dot{K}\varphi$ be an abbreviation for $\varphi \wedge K\varphi$.

**Proposition 4.9.** The following hold for all formulas $\varphi, \psi \in \mathcal{L}_{LPOA}$:

1. $\approx_P \neg \varphi \rightarrow \varphi$.

2. $\approx_O \neg \varphi \rightarrow \varphi$.

3. $\approx_P \neg \varphi \rightarrow \varphi$.

4. $\approx_4 \dot{K}(\varphi \leftrightarrow \psi) \rightarrow (P^+ \leftrightarrow P^+ \psi)$.

5. $\approx_4 \neg P^- \varphi \rightarrow (P^+ \psi \rightarrow \neg \dot{K}(\psi \rightarrow \varphi))$.

*Proof.* 1 – 3 follow immediately from the semantics.

4. Suppose $M, w_i \approx \dot{K}(\varphi \leftrightarrow \psi)$. Assume $M, w_i \approx P^+\varphi$. Then $M, w_i \approx \varphi$. Thus $M, w_i \approx \psi$. On the other hand, by semantics, there is $w_j \in \mathcal{N}(w_i)$ such that $M_j, w_j \stackrel{\leftrightarrow}{\models} M_i|_{\varphi}, w_i$. Let $Z$ be a bisimulation from $M_j$ to $M_i|_{\varphi}$ with $(w_j, w_i) \in Z$. Since $M, w_i \approx K(\varphi \leftrightarrow \psi)$, $R_i|_{\llbracket \varphi \rrbracket_M^i}(w_i) = R_i|_{\llbracket \psi \rrbracket_M^i}(w_i)$. Let $Z'$ be the identity relation on $R_i|_{\llbracket \varphi \rrbracket_M^i}(w_i) \cup \{w_i\}$. It is not hard to verify that $Z'$ is a bisimulation from $M_i|_{\varphi}$ to $M_i|_{\psi}$ (as $R_i$ is transitive). Thus the composition of $Z$ and $Z'$, $Z \circ Z'$, is a bisimulation from $M_j$ to $M_i|_{\psi}$ (see, e.g., Blackburn et al., 2001, p. 71). Note that $(w_j, w_i) \in Z \circ Z'$. Hence, $M_j, w_j \stackrel{\leftrightarrow}{\models} M_i|_{\psi}, w_i$. By semantics, $M, w_i \approx P^+\psi$. Thus, $M, w_i \approx P^+\varphi \rightarrow P^+\psi$. By symmetry, $M, w_i \approx P^+\psi \rightarrow P^+\varphi$. Therefore $M, w_i \approx P^+\varphi \leftrightarrow P^+\psi$.

5. Suppose $M, w_i \approx P^+\psi$ and $M, w_i \approx \dot{K}(\psi \rightarrow \varphi)$. It suffices to show that $M, w_i \approx P^-\varphi$. Since $M, w_i \approx P^+\psi$, $M, w_i \approx \psi$. Thus $M, w_i \approx \varphi$. On the other hand, by semantics, there is $w_j \in \mathcal{N}(w_i)$ such that $M_i|_{\psi}, w_i \stackrel{\leftrightarrow}{\models} M_j, w_j$. Let $Z$ be a bisimulation between $M_i|_{\psi}$ and $M_j$ such that $(w_i, w_j) \in Z$. Since $M, w_i \approx K(\psi \rightarrow \varphi)$, $R_i|_{\llbracket \psi \rrbracket_M^i}(w_i) \subseteq R_i|_{\llbracket i \rrbracket_M \varphi}(w_i)$. Let $Z'$ be the identity relation on $R_i|_{\llbracket \psi \rrbracket_M^i}(w_i) \cup \{w_i\}$. It is not hard to verify that $Z'$ is a refinement from $M_i|_{\varphi}$ to $M_i|_{\psi}$ (as $R_i$ is transitive). Thus the composition of $Z$ and $Z'$, $Z \circ Z'$, is a refinement from $M_i|_{\varphi}$ to $M_j$ (see Bozzelli et al., 2014, Proposition 2). Since $(w_i, w_j) \in Z \circ Z'$, $M_i|_{\varphi}, w_i \supseteq M_j, w_j$. It follows that $M, w_i \approx P^-\varphi$. $\square$

**Proposition 4.10.** The following hold:

1. $\approx_{S4} \mathcal{O}^{-} \varphi \rightarrow (P^{+} \psi \rightarrow K(\psi \rightarrow \varphi))$ for some $\varphi, \psi \in \mathcal{L}_{el}$.

2. $\approx_{S4.4} \mathcal{O}^{-} \varphi \rightarrow (P^{+} \psi \rightarrow K(\psi \rightarrow \varphi))$ for all $\varphi, \psi \in \mathcal{L}_{el}$.

3. $\approx_{S5} \mathcal{O}^{-} \varphi \rightarrow (P^{+} \psi \rightarrow K(\psi \rightarrow \varphi))$ for some $\varphi, \psi \in \mathcal{L}_{LPOA}$.
*Proof.* 1. Consider the *I*-deontic-epistemic-model $\mathcal{M} = (\mathcal{S}, \mathcal{N})$ (as illustrated in Figure 4) where $I = \{0, 1\}$ and:

- $\mathcal{S} = \{M_0, M_1\}$ with $M_0 = (W_0, R_0, V_0)$ and $M_1 = (W_1, R_1, V_1)$ where:

- $W_0 = \{w_0, u_0, v_0\}$ and $W_1 = \{w_1, u_1, v_1\}$;

- $R_0$ is the reflexive closure of $\{(w_0, u_0), (w_0, v_0)\}$;

- $R_1$ is the reflexive closure of $\{(w_1, u_1), (w_1, v_1)\}$;

- $V_0(p) = \{u_0\}$ and $V_1(p) = \{u_1\}$.

- $\mathcal{N}(w_0) = \{w_1\}$ and $\mathcal{N}(x) = \emptyset$ for all $x \in (W_0 \cup W_1) \setminus \{w_0\}$.

$\mathcal{M}$ is an S4-deontic-epistemic-model and $\mathcal{M}, w_0 \not\leq_O \neg K \neg p \to (\mathbb{P}^+ \to K(\to \neg K \neg p))$.

2. We prove it by contradiction. Suppose, for some S4.4 deontic-epistemic-model $\mathcal{M}$ and $w_i \in \mathcal{M}$, we have $\mathcal{M}, w_i \asymp_O \neg \varphi$, $\mathcal{M}, w_i \asymp \mathbb{P}^+ \psi$, and $\mathcal{M}, w_i \not\asymp_K \psi \to \varphi$. Since $\mathcal{M}, w_i \asymp \mathbb{P}^+ \psi$, by semantics $\mathcal{M}, w_i \asymp \psi$ and there is $w_j \in \mathcal{N}(w_i)$ such that $M_j, w_j \leftrightarrow M_i|_\psi, w_i$. Since we assume $\mathcal{M}, w_i \asymp_O \neg \varphi$, it follows that $M_i|_\varphi, w_i \succeq M_j, w_j$. Thus, $M_i|_\varphi, w_i \succeq M_i|_\psi, w_i$ since $M_j, w_j \leftrightarrow M_i|_\psi, w_i$. Remember that we assume $\mathcal{M}, w_i \not\asymp_K \psi \to \varphi$. By semantics, there must be $v_i \in R_i(w_i)$ such that $\mathcal{M}, v_i \asymp \psi$ and $\mathcal{M}, v_i \not\asymp \varphi$. Since $M_i|_\varphi, w_i \succeq M_i|_\psi, w_i$, there must be $u_i \in R_i|_{\llcorner \varphi \rrcorner}^i(w_i)$ such that $M_i|_\psi, v_i \succeq M_i|_\varphi, u_i$. This implies that $V_i(v_i) = V_i(u_i)$. Thus $M_i, v_i \leftrightarrow M_i, u_i$ by Proposition 4.2. However, $\mathcal{M}, v_i \not\asymp \varphi$ and $\mathcal{M}, u_i \asymp \varphi$, which contradicts the fact that epistemic formulas are invariant under bisimulation.

3. We show that $\not\asymp_{S5} O^- \mathbb{P}^+ \to (\mathbb{P}^+ \to K(\to \mathbb{P}^+))$. Consider the *I*-deontic-epistemic model $\mathcal{M} = (\mathcal{S}, \mathcal{N})$ where $I = \{0, 1\}$ and:

- $\mathcal{S} = \{M_0, M_1\}$ with $M_0 = (W_0, R_0, V_0)$ and $M_1 = (W_1, R_1, V_1)$ where:

- $W_0 = \{w_0, v_0\}$ and $W_1 = \{w_1\}$;

- $R_0 = W_0 \times W_0$ and $R_1 = \{(w_1, w_1)\}$;

- for all atoms $p$, $V_0(p) = V_1(p) = \emptyset$.

- $\mathcal{N}(w_0) = \{w_1\}$ and $\mathcal{N}(x) = \emptyset$ for all $x \in (W_0 \cup W_1) \setminus \{w_0\}$.

$\mathcal{M}$ is an S4-deontic-epistemic-model and $\mathcal{M}, w_0 \not\leq_O \neg \mathbb{P}^+ \to (\mathbb{P}^+ \to K(\to \mathbb{P}^+))$. $\square$

<figure><img src="image_6.png" /><figcaption>Figure 4: The *I*-deontic-epistemic-model $\mathcal{M}$.</figcaption></figure>
## 4.4 Correspondence Between $\models$ and $\vDash$

In this section, we give a correspondence result between the general semantics $\vDash$ and the semantics $\models$ in Section 2.2. Specifically, we show that, when the language is restricted to $\mathcal{L}_{LPOA}^-$ below, $\vDash_{S5}$ gives the same logic as $\models$.

$$ \varphi ::= p \mid \neg \varphi \mid (\varphi \rightarrow \varphi) \mid K\varphi \mid \mathcal{O}^{-}\alpha \mid \mathbb{P}^{-}\alpha \mid \mathbb{P}^{+}\alpha \quad (\mathcal{L}_{LPOA}^{-}) $$

where $p \in \text{PROP}$ and $\alpha \in \mathcal{L}_{el}$. Therefore, to a certain extent, the semantics $\vDash$ generalizes the two-dimensional semantics $\models$. The correspondence does not hold when the deontic operators are allowed to be nested, as shown in Item 3 of Proposition 4.10. The reason is fundamental: we regard “epistemic states” as pointed Kripke models, which do not encode the receiver’s knowledge about the sender’s deontic status.

**Lemma 4.11.** For all models $M = (W, N, V)$, $w \in X \subseteq W$, and $\varphi \in \mathcal{L}_{LPOA}^-$, if $M, w, X \models \varphi$ then there is an S5-deontic-epistemic-model $\mathcal{M}$ and $w_0$ in $\mathcal{M}$ such that $\mathcal{M}, w_0 \models \varphi$.

*Proof.* By the definition of the canonical model (Definition 3.24) and the completeness result in the subsection 3.5, we can assume that $X = W$ and, for all $x \in W$ and $U \in N(x)$, $U = V(p)$ for some atom $p$.<fnref n="17" /> Let $I = (\wp(W) \setminus \{\emptyset\}) \cup \{0\}$. We construct the I-deontic-epistemic model $\mathcal{M} = (S, \mathcal{N})$ as follows:

- for each $i \in I \setminus \{0\}$, $M_i = (W_i, R_i, V_i)$ such that $W_i = i \times \{i\}$, $R_i = W_i \times W_i$, and $V_i(p) = (V(p) \cap i) \times \{i\}$;

- $M_0 = (W, R_0, V)$ such that $R_0 = W_0 \times W_0$;

- $\mathcal{N}(x) = \{(x, j) \mid j \in N(x)\}$ for all $x \in W$ (below we will denote $(x, j)$ by $x_j$) and $\mathcal{N}(x) = \emptyset$ if $x \notin W$;

- $w_0 = w$.

It is clear that $\mathcal{M}$ is an S5-deontic-epistemic-model. We show that, for all $x \in W$ and $\varphi \in \mathcal{L}_{LPOA}^-$, $M, x, W \models \varphi$ iff $\mathcal{M}, x \vDash \varphi$. This is done by induction on the structure of $\varphi$. Here we show only the cases for $\mathbb{P}^+\alpha$, $\mathbb{P}^-\alpha$, and $\mathcal{O}^-\alpha$:

**Case $\mathbb{P}^+\alpha$.** The direction from left to right is trivial. From right to left. Suppose $\mathcal{M}, x \vDash \mathbb{P}^+\alpha$. Then $\mathcal{M}, x \vDash \alpha$ and there exists $x_j \in \mathcal{N}(x)$ such that $M_j, x_j \stackrel{\leftrightarrow}{\models} M_0|_\alpha, x$. By the definition of $\mathcal{N}$, $j \in N(x)$ and $M_j, x_j$ is isomorphic to $M_0|_j, x$. Hence $M_0|_j, x \stackrel{\leftrightarrow}{\models} M_0|_\alpha, x$. Note that $j = V(p)$ for some atom $p$. Therefore, by Proposition 4.3, $j = [[\alpha]]_{\mathcal{M}}^0$. Note that, by the IH, $[[\alpha]]_{M,W} = [[\alpha]]_{\mathcal{M}}^0$. Thus $j = [[\alpha]]_{M,W}$. Since $j \in N(x)$, $[[\alpha]]_{M,W} \in N(x)$. That is $M, x, W \models \mathbb{P}^+\alpha$.

**Case $\mathbb{P}^-\alpha$.** The direction from left to right is trivial. From right to left. Suppose $\mathcal{M}, x \vDash \mathbb{P}^-\alpha$. Then $\mathcal{M}, x \vDash \alpha$ and there is $x_j \in \mathcal{N}(x)$ such that $M_0|_\alpha, x \succeq M_j, x_j$. By the definition of $\mathcal{N}$, $j \in N(x)$ and $M_j, x_j$ is isomorphic to $M_0|_j, x$. Hence $M_0|_\alpha, x \succeq M_0|_j, x$. By Proposition 4.3, $j \subseteq [[\alpha]]_{\mathcal{M}}^0$. Note that, by the IH, $[[\alpha]]_{M,W} = [[\alpha]]_{\mathcal{M}}^0$. Hence $j \subseteq [[\alpha]]_{M,W}$. Since $j \in N(x)$, $M, x, W \models \mathbb{P}^-\alpha$.

<footnote n="17">17. Specifically, if $\varphi$ is satisfiable under $\models$, then, by the soundness of $\mathbf{DLPOA}^\omega$, $\not\models_{\mathbf{DLPOA}^\omega} \neg\varphi$. Therefore, there is $x \in MCT$ containing $\varphi$. By the truth lemma, for the canonical model $M(x)$ of $x$, we have $M(x), x, W \models \varphi$.</footnote>
**Case** $\mathcal{O}^{-}\alpha$. The direction from left to right is trivial. From right to left. Suppose $M, x \models \mathcal{O}^{-}\alpha$. Then $M, x \models \alpha$ and, by the IH, $M, x, W \models \alpha$. Besides, let $Y \in N(x)$. By the definition of $\mathcal{N}$, $x_Y \in \mathcal{N}(x)$. Note that $M_Y, x_Y$ is isomorphic to $M_0|_Y, x$. Since we assume that $M, x \models \mathcal{O}^{-}\alpha$, $M_0|_{\alpha}, x \succeq M_Y, x_Y$. Hence $M_0|_{\alpha}, x \succeq M_0|_Y, x$. It then follows from Proposition 4.3 that $Y \subseteq [\alpha]^0_M$. Note that, by the IH, $[\alpha]_{M,W} = [\alpha]^0_M$. Hence $Y \subseteq [\alpha]_{M,W}$. Since $Y$ is arbitrary, $M, x, W \models \mathcal{O}^{-}\alpha$. $\square$

**Lemma 4.12.** For all S5-deontic-epistemic-model $\mathcal{M} = (\mathcal{S}, \mathcal{N})$, $w_0$ in $\mathcal{M}$, and $\varphi \in \mathcal{L}_{LPOA}^-$, if $\mathcal{M}, w_0 \models \varphi$ then there is a model $\mathcal{M} = (W, N, V)$ and $w \in X \subseteq W$ such that $M, w, X \models \varphi$.

*Proof.* Let $S = \{M_i = (W_i, R_i, V_i) \mid i \in I\}$. We construct the model $\mathcal{M} = (W, N, V)$ s.t.:

- $W = X = R_0(w_0)$

- for all $x \in W$, $N(x) = \{U \subseteq W \mid x \in U \& \exists x_i \in \mathcal{N}(x) \text{ such that } M_0|_U, x \triangleleft M_i, x_i\}$

- for all atoms $p, V(p) = V_0(p) \cap W$

- $w = w_0$

We show that, for all $x \in W$ and $\varphi \in \mathcal{L}_{LPOA}^-$, $M, x, W \models \varphi$ iff $M, x \approx \varphi$. This is done by induction on the structure of $\varphi$. Here we show only the cases for $\mathbb{P}^+\alpha$, $\mathbb{P}^-\alpha$, and $\mathcal{O}^-\alpha$:

**Case** $\mathbb{P}^+\alpha$. From left to right. Suppose $M, x, W \models \mathbb{P}^+\alpha$. Then $M, x, W \models \alpha$ and, by the IH, $M, x \models \alpha$. On the other hand, since $[\alpha]_{M,W} \in N(x)$, by the definition of $N$, there is $x_i \in \mathcal{N}(x)$ such that $M_0|_{[\alpha]_{M,W}}, x \triangleleft M_i, x_i$. Note that, by the IH, $[\alpha]_{M,W} = [\alpha]^0_M \cap W$. Hence $M_0|_{\alpha}, x \triangleleft M_i, x_i$ (note that $M_0|_{\alpha}, x \triangleleft M_0|_{[\alpha]^0_M \cap W}, x$). Therefore $M, x \models \mathbb{P}^+\alpha$. From right to left. Suppose $M, x \models \mathbb{P}^+\alpha$. Then $M, x \models \alpha$ and there is $x_j \in \mathcal{N}(x)$ such that $M_j, x_j \triangleleft M_0|_{\alpha}, w$. Hence $M_j, x_j \triangleleft M_0|_{[\alpha]^0_M \cap W}, w$. Since $[\alpha]_{M,W} = [\alpha]^0_M \cap W$ and $M, x, W \models \alpha$ by the IH, $[\alpha]_{M,W} \in N(x)$ by the definition of $N$. Therefore $M, x, W \models \mathbb{P}^+\alpha$.

**Case** $\mathbb{P}^-\alpha$. From left to right. Suppose $M, x, W \models \mathbb{P}^-\alpha$. Then $M, x, W \models \alpha$. By the IH, $M, x \models \alpha$. Besides, there is $Y \in N(x)$ such that $Y \subseteq [\alpha]_{M,W}$. From the definition of $N$, there must be $x_i \in \mathcal{N}(x)$ such that $M_0|_Y, x \triangleleft M_i, x_i$. Then $M_0|_{[\alpha]_{M,W}}, x \succeq M_i, x_i$. Note that $[\alpha]_{M,W} = [\alpha]^0_M \cap W$ by the IH. Hence $M_0|_{\alpha}, x \succeq M_i, x_i$. Therefore, $M, x \models \mathbb{P}^-\alpha$. From right to left. Suppose $M, x \models \mathbb{P}^-\alpha$. Then $M, x \models \alpha$ and there is $x_j \in \mathcal{N}(x)$ s.t. $M_0, x \succeq M_j, x_j$ and $M_0|_{\alpha}, x \succeq M_j, x_j$. It follows that there must be some $x \in U \subseteq W$ such that $M_0|_U, x \triangleleft M_j, x_j$. By the definition of $N$, $U \in N(x)$. Since $M_0|_{\alpha}, x \triangleleft M_0|_{[\alpha]^0_M \cap W}, x$, $M_0|_{[\alpha]^0_M \cap W}, x \succeq M_0|_U, x$. By Proposition 4.3, $U \subseteq [\alpha]^0_M \cap W$. Using the IH, $U \subseteq [\alpha]_{M,W}$. Hence $M, x, W \models \mathbb{P}^-\alpha$.

**Case** $\mathcal{O}^-\alpha$. From left to right. Suppose $M, x, W \models \mathcal{O}^-\alpha$. Then $M, x, W \models \alpha$ and, by the IH, $M, x \models \alpha$. Let $x_j \in \mathcal{N}(x)$ be such that $M_0, x \succeq M_j, x_j$. Then $M_0|_Y, x \triangleleft M_j, x_j$ for some $x \in Y \subseteq W$. By the definition of $N$, $Y \in N(x)$. Thus $Y \subseteq [\alpha]_{M,W}$ by the assumption. Hence $Y \subseteq [\alpha]^0_M$ by the IH. Thus $M_0|_{\alpha}, x \succeq M_j, x_j$. Since $x_j$ is arbitrary, $M, x \models \mathcal{O}^-\alpha$. From right to left. Suppose $M, x \models \mathcal{O}^-\alpha$. Then $M, x \models \alpha$ and, by the IH, $M, x, W \models \alpha$. Besides, let $Y \in N(x)$. By the definition of $N$, there is $x_j \in \mathcal{N}(x)$ such that $M_0|_Y, x \triangleleft M_j, x_j$. Since we assume $M, x \models \mathcal{O}^-\alpha$, $M_0|_{\alpha}, x \succeq M_j, x_j$. Then $M_0|_{\alpha}, x \succeq M_0|_Y, x$. Thus $M_0|_{[\alpha]^0_M \cap W}, x \succeq M_0|_Y, x$. This implies that $Y \subseteq [\alpha]^0_M \cap W$ by Proposition 4.3. Using the IH, $Y \subseteq [\alpha]_{M,W}$. Hence $M, x, W \models \mathcal{O}^-\alpha$. $\square$
Given Lemmas 4.11 and 4.12, the next theorem follows immediately:

**Theorem 5 (Correspondence).** For all formulas $\varphi \in \mathcal{L}_{LPOA}^{-}$, $\varphi$ is satisfiable under $\models_{S5}$ if and only if $\varphi$ is satisfiable under $\models$ in Section 2.2.

It also follows that the axiomatization **LPOA** (and **DLPOA**) restricted to $\mathcal{L}_{LPOA}^{-}$ is sound and weakly complete with respect to $\models_{S5}$. The complete axiomatizations of $\models$, $\models_{4}$, $\models_{S4}$, and $\models_{S4.4}$ remain still open problems.

## 5. Related Work

*Deontic logic for epistemic actions.* Our paper aims to bring together two areas of philosophical logic: deontic logic and dynamic epistemic logic. Several attempts to develop deontic logic for epistemic actions can be found in the literature (e.g., Aucher et al., 2011, 2010; Balbiani & Seban, 2011; Li et al., 2022).

As mentioned in the Introduction, Aucher et al. (2011) propose a dynamic modal logic for reasoning about which information is permitted to be sent (announced) by a security monitor in order to comply with a privacy policy. Our paper and Aucher et al.’s (2011) share the same idea of defining permitted and obligatory announcements in terms of the deontic status of the receiver’s epistemic state after announcements. For example, according to Aucher et al. (2011), a message $\varphi$ is a permitted message for the sender if the epistemic state after sending $\varphi$ is compliant with respect to a given privacy policy. Since privacy policies specify which epistemic states are ideal, the notion of “permitted message” in Aucher et al.’s (2011) work corresponds to our operator $\mathbb{P}^{+}\varphi$ for strongly permitted announcements. Aucher et al. (2011) also define the obligatory message of a security monitor as the *minimal* informative message such that, by sending it, compliance with privacy policy is restored. This notion of “obligatory message” can be roughly seen as the operator $\mathbb{O}^{+}\varphi$ in our paper. However, our interpretation of $\mathbb{O}^{+}\varphi$ is that “Announcing $\varphi$ is the *least* informative (strongly) permitted announcement”. In cases where the least informative permitted announcement does not exist, these two notions do make a difference. For instance, in Example 2.2, both $n \wedge p$ and $n \wedge e$ are minimal informative permitted announcements, but neither is the least informative. In such a case, the behavior of our operator $\mathbb{O}^{+}\varphi$ is more consistent with our intuition, as it predicts that Alice is obliged to announce neither $n \wedge p$ nor $n \wedge e$. Despite the similarities between the core ideas, the main difference between our paper and Aucher et al.’s (2011) is as follows: Since a privacy policy is represented by a finite and consistent set of formulas (like $OKq$ or $Kp \rightarrow PKq$), Aucher et al. (2011) can express the notion of compliance as a single compound formula. Thus, they easily get a complete axiomatization for their logic. This does not work for LPOA and DLPOA. We think that our axiomatization better captures valid reasoning principles of permitted and obligatory announcements.

Inspired by Aucher et al. (2011), a logic for permitted announcements has been developed by Li et al. (2022). In that paper, the so-called “neighbourhood epistemic model” is employed to provide the semantics for permitted announcements. Formally, they are structures $M = (W, \sim, N, V)$ where $W, \sim$, and $V$ are the same as in standard epistemic models (S5 models) and $N: W \rightarrow \wp(\wp(W))$ is a neighbourhood function that assigns a set of *ideal* epistemic states to each possible world. Observed that the public announcement
of a proposition $\varphi$ will restrict the current epistemic state to only those possible worlds satisfying $\varphi$, Li et al. (2022) introduce an operator $\mathbb{P}\varphi$ for permitted announcements that is true in a possible world $w$ iff the epistemic state after the announcement of $\varphi$ is an element of $N(w)$. This corresponds exactly to the operator $\mathbb{P}^+\varphi$ in our paper. Our paper extends Li et al.'s (2022) work by incorporating the notion of obligatory announcements.

Another work on logics of permitted and obligatory announcements is done by Balbiani and Seban (2011). In that paper, two binary operators $P(\psi, \varphi)$ and $O(\psi, \varphi)$ are introduced to express that “($\psi$ is true and) after announcing $\psi$, it is permitted/obligatory to announce $\varphi$”. Conceptually, they express the same meaning as the formulas $\langle\psi\rangle\mathbb{P}^-\varphi$ and $\langle\psi\rangle\mathbb{O}^-\varphi$ in DLPOA, respectively. Translated in this way, it can also be verified that all the axioms and rules of the logic POPAL developed by Balbiani and Seban (2011) are valid in DLPOA, except for the axiom called “Obligation and prohibition”: $\psi\wedge O(\psi, \varphi)\wedge\neg P(\psi, \varphi) \leftrightarrow \psi\wedge\neg P(\psi, \top)$.<fnref n="18" /> But the semantics for $P(\psi, \varphi)$ and $O(\psi, \varphi)$ is quite different from ours. According to Balbiani and Seban (2011), a ternary relation $\mathcal{P} \subseteq S \times \wp(S) \times \wp(S)$ is used to provide the semantics for $P(\psi, \varphi)$ and $O(\psi, \varphi)$ such that:

- $\mathcal{M}, s \models P(\psi, \varphi)$ iff for some $(s, [[\psi]]_{\mathcal{M}}, S'') \in \mathcal{P}, S'' \subseteq [[\langle\psi\rangle\varphi]]_{\mathcal{M}}$

- $\mathcal{M}, s \models O(\psi, \varphi)$ iff for all $(s, [[\psi]]_{\mathcal{M}}, S'') \in \mathcal{P}, S'' \subseteq [[\langle\psi\rangle\varphi]]_{\mathcal{M}}$

where $S$ is the domain of the model $\mathcal{M}$. The main difference here lies in the fact that our semantics for $\mathbb{P}^-\varphi$ and $\mathbb{O}^-\varphi$ is specific to the receiver's knowledge, whereas the above is not. This is reflected in the fact that the logic POPAL developed by Balbiani and Seban (2011) lacks interaction axioms between the two deontic operators $P(-, -)$ and $O(-, -)$ and the $K$ operator for receiver's knowledge, e.g., $K(\varphi \rightarrow \psi) \rightarrow (\mathbb{P}^-\varphi \rightarrow \mathbb{P}^-\psi)$. We argue that our logical framework DLPOA is more suitable for reasoning about obligatory announcements in the context of, e.g., privacy policy compliance, because the receiver's initial knowledge is crucial for the sender's decision on which information should be disclosed, as suggested by Examples 1.1 and 2.3. Another difference between our paper and Balbiani and Seban's (2011) is that, like Aucher et al. (2011) and Li et al. (2022), Balbiani and Seban (2011) do not make a distinction between weakly and strongly permitted announcements. The weakening of permitted announcements, $P(p \wedge q) \rightarrow Pp$, is a valid principle in Balbiani and Seban's (2011) work. The announcement of $p$ provides less information than the announcement of $p \wedge q$. However, sometimes ignorance about some facts may be forbidden, or in other words, knowledge of these facts is obligatory. For example, in many countries, it is not permitted for a pharmacist to only advertise over-the-counter medicines to customers while not telling them about the possible side effects. This phenomenon can be explained only if we distinguish between weakly and strongly permitted announcements: the weakening of permitted announcements is valid only for weakly permitted announcements, while failing for strongly ones.

van Benthem et al. (2009) propose a logic for protocols in dynamic epistemic logic. We can interpret it as a logic for permitted epistemic actions. We only mention here that the permitted epistemic actions (represented by the event models of dynamic epistemic

<footnote n="18">18. Specifically, the implication from right to left fails. This is because, in the truth definition of $\mathbb{O}^-\varphi$, we require that $\varphi$ must be true. If we remove such a requirement, (the translated version of) this axiom would be valid.</footnote>
logic) are listed in the protocols, and there is no notion of “ideal epistemic states” in their
framework. Recently, a logic called LRK was developed by Li and Markovich (2023) for
reasoning about the power to know, the obligatory announcements, and the dynamics of
questions and public announcements. The operator for obligatory announcements in their
work has the same semantics as ours.

*Deontic logic about knowledge and belief.* Our paper aims to derive permitted and obligatory announcements from the permitted and obligatory knowledge for the receiver. Although the notion of permitted and obligatory knowledge does not appear in our formal language, we implicitly assume in the semantics that the “ideal epistemic states” (i.e., the neighbourhood function *N*) are determined by permitted and obligatory knowledge prescribed by certain privacy policies. While it is meaningful and interesting to extend our logical framework to include the notion of permitted and obligatory knowledge, we do not consider it in this paper. This is because there are fundamental problems in combining deontic logic and epistemic logic, as we shall discuss below.

The notions of permission and prohibition to know have been investigated by Cuppens and Demolombe (1996) in the context of database security. In their framework, two modalities $PK\varphi$ and $FK\varphi$ are introduced to express that “some users are permitted/forbidden to know that the database believes $\varphi$”.<fnref n="19" /> There are two binary relations in their models, one for knowledge and one for obligation. $PK\varphi$ is true at a world $w$ if there is an ideal world of $w$ in which $K\varphi$ holds and similarly for $FK\varphi$.

In Cuppens and Demolombe's (1996) formal language, the deontic and epistemic op-
erators are not allowed to combine with each other freely. One reason for this constraint
is Åqvist's paradox of epistemic obligation (Åqvist, 1967). Simply speaking, this paradox
concerns a problematic schema $OK\varphi \rightarrow O\varphi$ ("if $\varphi$ ought to be known, then it ought to
be the case"), which is a theorem of any normal bimodal logic combining knowledge and
obligation where knowledge is assumed to be veridical. To see the absurdity of this schema,
consider a scenario where a bank is being robbed. As a guard of the bank, Jones ought to
know the bank is being robbed. However, this does not imply that the bank ought to be
robbed. Several solutions to Åqvist's paradox have been proposed in the literature (e.g.,
Feldman, 1990; Hulstijn, 2008; Åqvist, 2014; Li, 2023).

Recently, there are also works studying deontic concepts of knowledge other than “ought to know”, like “the right to know” (Markovich & Roy, 2021a, 2021b; Li & Markovich, 2023). The notion of knowledge-based obligation has also received some attention (Horty, 2001; Pacuit et al., 2006; Grossi et al., 2021).

*Dynamic deontic logic.* Our work shares the same spirit with dynamic deontic logic (Meyer, 1987). In dynamic deontic logic, an action is permitted if performing it would not lead to getting into trouble (i.e., $P\alpha := \neg[\alpha]V$). Thus, permissions about actions are reduced to the normative status after executing the actions. Analogously, in our framework, an announcement is permitted if the epistemic state after the announcement is ideal (has no violation). However, in dynamic deontic logic, the definition of obligatory actions is more complicated, as it involves the notion of “the negation of an action”, which is doubted by several authors (Broersen, 2004; Sun & Huimin, 2014; Ju & van Eijck, 2016). In our paper,

<footnote n="19">19. We reformulate their notations for a clear presentation.</footnote>
we define obligatory announcements in a different way than employing the notion of “the negation of an announcement”.

van der Meyden (1996) criticize Meyer’s dynamic deontic logic for it contains a problem-
atic validity: ⟨α⟩Pβ → P(α; β). The idea is that the action α may be a forbidden action.
Thus, as per their example, even if we are permitted to remain silent after shooting the
president, we are not permitted to shoot the president and remain silent. In DLPOA, we
have an analog: ⟨ϕ⟩P⁺ψ → P⁺⟨ϕ⟩ψ. However, in the consequent of the implication, what
falls into the scope of the operator P⁺ is not a sequel announcement but a single announce-
ment of formula ⟨ϕ⟩ψ. The free choice paradox (Ross, 1941; Dignum, Meyer, & Wieringa,
1994) is another paradox concerning dynamic deontic logic. But in our framework, there is
no notion of a choice between two announcements.

6. Conclusion

We formalize the notions of “permitted and obligatory announcements” by defining them
in terms of the ideal epistemic states (of the receiver). We propose two logics LPOA and
DLPOA to reason about permitted and obligatory announcements in both static and dy-
namic contexts. These two logics are completely axiomatized, and we also explore general-
izations where the receiver’s knowledge or belief is characterized by non-S5 logics. Our paper
makes two main contributions to the formalization of permitted and obligatory announce-
ments: First, we clarify the interplay between permitted and obligatory announcements
(of the sender) and the receiver’s knowledge. Second, we distinguish between weakly and
strongly permitted announcements.

There are many directions for future research. The most crucial is to find complete axiomatizations for the general semantics in Section 4. Another unsolved issue is whether the logics LPOA and DLPOA are decidable. Other issues for future research include how to generalize our frameworks to the multi-agent case, how to incorporate operators for permitted and obligatory knowledge.

Acknowledgments

A preliminary version of this paper has been published in the Proceedings of the 19th In-
ternational Conference on Principles of Knowledge Representation and Reasoning (Li et al.,
2022). We thank three anonymous referees of this journal for their valuable comments which
clarified some conceptual confusion and improved the exposition of this paper. Thanks are
also given to Leendert van der Torre for discussions and comments on earlier drafts of
this paper. This work was supported by the Fonds National de la Recherche Luxembourg
through the project Deontic Logic for Epistemic Rights (OPEN O20/14776480).

References

Anglberger, A. J., Gratzl, N., & Roy, O. (2015). Obligation, free choice, and the logic of weakest permissions. *The Review of Symbolic Logic*, 8(4), 807–827.
Aucher, G. (2014). Principles of knowledge, belief and conditional belief. In Heinzmann, G., Musiol, M., Rebuschi, M., & Trognon, A. (Eds.), *Interdisciplinary Works in Logic, Epistemology, Psychology and Linguistics*, Vol. 3 of Logic, Argumentation and Reasoning. Springer.

Aucher, G., Boella, G., & van der Torre, L. (2010). Prescriptive and descriptive obligations in dynamic epistemic deontic logic. In *AI approaches to the complexity of legal systems (AICOL 2009)*, Vol. LNAI 6237, pp. 150–161.

Aucher, G., Boella, G., & van der Torre, L. (2011). A dynamic logic for privacy compliance. *Artificial Intelligence and Law*, 19(2), 187.

Balbiani, P., & Seban, P. (2011). Reasoning about permitted announcements. *Journal of Philosophical Logic*, 40(4), 445–472.

Balbiani, P., Baltag, A., van Ditmarsch, H., Herzig, A., Hoshi, T., & de Lima, T. (2008). ‘Knowable’ as ‘known after an announcement’. *The Review of Symbolic Logic*, 1(3), 305–334.

Baltag, A., & Moss, L. S. (2004). Logics for epistemic programs. *Synthese*, 139(2), 165–224.

Barth, A., Datta, A., Mitchell, J., & Nissenbaum, H. (2006). Privacy and contextual integrity: framework and applications. In *2006 IEEE Symposium on Security and Privacy*, pp. 15 pp.–198.

Blackburn, P., de Rijke, M., & Venema, Y. (2001). *Modal Logic*, Vol. 53 of *Cambridge Tracts in Theoretical Computer Science*. Cambridge University Press.

Bonatti, P., Kraus, S., & Subrahmanian, V. (1995). Foundations of secure deductive databases. *IEEE Transactions on Knowledge and Data Engineering*, 7(3), 406–422.

Bozzelli, L., van Ditmarsch, H., French, T., Hales, J., & Pinchinat, S. (2014). Refinement modal logic. *Information and Computation*, 239, 303–339.

Broersen, J. (2004). Action negation and alternative reductions for dynamic deontic logics. *Journal of Applied Logic*, 2(1), 153–168. The Sixth International Workshop on Deontic Logic in Computer Science.

Cuppens, F., & Demolombe, R. (1996). A deontic logic for reasoning about confidentiality. In Brown, M. A., & Carmo, J. (Eds.), *Deontic Logic, Agency and Normative Systems*, pp. 66–79, London. Springer London.

Dabrowski, A., Moss, L. S., & Parikh, R. (1996). Topological reasoning and the logic of knowledge. *Annals of Pure and Applied Logic*, 78(1), 73–110. Papers in honor of the Symposium on Logical Foundations of Computer Science, "Logic at St. Petersburg".

Dignum, F., Meyer, J.-J. Ch., & Wieringa, R. J. (1994). Contextual permission: A solution to the free choice paradox. In *Proceedings of the 2nd International Workshop on Deontic Logic in Computer Science (DEON 1994)*, pp. 107–135.

Dwork, C. (2006). Differential privacy. In Bugliesi, M., Preneel, B., Sassone, V., & Wegener, I. (Eds.), *Automata, Languages and Programming*, pp. 1–12, Berlin, Heidelberg. Springer Berlin Heidelberg.

Feldman, F. (1990). A simpler solution to the paradoxes of deontic logic. *Philosophical Perspectives*, 4, 309–341.
Gargov, G., & Passy, S. (1990). *A note on Boolean modal logic*, pp. 299–309. Springer US,
Boston, MA.

Gerbrandy, J., & Groeneveld, W. (1997). Reasoning about information change. *Journal of Logic, Language, and Information*, 6(2), 147–169.

Goldblatt, R. (1982). *Axiomatising the Logic of Computer Programming*. Springer-Verlag.

Grossi, D., Kooi, B., Su, X., & Verbrugge, R. (2021). How knowledge triggers obligation. In Ghosh, S., & Icard, T. (Eds.), *Logic, Rationality, and Interaction*, pp. 201–215, Cham. Springer International Publishing.

Hilpinen, R., & McNamara, P. (2013). Deontic logic: A historical survey and introduction. In Gabbay, D., Horty, J., Parent, X., van der Meyden, R., & van der Torre, L. (Eds.), *Handbook of Deontic Logic and Normative Systems*, pp. 3–136. College Publications.

Horty, J. F. (2001). *Agency and Deontic Logic*. Oxford University Press.

Hulstijn, J. (2008). Need to know: Questions and the paradox of epistemic obligation. In van der Meyden, R., & van der Torre, L. (Eds.), *Deontic Logic in Computer Science*, pp. 125–139, Berlin, Heidelberg. Springer Berlin Heidelberg.

Jafari, M., Safavi-Naini, R., Fong, P. W. L., & Barker, K. (2014). A framework for expressing and enforcing purpose-based privacy policies. *ACM Trans. Inf. Syst. Secur.*, 17(1).

Ju, F., & van Eijck, J. (2016). To do something else. In *Deontic Logic and Normative Systems. 13th International Conference, DEON 2016*, pp. 109–122.

Lenzen, W. (1978). *Recent work in epistemic logic*. North Holland Publishing Company, Amsterdam.

Lenzen, W. (1995). On the semantics and pragmatics of epistemic attitudes. In Laux, A., & Wansing, H. (Eds.), *Knowledge and belief in philosophy and AI*, pp. 181–197, Berlin. Akademie Verlag.

Li, X. (2023). The logic of epistemic obligation and two-dimensional semantics. In *Trends in Logic XXIII: Bridges between Logic, Ethics and Social Sciences (BLESS)*.

Li, X., Gabbay, D., & Markovich, R. (2022). Dynamic deontic logic for permitted announcements. In *Proceedings of the 19th International Conference on Principles of Knowledge Representation and Reasoning*, pp. 226–235.

Li, X., & Markovich, R. (2023). A dynamic logic of the right to know. In Maranhão, J., Peterson, C., Straßer, C., & van der Torre, L. (Eds.), *The 16th International Conference on Deontic Logic and Normative Systems (DEON 2023)*, pp. 39–56. College Publications.

Machanavajjhala, A., Kifer, D., Gehrke, J., & Venkitasubramaniam, M. (2007). L-diversity: Privacy beyond k-anonymity. *ACM Trans. Knowl. Discov. Data*, 1(1), 3–es.

Markovich, R., & Roy, O. (2021a). Formalizing the right to know: Epistemic rights as normative positions. In *The First International Workshop on Logics for New-Generation Artificial Intelligence (LNGAI 2021)*.

Markovich, R., & Roy, O. (2021b). A logical analysis of freedom of thought. In *Deontic Logic and Normative Systems. 14th International Conference, DEON 2018*, pp. 323–338.
Meyer, J.-J. C. (1987). A different approach to deontic logic: deontic logic viewed as a variant of dynamic logic.. *Notre Dame Journal of Formal Logic*, **29**(1), 109 – 136.

Pacuit, E. (2017). *Neighborhood Semantics for Modal Logic*. Springer Cham.

Pacuit, E., Parikh, R., & Cogan, E. (2006). The logic of knowledge based obligation. *Synthese*, **149**(2), 311–341.

Passy, S., & Tinchev, T. (1991). An essay in combinatory dynamic logic. *Information and Computation*, **93**(2), 263–332.

Plaza, J. (1989). Logics of public communications. In Emrich, M., Pfeifer, M., Hadzikadic, M., & Ras, Z. (Eds.), *Proceedings of the 4th International Symposium on Methodologies for Intelligent Systems*, pp. 201–216.

Ross, A. (1941). Imperatives and logic. *Theoria*, **7**, 53–71.

Sun, X., & Huimin, D. (2014). Stratified action negation for dynamic logic. In *26th BENELUX Conference on Artificial Intelligence (BNAIC)*.

Sweeney, L. (2002). k-anonymity: A model for protecting privacy. *International Journal of Uncertainty, Fuzziness and Knowledge-Based Systems*, **10**(05), 557–570.

van Benthem, J. (1979). Minimal deontic logics. *Bulletin of the Section of Logic*, **8**(1), 36–42.

van Benthem, J., Gerbrandy, J., Hoshi, T., & Pacuit, E. (2009). Merging frameworks for interaction. *Journal of Philosophical Logic*, **38**(5), 491–526.

Van De Putte, F. (2017). “That will do”: Logics of deontic necessity and sufficiency. *Erken-
ntnis*, **82**(3), 473–511.

van der Meyden, R. (1996). The dynamic logic of permission. *Journal of Logic and Com-
putation*, **6**(3), 465–479.

van Ditmarsch, H., van der Hoek, W., & Kooi, B. (2008). *Dynamic Epistemic Logic*.
Springer, Dordrecht.

Yalcin, S. (2007). Epistemic modals. *Mind*, **116**(464), 983–1026.

Åqvist, L. (1967). Good samaritans, contrary-to-duty imperatives, and epistemic obligations. *Noûs*, **1**(4), 361–379.

Åqvist, L. (2014). Deontic tense logic with historical necessity, frame constants, and a solution to the epistemic obligation paradox (the “knower”). *Theoria*, **80**(4), 319–349.