Preservation in Dynamic Epistemic Logic

Abstract

This article examines the preservation of structural properties in epistemic and doxastic logic, with a particular focus on action model logic and the dynamics of group belief. Two central questions guide the analysis: (a) which frame conditions remain invariant under the execution of epistemic actions? and (b) do group conditions—properties allowing groups to be modeled as unified agents—persist after such actions? The study further explores specific subclasses of epistemic actions, including public announcements and unconditional actions, highlighting their distinctive preservation features. These findings contribute to a deeper understanding of the logical foundations of epistemic and doxastic reasoning, particularly within dynamic multi-agent frameworks.

1. Introduction

Epistemic and doxastic logic serve as foundational frameworks for modeling knowledge and belief, employing Kripke models to represent agents’ uncertainty across possible worlds (Fagin et al., 1995; Hintikka, 1962; Meyer & van der Hoek, 1995). Within this paradigm, three canonical notions of group belief emerge: mutual belief, common belief, and distributed belief. ¹ Specifically, each individual $i$ is associated with a binary accessibility relation $R_i$ , capturing their uncertainty between worlds. For a group $G$ , these individual relations give rise to three distinct group-level relations: $R_G^E=\bigcup _{i\in G}{R}_i$ for mutual uncertainty, $R_G^C=\underset{i\in G}{⨄}{R}_i$ (the transitive closure of $R_G^E$ ) for common uncertainty, and $R_G^D=\bigcap _{i\in G}{R}_i$ for distributed uncertainty. These constructions utilize the set-theoretic operations $\cup$ , $\uplus$ and $\cap$ , which we call group operations on a Kripke frame. When a group is conceptualized as a collective agent, these definitions impose specific group conditions on epistemic and doxastic structures. While we focus on these group operations in this article, we note that there are other notions of group belief, such as somebody-believes (Ågotnes & Wáng, 2021), that are not captured by such operations.

While the properties of frames in modal logic are extensively studied, their preservation under group operations in epistemic and doxastic logic raises important and subtle questions. Recent work indicates that frame conditions are not necessarily preserved when moving from individual to group-level uncertainty (Ågotnes & Wáng, 2020, 2021). For instance, starting from a KD45 frame—defined by seriality, transitivity, and Euclidicity—the resulting frames for mutual, common, and distributed uncertainty differ significantly. Specifically, mutual uncertainty preserves only seriality, common uncertainty yields KD4 properties (seriality and transitivity, potentially losing Euclidicity), and distributed uncertainty yields K45 properties (transitivity and Euclidicity, potentially losing seriality). Consequently, none of these derived group-level notions fully retain the original KD45 conditions that characterize individual belief. By contrast, S5 frames, characterized by equivalence relations, preserve their defining properties across mutual, common, and distributed uncertainty.

This article extends the analysis of frame and group conditions to the setting of action model logic, also known as dynamic epistemic logic, a prominent framework for analyzing the logical dynamics of epistemic and doxastic scenarios (Baltag & Moss, 2004; Baltag et al., 1998; van Ditmarsch et al., 2007). Our investigation centers around two primary research questions:

(a)

Which frame conditions are preserved under epistemic actions? Specifically, when epistemic actions transform a model satisfying certain frame conditions, does the resulting model retain these conditions? This question is addressed in Section 3.1, with a generalized result provided in Section 3.2.

(b)

Are the three group conditions—mutual, common, and distributed—preserved under epistemic actions? This question is analyzed in Section 3.3.

Public announcement logic (Plaza, 1989), a well-known sublogic of action model logic, studies a restricted class of epistemic actions—public announcements. While public announcements behave similarly to general actions regarding frame condition preservation, they diverge in their preservation of group conditions, a contrast explored in Section 4.1. Additionally, in Section 4.2, we identify another special class of actions—unconditional actions, i.e., actions without preconditions—which exhibit distinct preservation properties diverging from both general actions and public announcements. Notably, seriality—a frame condition corresponding syntactically to the consistency of beliefs—is typically not preserved under public announcements. Unconditional actions, however, do preserve seriality.

These findings carry implications for the development and application of action model logic, as we discuss in the concluding section.

2. Definitions and Conventions

This section introduces key definitions and conventions used throughout the article. We present the definitions of epistemic frames, models, actions, execution of actions, and the language and semantics of action model logic. We also introduce standard frame and group conditions from modal logic, generalized appropriately to action models.

A countably infinite set of propositional atoms, denoted prop, and a finite set of agents, denoted ag, are assumed throughout. The set of all non-empty groups of agents is defined as $\mathrm{gr}=\mathrm{\wp }(\mathrm{ag})\setminus \{\mathrm{\varnothing }\}$ , where $\mathrm{\wp }(\mathrm{ag})$ is the power set of ag.

2.1. Extended Frames, Models, and Actions

We start by introducing generalized definitions that extend classical Kripke structures.

A frame is a pair $(W,R)$ , where: (i) $W$ is a (possibly empty) domain of states ² , and (ii) $R$ is a quadruple $(R^I,R^D,R^E,R^C)$ consisting of: an individual uncertainty function $R^I:\mathrm{ag}\to \mathrm{\wp }(W\times W)$ , assigning each agent $i$ a binary relation $R^I(i)$ , and group uncertainty functions $R^D,R^E,R^C:\mathrm{gr}\to \mathrm{\wp }(W\times W)$ , assigning each group $G$ binary relations $R^D(G)$ , $R^E(G)$ and $R^C(G)$ , respectively.

For convenience, we write $R_i$ , $R_G^D$ , $R_G^E$ and $R_G^C$ instead of $R^I(i)$ , $R^D(G)$ , $R^E(G)$ and $R^C(G)$ , respectively. When $G$ is explicitly given as a simple set, we remove brackets and comma(s) from subscripts (e.g., $R_a^D$ instead of $R_{\{a\}}^D$ , and $R_{ab}^C$ instead of $R_{\{a,b\}}^C$ ).

A model is a triple $M=(W,R,V)$ , where $(W,R)$ is a frame (the base frame of $M$ ) and $V:\mathrm{prop}\to \mathrm{\wp }(W)$ is a valuation function assigning set of states to propositional atoms. A pair $(M,s)$ , with $s\in W$ , is called a pointed model.

Given a language $\mathcal{L}$ over propositional atoms prop and agents ag, an action $\mathsf{M}$ is a triple $(\mathsf{W},\mathsf{R},\mathsf{p}\mathsf{r}\mathsf{e})$ , where $(\mathsf{W},\mathsf{R})$ is a finite frame (the base frame of $\mathsf{M}$ ) and $\mathsf{p}\mathsf{r}\mathsf{e}:\mathsf{W}\to \mathcal{L}$ is a precondition function assigning formulas to action states. We write $(\mathsf{M},\mathsf{s})$ , with $\mathsf{s}\in \mathsf{W}$ , to denote a pointed action.

Remark 1

Classical structures from the epistemic logic literature emerge naturally as special cases of our definitions:

(a) A standard Kripke frame $(W,R)$ , with $R:\mathrm{ag}\to \mathrm{\wp }(W\times W)$ , corresponds exactly to our frame definition by setting $R^I=R$ , $R_G^D:=\bigcap _{i\in G}{R}_i$ , $R_G^E:=\bigcup _{i\in G}{R}_i$ , and $R_G^C:=\underset{i\in G}{⨄}{R}_i$ , where $\underset{i\in G}{⨄}{R}_i$ is the transitive closure of $R_G^E=\bigcup _{i\in G}{R}_i$ . Similarly, standard Kripke models and classical action models (also called “action structures” Baltag et al., 1998) are special cases of our definitions.

(b) A pseudo model Fagin et al. (1992); Wáng and Ågotnes (2013) is also a model by the above definition. It differs from a Kripke model by treating distributed relations $R_G^D$ as primitive, while defining only mutual and common uncertainty relations from individual ones.

2.2. Languages

The base language—the language of classical multi-agent epistemic logic—is denoted by ${\mathcal{L}}_0$ . Its extensions, denoted ${\mathcal{L}}_n$ for each natural number $n$ , incorporate action operators. These languages are defined inductively as follows (with $p\in \mathrm{prop}$ , $i\in \mathrm{ag}$ and $G\in \mathrm{gr}$ ):

$$\begin{array}{ll}({\mathcal{L}}_0)& \varphi ::=p\mid \mathrm{\neg }\varphi \mid (\varphi \wedge \varphi )\mid B_i\varphi \mid D_G\varphi \mid E_G\varphi \mid C_G\varphi \\ ({\mathcal{L}}_{n+1})& \varphi ::=p\mid \mathrm{\neg }\varphi \mid (\varphi \wedge \varphi )\mid B_i\varphi \mid [{\mathsf{M}}^{{\mathcal{L}}_n},\mathsf{s}]\varphi \mid D_G\varphi \mid E_G\varphi \mid C_G\varphi \end{array}$$

Here, $({\mathsf{M}}^{{\mathcal{L}}_n},\mathsf{s})$ denotes a pointed action whose preconditions are formulas from language ${\mathcal{L}}_n$ . The language that accommodates formulas of arbitrary complexity is denoted by (where $\mathbb{N}$ are the natural numbers):

$${\mathcal{L}}_{\mathrm{\infty }}=\bigcup _{n\in \mathbb{N}}{\mathcal{L}}_n.$$

In the following, it is assumed that all action models are over the language $\mathcal{L}={\mathcal{L}}_{\mathrm{\infty }}$ (i.e., with preconditions from ${\mathcal{L}}_{\mathrm{\infty }}$ . Other Boolean connectives, such as $\to$ , $\mathrm{\top }$ , and $\mathrm{\perp }$ , are treated as abbreviations in a usual way.

2.3. Semantics

This subsection briefly recalls the standard semantics of action model logic (AML) (Baltag & Moss, 2004; Baltag et al., 1998; van Ditmarsch et al., 2007). Although semantic interpretations are not strictly necessary for the analysis of preservation of frame and group conditions, the following summary provides a concise overview of AML’s semantic framework and may facilitate a broader understanding of the logical context.

Given a pointed model $(M,s)$ , the satisfaction relation ( $\models$ ) defining the truth of formulas in AML is inductively defined as follows:

$$\begin{array}{lll}M,s\models p& \text{iff}& s\in V(p)\text{, for atomic }p\in \mathrm{prop}\\ M,s\models \mathrm{\neg }\varphi & \text{iff}& \text{not }M,s\models \varphi \\ M,s\models (\varphi \wedge \psi )& \text{iff}& M,s\models \varphi \text{ and }M,s\models \psi \\ M,s\models B_i\varphi & \text{iff}& \text{for all }t\in W\text{, }(s,t)\in R_i\text{implies }M,t\models \varphi \\ M,s\models D_G\varphi & \text{iff}& \text{for all }t\in W\text{, }(s,t)\in R_G^D\text{implies }M,t\models \varphi \\ M,s\models E_G\varphi & \text{iff}& \text{for all }t\in W\text{, }(s,t)\in R_G^E\text{implies }M,t\models \varphi \\ M,s\models C_G\varphi & \text{iff}& \text{for all }t\in W\text{, }(s,t)\in R_G^C\text{implies }M,t\models \varphi \\ M,s\models [\mathsf{M},\mathsf{s}]\varphi & \text{iff}& M,s\models \mathsf{p}\mathsf{r}\mathsf{e}(\mathsf{s})\text{implies }M\otimes \mathsf{M},(s,\mathsf{s})\models \varphi .\end{array}$$

where $M\otimes \mathsf{M}$ is defined in the next subsection.

2.4. Action Execution

Two types of action execution are defined: the generalized $⊛$ -type execution, and the classical $\otimes$ -type execution. ³

Let $M=(W,R,V)$ be a model and $\mathsf{M}=(\mathsf{W},\mathsf{R},\mathsf{p}\mathsf{r}\mathsf{e})$ an action. The $⊛$ -type execution of action $\mathsf{M}$ on model $M$ results in the model $M⊛\mathsf{M}=(\overline{W},\overline{R},\overline{V})$ , defined as follows ⁴

Domain of states: $\overline{W}=\{(s,\mathsf{s})\in W\times \mathsf{W}\mid M,s\models \mathsf{p}\mathsf{r}\mathsf{e}(\mathsf{s})\}$ .

Accessibility relations: for each agent $i\in \mathrm{ag}$ and group $g\in \mathrm{gr}$ : any $(s,\mathsf{s}),(t,\mathsf{t})\in \overline{W}$ , $i\in \mathrm{ag}$ and $G\in \mathrm{gr}$ :

Valuation: for each proposition $p\in \mathrm{prop}$ : $\overline{V}(p)=\{(s,\mathsf{s})\in \overline{W}\mid s\in V(p)\}$ .

It is possible that the resulting model is empty ( $\overline{W}=\mathrm{\varnothing }$ ). An empty model satisfies all frame and group conditions trivially, as these conditions begin with universal quantifiers.

The $\otimes$ -type execution of an action $\mathsf{M}=(\mathsf{W},\mathsf{R},\mathsf{p}\mathsf{r}\mathsf{e})$ on a model $M=(W,R,V)$ results in the model $M\otimes \mathsf{M}=(\overline{W},\overline{R},\overline{V})$ defined similarly to the $⊛$ -type execution, except that the resulting frame is defined to be collective. Specifically: ${\overline{R}}_i$ as defined above, and for each $G\in \mathrm{gr}$ : ${\overline{R}}_G^D=\bigcap _{i\in G}{\overline{R}}_i$ , ${\overline{R}}_G^E=\bigcup _{i\in G}{\overline{R}}_i$ and ${\overline{R}}_G^C=\underset{i\in G}{⨄}{\overline{R}}_i$ .

Example 2 (action execution)

Consider agents $a,b\in \mathrm{ag}$ , states $W=\{s,t,u\}$ , and model $M=(W,R,V)$ with:

Individual relations: $R_a=\{(s,s),(s,t),(t,s),(t,t),(u,u)\}$ and $R_b=\{(s,s),(t,t),(t,u),(u,t),(u,u)\}$ ;

Collective $R$ , thus: $R_{ab}^D=R_a\cap R_b=\{(s,s),(t,t),(u,u)\}$ , $R_{ab}^E=R_a\cup R_b$ , and $R_{ab}^C=R_a\uplus R_b=W\times W$ ;

Valuation: $V(p)=\{s,u\}$ .

Next, consider an action $\mathsf{M}=(\{\mathsf{s}\},\mathsf{R},\mathsf{p}\mathsf{r}\mathsf{e})$ defined as follows:

• Individual uncertainty relations: ${\mathsf{R}}_a={\mathsf{R}}_b=\{(\mathsf{s},\mathsf{s})\}$ ;

• Group relations (which are collective): ${\mathsf{R}}_{ab}^D={\mathsf{R}}_{ab}^E={\mathsf{R}}_{ab}^C=\{(\mathsf{s},\mathsf{s})\}$ ;

• Precondition: $\mathsf{p}\mathsf{r}\mathsf{e}(\mathsf{s})=p$ .

The model $M$ and action $\mathsf{M}$ are illustrated in Figure 1, following standard conventions. Specifically, nodes represent states, labeled with their state names. A node split into upper and lower parts indicates a state name (upper) and atomic propositions true in the state or action preconditions (lower). Edges depict binary relations labeled with agent names. Solid edges represent individual uncertainty relations, while dashed edges represent selected group-level relations—in this example, specifically the relation $R_{ab}^C$ .

Figure 1.

Illustration of a model, an action, and their executions.

Executing action $\mathsf{M}$ on model $M$ produces the model $M⊛\mathsf{M}=(\overline{W},\overline{R},\overline{V})$ where:

Domain: $\overline{W}=\{(s,\mathsf{s}),(u,\mathsf{s})\}$ ;

Relations:

${\overline{R}}_a={\overline{R}}_b=\{((s,\mathsf{s}),(s,\mathsf{s})),((u,\mathsf{s}),(u,\mathsf{s}))\}$ ,

${\overline{R}}_{ab}^C=\{((s,\mathsf{s}),(s,\mathsf{s})),((s,\mathsf{s}),(u,\mathsf{s})),((u,\mathsf{s}),(s,\mathsf{s})),((u,\mathsf{s}),(u,\mathsf{s}))\}$ ;

Valuation: $\overline{V}(p)=\{(s,\mathsf{s}),(u,\mathsf{s})\}$ .

The classical ( $\otimes$ -type) action execution of $\mathsf{M}$ on $M$ yields model $M\otimes \mathsf{M}=(\overline{\overline{W}},\overline{\overline{R}},\overline{\overline{V}})$ , which coincides with the $⊛$ -type execution for individual relations and valuation, i.e., $\overline{\overline{W}}=\overline{W}$ , ${\overline{\overline{R}}}_i={\overline{R}}_i$ for $i\in \{a,b\}$ , and $\overline{\overline{V}}=\overline{V}$ . However, the group-level common uncertainty relation differs significantly:

$${\overline{\overline{R}}}_{ab}^C={\overline{\overline{R}}}_a\cup {\overline{\overline{R}}}_b={\overline{R}}_a.$$

This relation is not depicted explicitly in Figure 1, as it can be directly computed from individual relations.

2.5. Frame and Group Conditions

This subsection recalls standard frame conditions from modal logic and introduces group conditions, which specify how group uncertainty relations are derived from individual ones. A frame $F=(W,R)$ with $R=(R^I,R^D,R^E,R^C)$ is:

Serial ( $\lambda$ ), if $\mathrm{\forall }i\in \mathrm{ag},\mathrm{\forall }s\in W,\mathrm{\exists }t\in W:(s,t)\in R_i$ ;

Reflexive ( $\rho$ ), if $\mathrm{\forall }i\in \mathrm{ag},\mathrm{\forall }s\in W:(s,s)\in R_i$ ;

Transitive ( $\tau$ ), if $\mathrm{\forall }i\in \mathrm{ag},\mathrm{\forall }s,t,u\in W:((s,t)\in R_i\wedge (t,u)\in R_i)\to (s,u)\in R_i$ ;

Symmetric ( $\sigma$ ), if $\mathrm{\forall }i\in \mathrm{ag},\mathrm{\forall }s,t\in W:(s,t)\in R_i\to (t,s)\in R_i$ ;

Euclidean ( $ϵ$ ), if $\mathrm{\forall }i\in \mathrm{ag},\mathrm{\forall }s,t,u\in W:((s,t)\in R_i\wedge (s,u)\in R_i)\to (t,u)\in R_i$ .

Intersective ( $\iota$ ) if, for all $G\in \mathrm{gr}$ , $R_G^D=\bigcap _{i\in G}{R}_i$ ;

Unioned ( $\upsilon$ ) if, for all $G\in \mathrm{gr}$ , $R_G^E=\bigcup _{i\in G}{R}_i$ ;

Transitive-unioned ( ${\upsilon }^{+}$ ) if, for all $G\in \mathrm{gr}$ , $R_G^C=\underset{i\in G}{⨄}{R}_i$ ;

Collective: intersective, unioned and transitive-unioned.

If a frame $(W,R)$ satisfies any of these conditions, it is also said that $R$ itself satisfies these conditions; for instance, $R$ is intersective if and only if $(W,R)$ is intersective. These conditions naturally carry over to models and actions based upon such frames.

Let ${\mathcal{C}}^{+}=\{\lambda ,\rho ,\tau ,\sigma ,ϵ,\iota ,\upsilon ,{\upsilon }^{+}\}$ denote the set of all frame and group conditions defined above. For any condition $x\in {\mathcal{C}}^{+}$ , the notation $F⊩x$ indicates that frame $F$ satisfies condition $x$ . For instance, $F⊩\lambda$ means $F$ is serial. For sets of conditions $\mathrm{\Gamma },\mathrm{\Delta },\mathrm{\Theta }\subseteq {\mathcal{C}}^{+}$ , frame satisfaction is extended as follows:

$F$ satisfies conditions $\mathrm{\Gamma }$ , written $F⊩\mathrm{\Gamma }$ , if and only if $F⊩x$ for every $x\in \mathrm{\Gamma }$ .

$F$ satisfies exactly conditions $\mathrm{\Gamma }$ , written $F⊩!\mathrm{\Gamma }$ , if and only if $F⊩\mathrm{\Gamma }$ and $F⊮x$ for all $x\in {\mathcal{C}}^{+}\setminus \mathrm{\Gamma }$ .

These notations naturally extend to models $M$ and actions $\mathsf{M}$ based on frame $F$ . Specifically, $M⊩\mathrm{\Gamma }$ , $\mathsf{M}⊩\mathrm{\Gamma }$ , $M⊩!\mathrm{\Gamma }$ and $\mathsf{M}⊩!\mathrm{\Gamma }$ signify that the underlying frames satisfy or exactly satisfy the given conditions. When $\mathrm{\Gamma }$ is a singleton $\{x\}$ , curly brackets are omitted (e.g., $M⊩x$ ).

Given sets of conditions $\mathrm{\Gamma },\mathrm{\Delta },\mathrm{\Theta }\subseteq {\mathcal{C}}^{+}$ :

The pair $(\mathrm{\Gamma },\mathrm{\Delta })$ guarantees $\mathrm{\Theta }$ , denoted $\mathrm{\Gamma }\otimes \mathrm{\Delta }⊩\mathrm{\Theta }$ , if for every model $M⊩\mathrm{\Gamma }$ and action $\mathsf{M}⊩\mathrm{\Delta }$ , it holds that $M\otimes \mathsf{M}⊩\mathrm{\Theta }$ .

The pair $(\mathrm{\Gamma },\mathrm{\Delta })$ guarantees exactly $\mathrm{\Theta }$ , denoted $\mathrm{\Gamma }\otimes \mathrm{\Delta }⊩!\mathrm{\Theta }$ , if (i) $\mathrm{\Gamma }\otimes \mathrm{\Delta }⊩\mathrm{\Theta }$ , and (ii) for every condition $x\in {\mathcal{C}}^{+}\setminus \mathrm{\Theta }$ , $\mathrm{\Gamma }\otimes \mathrm{\Delta }⊮x$ (i.e., there exist $M⊩\mathrm{\Gamma }$ and $\mathsf{M}⊩\mathrm{\Delta }$ such that $M\otimes \mathsf{M}⊮x$ ).

Proposition 3 characterization of Kripke and pseudo frames

The special types of frames introduced in Remark 1 are characterized as follows:

(a)

A frame is a Kripke frame if any only if it is collective (i.e., intersective, unioned, and transitive-unioned);

(b)

A frame is a pseudo frame if and only if it is unioned and transitive-unioned.

3. Preservation in Action Model Logic

3.1. Preservation of Frame Conditions

This section investigates the preservation of standard frame conditions under classical ( $\otimes$ -type) action execution in action model logic. The main question addressed is whether executing an action on a model preserves the frame conditions satisfied by the original model and action. ⁵

Let $\mathcal{C}=\{\lambda ,\rho ,\tau ,\sigma ,ϵ\}$ denote the set of standard frame conditions under consideration (seriality, reflexivity, transitivity, symmetry, and Euclidicity, respectively). Not all subsets of these conditions are independent. For instance, reflexivity ( $\rho$ ) implies seriality ( $\lambda$ ), and the combination of symmetry ( $\sigma$ ) with transitivity ( $\tau$ ) implies Euclidicity ( $ϵ$ ). As noted in Ågotnes and Wáng (2020), exactly 15 independent combinations of these conditions exist. To handle these systematically, the notion of closure of a set of conditions is introduced.

Definition 4 closure

Let $\mathrm{\Delta }\subseteq \mathcal{C}$ . The closure of $\mathrm{\Delta }$ in $\mathcal{C}$ , denoted ${\mathrm{\Delta }}^c$ , is defined as the smallest superset of $\mathrm{\Delta }$ satisfying the conditions:

(1)

For every frame $F$ , if $F⊩\mathrm{\Delta }$ , then $F⊩{\mathrm{\Delta }}^c$ ;

(2)

For every condition $x\in \mathcal{C}\setminus {\mathrm{\Delta }}^c$ , there exists a frame $F$ such that $F⊩\mathrm{\Delta }$ but $F⊮x$ .

It can be verified that the closure is unique and well-defined for any subset of $\mathcal{C}$ . Among the $2^5=32$ possible subsets of $\mathcal{C}$ , exactly 15 subsets correspond to distinct closures. These closures align with the classical modal logical systems listed below along with their standard names (cf. Chellas, 1980):

Table 1 summarizes our preservation results. For given condition subsets $\mathrm{\Gamma },\mathrm{\Delta }\subseteq \mathcal{C}$ , the table indicates precisely which conditions $\mathrm{\Theta }$ are exactly guaranteed by the pair $(\mathrm{\Gamma },\mathrm{\Delta })$ after classical ( $\otimes$ -type) action execution. The preservation relation is symmetric: interchanging the roles of the model and the action (or equivalently, swapping $\mathrm{\Gamma }$ and $\mathrm{\Delta }$ ) yields identical preservation results. In most cases, the guaranteed conditions $\mathrm{\Theta }=\mathrm{\Gamma }\cap \mathrm{\Delta }$ . The notable exception is seriality ( $\lambda$ ): in the absence of reflexivity ( $\rho$ ), seriality generally fails to be preserved under classical action execution.

Table 1.

Preservation of Frame Conditions Under Classical ( $\otimes$ -type) Action Execution.

The rest of this section provides general theorems and lemmas justifying the preservation results summarized in Table 1. Although each cell in Table 1 could, in principle, be individually verified, such an approach would require checking 225 cases. Instead, the following general results efficiently cover multiple cases simultaneously.

Lemma 5

Let $\mathrm{\Gamma },\mathrm{\Delta }\subseteq \mathcal{C}$ and $x\in \mathcal{C}$ . The following statements hold:

• (a)

For every model $M$ and action $\mathsf{M}$ , if $M⊩x$ , $\mathsf{M}⊩x$ and $x\ne \lambda$ , then $M\otimes \mathsf{M}⊩x$ ;

(b)

If $x\notin {\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c$ , then $\mathrm{\Gamma }\otimes \mathrm{\Delta }⊮x$ ;

(c)

$\mathrm{\Gamma }\otimes \mathrm{\Delta }⊩(({\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c)\setminus \{\lambda \}{)}^c$ ;

(d)

If $\rho \notin {\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c$ , then $\mathrm{\Gamma }\otimes \mathrm{\Delta }⊮\lambda$ .

Proof.

(a) follows directly from the definitions of frame conditions and the construction of the $\otimes$ -type execution. The preservation of each condition $x\in \mathcal{C}\setminus \{\lambda \}$ can be verified by standard logical reasoning. For example, when $x=ϵ$ : let $M=(W,R,V)$ , $\mathsf{M}=(\mathsf{W},\mathsf{R},\mathsf{p}\mathsf{r}\mathsf{e})$ , and $M\otimes \mathsf{M}$ be the resulting model $(\overline{W},\overline{R},\overline{V})$ . Preservation is straightforward: if $((s,\mathsf{s}),(t,\mathsf{t})),((s,\mathsf{s}),(u,\mathsf{u}))\in {\overline{R}}_i$ , this implies $(s,t),(s,u)\in R_i$ and $(\mathsf{s},\mathsf{t}),(\mathsf{s},\mathsf{u})\in {\mathsf{R}}_i$ . Since both $M,\mathsf{M}$ satisfy $ϵ$ , we have $(t,u)\in R_i$ , $(\mathsf{t},\mathsf{u})\in {\mathsf{R}}_i$ , and thus $((t,\mathsf{t}),(u,\mathsf{u}))\in {\overline{R}}_i$ . Other cases follow analogously.

(b) Consider the cases $x\notin {\mathrm{\Gamma }}^c$ and $x\notin {\mathrm{\Delta }}^c$ separately. Suppose $x\notin {\mathrm{\Gamma }}^c$ . Consider a model $M=(W,R,V)$ witnessing $M⊩\mathrm{\Gamma }$ but $M⊮x$ (such a model must exist). Construct a trivial action $\mathsf{M}$ with singleton domain, universal self-loop and no precondition, namely, $\mathsf{M}=(\mathsf{W},\mathsf{R},\mathsf{p}\mathsf{r}\mathsf{e})$ where (i) $\mathsf{W}=\{\mathsf{s}\}$ , (ii) ${\mathsf{R}}_i=\{(\mathsf{s},\mathsf{s})\}$ for all $i\in \mathrm{ag}$ , and (iii) $\mathsf{p}\mathsf{r}\mathsf{e}(\mathsf{s})=\mathrm{\top }$ . Action $\mathsf{M}$ satisfies all the frame conditions of $\mathcal{C}$ trivially, and thus $\mathsf{M}⊩\mathrm{\Delta }$ . Then, $M\otimes \mathsf{M}=(\overline{W},\overline{R},\overline{V})$ is such that $\overline{W}=\{(s,\mathsf{s})\mid s\in W\}$ and ${\overline{R}}_i=\{((s,\mathsf{s}),(t,\mathsf{s}))\mid (s,t)\in R_i\}$ for all $i\in \mathrm{ag}$ , which remains isomorphic to $M$ , thus not satisfying condition $x$ . A symmetric argument applies if $x\notin {\mathrm{\Delta }}^c$ . We need to show $\mathrm{\Gamma }\otimes \mathrm{\Delta }⊮x$ . Given an action $\mathsf{M}=(\mathsf{W},\mathsf{R},\mathsf{p}\mathsf{r}\mathsf{e})$ witnessing $\mathsf{M}⊩\mathrm{\Delta }$ , $\mathsf{M}⊮x$ and $\mathsf{p}\mathsf{r}\mathsf{e}(\mathsf{s})=\mathrm{\top }$ for all $\mathsf{s}\in \mathsf{W}$ (such an action exists), it suffices to show that there exists a model $M$ such that $M⊩\mathrm{\Gamma }$ and $M\otimes \mathsf{M}⊮x$ . Let $M$ be a trivial single-state model with universal self-loop. $M\otimes \mathsf{M}$ is isomorphic to $\mathsf{M}$ , witnessing failure of condition $x$ . Hence, either case yields $\mathrm{\Gamma }\otimes \mathrm{\Delta }⊮x$ .

(c) follows immediately from (a) and the definition of closure: if $M$ and $\mathsf{M}$ satisfy conditions $\mathrm{\Gamma }$ and $\mathrm{\Delta }$ , respectively, they both satisfy conditions ${\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c$ , and their execution preserves all conditions except possibly seriality ( $\lambda$ ). Thus, the closure $(({\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c)\setminus \{\lambda \}{)}^c$ is guaranteed.

(d) Suppose $\rho \notin {\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c$ . By statement (b), if $\lambda \notin {\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c$ , then $\mathrm{\Gamma }\otimes \mathrm{\Delta }⊮\lambda$ . We now consider the case when $\lambda \in {\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c$ .

Suppose $\rho \notin {\mathrm{\Gamma }}^c$ . Then either ${\mathrm{\Gamma }}^c\subseteq \{\lambda ,\tau ,ϵ\}$ or ${\mathrm{\Gamma }}^c\subseteq \{\lambda ,\sigma \}$ . Let

• –

$M=(\{s,t\},R,V)$ where $R_i=\{(s,t),(t,t)\}$ for all $i\in \mathrm{ag}$ and $V(p)=\{s\}$ (other atoms are irrelevant),

–

$M^{\prime }=(\{s,t\},R^{\prime },V)$ where $R_i^{\prime }=\{(s,t),(t,s)\}$ for all $i\in \mathrm{ag}$ ( $V$ is the same as the above), and

–

$\mathsf{M}=(\{\mathsf{s}\},\mathsf{R},\mathsf{p}\mathsf{r}\mathsf{e})$ where ${\mathsf{R}}_i=\{(\mathsf{s},\mathsf{s})\}$ and $\mathsf{p}\mathsf{r}\mathsf{e}(\mathsf{s})=p$ .

One can verify that either $M⊩{\mathrm{\Gamma }}^c$ (since $M⊩\{\lambda ,\tau ,ϵ\}$ ) or $M^{\prime }⊩{\mathrm{\Gamma }}^c$ (since $M^{\prime }⊩\{\lambda ,\sigma \}$ ). Moreover, $\mathsf{M}⊩{\mathrm{\Delta }}^c$ since $\mathsf{M}⊩\mathcal{C}$ . It can be shown that $M\otimes \mathsf{M}=M^{\prime }\otimes \mathsf{M}$ is based on the frame $(\{(s,\mathsf{s})\},\overline{R})$ with ${\overline{R}}_i=\mathrm{\varnothing }$ for all $i\in \mathrm{ag}$ . Hence, $M\otimes \mathsf{M}⊮\lambda$ and $M^{\prime }\otimes \mathsf{M}⊮\lambda$ , implying $\mathrm{\Gamma }\otimes \mathrm{\Delta }⊮\lambda$ .

Otherwise, suppose $\rho \notin {\mathrm{\Delta }}^c$ . Then either ${\mathrm{\Delta }}^c\subseteq \{\lambda ,\tau ,ϵ\}$ or ${\mathrm{\Delta }}^c\subseteq \{\lambda ,\sigma \}$ . Let

• –

$M=(\{s\},R,V)$ where $R_i=\{(s,s)\}$ for all $i\in \mathrm{ag}$ ,

–

$\mathsf{M}=(\{\mathsf{s},\mathsf{t}\},\mathsf{R},\mathsf{p}\mathsf{r}\mathsf{e})$ where ${\mathsf{R}}_i=\{(\mathsf{s},\mathsf{t}),(\mathsf{t},\mathsf{t})\}$ for all $i\in \mathrm{ag}$ , $\mathsf{p}\mathsf{r}\mathsf{e}(\mathsf{s})=\mathrm{\top }$ and $\mathsf{p}\mathsf{r}\mathsf{e}(\mathsf{t})=\mathrm{\perp }$ , and

–

${\mathsf{M}}^{\prime }=(\{\mathsf{s},\mathsf{t}\},{\mathsf{R}}^{\prime },\mathsf{p}\mathsf{r}\mathsf{e})$ where ${\mathsf{R}}_i^{\prime }=\{(\mathsf{s},\mathsf{t}),(\mathsf{t},\mathsf{s})\}$ for all $i\in \mathrm{ag}$ (and $\mathsf{p}\mathsf{r}\mathsf{e}$ is the same as the above).

We have either $\mathsf{M}⊩{\mathrm{\Delta }}^c$ (since $\mathsf{M}⊩\{\lambda ,\tau ,ϵ\}$ ) or ${\mathsf{M}}^{\prime }⊩{\mathrm{\Delta }}^c$ (since ${\mathsf{M}}^{\prime }⊩\{\lambda ,\sigma \}$ ). Moreover, $M⊩{\mathrm{\Gamma }}^c$ since $M⊩\mathcal{C}$ . It can be verified that $M\otimes \mathsf{M}=M\otimes {\mathsf{M}}^{\prime }$ is based on the frame $(\{(s,\mathsf{s})\},\overline{R})$ with ${\overline{R}}_i=\mathrm{\varnothing }$ for all $i\in \mathrm{ag}$ . Hence, $M\otimes \mathsf{M}⊮\lambda$ and $M\otimes {\mathsf{M}}^{\prime }⊮\lambda$ , implying $\mathrm{\Gamma }\otimes \mathrm{\Delta }⊮\lambda$ .

Theorem 6

Let $\mathrm{\Gamma },\mathrm{\Delta }\subseteq \mathcal{C}$ be arbitrary sets of frame conditions. Then $\mathrm{\Gamma }\otimes \mathrm{\Delta }⊩!(({\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c)\setminus \{\lambda \}{)}^c$ .

Proof.

First of all, we have the following immediate results:

Suppose $\rho \in {\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c$ . By $(*)$ , given $x\in \mathcal{C}\setminus (({\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c)\setminus \{\lambda \}{)}^c$ , it suffices to show that $\mathrm{\Gamma }\otimes \mathrm{\Delta }⊮x$ . In this case, $(({\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c)\setminus \{\lambda \}{)}^c=({\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c{)}^c$ . Therefore, $x\in \mathcal{C}\setminus ({\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c{)}^c$ , and so $x\in \mathcal{C}\setminus ({\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c)$ . It follows from $(†)$ that $\mathrm{\Gamma }\otimes \mathrm{\Delta }⊮x$ , as we wish to show.

Otherwise $\rho \notin {\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c$ . Since that there are only finitely many subsets of $\mathcal{C}$ , there exists a unique $S\subseteq \mathcal{C}$ such that $\mathrm{\Gamma }\otimes \mathrm{\Delta }⊩!S$ . It follows that: (i) by $(*)$ , $(({\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c)\setminus \{\lambda \}{)}^c\subseteq S$ , and (ii) by $(†)$ , $S\subseteq {\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c$ . By Lemma 5(d), $\mathrm{\Gamma }\otimes \mathrm{\Delta }⊮\lambda$ , and so $S\subseteq ({\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c)\setminus \{\lambda \}$ . Since $({\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c)\setminus \{\lambda \}\subseteq (({\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c)\setminus \{\lambda \}{)}^c$ , it follows that $S=({\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c)\setminus \{\lambda \}=(({\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c)\setminus \{\lambda \}{)}^c$ . Thus $\mathrm{\Gamma }\otimes \mathrm{\Delta }⊩!(({\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c)\setminus \{\lambda \}{)}^c$ .

In summary, classical ( $\otimes$ -type) action execution preserves all frame conditions satisfied by both the model and the action, except possibly seriality ( $\lambda$ ). Seriality is preserved only when implied by stronger frame conditions such as reflexivity ( $\rho$ ). Thus, Theorem 6 provides a concise and general characterization that efficiently covers all individual preservation results presented in Table 1.

3.2. Generalizations

Lemma 5(a, b) plays a crucial role in establishing the preservation of frame conditions. It suggests two fundamental principles:

(a)

Preservation of shared properties: Action execution does not eliminate the frame conditions $\rho$ , $\tau$ , $\sigma$ , and $ϵ$ if they are satisfied by both the original model and the action model (though $\lambda$ may be lost);

(b)

Prevention of new properties: Action execution does not generate new frame conditions from the set $\mathcal{C}$ : any frame condition satisfied after executing an action must generally be satisfied by both the original model and the action model.

While Lemma 5(a) is restricted to four frame conditions ( $\rho$ , $\tau$ , $\sigma$ , and $ϵ$ ), this principle can be generalized to any condition defined by a Horn clause ⁶ . A Horn clause is a first-order formula of the form:

$$\mathrm{\forall }{i}_1,\dots ,i_k\in \mathrm{ag},\mathrm{\forall }{s}_1,\dots ,s_n\in W:(P_1\wedge \cdots \wedge P_{m-1})\to P_m,$$

where each $P_1,\dots ,P_m$ ( $m\ge 1$ ) is either an accessibility relation $(s,t)\in R_i$ or an equality $s=t$ , for $s,t\in \{s_1,\dots ,s_n\}$ and $i\in \{i_1,\dots ,i_k\}$ . It is easily verified that $\rho$ , $\tau$ , $\sigma$ , and $ϵ$ are all Horn clauses.

Theorem 7

Let $x$ be a frame condition defined by a Horn clause. For every model $M$ and action $\mathsf{M}$ , if $M⊩x$ and $\mathsf{M}⊩x$ , then $M\otimes \mathsf{M}⊩x$ .

Proof.

Suppose $x$ is defined the by the Horn clause $\varphi =\mathrm{\forall }{i}_1,\dots ,i_k\in \mathrm{ag},\mathrm{\forall }{s}_1,\dots ,s_n\in W:(P_1\wedge \cdots \wedge P_{m-1})\to P_m$ . Let $M=(W,R,V)$ , $\mathsf{M}=(\mathsf{W},\mathsf{R},\mathsf{p}\mathsf{r}\mathsf{e})$ , and $M\otimes \mathsf{M}=(\overline{W},\overline{R},\overline{V})$ such that both $M⊩x$ and $\mathsf{M}⊩x$ . Suppose towards a contradiction that $M\otimes \mathsf{M}⊮x$ . This implies there exist $i_1,\dots ,i_k\in \mathrm{ag}$ , $(s_1,{\mathsf{s}}_1),\dots ,(s_n,{\mathsf{s}}_n)\in \overline{W}$ such that the antecedents $P_1,\dots ,P_{m-1}$ hold for $M\otimes \mathsf{M}$ , but the consequent $P_m$ does not. By the definition of the $\otimes$ -type execution, the antecedents hold for both $M$ and $\mathsf{M}$ . Since $M⊩x$ and $\mathsf{M}⊩x$ , $P_m$ must hold for both $M$ and $\mathsf{M}$ . Consequently, $P_m$ must also hold for $M\otimes \mathsf{M}$ , contradicting the assumption.

Theorem 7 significantly extends the scope of preservation beyond Lemma 5(a). Examples of other Horn clause properties that are modally definable include:

$\underset{i\in \mathrm{ag}}{\bigwedge }{B}_i(B_i\varphi \to \varphi )$ defines shift reflexivity, i.e., $\mathrm{\forall }i\in \mathrm{ag},\mathrm{\forall }s,t\in W:(s,t)\in R_i\to (t,t)\in R_i$ ;

$\underset{i\in \mathrm{ag}}{\bigwedge }(\mathrm{\neg }{B}_i\mathrm{\perp }\to (B_i\varphi \to \varphi ))$ defines semi-reflexivity, i.e., $\mathrm{\forall }i\in \mathrm{ag},\mathrm{\forall }s,t\in W:(s,t)\in R_i\to (s,s)\in R_i$ (Liang & Wáng, 2022);

$\underset{i\in \mathrm{ag}}{\bigwedge }(\mathrm{\neg }{B}_i\mathrm{\neg }\varphi \to B_i\varphi )$ defines uniqueness, i.e., $\mathrm{\forall }i\in \mathrm{ag},\mathrm{\forall }s,t,u\in W:((s,t)\in R_i\wedge (s,u)\in R_i)\to t=u$ ;

$\underset{i\in \mathrm{ag}}{\bigwedge }(B_i\varphi \to B_j\varphi )$ defines inclusion, i.e., $\mathrm{\forall }i,j\in \mathrm{ag},\mathrm{\forall }s,t\in W:(s,t)\in R_j\to (s,t)\in R_i$ .

All these are Horn clauses as well. Theorem 7 tells us that they are preserved in the same way as the four frame properties are.

On the other hand, the second principle—that action execution cannot generate new conditions (Lemma 5(b))—does not hold in general for all frame properties. Consider the following counterexample. Let $M=(W,R,V)$ be a model where (i) $W=\{s,t\}$ , (ii) $R_i=\{(s,s)\}$ for all $i\in \mathrm{ag}$ , and (iii) $V(p)=\{s\}$ for some propositional atom $p$ . The frame underlying $M$ satisfies antisymmetry ( $\mathrm{\forall }i\in \mathrm{ag},\mathrm{\forall }s,t\in W:((s,t)\in R_i\wedge (t,s)\in R_i)\to s=t$ ), but fails asymmetry ( $\mathrm{\forall }i\in \mathrm{ag},\mathrm{\forall }s,t\in W:(s,t)\in R_i\to (t,s)\notin R_i$ ). Now, consider an action $\mathsf{M}=(\mathsf{W},\mathsf{R},\mathsf{\text{V}})$ such that (i) $\mathsf{W}=\{\mathsf{s},\mathsf{t}\}$ , (ii) ${\mathsf{R}}_i=\{(\mathsf{t},\mathsf{t})\}$ for all $i\in \mathrm{ag}$ , and (iii) $\mathsf{p}\mathsf{r}\mathsf{e}(s)=\mathsf{p}\mathsf{r}\mathsf{e}(t)=\mathrm{\top }$ . The frame underlying $\mathsf{M}$ similarly satisfies antisymmetry but not asymmetry. The resulting model $M\otimes \mathsf{M}=(\overline{W},\overline{R},\overline{V})$ is given by $\overline{W}=\{(s,\mathsf{s}),(s,\mathsf{t}),(t,\mathsf{s}),(t,\mathsf{t})\}$ and ${\overline{R}}_i=\mathrm{\varnothing }$ for all $i\in \mathrm{ag}$ . An empty relation trivially satisfies both antisymmetry and asymmetry. Thus, the condition of asymmetry was generated by the execution, despite being absent in both the original model and the action.

To formalize when this generation of new properties is impossible, we introduce weak irreflexivity: a frame $(W,R)$ is weakly irreflexive if $\mathrm{\forall }s\in W,\mathrm{\exists }i\in \mathrm{ag}:(s,s)\notin R_i$ .

Theorem 8

Let $\varphi \in \mathcal{F}$ be a frame condition, and let $\mathrm{\Gamma },\mathrm{\Delta }\subseteq \mathcal{F}$ . Assume neither ${\mathrm{\Gamma }}^c$ nor ${\mathrm{\Delta }}^c$ includes weak irreflexivity. Then, $\mathrm{\Gamma }\otimes \mathrm{\Delta }⊩\varphi$ implies $\varphi \in {\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c$ .

Proof.

The proof proceeds by contraposition, showing that if $\varphi \notin {\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c$ , then $\mathrm{\Gamma }\otimes \mathrm{\Delta }⊮\varphi$ . Two cases arise:

Case 1 ( $\varphi \notin {\mathrm{\Gamma }}^c$ ). Let $M$ be a model witnessing $M⊩\mathrm{\Gamma }$ and $M⊮\varphi$ . Such a model exists by definition of closure. Construct an action $\mathsf{M}=(\mathsf{W},\mathsf{R},\mathsf{p}\mathsf{r}\mathsf{e})$ satisfying: (i) $\mathsf{M}⊩\mathrm{\Delta }$ , (ii) $\mathsf{M}$ is not weakly irreflexive (i.e., there exists $\mathsf{s}\in \mathsf{W}$ such that $(\mathsf{s},\mathsf{s})\in {\mathsf{R}}_i$ for every agent $i\in \mathrm{ag}$ ), and (iii) $\mathsf{p}\mathsf{r}\mathsf{e}(\mathsf{s})=\mathrm{\top }$ and all other states have precondition $\mathrm{\perp }$ . Such an action exists because ${\mathrm{\Delta }}^c$ does not include weak irreflexivity by assumption. Then $M\otimes \mathsf{M}$ is isomorphic to $M$ itself, thereby failing condition $\varphi$ . Thus, $\mathrm{\Gamma }\otimes \mathrm{\Delta }⊮\varphi$ .

Case 2 ( $\varphi \notin {\mathrm{\Delta }}^c$ ). Let $M=(W,R,V)$ be a model satisfying (i) $M⊩\mathrm{\Gamma }$ , (ii) there exists $s\in W$ such that $(s,s)\in R_i$ for all $i\in \mathrm{ag}$ , and (iii) $V(p)=\{s\}$ for some propositional atom $p$ . Consider an action $\mathsf{M}=(\mathsf{W},\mathsf{R},\mathsf{p}\mathsf{r}\mathsf{e})$ satisfying: (i) $\mathsf{M}⊩\mathrm{\Delta }$ , (ii) $\mathsf{M}⊮\varphi$ , and (iii) $\mathsf{p}\mathsf{r}\mathsf{e}(\mathsf{s})=p$ for every $\mathsf{s}\in \mathsf{W}$ . Both $M$ and $\mathsf{M}$ guaranteed to exist. The resulting model $M\otimes \mathsf{M}$ is isomorphic to $\mathsf{M}$ , thus failing $\varphi$ . Hence, again, $\mathrm{\Gamma }\otimes \mathrm{\Delta }⊮\varphi$ .

Theorem 8 generalizes Lemma 5(b), establishing that classical action execution cannot introduce new frame conditions, provided weak irreflexivity is excluded.

3.3. Preservation of Group Conditions

Section 3.1 studied the preservation of individual frame conditions under classical ( $\otimes$ -type) action execution. However, when analyzing group notions of knowledge and belief, additional preservation questions naturally arise. In epistemic and doxastic logic over Kripke models, classical interpretations of group knowledge or belief—specifically, distributed knowledge, mutual knowledge, and common knowledge ( $D_G$ , $E_G$ , and $C_G$ , respectively)—are defined using group accessibility relations constructed via intersection, union, and the transitive closure of the union of individual accessibility relations, respectively. In the terminology of this article, a (general) model is called intersective, unioned and transitive-unioned if the group accessibility relations indeed correspond exactly to intersections, unions and transitive closures of unions of individual accessibility relations, respectively (see Section 2.5 for more details). Moreover, a model is called collective if it simultaneously satisfy all three conditions: intersectivity ( $\iota$ ), unionedness ( $\upsilon$ ) and transitive-unionedness ( ${\upsilon }^{+}$ ).

Groups often behave as collective agents, exhibiting unified epistemic or doxastic behaviors analogous to single individuals. For example, the head or representative of an organization frequently speaks on behalf of the entire organization as a collective agent. Technically, groups can also be treated exactly like individuals. For instance, completeness proofs for logics involving distributed knowledge commonly introduce pseudo-structures in which groups behave precisely as individual agents (Fagin et al., 1992; Wáng & Ågotnes, 2013). Here, this idea of collective agency is extended from distributed knowledge to all three group modalities mentioned above.

Thus, the following preservation questions arise naturally. Given a model $M$ and an action $\mathsf{M}$ , each belonging to certain classes characterized by particular frame conditions, consider the following questions regarding preservation under generalized ( $⊛$ -type) action execution:

(a)

Is intersectivity preserved under action execution? Formally, if $M⊩\iota$ and $\mathsf{M}⊩\iota$ , does it follow that $M⊛\mathsf{M}⊩\iota$ ?

(b)

Is unionedness preserved under action execution? Formally, if $M⊩\upsilon$ and $\mathsf{M}⊩\upsilon$ , does it follow that $M⊛\mathsf{M}⊩\upsilon$ ?

(c)

Is transitive-unionedness preserved under action execution? Formally, if $M⊩{\upsilon }^{+}$ and $\mathsf{M}⊩{\upsilon }^{+}$ , does it follow that $M⊛\mathsf{M}⊩{\upsilon }^{+}$ ?

An immediate corollary follows from the above definitions and questions: if all three preservation questions have affirmative answers, then the generalized ( $⊛$ -type) execution coincides exactly with the classical ( $\otimes$ -type) execution. As shown below, however, the answer is not always affirmative.

The rest of this section systematically investigate these group-condition preservation questions. The analysis proceeds case-by-case, depending on the frame conditions satisfied by the original model $M$ and the action $\mathsf{M}$ . Specifically, given subsets $\mathrm{\Gamma },\mathrm{\Delta }\subseteq \mathcal{C}=\{\lambda ,\rho ,\tau ,\sigma ,ϵ\}$ of standard frame conditions, the preservation questions are examined under the assumptions $M⊩\mathrm{\Gamma }$ and $\mathsf{M}⊩\mathrm{\Delta }$ .

Theorem 9

The following preservation results hold for group conditions under action execution:

• (a)

Intersectivity is preserved under action execution. Formally, for every model $M$ and action $\mathsf{M}$ , if $M⊩\iota$ and $\mathsf{M}⊩\iota$ , then $M⊛\mathsf{M}⊩\iota$ .

(b)

Unionedness is not guaranteed to be preserved under action execution, regardless of the considered class of frames. ⁷ Formally, for every pair of subsets $\mathrm{\Gamma },\mathrm{\Delta }\subseteq \mathcal{C}$ , there exist a model $M$ and an action $\mathsf{M}$ such that $M⊩\mathrm{\Gamma }\cup \{\upsilon \}$ and $\mathsf{M}⊩\mathrm{\Delta }\cup \{\upsilon \}$ , but $M⊛\mathsf{M}⊮\upsilon$ .

(c)

Transitive-unionedness is also not guaranteed to be preserved under action execution, regardless of the considered class of frames. Formally, for every $\mathrm{\Gamma },\mathrm{\Delta }\subseteq \mathcal{C}$ , there exist a model $M$ and an action $\mathsf{M}$ such that $M⊩\mathrm{\Gamma }\cup \{{\upsilon }^{+}\}$ and $\mathsf{M}⊩\mathrm{\Delta }\cup \{{\upsilon }^{+}\}$ , but $M⊛\mathsf{M}⊮{\upsilon }^{+}$ .

Proof.

(a) Let $M=(W,R,V)$ , $\mathsf{M}=(\mathsf{W},\mathsf{R},\mathsf{p}\mathsf{r}\mathsf{e})$ , and $M⊛\mathsf{M}=(\overline{W},\overline{R},\overline{V})$ . We show that ${\overline{R}}_G^D=\bigcap _{i\in G}{\overline{R}}_i$ for all $G\in \mathrm{gr}$ . For any $(s,\mathsf{s}),(t,\mathsf{t})\in \overline{W}$ , $((s,\mathsf{s}),(t,\mathsf{t}))\in {\overline{R}}_G^D$ iff [ $(s,t)\in R_i$ and $(\mathsf{s},\mathsf{t})\in {\mathsf{R}}_i$ for all $i\in G$ (since $M⊩\iota$ and $\mathsf{M}⊩\iota$ )] iff [ $((s,\mathsf{s}),(t,\mathsf{t}))\in {\overline{R}}_i$ for all $i\in G$ ].

(b) Let $a$ and $b$ be two distinct agents. Construct a model $M=(W,R,V)$ such that (i) $W=\{s,t\}$ , (ii) $R_a=\{(s,s),(t,t)\}$ , (iii) $R_b=W\times W$ , and (iv) $R$ is collective (it follows that $R_{ab}^E=W\times W$ ). Construct an action $\mathsf{M}=(\mathsf{W},\mathsf{R},\mathsf{p}\mathsf{r}\mathsf{e})$ such that (i) $\mathsf{W}=\{\mathsf{s},\mathsf{t}\}$ , (ii) ${\mathsf{R}}_a=\mathsf{W}\times \mathsf{W}$ , (iii) ${\mathsf{R}}_b=\{(\mathsf{s},\mathsf{s}),(\mathsf{t},\mathsf{t})\}$ , (iv) $\mathsf{p}\mathsf{r}\mathsf{e}(\mathsf{s})=\mathsf{p}\mathsf{r}\mathsf{e}(\mathsf{t})=\mathrm{\top }$ , and (v) $\mathsf{R}$ is collective (it follows that ${\mathsf{R}}_{ab}^E=\mathsf{W}\times \mathsf{W}$ ). The resulting model $M⊛\mathsf{M}=(\{(s,\mathsf{s}),(s,\mathsf{t}),(t,\mathsf{s}),(t,\mathsf{t})\},\overline{R},\overline{V})$ satisfies $((s,\mathsf{s}),(t,\mathsf{t}))\notin {\overline{R}}_a\cup {\overline{R}}_b$ , because $((s,\mathsf{s}),(t,\mathsf{t}))\notin {\overline{R}}_a$ and $((s,\mathsf{s}),(t,\mathsf{t}))\notin {\overline{R}}_b$ . On the other hand, $((s,\mathsf{s}),(t,\mathsf{t}))\in {\overline{R}}_{ab}^E$ , since $R_{ab}^E$ and ${\mathsf{R}}_{ab}^E$ are both fully connected in their own model. See the following illustrations.

Thus, ${\overline{R}}_{ab}^E\ne {\overline{R}}_a\cup {\overline{R}}_b$ , and so $M⊛\mathsf{M}⊮\upsilon$ . Notice that the frames on which the model and the action are based satisfy all the conditions in $\mathcal{C}$ , hence $M⊩\mathrm{\Gamma }\cup \{\upsilon \}$ and $\mathsf{M}⊩\mathrm{\Delta }\cup \{\upsilon \}$ .

(c) The model $M$ and action $\mathsf{M}$ introduced in Example 2 satisfy all the conditions in $\mathcal{C}$ , hence $M⊩\mathrm{\Gamma }\cup \{{\upsilon }^{+}\}$ and $\mathsf{M}⊩\mathrm{\Delta }\cup \{{\upsilon }^{+}\}$ . However, as explained there, the resulting model $M⊛\mathsf{M}=(\overline{W},\overline{R},\overline{V})$ is such that ${\overline{R}}_{ab}^C\ne {\overline{R}}_a\uplus {\overline{R}}_b$ , meaning that $M⊛\mathsf{M}⊮{\upsilon }^{+}$ .

These results are summarized in the first column of Table 2.

Table 2.

Preservation of Group Conditions Under Action Execution.

	Action Types
Group Conditions	Classical Actions	Public Announcements (either variant)	Unconditional Actions
Intersectivity $(\iota )$	preserved	preserved	preserved
Unionedness $(\upsilon )$	not preserved	preserved	not preserved
Transitive-unionedness $({\upsilon }^{+})$	not preserved	not preserved	partially preserved

A summary of preservation results for intersectivity ( $\iota$ ), unionedness ( $\upsilon$ ), and transitive-unionedness ( ${\upsilon }^{+}$ ), under classical actions, public announcements (point-removing or arrow-removing), and unconditional actions. “Preserved” indicates the condition always holds after execution whenever it initially holds in both the model and the action; “not preserved” indicates there exist cases where the condition fails after execution despite holding initially; “partially preserved” indicates preservation depends on additional specific conditions; see Table 5.

4. Preservation Under Specific Types of Actions

4.1. Public Announcements

A point-removing public announcement (Plaza, 1989) constitutes a specialized action that alters a model’s states and, consequently, its uncertainty relations. An alternative formulation, termed an arrow-removing public announcement (Gerbrandy, 1999; Gerbrandy & Groeneveld, 1997), interprets the announcement as a process that contracts the uncertainty relations within the model. These concepts are formalized as follows.

Definition 10 public announcements

Let $\varphi$ be any formula in the language.

The point-removing public announcement of $\varphi$ , denoted $\mathsf{P}\mathsf{u}\mathsf{b}(\varphi )$ , is defined as the action $\mathsf{M}=(\{\mathsf{s}\},\mathsf{R},\mathsf{p}\mathsf{r}\mathsf{e})$ , where $\mathsf{p}\mathsf{r}\mathsf{e}(\mathsf{s})=\varphi$ and the relations satisfy ${\mathsf{R}}_i={\mathsf{R}}_G^D={\mathsf{R}}_G^E={\mathsf{R}}_G^C=\{(\mathsf{s},\mathsf{s})\}$ for all $i\in \mathrm{ag}$ and $G\in \mathrm{gr}$ .

The arrow-removing public announcement of $\varphi$ , denoted $\mathsf{P}\mathsf{u}\mathsf{b}\circ (\varphi )$ , is defined as the action $\mathsf{P}\mathsf{u}\mathsf{b}\circ (\varphi )=(\{\mathsf{s},\mathsf{t}\},\mathsf{R},\mathsf{p}\mathsf{r}\mathsf{e})$ , where $\mathsf{p}\mathsf{r}\mathsf{e}(\mathsf{s})=\varphi$ , $\mathsf{p}\mathsf{r}\mathsf{e}(\mathsf{t})=\mathrm{\neg }\varphi$ , and the relations satisfy ${\mathsf{R}}_i={\mathsf{R}}_G^D={\mathsf{R}}_G^E={\mathsf{R}}_G^C=\{(\mathsf{s},\mathsf{s}),(\mathsf{t},\mathsf{s})\}$ for all $i\in \mathrm{ag}$ and $G\in \mathrm{gr}$ .

Both variants capture the effect of a public announcement of $\varphi$ : the states where $\varphi$ held become the sole accessible states, either by eliminating states where $\varphi$ is false (point-removing) or by eliminating transitions to such states (arrow-removing). By their construction, both types of public announcements operate as actions grounded in collective frames.

This subsection examines the preservation of frame conditions and group conditions under these two types of public announcements. The class of all point-removing public announcements is treated as satisfying a specific set of frame conditions, denoted Pub, as follows. To express preservation, the notation $\mathrm{\Gamma }\otimes \text{Pub}⊩\mathrm{\Theta }$ (where $\mathrm{\Gamma },\mathrm{\Theta }\subseteq \mathcal{C}$ ) indicates that the pair $(\mathrm{\Gamma },\text{Pub})$ guarantees $\mathrm{\Theta }$ . Formally, for any model $M⊩\mathrm{\Gamma }$ and any formula $\varphi$ , the updated model $M\otimes \mathsf{P}\mathsf{u}\mathsf{b}(\varphi )⊩\mathrm{\Theta }$ holds (cf. Section 2.5). Similarly, $\mathrm{\Gamma }\otimes \text{Pub}⊩!\mathrm{\Theta }$ denotes that $(\mathrm{\Gamma },\text{Pub})$ guarantees exactly $\mathrm{\Theta }$ , meaning $\mathrm{\Gamma }\otimes \text{Pub}⊩\mathrm{\Theta }$ and, for every $x\in \mathcal{C}\setminus \mathrm{\Theta }$ , there exists a model $M⊩\mathrm{\Gamma }$ and a formula $\varphi$ such that $M\otimes \mathsf{P}\mathsf{u}\mathsf{b}(\varphi )⊮x$ . The set of frame conditions characterizing arrow-removing public announcements is denoted Pub $\circ$ , with the notations $\mathrm{\Gamma }\otimes \text{Pub}\circ ⊩\mathrm{\Theta }$ and $\mathrm{\Gamma }\otimes \text{Pub}\circ ⊩!\mathrm{\Theta }$ defined analogously.

The analysis addresses two key questions:

(a)

For any set of frame conditions $\mathrm{\Gamma }\subseteq \mathcal{C}$ , what is the set $\mathrm{\Theta }$ of frame conditions guaranteed exactly by $(\mathrm{\Gamma },\text{Pub})$ , i.e., such that $\mathrm{\Gamma }\otimes \text{Pub}⊩!\mathrm{\Theta }$ ?

(b)

For any set of frame conditions $\mathrm{\Gamma }\subseteq \mathcal{C}$ , what is the set $\mathrm{\Theta }$ of frame conditions guaranteed exactly by $(\mathrm{\Gamma },\text{Pub}\circ )$ , i.e., such that $\mathrm{\Gamma }\otimes \text{Pub}\circ ⊩!\mathrm{\Theta }$ ?

The results, summarized in Table 3, reveal distinct patterns: point-removing public announcements align with the preservation behavior of S5 actions, maintaining properties like reflexivity and symmetry where applicable, while arrow-removing public announcements mirror the properties of KD45 actions, preserving transitivity and Euclidicity but not necessarily seriality.

Table 3.

Preservation of Frame Conditions Under Public Announcements.

	Frame conditions $\mathrm{\Gamma }$
	(1)	(2)	(3)	(4)	(5)	(6)	(7)	(8)	(9)	(10)	(11)	(12)	(13)	(14)	(15)
Ann. types	K	D	K4	KB	K5	T	KD4	KDB	KD5	K45	S4	B	KD45	K4B5	S5
$\text{Pub}$	K	K	K4	KB	K5	T	K4	KB	K5	K45	S4	B	K45	K4B5	S5
$\text{Pub}\circ$	K	K	K4	K	K5	K	K4	K	K5	K45	K4	K	K45	K45	K45

$\mathrm{\Theta }$ denotes the set of frame conditions such that $\mathrm{\Gamma }\otimes \text{Pub}⊩!\mathrm{\Theta }$ (first row) and $\mathrm{\Gamma }\otimes \text{Pub}\circ ⊩!\mathrm{\Theta }$ (second row), where $\mathrm{\Gamma }$ represents the initial frame conditions and Pub and Pub $\circ$ denote point-removing and arrow-removing public announcements, respectively.

Explicit proofs for the preservation of these frame conditions under point-removing and arrow-removing public announcements are not provided here. However, such proofs can be readily derived by adapting the arguments presented in Section 3.1 with minor modifications.

The following theorem addresses the preservation of group conditions under public announcements, with results compared to other action types in Table 2.

Theorem 11

• (a)

Intersectivity is preserved under public announcements. For any model $M$ and formula $\varphi$ , if $M⊩\iota$ , then $M⊛\mathsf{P}\mathsf{u}\mathsf{b}(\varphi )⊩\iota$ and $M⊛\mathsf{P}\mathsf{u}\mathsf{b}\circ (\varphi )⊩\iota$ .

(b)

Unionedness is preserved under public announcements. For any model $M$ and formula $\varphi$ , if $M⊩\upsilon$ , then $M⊛\mathsf{P}\mathsf{u}\mathsf{b}(\varphi )⊩\upsilon$ and $M⊛\mathsf{P}\mathsf{u}\mathsf{b}\circ (\varphi )⊩\upsilon$ .

(c)

Transitive-unionedness is not preserved under public announcements. For any set of frame conditions $\mathrm{\Gamma }\subseteq \mathcal{C}$ , there exist a model $M$ and a formula $\varphi$ such that $M⊩\mathrm{\Gamma }\cup \{{\upsilon }^{+}\}$ , yet $M⊛\mathsf{P}\mathsf{u}\mathsf{b}(\varphi )⊮{\upsilon }^{+}$ and $M⊛\mathsf{P}\mathsf{u}\mathsf{b}\circ (\varphi )⊮{\upsilon }^{+}$ . ⁸

Proof.

(a) The preservation of intersectivity follows directly from Theorem 9(a).

(b) To establish unionedness, consider a model $M=(W,R,V)$ and the updated model $M⊛\mathsf{P}\mathsf{u}\mathsf{b}(\varphi )=(\overline{W},\overline{R},\overline{V})$ . We show that ${\overline{R}}_G^E=\bigcup _{i\in G}{\overline{R}}_i$ for all $G\in \mathrm{gr}$ . For any $(s,\mathsf{s}),(t,\mathsf{t})\in \overline{W}$ , $((s,\mathsf{s}),(t,\mathsf{t}))\in {\overline{R}}_G^E$ iff [ $(s,t)\in R_G^E$ and $(\mathsf{s},\mathsf{t})\in {\mathsf{R}}_G^E$ ] iff [ $(s,t)\in R_i$ and $(\mathsf{s},\mathsf{t})\in {\mathsf{R}}_j$ for some $i,j\in G$ ] iff [ $(s,t)\in R_i$ and $(\mathsf{s},\mathsf{t})\in {\mathsf{R}}_i$ for some $i\in G$ (since ${\mathsf{R}}_i={\mathsf{R}}_j$ for any $i,j\in \mathrm{ag}$ )] iff [ $((s,\mathsf{s}),(t,\mathsf{t}))\in {\overline{R}}_i$ for some $i\in G$ ] iff $((s,\mathsf{s}),(t,\mathsf{t}))\in \bigcup _{i\in G}{\overline{R}}_i$ . Therefore ${\overline{R}}_G^E=\bigcup _{i\in G}{\overline{R}}_i$ . The argument for $\mathsf{P}\mathsf{u}\mathsf{b}\circ$ is proceeds similarly.

(c) For point-removing public announcements, the proof of Theorem 9(c) also works here, since the action $\mathsf{M}$ there is in fact $\mathsf{P}\mathsf{u}\mathsf{b}(p)$ . As for arrow-removing public announcements, consider the model $M$ in the proof of Theorem 9(c) which satisfies $\mathrm{\Gamma }$ and the action $\mathsf{P}\mathsf{u}\mathsf{b}\circ (p)=(\{\mathsf{s},\mathsf{t}\},\mathsf{R},\mathsf{p}\mathsf{r}\mathsf{e})$ where $\mathsf{p}\mathsf{r}\mathsf{e}(\mathsf{s})=p$ , $\mathsf{p}\mathsf{r}\mathsf{e}(\mathsf{t})=\mathrm{\neg }p$ , and ${\mathsf{R}}_i={\mathsf{R}}_G^D={\mathsf{R}}_G^E={\mathsf{R}}_G^C=\{(\mathsf{s},\mathsf{s}),(\mathsf{t},\mathsf{s})\}$ for all $i\in \mathrm{ag}$ and $G\in \mathrm{gr}$ . The resulting model $M⊛\mathsf{P}\mathsf{u}\mathsf{b}\circ (p)=(\{s\mathsf{s},u\mathsf{s},t\mathsf{t}\},\overline{R},\overline{V})$ (for simplicity we write $s\mathsf{s}$ instead of $(s,\mathsf{s})$ , and similarly for other pairs) is such that ${\overline{R}}_a=\{(s\mathsf{s},s\mathsf{s}),(t\mathsf{t},s\mathsf{s}),(u\mathsf{s},u\mathsf{s})\}$ , ${\overline{R}}_b=\{(s\mathsf{s},s\mathsf{s}),(s\mathsf{s},u\mathsf{s}),(u\mathsf{s},s\mathsf{s}),(u\mathsf{s},u\mathsf{s})\}$ , and ${\overline{R}}_{ab}^C=\{(s\mathsf{s},s\mathsf{s}),(s\mathsf{s},u\mathsf{s}),(u\mathsf{s},s\mathsf{s}),(u\mathsf{s},u\mathsf{s}),(t\mathsf{t},s\mathsf{s}),(t\mathsf{t},u\mathsf{s})\}$ . It follows that ${\overline{R}}_{ab}^C\ne {\overline{R}}_a\uplus {\overline{R}}_b$ , confirming non-preservation.

4.2. Unconditional Actions

Prior sections have demonstrated that actions preserve only specific frame and group conditions, a phenomenon that extends to public announcements, a particular class of actions. Various action types can be designed with different preservation properties for group conditions. This section introduces unconditional actions, a subtype executable without preconditions, and establishes that this subtype yields unique preservation results.

Definition 12 ( $*$ - and $\times$ -types action execution)

Let ${\mathsf{M}}^{\mathrm{\top }}=(\mathsf{W},\mathsf{R},{\mathsf{p}\mathsf{r}\mathsf{e}}^{\mathrm{\top }})$ be an action where ${\mathsf{p}\mathsf{r}\mathsf{e}}^{\mathrm{\top }}(\mathsf{s})=\mathrm{\top }$ for all $\mathsf{s}\in \mathsf{W}$ . Given a model $M=(W,R,V)$ and an action $\mathsf{M}=(\mathsf{W},\mathsf{R},\mathsf{p}\mathsf{r}\mathsf{e})$ , we define:

$M*\mathsf{M}=M⊛{\mathsf{M}}^{\mathrm{\top }}$ ;

$M\times \mathsf{M}=M\otimes {\mathsf{M}}^{\mathrm{\top }}$ .

The $*$ - and $\times$ -types of action execution correspond to the previously defined $⊛$ - and $\otimes$ -type executions applied to specialized action classes. Moreover, $M*\mathsf{M}$ serves as a supermodel of $M⊛\mathsf{M}$ , and $M\times \mathsf{M}$ as a supermodel of $M\otimes \mathsf{M}$ . These relationships are formalized in the following proposition.

Proposition 13

For a model $M=(W,R,V)$ and an action $\mathsf{M}=(\mathsf{W},\mathsf{R},\mathsf{p}\mathsf{r}\mathsf{e})$ :

• (a)

$M*\mathsf{M}$ is a model. If, in addition, $M$ is a Kripke model and $\mathsf{M}$ is a Kripke action, then $M\times \mathsf{M}$ is a Kripke model.

(b)

If $M,s\models \mathsf{p}\mathsf{r}\mathsf{e}(\mathsf{s})$ for all $s\in W$ and $\mathsf{s}\in \mathsf{W}$ , then $M*\mathsf{M}=M⊛\mathsf{M}$ and $M\times \mathsf{M}=M\otimes \mathsf{M}$ .

For notational convenience, a variant of the “guarantee” concept (cf. Section 2.5) is introduced tailored to unconditional actions.

Definition 14

Let $\mathrm{\Gamma },\mathrm{\Delta },\mathrm{\Theta }\subseteq \{\lambda ,\rho ,\tau ,\sigma ,ϵ,\iota ,\upsilon ,{\upsilon }^{+}\}$ be sets of frame and group conditions.

We write $\mathrm{\Gamma }\times \mathrm{\Delta }⊩\mathrm{\Theta }$ if, for any model $M$ and any action $\mathsf{M}$ , $M⊩\mathrm{\Gamma }$ and $\mathsf{M}⊩\mathrm{\Delta }$ imply $M\times \mathsf{M}⊩\mathrm{\Theta }$ .

We write $\mathrm{\Gamma }\times \mathrm{\Delta }⊩!\mathrm{\Theta }$ if $\mathrm{\Gamma }\times \mathrm{\Delta }⊩\mathrm{\Theta }$ and for any $x\in \mathcal{C}\setminus \mathrm{\Theta }$ , there exist $M⊩\mathrm{\Gamma }$ and $\mathsf{M}⊩\mathrm{\Delta }$ such that $M\times \mathsf{M}⊮x$ .

We first study the preservation of frame conditions under unconditional actions. The result is given in Table 4 which follows from Theorem 16 given below.

Table 4.

Preservation of Frame Conditions Under Execution of Unconditional Actions ( $\mathrm{\Theta }$ Represents the Combination of Frame Conditions Such That $\mathrm{\Gamma }\times \mathrm{\Delta }⊩!\mathrm{\Theta }$ ).

Lemma 15

Given frame conditions $\mathrm{\Gamma },\mathrm{\Delta }\subseteq \mathcal{C}$ and $x\in \mathcal{C}$ , the following hold:

• (a)

For any model $M$ and action $\mathsf{M}$ , if $M⊩x$ and $\mathsf{M}⊩x$ , then $M\times \mathsf{M}⊩x$ ;

(b)

If $x\notin {\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c$ , then $\mathrm{\Gamma }\times \mathrm{\Delta }⊮x$ .

Proof.

(a) Let $M=(W,R,V)$ , $\mathsf{M}=(\mathsf{W},\mathsf{R},\mathsf{p}\mathsf{r}\mathsf{e})$ , and $M\times \mathsf{M}=(\overline{W},\overline{R},\overline{V})$ . We consider only seriality here (the rest follows from Lemma 5(a) and Definition 12. Case $x=\lambda$ . For any $(s,\mathsf{s})\in \overline{W}$ and $i\in \mathrm{ag}$ , there exist $t\in W$ and $\mathsf{t}\in \mathsf{W}$ such that $(s,t)\in R_i$ and $(\mathsf{s},\mathsf{t})\in {\mathsf{R}}_i$ . So there exists $(t,\mathsf{t})\in \overline{W}$ such that $((s,\mathsf{s}),(t,\mathsf{t}))\in {\overline{R}}_i$ . Thus, $M\times \mathsf{M}⊩\lambda$ .

Statement (b) can be shown in a similar way to the proof of Lemma 5(b).

Theorem 16

For any frame conditions $\mathrm{\Gamma },\mathrm{\Delta }\subseteq \mathcal{C}$ , $\mathrm{\Gamma }\times \mathrm{\Delta }⊩!{\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c$ .

Proof.

For any model $M=(W,R,V)$ and action $\mathsf{M}=(\mathsf{W},\mathsf{R},\mathsf{p}\mathsf{r}\mathsf{e})$ such that $M⊩\mathrm{\Gamma }$ and $\mathsf{M}⊩\mathrm{\Delta }$ , we have $M⊩{\mathrm{\Gamma }}^c$ and $\mathsf{M}⊩{\mathrm{\Delta }}^c$ by definition. Hence $M⊩{\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c$ and $\mathsf{M}⊩{\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c$ . By Lemma 15(a), $M\times \mathsf{M}⊩{\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c$ . Moreover, by Lemma 15(b), $\mathrm{\Gamma }\times \mathrm{\Delta }⊮x$ for any $x\in \mathcal{C}\setminus ({\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c)$ . Therefore, $\mathrm{\Gamma }\times \mathrm{\Delta }⊩!{\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c$ .

We now come to the preservation of group conditions. The result is presented in Theorems 18 and 19, and summarized in Tables 2 and 5.

Table 5.

Preservation of Transitive-Unionedness Under the Execution of Unconditional Actions (i.e., For Each $\mathrm{\Gamma },\mathrm{\Delta }\in \mathcal{C}$ , Does $(\mathrm{\Gamma }\cup \{{\upsilon }^{+}\})*(\mathrm{\Delta }\cup \{{\upsilon }^{+}\})⊩{\upsilon }^{+}$ Hold?).

	Frame Conditions $\mathrm{\Delta }$ of Unconditional Actions
Conditions $\mathrm{\Gamma }$ of Models	KDB	T	S4	B	S5	Others
KDB	No	Yes	Yes	Yes	Yes	No
T	Yes	Yes	Yes	Yes	Yes	No
S4	Yes	Yes	Yes	Yes	Yes	No
B	Yes	Yes	Yes	Yes	Yes	No
S5	Yes	Yes	Yes	Yes	Yes	No
Others	No	No	No	No	No	No

Lemma 17

• (a)

Let $M=(W,R,V)$ be a model, $\mathsf{M}=(\mathsf{W},\mathsf{R},\mathsf{\text{V}})$ an action and $M*\mathsf{M}=(\overline{W},\overline{R},\overline{V})$ . For any group $G\in \mathrm{gr}$ , $\underset{i\in G}{⨄}{\overline{R}}_i\subseteq {\overline{R}}_G^C$ .

(b)

$\{\rho ,{\upsilon }^{+}\}*\{\rho ,{\upsilon }^{+}\}⊩{\upsilon }^{+}$ .

(c)

$\{\rho ,{\upsilon }^{+}\}*\{\lambda ,\sigma ,{\upsilon }^{+}\}⊩{\upsilon }^{+}$ .

(d)

$\{\lambda ,\sigma ,{\upsilon }^{+}\}*\{\rho ,{\upsilon }^{+}\}⊩{\upsilon }^{+}$ .

Proof.

(a) Suppose $((s,\mathsf{s}),(t,\mathsf{t}))\in \underset{i\in G}{⨄}{\overline{R}}_i$ . There must be a path of $M*\mathsf{M}$ from $(s,\mathsf{s})$ to $(t,\mathsf{t})$ . It follows that there exist $s_0,\dots ,s_n\in W$ , $i_1,\dots ,i_n\in G$ and ${\mathsf{s}}_0,\dots ,{\mathsf{s}}_n\in \mathsf{W}$ such that $s=s_0$ , $t=s_n$ , $\mathsf{s}={\mathsf{s}}_0$ , $\mathsf{t}={\mathsf{s}}_n$ , and for $0\le x<n$ , $((s_x,{\mathsf{s}}_x),(s_{x+1},{\mathsf{s}}_{x+1}))\in {\overline{R}}_{i_{x+1}}$ . For $0\le x<n$ , it follows that $(s_x,s_{x+1})\in R_{i_{x+1}}$ and $({\mathsf{s}}_x,{\mathsf{s}}_{x+1})\in R_{i_{x+1}}$ . Hence, $(s,t)\in R_G^C$ and $(\mathsf{s},\mathsf{t})\in {\mathsf{R}}_G^C$ , implying that $((s,\mathsf{s}),(t,\mathsf{t}))\in {\overline{R}}_G^C$ .

(b) Given a model $M=(W,R,V)$ such that $M⊩\{\rho ,{\upsilon }^{+}\}$ , an action $\mathsf{M}=(\mathsf{W},\mathsf{R},\mathsf{\text{V}})$ such that $\mathsf{M}⊩\{\rho ,{\upsilon }^{+}\}$ , Let $M*\mathsf{M}=(\overline{W},\overline{R},\overline{V})$ . We show that $M*\mathsf{M}⊩{\upsilon }^{+}$ . By statement (a), it suffices to show that ${\overline{R}}_G^C\subseteq \underset{i\in G}{⨄}{\overline{R}}_i$ . Specifically, we need to show that $((s,\mathsf{s}),(t,\mathsf{t}))\in \underset{i\in G}{⨄}{\overline{R}}_i$ follows from $(s,t)\in R_G^C$ and $(\mathsf{s},\mathsf{t})\in {\mathsf{R}}_G^C$ . Suppose that there are $i_1,\dots ,i_n,j_1,\dots ,j_m\in G$ , $s_0,\dots ,s_n\in W$ and ${\mathsf{s}}_0,\dots ,{\mathsf{s}}_m\in \mathsf{W}$ such that $⟨s_0,R_{i_1},s_1,R_{i_2},\dots ,R_{i_n},s_n⟩$ is a path of $M$ from $s$ to $t$ and $⟨{\mathsf{s}}_0,{\mathsf{R}}_{j_1},{\mathsf{s}}_1,{\mathsf{R}}_{j_2},\dots ,{\mathsf{R}}_{j_m},{\mathsf{s}}_m⟩$ is a path of $\mathsf{M}$ from $\mathsf{s}$ to $\mathsf{t}$ . Since $M⊩\rho$ , $⟨(s_0,{\mathsf{s}}_0),{\overline{R}}_{j_1},(s_0,{\mathsf{s}}_1),{\overline{R}}_{j_2},\dots ,{\overline{R}}_{j_m},(s_0,{\mathsf{s}}_m)⟩$ is a path of $M*\mathsf{M}$ from $(s,\mathsf{s})$ to $(s,\mathsf{t})$ . Thus, $((s,\mathsf{s}),(s,\mathsf{t}))\in \underset{i\in G}{⨄}{\overline{R}}_i$ . Similarly, since $\mathsf{M}⊩\rho$ , we have $((s,\mathsf{t}),(t,\mathsf{t}))\in \underset{i\in G}{⨄}{\overline{R}}_i$ . Therefore, $((s,\mathsf{s}),(t,\mathsf{t}))\in \underset{i\in G}{⨄}{\overline{R}}_i$ .

(c) We start by similar argument to the proof of statement (b). We need to show $((s,\mathsf{s}),(t,\mathsf{t}))\in \underset{i\in G}{⨄}{\overline{R}}_i$ and we have obtained $((s,\mathsf{s}),(s,\mathsf{t}))\in \underset{i\in G}{⨄}{\overline{R}}_i$ . Now, since $\mathsf{M}⊩\{\lambda ,\sigma \}$ , for any $i\in G$ , there exists ${\mathsf{u}}_i\in \mathsf{W}$ such that both $(\mathsf{t},\mathsf{u}),(\mathsf{u},\mathsf{t})\in {\mathsf{R}}_i$ . Hence $⟨(s_0,\mathsf{t}),{\overline{R}}_{i_1},(s_0,{\mathsf{u}}_{i_1}),{\overline{R}}_{i_1},(s_1,\mathsf{t}),{\overline{R}}_{i_2},(s_1,{\mathsf{u}}_{i_2}),{\overline{R}}_{i_2},\dots ,{\overline{R}}_{i_n},(s_{n-1},{\mathsf{u}}_{i_n}),{\overline{R}}_{i_n},(s_n,\mathsf{t}))$ is a path of $M*\mathsf{M}$ from $(s,\mathsf{t})$ to $(t,\mathsf{t})$ . It follows that $((s,\mathsf{t}),(t,\mathsf{t}))\in \underset{i\in G}{⨄}{\overline{R}}_i$ . Therefore, $((s,\mathsf{s}),(t,\mathsf{t}))\in \underset{i\in G}{⨄}{\overline{R}}_i$ .

Statement (d) can be shown by similar argument to that of statement (c).

Theorem 18

• (a)

Intersectivity is preserved under unconditional actions. That is, for any model $M$ and action $\mathsf{M}$ , if $M⊩\iota$ and $\mathsf{M}⊩\iota$ , then $M*\mathsf{M}⊩\iota$ .

(b)

Unionedness is not preserved under unconditional actions. That is, for any $\mathrm{\Gamma },\mathrm{\Delta }\subseteq \mathcal{C}$ , there exist a model $M$ and an action $\mathsf{M}$ , such that $M⊩\mathrm{\Gamma }\cup \{\upsilon \}$ and $\mathsf{M}⊩\mathrm{\Delta }\cup \{\upsilon \}$ , but $M*\mathsf{M}⊮\upsilon$ .

Proof.

Statement (a) follows from Theorem 9(a) and Definition 12. For statement (b), we can reuse the proof of Theorem 9(b), where the action constructed is in fact an unconditional action, and the statement follows from Definition 12.

Theorem 19 (partial preservation of ${\upsilon }^{+}$ under unconditional actions)

Given frame conditions $\mathrm{\Gamma },\mathrm{\Delta }\subseteq \mathcal{C}$ :

(a)

If $\rho \in {\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c$ , then $(\mathrm{\Gamma }\cup \{{\upsilon }^{+}\})*(\mathrm{\Delta }\cup \{{\upsilon }^{+}\})⊩{\upsilon }^{+}$ ;

(b)

If $\rho \in {\mathrm{\Gamma }}^c$ and $\lambda ,\sigma \in {\mathrm{\Delta }}^c$ , then $(\mathrm{\Gamma }\cup \{{\upsilon }^{+}\})*(\mathrm{\Delta }\cup \{{\upsilon }^{+}\})⊩{\upsilon }^{+}$ ;

(c)

If $\lambda ,\sigma \in {\mathrm{\Gamma }}^c$ and $\rho \in {\mathrm{\Delta }}^c$ , then $(\mathrm{\Gamma }\cup \{{\upsilon }^{+}\})*(\mathrm{\Delta }\cup \{{\upsilon }^{+}\})⊩{\upsilon }^{+}$ ;

(d)

In all other cases, $(\mathrm{\Gamma }\cup \{{\upsilon }^{+}\})*(\mathrm{\Delta }\cup \{{\upsilon }^{+}\})⊮{\upsilon }^{+}$ .

Proof.

Statements (a–c) follow from Lemmas 17(b–d), respectively. We show statement (d). The exceptions can be divided into the following subcases, by first negating the condition of statement (a):

(d1) $\rho \in {\mathrm{\Gamma }}^c$ and $\rho \notin {\mathrm{\Delta }}^c$ . The condition of statement (b) further rules out the case when $\lambda ,\sigma \in {\mathrm{\Delta }}^c$ . So we assume $\rho \notin {\mathrm{\Delta }}^c$ and $\{\lambda ,\sigma \}⊈{\mathrm{\Delta }}^c$ . It follows that either ${\mathrm{\Delta }}^c\subseteq \{\lambda ,\tau ,ϵ\}$ or ${\mathrm{\Delta }}^c\subseteq \{\tau ,\sigma ,ϵ\}$ . We first show the case for ${\mathrm{\Delta }}^c\subseteq \{\lambda ,\tau ,ϵ\}$ . Namely, we show that if ${\mathrm{\Delta }}^c\subseteq \{\lambda ,\tau ,ϵ\}$ , then there exist a model $M$ and an action $\mathsf{M}$ such that $M⊩\mathrm{\Gamma }\cup \{{\upsilon }^{+}\}$ and $\mathsf{M}⊩\mathrm{\Delta }\cup \{{\upsilon }^{+}\}$ , but $M*\mathsf{M}⊮{\upsilon }^{+}$ . Let $a,b\in \mathrm{ag}$ be two distinct agents. Let $M=(W,R,V)$ be a model such that (i) $W=\{s,t\}$ , (ii) $R_a=W*W$ , (iii) $R_b=\{(s,s),(t,t)\}$ , and (iv) $R$ is transitive-unioned (i.e., $R_G^C=\underset{i\in G}{⨄}{R}_i$ for all $G$ ). Clearly, $M⊩\mathcal{C}\cup \{{\upsilon }^{+}\}$ . Furthermore, let $\mathsf{M}=(\mathsf{W},\mathsf{R},\mathsf{p}\mathsf{r}\mathsf{e})$ be an action such that (i) $\mathsf{W}=\{\mathsf{s},\mathsf{t},\mathsf{u}\}$ , (ii) ${\mathsf{R}}_a=\{(\mathsf{s},\mathsf{u}),(\mathsf{t},\mathsf{u}),(\mathsf{u},\mathsf{u})\}$ , ${\mathsf{R}}_b=\{(\mathsf{s},\mathsf{t}),(\mathsf{t},\mathsf{t}),(\mathsf{u},\mathsf{u})\}$ , and (iv) $\mathsf{R}$ is transitive-unioned. Let $M*\mathsf{M}=(\overline{W},\overline{R},\overline{V})$ . Clearly, $\mathsf{M}$ only satisfies the frame conditions $\lambda$ , $\tau$ and $ϵ$ (and group condition ${\upsilon }^{+}$ ). See the illustration below.

It can be verified that $((s,\mathsf{s}),(t,\mathsf{t}))\notin {\overline{R}}_a\uplus {\overline{R}}_b$ . However, $(s,t)\in R_{ab}^C$ and $(\mathsf{s},\mathsf{t})\in {\mathsf{R}}_{ab}^C$ , implying $((s,\mathsf{s}),(t,\mathsf{t}))\in {\overline{R}}_{ab}^C$ . Therefore, ${\overline{R}}_{ab}^C\ne {\overline{R}}_a\uplus {\overline{R}}_b$ , and consequently $M*\mathsf{M}⊮{\upsilon }^{+}$ .

Case for ${\mathrm{\Delta }}^c\subseteq \{\tau ,\sigma ,ϵ\}$ . Let $a,b\in \mathrm{ag}$ be two different agents. Let $M=(W,R,V)$ , where $W=\{s,t\}$ , $R_a=W*W$ , $R_b=\{(s,s),(t,t)\}$ and $R$ is transitive-unioned. Moreover, let $\mathsf{M}=(\mathsf{W},\mathsf{R},\mathsf{p}\mathsf{r}\mathsf{e})$ where $\mathsf{W}=\{\mathsf{s},\mathsf{t}\}$ , ${\mathsf{R}}_a=\mathrm{\varnothing }$ , ${\mathsf{R}}_b=\mathsf{W}*\mathsf{W}$ and $\mathsf{R}$ is transitive-unioned. One can verify that $M⊩\mathcal{C}\cup \{{\upsilon }^{+}\}$ , and $\mathsf{M}$ has the frame conditions $\tau$ , $\sigma$ and $ϵ$ (together with group condition ${\upsilon }^{+}$ ), but not the others. Let $M*\mathsf{M}=(\overline{W},\overline{R},\overline{V})$ . It can be verified that both $(s,\mathsf{s})$ and $(s,\mathsf{t})$ have no successor under the relation ${\overline{R}}_a$ , while for the relation ${\overline{R}}_b$ , the only successors of $(s,\mathsf{s})$ and $(s,\mathsf{t})$ are themselves. We conclude that $((s,\mathsf{s}),(t,\mathsf{t}))\notin {\overline{R}}_a\uplus {\overline{R}}_b$ . However, $((s,\mathsf{s}),(t,\mathsf{t}))\in {\overline{R}}_{ab}^C$ since $(s,t)\in R_{ab}^C$ and $(\mathsf{s},\mathsf{t})\in {\mathsf{R}}_{ab}^C$ . Therefore, ${\overline{R}}_{ab}^C\ne {\overline{R}}_a\uplus {\overline{R}}_b$ , and so $M*\mathsf{M}⊮{\upsilon }^{+}$ .

(d2) $\rho \notin {\mathrm{\Gamma }}^c$ and $\rho \in {\mathrm{\Delta }}^c$ . The condition of statement (c) further rules out the case when $\lambda ,\sigma \in {\mathrm{\Gamma }}^c$ . So the condition for this subcase is $\rho \notin {\mathrm{\Gamma }}^c$ and $\{\lambda ,\sigma \}⊈{\mathrm{\Gamma }}^c$ . This can be shown in a similar way to the above.

(d3) $\rho \notin {\mathrm{\Gamma }}^c$ and $\rho \notin {\mathrm{\Delta }}^c$ . Note that subcase (d1) has covered the situation when “ $\rho \notin {\mathrm{\Delta }}^c$ and $\{\lambda ,\sigma \}⊈{\mathrm{\Delta }}^c$ ,” and subcase (d2) the situation when “ $\rho \notin {\mathrm{\Gamma }}^c$ and $\{\lambda ,\sigma \}⊈{\mathrm{\Gamma }}^c$ .” So it suffices to show here that “ $\rho \notin {\mathrm{\Delta }}^c$ and $\{\lambda ,\sigma \}\subseteq {\mathrm{\Delta }}^c$ ” and that “ $\rho \notin {\mathrm{\Gamma }}^c$ and $\{\lambda ,\sigma \}\subseteq {\mathrm{\Gamma }}^c$ .” As the reader can verify, $\text{KDB}=\{\lambda ,\sigma \}$ is the only closure of frame conditions satisfying the condition (see Section 3.1). Hence ${\mathrm{\Gamma }}^c={\mathrm{\Delta }}^c=\{\lambda ,\sigma \}$ . Construct a model $M=(W,R,V)$ where $W=\{s,t\}$ , $R_a=\{(s,t),(t,s)\}$ (for an $a\in \mathrm{ag}$ ) and $R$ is transitive-unioned. Construct an action $\mathsf{M}=(\mathsf{W},\mathsf{R},\mathsf{p}\mathsf{r}\mathsf{e})$ where $\mathsf{W}=\{\mathsf{s},\mathsf{t}\}$ , ${\mathsf{R}}_a=\{(\mathsf{s},\mathsf{t}),(\mathsf{t},\mathsf{s})\}$ and $\mathsf{R}$ is transitive-unioned. One can verify that $M$ and $\mathsf{M}$ have the frame conditions $\lambda$ and $\sigma$ , but not $\rho$ , $\tau$ or $ϵ$ . Let $M*\mathsf{M}=(\overline{W},\overline{R},\overline{V})$ . The unique successor of $(s,\mathsf{s})$ under ${\overline{R}}_a$ is $(t,\mathsf{t})$ , and the unique successor of $(t,\mathsf{t})$ under ${\overline{R}}_a$ is $(s,\mathsf{s})$ . Thus, $((s,\mathsf{s}),(s,\mathsf{t}))\notin \underset{i\in \{a\}}{⨄}{\overline{R}}_i$ . However, $((s,\mathsf{s}),(s,\mathsf{t}))\in {\overline{R}}_a^C$ since $(s,s)\in R_a^C$ and $(\mathsf{s},\mathsf{t})\in {\mathsf{R}}_a^C$ . Therefore, ${\overline{R}}_a^C\ne \underset{i\in \{a\}}{⨄}{\overline{R}}_i$ , implying $M*\mathsf{M}⊮{\upsilon }^{+}$ .

5. Discussion

This study has systematically explored frame and group conditions within the framework of action model logic (AML), yielding several key insights:

(a) Compatibility of frame conditions: Defining actions with frame conditions distinct from those of the model proves counterproductive, as the resulting model retains only the frame conditions shared by both. For example, when modeling knowledge with S5 frames, employing S5 action models is recommended to ensure consistency, aligning with established practices (van Ditmarsch et al., 2007).

(b) Preservation of frame conditions under action execution: Not all frame conditions persist under classical action execution. Seriality, in particular, is not preserved in frames lacking reflexivity. This to a certain extent supports the view that AML is better suited for epistemic logic, which typically assumes reflexivity (e.g., S4, S5), than for doxastic logic, which often relies on seriality without reflexivity (e.g., KD45). When modeling belief with KD45 frames, action execution yields only K45 properties, complicating the representation of belief dynamics. This is, of course, well-known in the dynamic epistemic logic community, having, e.g., been pointed out by Aucher (2008), and other types of models, such as plausibility models (Baltag & Smets, 2016), that to a certain extent avoids the problem have been introduced. Public announcements exhibit similar preservation limitations, whereas unconditional actions perform notably better, preserving exactly the frame conditions present before execution. However, this situation is a direct consequence of the fundamental assumption in dynamic epistemic logics that the new information (whether it is a public announcement or a partial observation of a more complex event) is automatically believed: if the agent can have consistent but wrong beliefs, it follows immediately that her beliefs might become inconsistent after receiving new (even potentially true) information, reflecting a situation where the agent has discovered that either her old beliefs were wrong or the new information is, or both. It is a classic problem in belief revision (Alchourrón et al., 1985) that accepting new truths without adjusting prior assumptions can create logical problems, and potential solutions include resolving inconsistencies syntactically (say, in the way of Alchourrón et al., 1985) or semantically (as in Lindqvist et al., 2023). The goal of this article has been to point out when and where such situations can occur, and when they can not.

(c) Preservation of group conditions under action execution: General actions align with group conditions tied to distributed belief but fail to preserve those associated with mutual or common belief. Unconditional actions show partial preservation of transitive-unionedness, though their overall preservation advantage remains modest. In contrast, public announcements demonstrate compatibility with mutual belief, highlighting a distinct preservation profile.

On one hand, AML excels in preserving most frame condition classes—particularly K, S4, and S5—under action execution, making it robust for certain epistemic contexts. However, challenges arise with frame conditions defined by existential formulas, such as seriality. Action execution retains successors only when they exist in both the original model and the action, forming a conjunctive requirement. Since existential quantifiers do not distribute over conjunctions, counterexamples emerge: a successor may exist in the model and another in the action, yet no single witness satisfies both, resulting in the loss of seriality post-execution. This issue extends to other epistemic frame conditions expressed existentially. For instance, the .2 axiom $(\mathrm{\neg }{B}_i\mathrm{\neg }{B}_i\varphi \to B_i\mathrm{\neg }{B}_i\mathrm{\neg }\varphi )$ , which encodes “convergence” ( $\mathrm{\forall }i\in \mathrm{ag},\mathrm{\forall }s,t,u\in W:((s,t)\in R_i\wedge (s,u)\in R_i)\to \mathrm{\exists }v\in W:((t,v)\in R_i\wedge (u,v)\in R_i)$ , has been proposed for epistemic logic systems like S4.2 (Lenzen, 1978; Stalnaker, 2006). Such conditions underscore the limitations of AML in fully capturing epistemic dynamics.

Plenty of opportunities present themselves for future work. Regarding belief updates (say, for KD45 models and actions) and the problem with seriality discussed above, while the result of the execution of a KD45 action on a KD45 model might be a K45 model without seriality, reflecting a situation where the combination of an agent’s existing beliefs and the new information is inconsistent, this does not happen for all KD45 actions. An interesting question, then, is: are there any actions that always preserve seriality after action execution? We have in fact already seen a class of such actions: the unconditional actions (Section 4.2). However, their use is relatively limited. It would be interesting to find other subclasses that makes sense in modeling beliefs and belief revision. We can in fact point out one such (broader) class, which we can call coherent actions, that will ensure that beliefs are always consistent after action execution. Given a model $M$ , a state $s$ in $M$ , an action $\mathsf{M}$ and an action state $\mathsf{s}$ in $\mathsf{M}$ , we say that the pointed action $(\mathsf{M},\mathsf{s})$ is coherent for $(M,s)$ if, whenever both $s$ and $\mathsf{s}$ have a successor, the precondition of an ${\mathsf{R}}_i$ -successor of $\mathsf{s}$ is true in an $R_i$ -successor state of $s$ for all agent $i$ . We can then say that an action $\mathsf{M}$ is coherent for a model $M$ , if for all action states $\mathsf{s}$ of $\mathsf{M}$ and all states $s$ of $M$ , $(\mathsf{M},\mathsf{s})$ is coherent for $(M,s)$ .

We can then observe that seriality is preserved under coherent actions—the following can be shown ⁹ :

• (a)

For any model $M$ and any action $\mathsf{M}$ that is coherent for $M$ , if $M⊩\lambda$ and $\mathsf{M}⊩\lambda$ , then $M\otimes \mathsf{M}⊩\lambda$ ;

(b)

For any sets $\mathrm{\Gamma },\mathrm{\Delta }\subseteq \mathcal{C}$ , $\mathrm{\Gamma }◯\mathrm{\Delta }⊩!{\mathrm{\Gamma }}^c\cap {\mathrm{\Delta }}^c$ .

While this works technically, it is, first, somewhat unsatisfactory in the sense that coherence is a property not of an action but of an action relative to a given model—the same action might be coherent in one model but not in another. Second, the practical relevance of coherent actions is not immediately obvious, and we leave finding interesting and practically relevant classes of seriality-preserving actions, possibly including classes of coherent actions, for future work.

Conversely, taking “natural” classes of action models, such as different variants of (semi-)private announcements, as starting points and mapping out their preservation properties is also of interest for future work. Also of interest is looking at other, perhaps less standard, notions of group belief and knowledge, such as somebody-knows (Ågotnes & Wáng, 2021), cautious and bold distributed belief (Lindqvist et al., 2023, 2024) and graded distributed belief (Lorini & Rozplokhas, 2025), as well as at other types of belief models such as plausibility models (Baltag & Smets, 2016) or evidence models and topological models (Baltag et al., 2022; Moss & Parikh, 1992; Özgün, 2017).