(Arbitrary) Partial Communication

TL;DR

This paper explores a novel form of partial, topic-based communication in multi-agent systems within dynamic epistemic logic, analyzing its properties, complexity, and how it compares to public announcements, including an extension with quantification over topics.

Contribution

It introduces a formal framework for topic-based partial communication, provides a complete axiomatisation, and compares its expressivity and complexity to public announcement models.

Findings

Partial communication is incomparable to public announcements in update effects.

Model checking for the extended language is PSPACE-complete.

The new language's expressivity is incomparable to that of public announcements.

Abstract

Communication within groups of agents has been lately the focus of research in dynamic epistemic logic (DEL). This paper studies a recently introduced form of partial (more precisely, topic-based) communication. This type of communication allows for modelling scenarios of multi-agent collaboration and negotiation, and it is particularly well-suited for situations in which sharing all information is not feasible/advisable. After presenting results on invariance and complexity of model checking, the paper compares partial communication to public announcements, probably the most well-known type of communication in DEL. It is shown that the settings are, update-wise, incomparable: there are scenarios in which the effect of a public announcement cannot be replicated by partial communication, and vice versa. Then, the paper shifts its attention to strategic topic-based communication. It does so by extending the language with a modality that quantifies over the topics the agents can `talk about'. For this new framework, it provides a complete axiomatisation, showing also that the new language's model checking problem is PSPACE-complete. The paper closes showing that, in terms of expressivity, this new language of arbitrary partial communication is incomparable to that of arbitrary public announcements.

Tables

Table 1. ?tablename? 1. Axiom system 𝖫 𝖫 \mathsf{L} .

PR: $⊢\phi$    for $\phi$ a propositionally valid scheme MP: If $⊢\phi$ and $⊢\phi \to \psi$ then $⊢\psi$

K${}_D$: $⊢D_{𝙶}\left(\phi \to \psi \right)\to \left(D_{𝙶}\phi \to D_{𝙶}\psi \right)$ G${}_D$: If $⊢\phi$ then $⊢D_{𝙶}\phi$ M${}_D$: $⊢D_{𝙶}\phi \to D_{{𝙶}^{\prime }}\phi$    for $𝙶\subseteq {𝙶}^{\prime }$

Table 2. ?tablename? 2. Additional axioms and rules for 𝖫 𝚂 : χ ! subscript 𝖫 : 𝚂 𝜒 \mathsf{L}_{{\mathtt{S}{:}\,\!\chi}!} .

A${}_{𝚂:\chi !}{}^{}{}_{}{}^p$:	$⊢\left[𝚂:\chi !\right]p\leftrightarrow p$
A${}_{𝚂:\chi !}{}^{}{}_{}{}^{\neg }$:	$⊢\left[𝚂:\chi !\right]\neg \phi \leftrightarrow \neg \left[𝚂:\chi !\right]\phi$
A${}_{𝚂:\chi !}{}^{}{}_{}{}^{\wedge }$:	$⊢\left[𝚂:\chi !\right](\phi \wedge \psi )\leftrightarrow (\left[𝚂:\chi !\right]\phi \wedge \left[𝚂:\chi !\right]\psi )$
A${}_{𝚂:\chi !}{}^{}{}_{}{}^D$:	$⊢\left[𝚂:\chi !\right]D_{𝙶}\phi \leftrightarrow (D_{𝚂\cup 𝙶}\left[𝚂:\chi !\right]\phi \wedge D_{𝙶}^{\chi }\left[𝚂:\chi !\right]\phi )$
RE${}_{𝚂:\chi !}$:	If $⊢{\phi }_1\leftrightarrow {\phi }_2$ then $⊢\left[𝚂:\chi !\right]{\phi }_1\leftrightarrow \left[𝚂:\chi !\right]{\phi }_2$

Table 3. ?tablename? 3. Axiom and rule of inference for the arbitrary case.

A${}_{𝚂:\ast !}$:	$⊢[𝚂:\ast !]\phi \to \left[𝚂:\chi !\right]\phi$  for $\chi \in ℒ$
R${}_{𝚂:\ast !}$:	If $⊢\eta \left(\left[𝚂:\chi !\right]\phi \right)$ for all $\chi \in ℒ$, then $⊢\eta \left([𝚂:\ast !]\phi \right)$

Equations

$$\phi ,\psi ::=p\mid \neg \phi \mid \phi \wedge \psi \mid D_{\mathtt{G}}\phi$$

$${\sim^{M}_{\varphi}}:=(\left\llbracket\varphi\right\rrbracket^{M}\times\left\llbracket\varphi\right\rrbracket^{M})\cup(\left\llbracket\lnot\varphi\right\rrbracket^{M}\times\left\llbracket\lnot\varphi\right\rrbracket^{M})$$

$$\begin{array}[]{c}\mathop{\operatorname{D}^{\chi}_{\mathtt{G}}}\varphi:=(\chi\rightarrow\mathop{\operatorname{D}_{\mathtt{G}}}(\chi\rightarrow\varphi))\land(\lnot\chi\rightarrow\mathop{\operatorname{D}_{\mathtt{G}}}(\lnot\chi\rightarrow\varphi))\\ \text{\small(\emph{``agents in $\mathtt{G}$ know distributively that $\chi$'s truth value implies $\varphi$''}),}\end{array}$$

$$\eta (♯)::=♯\mid \phi \to \eta (♯)\mid D_{\mathtt{G}}\eta (♯)\mid [\mathtt{S}:\chi !]\eta (♯)$$

$${chosen}_k:=\underset{1⩽i⩽k}{\bigwedge }({\hat{K}}_{\mathtt{a}}{p}_i\leftrightarrow \neg {\hat{K}}_{\mathtt{a}}{q}_i)\wedge \underset{k<i⩽n}{\bigwedge }({\hat{K}}_{\mathtt{a}}{p}_i\wedge {\hat{K}}_{\mathtt{a}}{q}_i).$$

$${R^{\prime}}_{\mathtt{i}}:={R}_{\mathtt{i}}\cap(\left\llbracket\xi\right\rrbracket^{M}\times\left\llbracket\xi\right\rrbracket^{M})\qquad\text{and}\qquad V^{\prime}(p):=V(p)\cap\left\llbracket\xi\right\rrbracket^{M}.$$

$$Z:=\mathopen{\{}{(u,u)\in(W\times\left\llbracket\xi\right\rrbracket^{M})\mid u\in\left\llbracket\xi\right\rrbracket^{M}}\mathclose{\}}$$

Full text

Communication within groups of agents has been lately the focus of research in dynamic epistemic logic (DEL). This paper studies a recently introduced form of partial (more precisely, topic-based) communication. This type of communication allows for modelling scenarios of multi-agent collaboration and negotiation, and it is particularly well-suited for situations in which sharing all information is not feasible/advisable. After presenting results on invariance and complexity of model checking, the paper compares partial communication to public announcements, probably the most well-known type of communication in DEL. It is shown that the settings are, update-wise, incomparable: there are scenarios in which the effect of a public announcement cannot be replicated by partial communication, and vice versa. Then, the paper shifts its attention to strategic topic-based communication. It does so by extending the language with a modality that quantifies over the topics the agents can ‘talk about’. For this new framework, it provides a complete axiomatisation, showing also that the new language’s model checking problem is PSPACE-complete. The paper closes showing that, in terms of expressivity, this new language of arbitrary partial communication is incomparable to that of arbitrary public announcements.

{CCSXML}

¡ccs2012¿ ¡concept¿ ¡concept_id¿10003752.10003790.10003793¡/concept_id¿ ¡concept_desc¿Theory of computation Modal and temporal logics¡/concept_desc¿ ¡concept_significance¿500¡/concept_significance¿ ¡/concept¿ ¡/ccs2012¿

\ccsdesc[500]Theory of computation Modal and temporal logics

1. Introduction

Epistemic logic (EL; Hintikka (1962)) is a powerful framework for representing the individual and collective knowledge/beliefs of a group of agents. When using relational ‘Kripke’ models, its crucial idea is the use of uncertainty for defining knowledge. Indeed, such structures assign to each agent a binary relation indicating indistinguishability among epistemic possibilities. Then, it is said that agent $\mathtt{i}$ knows that $\varphi$ is the case (syntactically: $\mathop{\operatorname{K}_{\mathtt{i}}}\varphi$) when $\varphi$ holds in all situations $\mathtt{i}$ considers possible. Despite its simplicity, EL has become a widespread tool, contributing to the formal study of complex multi-agent epistemic phenomena in philosophy Hendricks (2006), computer science Fagin et al. (1995), AI Meyer and van der Hoek (1995) and economics de Bruin (2010).

One of the most appealing aspects of EL is that it can be used for reasoning about information change. This has been the main subject of dynamic epistemic logic (DEL; van Ditmarsch et al. (2008); van Benthem (2011)), a field whose main feature is that actions are semantically represented as operations that transform the underlying semantic model. Within DEL, one of the simplest meaningful epistemic actions is that of a public announcement: an external source providing the agents with truthful information in a fully public way Plaza (1989); Gerbrandy and Groeneveld (1997). Yet, the agents do not need an external entity to feed them with facts: they can also share their individual information with one another. This is arguably a more suitable way of modelling information change in multi-agent (and, in particular, distributed) systems. Agents might occasionally receive information ‘from the outside’, but the most common form of interaction is the one in which they themselves engage in ‘conversations’ for sharing what they have come to know so far. It is this form of information exchange that allows independent entities to engage in collaboration, negotiation and so on.

Communication between agents can take several forms, with some of these alternatives explored within DEL. A single agent might share all her information with everybody, as modelled in Baltag (2010). Alternatively, a group of agents might share all their information only among themselves, as represented by the action of “resolving distributed knowledge” from Ågotnes and Wáng (2017). One can even think about this form of communication not as a form of ‘sharing’, but rather as a form of ‘taking’ Baltag and Smets (2020, 2021), which allows the study of public and private forms of reading someone else’s information (e.g., hacking).

All these approaches for inter-agent communication have a common feature: the sharing agents share all their information. This is of course useful, as then one can reason about the best the agents can do together. But there are also scenarios (arguably more common) in which sharing all her available information might not be feasible or advisable for an agent. For the first, there might be constraints on the communication channels; for the second, agents might not be in a cooperative scenario, but rather in a competitive one. In such cases, one would be rather interested in studying forms of partial communication, through which agents share only ‘part of what they know’. There might be different ways to make precise what each agent shares, but a natural one is to assume that the ‘conversation’ is relative to a subject/topic, defined by a given formula $\chi$. Introduced in Velázquez-Quesada (2022), this type of communication allows a more realistic modelling of scenarios of multi-agent collaboration and negotiation. The first part of this paper studies computational aspects of this partial communication framework. It starts (section 2) by recalling the main definitions and axiom system, providing then novel invariance and model checking results. After that, it discusses (section 3) the setting’s relationship with the public announcement framework, showing that although the languages are equally expressive, in general the operations cannot mimic each other.

Still, in truly competitive scenarios, what matters the most is the decision of what to share. In other words, what matters is to reason about strategic topic-based communication. To do so, the second part of this paper introduces a framework for quantifying over the conversation’s topic. It presents (section 4) the basic definitions, providing then results on invariance, axiom system, expressivity and model checking. After that, it compares this new setting with that of arbitrary public announcements, proving that the languages are, expressivity-wise, incomparable. section 5 contrasts choices made with their alternatives, and section 6 summarises the paper’s contents, discussing also further research lines.

2. Background

Throughout this text, let $\mathtt{A}$ be a finite non-empty group of agents, and let $\mathtt{P}$ be a non-empty enumerable set of atomic propositions.

Definition \thetheorem (Model).

A multi-agent relational model (from now on, a model) is a tuple $M=\left\langle W,R,V\right\rangle$ where $W$ (also denoted as $\mathfrak{D}(M)$) is a non-empty set of objects called possible worlds, $R=\left\{{R}_{\mathtt{i}}\subseteq W\times W\mid\mathtt{i}\in\mathtt{A}\right\}$ assigns a binary “indistinguishability” relation on $W$ to each agent in $\mathtt{A}$ (for $\mathtt{G}\subseteq\mathtt{A}$, define ${R}_{\mathtt{G}}:=\bigcap_{\mathtt{k}\in\mathtt{G}}{R}_{\mathtt{k}}$), and $V:\mathtt{P}\to\wp({W})$ is an atomic valuation (with $V(p)$ the set of worlds in $M$ where $p\in\mathtt{P}$ holds). A pair $(M,w)$ with $M$ a model and $w\in\mathfrak{D}(M)$ is a pointed model, with $w$ being the evaluation point. A model $M$ is finite iff both $W$ and $\bigcup_{w\in W}\{p\in\mathtt{P}\mid w\in V(p)\}$ are finite. If $M=\left\langle W,R,V\right\rangle$ is finite, its size (notation: $|M|$) is $|W|+\sum_{\mathtt{i}\in\mathtt{A}}|{R}_{\mathtt{i}}|+\sum_{w\in W}|\left\{p\in\mathtt{P}\mid w\in V(p)\right\}|$.

In a model, the agents’ indistinguishability relations are arbitrary. In particular, they need to be neither reflexive nor symmetric nor Euclidean nor transitive. Hence, “knowledge” here is neither truthful nor positively/negatively introspective. It rather corresponds simply to “what is true in all the agent’s epistemic alternatives”.

Definition \thetheorem (Relative expressivity).

Let $\mathcal{L}_{1}$ and $\mathcal{L}_{2}$ be two languages interpreted over pointed models. It is said that $\mathcal{L}_{2}$ is at least as expressive as $\mathcal{L}_{1}$ (notation: $\mathcal{L}_{1}\preccurlyeq\mathcal{L}_{2}$) if and only if for every $\alpha_{1}\in\mathcal{L}_{1}$ there is $\alpha_{2}\in\mathcal{L}_{2}$ such that $\alpha_{1}$ and $\alpha_{2}$ have the same truth-value in every pointed model. Write $\mathcal{L}_{1}\approx\mathcal{L}_{2}$ when $\mathcal{L}_{1}\preccurlyeq\mathcal{L}_{2}$ and $\mathcal{L}_{2}\preccurlyeq\mathcal{L}_{1}$; write $\mathcal{L}_{1}\prec\mathcal{L}_{2}$ when $\mathcal{L}_{1}\preccurlyeq\mathcal{L}_{2}$ and $\mathcal{L}_{2}\not\preccurlyeq\mathcal{L}_{1}$; write $\mathcal{L}_{1}\asymp\mathcal{L}_{2}$ when $\mathcal{L}_{1}\not\preccurlyeq\mathcal{L}_{2}$ and $\mathcal{L}_{2}\not\preccurlyeq\mathcal{L}_{1}$.

Note: to show $\mathcal{L}_{1}\not\preccurlyeq\mathcal{L}_{2}$, it is enough to find two pointed models that agree in all $\alpha_{1}\in\mathcal{L}_{2}$ but can be distinguished by some $\alpha_{2}\in\mathcal{L}_{1}$.

2.1. Basic language

Here is this paper’s basic language for describing pointed models.

Definition \thetheorem (Language ${\mathcal{L}}$).

Formulas $\varphi,\psi$ in ${\mathcal{L}}$ are given by

[TABLE]

for $p\in\mathtt{P}$ and $\varnothing\subset\mathtt{G}\subseteq\mathtt{A}$. Boolean constants and other Boolean operators are defined as usual. Define also $\mathop{\operatorname{K}_{\mathtt{i}}}\varphi:=\mathop{\operatorname{D}_{\left\{\mathtt{i}\right\}}}\varphi$. The size of $\varphi$, denoted $|\varphi|$, is given by $|p|:=1$, $|\lnot\varphi|=|\mathop{\operatorname{D}_{\mathtt{G}}}\varphi|:=|\varphi|+1$ and $|\varphi\land\psi|:=|\varphi|+|\psi|+1$.

The language ${\mathcal{L}}$ contains a modality $\mathop{\operatorname{D}_{\mathtt{G}}}$ for each non-empty group of agents $\mathtt{G}\subseteq\mathtt{A}$. Formulas of the form $\mathop{\operatorname{D}_{\mathtt{G}}}\varphi$ are read as “the agents in $\mathtt{G}$ know $\varphi$ distributively”; thus, $\mathop{\operatorname{K}_{\mathtt{i}}}\varphi$ is read as “agent $\mathtt{i}$ knows $\varphi$”. The language’s semantic interpretation is as follows.

Definition \thetheorem (Semantic interpretation for ${\mathcal{L}}$).

Let $(M,w)$ be a pointed model with $M=\left\langle W,R,V\right\rangle$. The satisfiability relation $\Vdash$ between $(M,w)$ and formulas in ${\mathcal{L}}$ is defined inductively. Boolean cases are as usual; for the rest,

[TABLE]

Given a model $M$ and a formula $\varphi$,

• •

the set \left\llbracket\varphi\right\rrbracket^{M}:=\left\{w\in\mathfrak{D}(M)\mid(M,w)\Vdash\varphi\right\} contains the worlds in $\mathfrak{D}(M)$ in which $\varphi$ holds (also called $\varphi$-worlds);

• •

the (note: equivalence) relation

[TABLE]

splits $\mathfrak{D}(M)$ into (up to) two equivalence classes: one containing all $\varphi$-worlds, and the other containing all $\lnot\varphi$-worlds.

A formula $\varphi$ is valid (notation: $\Vdash\varphi$) if and only if $(M,w)\Vdash\varphi$ for every $w\in\mathfrak{D}(M)$ of every model $M$.

Axiom system.  The axiom system $\mathsf{L}$ (Table 1) characterises the formulas in ${\mathcal{L}}$ that are valid (see, e.g., Halpern and Moses (1990); Fagin et al. (1995)). Boolean operators are taken care of by PR and MP. For the modality $\mathop{\operatorname{D}_{\mathtt{G}}}$, while rule G${}_{\operatorname{D}}$ indicates that it ‘contains’ all validities, axiom K${}_{\operatorname{D}}$ indicates that it is closed under modus ponens, and axiom M${}_{\operatorname{D}}$ states that it is monotone on the group of agents (if $\varphi$ is distributively known by $\mathtt{G}$, then it is also distributively known by any larger group $\mathtt{G}^{\prime}$).

{theorem}

The axiom system $\mathsf{L}$ (Table 1) is sound and strongly complete for ${\mathcal{L}}$.

Structural equivalence.  The following notion will be useful.

Definition \thetheorem (Collective $\mathtt{Q}$-bisimulation Roelofsen (2007)).

Let $\mathtt{Q}\subseteq\mathtt{P}$ be a set of atoms; let $M=\langle W,R,V\rangle$ and $M^{\prime}=\langle W^{\prime},R^{\prime},V^{\prime}\rangle$ be two models. A non-empty relation $Z\subseteq W\times W^{\prime}$ is a collective $\mathtt{Q}$-bisimulation between $M$ and $M^{\prime}$ if and only if every $(u,u^{\prime})\in Z$ satisfies the following.

• •

Atoms. For every $p\in\mathtt{Q}$: $u\in V(p)$ if and only if $u^{\prime}\in V^{\prime}(p)$.

• •

Forth. For every $\mathtt{G}\subseteq\mathtt{A}$ and every $v\in W$: if ${R}_{\mathtt{G}}uv$ then there is $v^{\prime}\in W^{\prime}$ such that ${R^{\prime}}_{\mathtt{G}}u^{\prime}v^{\prime}$ and $(v,v^{\prime})\in Z$.

• •

Back. For every $\mathtt{G}\subseteq\mathtt{A}$ and every $v^{\prime}\in W^{\prime}$: if ${R^{\prime}}_{\mathtt{G}}u^{\prime}v^{\prime}$ then there is $v\in W$ such that ${R}_{\mathtt{G}}uv$ and $(v,v^{\prime})\in Z$.

Write $M\rightleftarrows_{C}^{\mathtt{Q}}M^{\prime}$ iff there is a collective $\mathtt{Q}$-bisimulation between $M$ and $M^{\prime}$. Write $(M,w)\rightleftarrows_{C}^{\mathtt{Q}}(M^{\prime},w^{\prime})$ iff a witness for $M\rightleftarrows_{C}^{\mathtt{Q}}M^{\prime}$ contains the pair $(w,w^{\prime})$. Remove the superindex “Q” when $\mathtt{Q}$ is the full set of atoms $\mathtt{P}$. Note: the relation of collective $\mathtt{Q}$-bisimilarity is an equivalence relation, both on models and pointed models.

The language ${\mathcal{L}}$ is invariant under collective bisimilarity.

{theorem}

[$\rightleftarrows_{C}$ implies ${\mathcal{L}}$-equivalence] Let $(M,w)$ and $(M^{\prime},w^{\prime})$ be two pointed models. If $(M,w)\rightleftarrows_{C}^{\mathtt{Q}}(M^{\prime},w^{\prime})$ then, for every $\psi\in{\mathcal{L}}$ containing only atoms from $\mathtt{Q}$,

[TABLE]

?proofname?

.

For showing that a form of model equivalence implies invariance for a language, one usually uses induction on the language’s formulas.111The proofs typically start by pulling out the universal quantifier over formulas, the statement becoming “for every $\varphi$, any structurally equivalent pointed models agree on $\varphi$’s truth-value”. This yields a stronger inductive hypothesis (IH) thanks to which the proof can go through. This will be done throughout the rest of the text. For $\mathtt{P}$-bisimilarity and ${\mathcal{L}}$, see Roelofsen (2007). ∎

Model checking  This problem for $\mathcal{L}$ is in P (Fagin et al., 1995, Page 67).

2.2. Partial (topic-based) communication

Through an action of partial communication, a group of agents $\mathtt{S}\subseteq\mathtt{A}$ share, with everybody, all their information about a given topic $\chi$. To define it, consider first a simpler action. After agents in $\mathtt{S}$ share all their information with everybody, an agent $\mathtt{i}$ will consider a world $u$ possible from a world $w$ if and only if she and every agent in $\mathtt{S}$ considered $u$ possible from $w$ (i.e., $\mathtt{i}$’s new relation ${R^{{\mathtt{S}}!}}_{\mathtt{i}}$ is the intersection of ${R}_{\mathtt{i}}$ and ${R}_{\mathtt{S}}$). In other words, after full communication, at $w$ agent $\mathtt{i}$ will consider $u$ possible if and only if neither her nor any agent in $\mathtt{S}$ could rule out $u$ from $w$ before the action. But if agents in $\mathtt{S}$ share only ‘their information about $\chi$’ (intuitively, only what has allowed them to distinguish between $\chi$- and $\lnot\chi$-worlds), edges between worlds agreeing in $\chi$’s truth-value are not ‘part of the discussion’; thus, they should not be eliminated.

Definition \thetheorem (Partial communication Velázquez-Quesada (2022)).

Let $M=\left\langle W,R,V\right\rangle$ be a model; take a group of agents $\mathtt{S}\subseteq\mathtt{A}$ and a formula $\chi$. The model ${M_{{\mathtt{S}{:}\,\chi}!}}=\langle W,R^{{\mathtt{S}{:}\,\chi}!},V\rangle$, the result of agents in $\mathtt{S}$ sharing all they know about $\chi$ with everybody, is such that

[TABLE]

Thus, ${R^{{\mathtt{S}{:}\,\chi}!}}_{\mathtt{G}}=\bigcap_{\mathtt{i}\in\mathtt{G}}{R^{{\mathtt{S}{:}\,\chi}!}}_{\mathtt{i}}={R}_{\mathtt{G}}\cap({R}_{\mathtt{S}}\cup{\sim^{M}_{\chi}})={R}_{\mathtt{G}\cup\mathtt{S}}\cup({R}_{\mathtt{G}}\cap{\sim^{M}_{\chi}})$. Additionally, ${R^{{\varnothing{:}\,\chi}!}}_{\mathtt{i}}={R}_{\mathtt{i}}$.

Definition \thetheorem (Modality $\mathop{[{\mathtt{S}{:}\,\chi}!]}$ and language $\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$ Velázquez-Quesada (2022)).

The language $\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$ extends ${\mathcal{L}}$ with a modality $\mathop{[{\mathtt{S}{:}\,\chi}!]}$ for each $\mathtt{S}\subseteq\mathtt{A}$ and each formula $\chi$. More precisely, define first $\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}^{0}={\mathcal{L}}$, and then define $\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}^{i+1}$ as the result of extending $\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}^{i}$ with an additional modality $\mathop{[{\mathtt{S}{:}\,\chi}!]}$ for $\mathtt{S}\subseteq\mathtt{A}$ and $\chi\in\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}^{i}$. The language $\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$ is then defined as $\bigcup_{i\in\mathbb{N}}\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}^{i}$. For its semantic interpretation,

[TABLE]

Defining $\mathop{\langle{\mathtt{S}{:}\,\chi}!\rangle}\varphi:=\lnot\mathop{[{\mathtt{S}{:}\,\chi}!]}\lnot\varphi$ implies $\Vdash\mathop{\langle{\mathtt{S}{:}\,\chi}!\rangle}\varphi\leftrightarrow\mathop{[{\mathtt{S}{:}\,\chi}!]}\varphi$. The size of a formula $\varphi\in\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$ is as in subsection 2.1, with the additional clause $|\mathop{[{\mathtt{S}{:}\,\chi}!]}\varphi|:=|\chi|+|\varphi|+1$.

Further motivation and details on partial communication can be found in Velázquez-Quesada (2022). Still, here are two revealing properties: $\Vdash\mathop{[{\mathtt{S}{:}\,\chi_{1}}!]}\varphi\leftrightarrow\mathop{[{\mathtt{S}{:}\,\chi_{2}}!]}\varphi$ for $\Vdash\chi_{1}\leftrightarrow\chi_{2}$ (logically equivalent topics have the same communication effect) and $\Vdash\mathop{[{\mathtt{S}{:}\,\chi}!]}\varphi\leftrightarrow\mathop{[{\mathtt{S}{:}\,\lnot\chi}!]}\varphi$ (communication on a topic is just as communication on its negation).

Axiom system.  The axioms and rule of Table 2 form, together with those in Table 1, a sound and strongly complete axiom system for $\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$. They rely on the DEL reduction axioms technique (for an explanation, see Wang and Cao (2013) or (van Ditmarsch et al., 2008, Section 7.4)), with axiom A${}^{\operatorname{D}}_{{\mathtt{S}{:}\,\!\chi}!}$ being the crucial one. Using the abbreviation

[TABLE]

the axiom indicates that a group $\mathtt{G}$ knows $\varphi$ distributively after the action ($\mathop{[{\mathtt{S}{:}\,\chi}!]}\mathop{\operatorname{D}_{\mathtt{G}}}\varphi$) if and only if the group $\mathtt{S}\cup\mathtt{G}$ knew, distributively, that $\varphi$ would hold after the action ($\mathop{\operatorname{D}_{\mathtt{S}\cup\mathtt{G}}}\mathop{[{\mathtt{S}{:}\,\chi}!]}\varphi$) and the agents in $\mathtt{G}$ know distributively that $\chi$’s truth-value implies the action will make $\varphi$ true ($\mathop{\operatorname{D}^{\chi}_{\mathtt{G}}}\mathop{[{\mathtt{S}{:}\,\chi}!]}\varphi$).

From Table 2 one can define a truth-preserving translation from $\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$ to ${\mathcal{L}}$, thanks to which the following theorem can be proved.

{theorem}

[Velázquez-Quesada (2022)] The axiom system $\mathsf{L}_{{\mathtt{S}{:}\,\!\chi}!}$ ($\mathsf{L}$ [Table 1]+Table 2) is sound and strongly complete for $\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$.

Structural equivalence.  The modality $\mathop{[{\mathtt{S}{:}\,\chi}!]}$ is invariant under collective bisimilarity.

{theorem}

[$\rightleftarrows_{C}$ implies $\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$-equivalence] Let $(M,w)$ and $(M^{\prime},w^{\prime})$ be two pointed models. If $(M,w)\rightleftarrows_{C}(M^{\prime},w^{\prime})$ then, for every $\psi\in\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$,

[TABLE]

?proofname?.

The language $\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$ is $\bigcup_{i\in\mathbb{N}}\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}^{i}$, so the proof proceeds by induction on $i$. The text proves a stronger statement: for every $\psi\in\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$ and every $M$ and $M^{\prime}$, if $(M,w)\rightleftarrows_{C}(M^{\prime},w^{\prime})$ then

(1) $(M,w)\Vdash\psi$iff $(M^{\prime},w^{\prime})\Vdash\psi$, and (2) $({M_{{\mathtt{S}{:}\,\psi}!}},w)\rightleftarrows_{C}({M^{\prime}_{{\mathtt{S}{:}\,\psi}!}},w^{\prime})$ . Details can be found in the appendix. ∎

Expressivity.  It is clear that ${\mathcal{L}}\preccurlyeq\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$, as every formula in the former is also in the latter. Moreover: the reduction axioms in Table 2 define a recursive translation $\mathit{tr}:\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}\to{\mathcal{L}}$ such that $\varphi\in\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$ implies $\Vdash\varphi\leftrightarrow\mathit{tr}(\varphi)$ Velázquez-Quesada (2022).222Note: the translation’s complexity might be exponential, as it is for similar DELs (e.g., public announcement: Lutz (2006)). This implies $\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}\preccurlyeq{\mathcal{L}}$ and thus ${\mathcal{L}}\approx\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$: the languages ${\mathcal{L}}$ and $\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$ are equally expressive.

Model checking  The original work on topic-based communication Velázquez-Quesada (2022) did not discuss computational complexity. Here we address that of the model checking problem for $\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$.

Given a finite pointed model $(M,w)$ and a formula $\varphi\in\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$, the model checking strategy is as follows. Start by creating the list $\operatorname{sub}(\varphi)$ of all subformulas of $\varphi$ and all partial communication modalities $\mathop{[{\mathtt{S}{:}\,\chi}!]}$ in it. Next, similarly to the approach in Kuijer (2015), label each element of $\operatorname{sub}(\varphi)$ with the sequence of partial communication modalities inside the scope of which it appears. Finally, order the resulting list as follows: for $\psi^{\sigma}_{1},\psi^{\tau}_{2}\in\operatorname{sub}(\varphi)$ (with $\sigma$ and $\tau$ the labellings) we have that $\psi^{\sigma}_{1}$ precedes $\psi^{\tau}_{2}$ if and only if

• •

$\psi^{\sigma}_{1}$ and $\psi^{\tau}_{2}$ are parts of modalities $\mathop{[{\mathtt{S}{:}\,\chi}!]}$, and $\sigma<\tau$,333That is, $\sigma$ is a proper prefix of $\tau$. or else

• •

$\psi^{\sigma}_{1}$ appears within some $\mathop{[{\mathtt{S}{:}\,\chi}!]}$, and $\psi^{\tau}_{2}$ does not, or else

• •

$\psi^{\sigma}_{1}$ is of the form $\mathop{[{\mathtt{S}{:}\,\chi}!]}$, $\psi^{\tau}_{2}$ is not, and $\sigma<\tau$, or else

• •

neither $\psi^{\sigma}_{1}$ nor $\psi^{\tau}_{2}$ are parts of some $\mathop{[{\mathtt{S}{:}\,\chi}!]}$, and $\tau<\sigma$, or else

• •

both $\psi^{\sigma}_{1}$ are $\psi^{\tau}_{2}$ are of the form $\mathop{[{\mathtt{S}{:}\,\chi}!]}$, and $\sigma<\tau$, or else

• •

$\sigma=\tau$, and $\psi^{\sigma}_{1}$ is a part of $\psi^{\tau}_{2}$, or else

• •

$\psi_{1}$ appears to the left of $\chi$ in $\varphi$.

The intuition behind such an ordering is to allow a model checking algorithm to deal with $\chi$’s within $\mathop{[{\mathtt{S}{:}\,\chi}!]}$’s before dealing with formulas within the scope of the modality. This way we ensure that, when we need to evaluate $\varphi$ in $\mathop{[{\mathtt{S}{:}\,\chi}!]}\varphi$, we already know the effect of $\mathop{[{\mathtt{S}{:}\,\chi}!]}$ on the model. As an example, consider $\varphi:=\mathop{[{\mathtt{S}_{1}{:}\,p\land q}!]}\mathop{[{\mathtt{S}_{2}{:}\,q}!]}\mathop{\operatorname{D}_{\mathtt{G}}}p$. The resulting ordered list $\operatorname{sub}(\varphi)$ is then $p$, $q$, $p\land q$, $\mathop{[{\mathtt{S}_{1}{:}\,p\land q}!]}$, $q^{\mathop{[{\mathtt{S}_{1}{:}\,p\land q}!]}}$, $\mathop{[{\mathtt{S}_{2}{:}\,q}!]}^{\mathop{[{\mathtt{S}_{1}{:}\,p\land q}!]}}$, $p^{\mathop{[{\mathtt{S}_{1}{:}\,p\land q}!]},\mathop{[{\mathtt{S}_{2}{:}\,q}!]}}$, $\mathop{\operatorname{D}_{\mathtt{G}}}p^{\mathop{[{\mathtt{S}_{1}{:}\,p\land q}!]},\mathop{[{\mathtt{S}_{2}{:}\,q}!]}}$, $\mathop{[{\mathtt{S}_{2}{:}\,q}!]}\mathop{\operatorname{D}_{\mathtt{G}}}p^{\mathop{[{\mathtt{S}_{1}{:}\,p\land q}!]}}$, $\varphi$.

Note: each subformula of $\varphi$ is labelled with exactly one (maybe empty) sequence of partial communication modalities. Moreover, we label communication modality symbols separately. The number of subformulas of $\varphi$ and modality symbols is bounded by $\mathcal{O}(|\varphi|)$. Since each element of $\operatorname{sub}(\varphi)$ is labelled by only one sequence of modalities, we use at most polynomial number of them.

\fname@algorithm** 1** An algorithm for global model checking for $\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$

1:procedure GlobalMC($M,\varphi$)

2:    for all $\psi^{\sigma}\in\operatorname{sub}(\varphi)$ do

3:        for all $w\in W$ do

4:           case $\psi^{\sigma}=\mathop{\operatorname{D}_{\mathtt{G}}}\chi^{\sigma}$

5:               $\mathit{check}\leftarrow\mathit{true}$

6:               for all $(w,v)\in R_{\mathtt{G}}$ do

7:                  if $(w,v)$ is labelled with $\sigma$ then

8:                      if $v$ is not labelled with $\chi^{\sigma}$ then

9:                          $\mathit{check}\leftarrow\mathit{false}$

10:                          break                                                        

11:               if $\mathit{check}$ then

12:                  label $w$ with $\mathop{\operatorname{D}_{\mathtt{G}}}\chi^{\sigma}$                           

13:           case $\psi^{\sigma}=\mathop{[{\mathtt{S}{:}\,\chi}!]}^{\sigma}$

14:               for all $\mathtt{i}\in\mathtt{A}$ do

15:                  for all $(v,u)\in R_{\mathtt{i}}$ do

16:                      if $(v,u)$ is labelled with $\sigma$ then

17:                          if $v$ is labelled with $\chi$ iff $u$ is labelled with $\chi$ then

18:                             label $(v,u)$ with $\sigma,\mathop{[{\mathtt{S}{:}\,\chi}!]}$

19:                          else

20:                             $\mathit{check}\leftarrow\mathit{true}$

21:                             for all $\mathtt{j}\in\mathtt{S}$ do

22:                                 if $(v,u)\not\in R_{\mathtt{j}}$ then

23:                                    $\mathit{check}\leftarrow\mathit{false}$

24:                                    break                                                               

25:                             if $\mathit{check}$ then

26:                                 label $(v,u)$ with $\sigma,\mathop{[{\mathtt{S}{:}\,\chi}!]}$                                                                                                                          

27:           case $\psi^{\sigma}=\mathop{[{\mathtt{S}{:}\,\chi}!]}\xi^{\sigma}$

28:               if $w$ is labelled with $\xi^{\sigma,\mathop{[{\mathtt{S}{:}\,\chi}!]}}$ then

29:                  label $w$ with $\mathop{[{\mathtt{S}{:}\,\chi}!]}\xi^{\sigma}$

The labelling Algorithm 2.2 is inspired by that for epistemic logic Halpern and Moses (1992). The crucial difference is that, besides labelling states, we also label transitions (case $\mathop{[{\mathtt{S}{:}\,\chi}!]}^{\sigma}$). This allows us to keep track of which relations ‘survive’ updates with partial communication modalities. The labelling of transitions is taken into account when dealing with the epistemic case $\mathop{\operatorname{D}_{\mathtt{G}}}\chi^{\sigma}$: we check only transitions that have ‘survived’ at a current step of an algorithm run.

Correctness of the algorithm can be shown by an induction on $\varphi$, noting that cases of the algorithm mimic the definition of semantics. From a computational perspective, the preparation of $\operatorname{sub}(\varphi)$ can be done in $\mathcal{O}(|\varphi|^{2})$ steps. The running time of GlobalMC is bounded by $\mathcal{O}(|\varphi|^{2}\cdot|W|\cdot|\mathtt{A}|\cdot|R|)$ for the case of $\mathop{[{\mathtt{S}{:}\,\chi}!]}^{\sigma}$.

{theorem}

The model checking problem for $\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$ is in P.

3. Partial communication vs. public announcements

The action for partial communication is, in a sense, similar to that for a public announcement: both are epistemic actions through which agents receive information about the truth-value of a specific formula. The difference is that, while in the latter the information comes from an external source, in the former the information comes from agents in the model. It makes sense to discuss the relationship between their formal representations.

Under its standard definition Plaza (1989), the public announcement of a formula $\xi$ transforms a model by eliminating all $\lnot\xi$-worlds. For a fair comparison with partial communication, here is an alternative public announcement definition that rather removes all edges between worlds disagreeing on $\xi$’s truth-value van Benthem and Liu (2007).444Cf. Gerbrandy and Groeneveld (1997), which removes only edges pointing to $\lnot\xi$-worlds. The option used here has the advantage of behaving, with respect to the preservation of certain relational properties (reflexivity, symmetry, transitivity), as the standard definition does.

Definition \thetheorem (Public announcement).

Let $M=\left\langle W,R,V\right\rangle$ be a model; take a formula $\xi$. The model $M_{\xi!}=\langle W,R^{\xi!},V\rangle$ is such that

[TABLE]

Thus, ${R^{\xi!}}_{\mathtt{G}}={R}_{\mathtt{G}}\cap{\sim^{M}_{\xi}}$.

The world-removing version and the edge-deleting alternative are collectively $\mathtt{P}$-bisimilar (see Proposition A.1 in the appendix), and thus interchangeable from ${\mathcal{L}}$’s perspective. Here is a modality for describing the operation’s effect.

Definition \thetheorem (Modality $\mathop{[\xi!]}$).

The language $\mathcal{L}_{\xi!}$ extends ${\mathcal{L}}$ with a modality $\mathop{[\xi!]}$ for $\xi$ a formula.555More precisely, $\mathcal{L}_{\xi!}^{1}$ extends $\mathcal{L}_{\xi!}^{0}={\mathcal{L}}$ with $\mathop{[\xi!]}$ for $\xi\in\mathcal{L}_{\xi!}^{0}$, $\mathcal{L}_{\xi!}^{2}$ extends $\mathcal{L}_{\xi!}^{1}$ with $\mathop{[\xi!]}$ for $\chi\in\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}^{1}$ and so on. The language $\mathcal{L}_{\xi!}$ is then defined as $\bigcup_{i\in\mathbb{N}}\mathcal{L}_{\xi!}^{i}$. For their semantic interpretation,

[TABLE]

Defining $\mathop{\langle\xi!\rangle}\varphi:=\lnot\mathop{[\xi!]}\lnot\varphi$ implies $\Vdash\mathop{\langle\xi!\rangle}\varphi\leftrightarrow(\xi\land\mathop{[\xi!]}\varphi)$.

It can be shown that $\mathcal{L}_{\xi!}$ is invariant under collective bisimilarity (see Theorem A.1 in the appendix). An axiom system can be obtained by using the reduction axioms technique, with the crucial axiom being $\mathop{[\xi!]}\mathop{\operatorname{D}_{\mathtt{G}}}\varphi\,\leftrightarrow\,(\xi\rightarrow\mathop{\operatorname{D}_{\mathtt{G}}}\mathop{[\xi!]}\varphi)$ Wáng and Ågotnes (2013). As before, the existence of the reduction axioms implies $\mathcal{L}_{\xi!}\preccurlyeq{\mathcal{L}}$. This, together with the straightforward ${\mathcal{L}}\preccurlyeq\mathcal{L}_{\xi!}$, implies ${\mathcal{L}}\approx\mathcal{L}_{\xi!}$: the languages ${\mathcal{L}}$ and $\mathcal{L}_{\xi!}$ are equally expressive.

When comparing partial communication with public announcements, a first natural question is about the languages’ relative expressivity. The answer is simple: $\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$ and $\mathcal{L}_{\xi!}$ are both reducible to ${\mathcal{L}}$, and thus they are equally expressive.

At the semantic level, one might wonder whether the operations can ‘mimic’ each other. More precisely, one can ask the following.

• •

Given $\xi\in{\mathcal{L}}$: are there $\mathtt{S}\subseteq\mathtt{A}$, $\chi\in{\mathcal{L}}$ such that $M_{\xi!}\rightleftarrows_{C}{M_{{\mathtt{S}{:}\,\chi}!}}$ for every $M$? (In symbols: $\forall\xi\,.\,\exists\mathtt{S}\,.\,\exists\chi\,.\,\forall M\,.\,(M_{\xi!}\rightleftarrows_{C}{M_{{\mathtt{S}{:}\,\chi}!}})$?)

• •

Given $\mathtt{S}\subseteq\mathtt{A}$, $\chi\in{\mathcal{L}}$: is there $\xi\in{\mathcal{L}}$ such that ${M_{{\mathtt{S}{:}\,\chi}!}}\rightleftarrows_{C}M_{\xi!}$ for every $M$? (In symbols: $\forall\mathtt{S}\,.\,\forall\chi\,.\,\exists\xi\,.\,\forall M\,.\,({M_{{\mathtt{S}{:}\,\chi}!}}\rightleftarrows_{C}M_{\xi!})$?)

Some known model-update operations have this relationship. For example, action models Baltag et al. (1998) generalise a standard public announcement: for every formula $\xi$ there is an action model that, when applied to any model, produces exactly the one that a public announcement of $\xi$ does. For another example, edge-deleting versions of a public announcement (both that in Gerbrandy and Groeneveld (1997) and that in Definition 3) can be represented within the arrow update framework of Kooi and Renne (2011).

Here, the answer to the first question is straightforward: the agents might not have, even together, the information that a public announcement provides.

Fact \thetheorem.

Take $\mathtt{A}=\left\{\mathtt{a}\right\}$ and $\mathtt{P}=\left\{p\right\}$; consider the (reflexive and symmetric) model $M$ below on the left. A public announcement of $p$ yields the model on the right.

[TABLE]

Now, there is no $\mathtt{S}\subseteq\mathtt{A}$ and $\chi\in{\mathcal{L}}$ such that ${M_{{\mathtt{S}{:}\,\chi}!}}\rightleftarrows_{C}M_{p!}$. The group $\mathtt{S}$ can be only $\varnothing$ or $\left\{\mathtt{a}\right\}$ and, in both cases, ${R^{{\mathtt{S}{:}\,\chi}!}}_{\mathtt{a}}={R}_{\mathtt{a}}$, regardless of the formula $\chi$.

Thus, $\forall M\,.\,\forall\xi\,.\,\exists\mathtt{S}\,.\,\exists\chi\,.\,(M_{\xi!}\rightleftarrows_{C}{M_{{\mathtt{S}{:}\,\chi}!}})$ fails: for the given model, the effect of a public announcement of $p$ cannot be replicated by any act of partial communication. This answers negatively the (stronger) first question above: there are no agents $\mathtt{S}$ and topic $\chi$ that can replicate the given public announcement in every model.

The answer to the second question is interesting: through partial communication, the agents can reach epistemic states that cannot be reached by a public announcement.

Fact \thetheorem.

Take $\mathtt{A}=\left\{\mathtt{a},\mathtt{b}\right\}$ and $\mathtt{P}=\left\{p,q\right\}$; consider the (reflexive and symmetric) model $M$ below on the left. A partial communication between all agents about $p\leftrightarrow q$ (equivalence classes highlighted) yields the model on the right.

[TABLE]

Now, there is no $\xi\in{\mathcal{L}}$ such that $M_{\xi!}\rightleftarrows_{C}{M_{{\left\{\mathtt{a},\mathtt{b}\right\}{:}\,(p\leftrightarrow q)}!}}$. For this, note that a public announcement preserves transitive indistinguishability relations; yet, while $M$ is transitive, ${M_{{\left\{\mathtt{a},\mathtt{b}\right\}{:}\,(p\leftrightarrow q)}!}}$ is not.

Thus, $\forall M\,.\,\forall\mathtt{S}\,.\,\forall\chi\,.\,\exists\xi\,.\,({M_{{\mathtt{S}{:}\,\chi}!}}\rightleftarrows_{C}M_{\xi!})$ fails: for the provided model, the effect of a ‘conversation’ among $\mathtt{a}$ and $\mathtt{b}$ on $p\leftrightarrow q$ cannot be replicated by any public announcement. This answers negatively the (stronger) second question above: there is no $\chi$ that can replicate the given partial communication in every model.

4. Arbitrary partial communication

The partial communication framework allows us to model inter-agent information exchange. Yet, consider competitive scenarios. While it is interesting to find out what a form of partial communication can achieve (fix the agents and the topic, then find the consequences), one might be also interested in deciding whether a given goal can be achieved by some form of partial communication (fix the goal: is there a group of agents and a topic that can achieve it?). This quantification over the sharing agents and the topic they discuss adds a strategic dimension to the framework. This is particularly useful when communication occurs over an insecure channel, as one would like to know whether some form of partial communication (who talks, and on which topic) can achieve a given goal (e.g., make something group or common knowledge while also precluding adversaries or eavesdroppers from learning it, as in van Ditmarsch (2003)). Thus, in the spirit of Balbiani et al. (2008), one can then quantify, either over the agents that communicate or over the topic they discuss.

Quantifying over the communicating agents does not need additional machinery: $\mathtt{A}$ is finite, so a modality stating that “$\varphi$ is true after any group of agents share all their information about $\chi$” is definable as $\mathop{[{\ast{:}\,\chi}!]}\varphi:=\bigwedge_{\mathtt{S}\subseteq\mathtt{A}}\mathop{[{\mathtt{S}{:}\,\chi}!]}\varphi$. Quantifying over the topic, though, requires additional tools.

4.1. Language, semantics, and basic results

Definition \thetheorem (Modality $\mathop{[{\mathtt{S}{:}\,\ast}!]}$).

The language ${\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$ extends $\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$ with a modality $\mathop{[{\mathtt{S}{:}\,\ast}!]}$ for each group of agents $\mathtt{S}\subseteq\mathtt{A}$. More precisely, take ${\mathcal{L}^{\ast,0}_{{\mathtt{S}{:}\,\!\chi}!}}={\mathcal{L}}^{\ast}$ to be ${\mathcal{L}}$ plus $\mathop{[{\mathtt{S}{:}\,\ast}!]}$. Then, define ${\mathcal{L}^{\ast,i+1}_{{\mathtt{S}{:}\,\!\chi}!}}$ as the result of extending ${\mathcal{L}^{\ast,i}_{{\mathtt{S}{:}\,\!\chi}!}}$ with $\mathop{[{\mathtt{S}{:}\,\chi}!]}$ for $\mathtt{S}\subseteq\mathtt{A}$ and $\chi\in{\mathcal{L}^{\ast,i}_{{\mathtt{S}{:}\,\!\chi}!}}$. The language ${\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$ is defined as $\bigcup_{i\in\mathbb{N}}{\mathcal{L}^{\ast,i}_{{\mathtt{S}{:}\,\!\chi}!}}$. For the semantic interpretation,

[TABLE]

If one defines $\mathop{\langle{\mathtt{S}{:}\,\ast}!\rangle}\varphi:=\lnot\mathop{[{\mathtt{S}{:}\,\ast}!]}\lnot\varphi$, then

[TABLE]

The size of $\varphi\in{\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$ is defined as in subsection 2.2 with the following additional clause: $|\mathop{[{\mathtt{S}{:}\,\ast}!]}\varphi|:=|\varphi|+1$.

Note: $\mathop{[{\mathtt{S}{:}\,\ast}!]}$ quantifies over formulas in ${\mathcal{L}}$, and not over formulas in ${\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$. As in Balbiani et al. (2008), this is to avoid circularity issues. One could have also chosen to quantify over formulas in $\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$, but ${\mathcal{L}}\approx\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$ (\autopagerefpar:trans.LAdSSE.to.LAd) so nothing is lost by using ${\mathcal{L}}$ instead.666Still, for languages with other types of group knowledge, adding a dynamic modality might increase the expressive power. For more on this (in the context of common knowledge and quantified announcements), the reader is referred to Galimullin and Ågotnes (2021).

Axiom system.  Axiomatising ${\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$ requires an additional notion.

Definition \thetheorem (Necessity Forms).

Take $\varphi\in{\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$, $\chi\in{\mathcal{L}}$, $\mathtt{S},\mathtt{G}\subseteq\mathtt{A}$ and $\sharp\not\in P$. The set of necessity forms Goldblatt (1982) is given by

[TABLE]

The result of replacing $\sharp$ with $\varphi$ in $\eta(\sharp)$ is denoted as $\eta(\varphi)$.

The (note: infinitary) axiom system for ${\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$ is given by the axioms and rules on Tables 1, 2 and 3. The system is similar to well-known axiomatisations of other logics of quantified epistemic actions (see van Ditmarsch (2020) for an overview). In Table 3, the soundness of A${}_{\mathop{[{\mathtt{S}{:}\,\ast}!]}}$ and R${}_{\mathop{[{\mathtt{S}{:}\,\ast}!]}}$ follow from $\mathop{[{\mathtt{S}{:}\,\ast}!]}$’s semantic interpretation. Completeness of the whole system can be shown by combining and adapting techniques from Wáng and Ågotnes (2013) (to deal with distributed knowledge) and Balbiani and van Ditmarsch (2015) (to tackle quantifiers). The reader interested in details is referred to Ågotnes et al. (2022), where the authors presented a relatively similar completeness proof for a system with distributed knowledge and quantification over public announcements.

{theorem}

The axioms and rules on Tables 1, 2 and 3 are sound and (together) complete for ${\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$.

Structural equivalence.  The modality $\mathop{[{\mathtt{S}{:}\,\ast}!]}{}$ is also invariant under collective bisimilarity.

{theorem}

[$\rightleftarrows_{C}$ implies ${\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$-equivalence] Let $(M,w)$ and $(M^{\prime},w^{\prime})$ be two pointed models. If $(M,w)\rightleftarrows_{C}(M^{\prime},w^{\prime})$ then, for every $\psi\in{\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$,

[TABLE]

?proofname?.

As for Table 2 (see the appendix). ∎

Expressivity.  The modality $\mathop{[{\mathtt{S}{:}\,\ast}!]}$ adds expressive power.

{theorem}

${\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$ is strictly more expressive than $\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$.

This result can be proven as the analogous result for APAL (Balbiani et al., 2008, Proposition 3.13). Assume towards a contradiction that the languages are equally expressive so, given a formula in ${\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$, there is an equivalent formula in $\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$. Since both formulas are finite, there is an atom $p$ that appears in neither. However, $\mathop{[{\mathtt{S}{:}\,\ast}!]}$ in ${\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$ quantifies over any formula, and thus over formulas including $p$. With this, one can build two models that include worlds that satisfy $p$. Then, using induction, we can show that the formula in $\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$ (without $p$) cannot tell the models apart, while the formula in ${\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$ (where quantification ranges also over formulas with $p$) can. This technique is used (with more details) in the proofs in Section 4.3.

4.2. Model checking

The complexity of the model checking problem for ${\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$ is PSPACE-complete: this is in line with the complexity of other logics of quantified information change as, e.g., arbitrary public announcements Balbiani et al. (2008), group announcement logic Ågotnes et al. (2010), coalition announcement logic Alechina et al. (2021) and arbitrary arrow update logic van Ditmarsch et al. (2017). However, this case has an interesting twist. Model checking algorithms for the aforementioned logics compute a bisimulation contraction of the model, and then continue working on the contracted model. This is not possible in our case: a model and its collective bisimulation contraction are not collectively bisimilar Roelofsen (2005): they might differ in some formulas’ truth-value. We still compute bisimulation contractions, but we use them just to inform our algorithm about bisimilar states. The computation continues on the original non-contracted model.

Definition \thetheorem ($\mathtt{S}$-definable restrictions).

Let $(M,w)$ be a pointed model; take $\mathtt{S}\subseteq\mathtt{A}$. A model $(N,w)$ is an $\mathtt{S}$-definable restriction of $(M,w)$ if and only if $(N,w)=({M_{{\mathtt{S}{:}\,\chi}!}},w)$ for some $\chi\in{\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$.

Fact \thetheorem.

Let $(M,w)$ be a finite pointed model. Then there is a finite number of $\mathtt{S}$-definable restrictions of $(M,w)$.

The proof below presents an algorithm $\mathit{MC}(M,w,\varphi)$ that returns true if and only if $(M,w)\Vdash\varphi$, and returns false if and only if $(M,w)\not\Vdash\varphi$. The main challenge is that modalities $\mathop{[{\mathtt{S}{:}\,\ast}!]}$ quantify over an infinite number of formulas. However, for any given finite model $M$, there is only a finite number of possible $\mathtt{S}$-definable model restrictions. Showing that the problem is PSPACE-hard uses the classic reduction from the satisfiability of QBF.

{theorem}

The model checking for ${\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$ is PSPACE-complete.

?proofname?.

Let $(M,w)$ be a pointed model, and $\varphi\in{\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$. In subsection 4.2, Boolean cases and the case for $\mathop{\operatorname{D}_{\mathtt{G}}}$ are as expected, and thus omitted.

\fname@algorithm** 2** An algorithm for model checking for ${\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$

1:procedure MC($M,w,\varphi$)

2:    case $\varphi=\mathop{[{\mathtt{S}{:}\,\chi}!]}\psi$

3:        return $\textsc{MC}({M_{{\mathtt{S}{:}\,\chi}!}},w,\psi)$     

4:    case $\varphi=\mathop{[{\mathtt{S}{:}\,\ast}!]}\psi$

5:        Compute collective $\mathtt{P}$-bisimulation contraction $\|M\|^{C}$

6:        for all $\mathtt{S}$-definable restrictions $(N,w)$ of $(M,w)$ do

7:           if $\textsc{MC}(N,w,\psi)$ returns false then

8:               return false                    

9:        return true     

The basic idea in the construction of $\mathtt{S}$-definable restrictions is to consider a subset of all possible bipartitions of $(M,w)$, taking care that bisimilar states end up in the same partition. This can be done by checking that for each state, if it is in a partition, then all states in the same collective bisimulation equivalence class are also in the same partition. Collective bisimulation equivalence classes can be computed by, e.g., a modification of Kanellakis-Smolka algorithm Kanellakis and Smolka (1990) that takes into account not only relations but also intersections thereof. Having computed collective bisimulation equivalence classes of $(M,w)$, one can construct an $\mathtt{S}$-definable restriction of the model by taking a bipartition such that if $v$ belongs to one partition, then all $u\in[v]$ also belong to the same partition, with $[v]$ being a collective bisimulation equivalence class.

Constructing restrictions takes polynomial time and thus space. The space required for the case of $\mathop{[{\mathtt{S}{:}\,\chi}!]}\psi$ is bounded by $\mathcal{O}(|\varphi|\cdot|M|)$. For the case of $\mathop{[{\mathtt{S}{:}\,\ast}!]}\psi$, collective bisimulation contraction can be computed in polynomial time and space, and each restriction has a size of at most $|M|$. If one traverses a given formula depth-first and reuses memory, the space to store model restrictions is polynomial in $|\varphi|$ (even though the algorithm itself runs in exponential time). Thus, the space required for the case of $\mathop{[{\mathtt{S}{:}\,\ast}!]}\psi$ is bounded by $\mathcal{O}(|\varphi|\cdot|M|)$.

Finally, since computing each subformula of $\varphi$ requires space bounded by $\mathcal{O}(|\varphi|\cdot|M|)$, the space required by the whole algorithm is bounded by $\mathcal{O}(|\varphi|^{2}\cdot|M|)$. The algorithm follows closely the semantics of ${\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$, and correctness can be shown via induction on $\varphi$. For the case of quantifiers note that, in order to switch from bipartitions to particular formulas corresponding to those partitions, one can use characteristic formulas van Ditmarsch et al. (2014). These formulas are built in such a way that they are true only in one state of a model (up to collective bisimularity).

For showing PSPACE-hardness, use the classic reduction from the satisfiability of QBF. W.l.o.g., consider QBFs without free variables in which every variable is quantified only once. Consider a QBF with $n$ variables $\left\{x_{1},\ldots,x_{n}\right\}$. We need a model and a formula in ${\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$ that are both of polynomial size of the QBF. The (reflexive and symmetric) model $M^{n}$ below satisfies this: $w_{0}$ is the evaluation point, and for each variable $x_{i}$ there are two states, $w_{i}^{1}$ and $w_{i}^{0}$, corresponding respectively to evaluating $x_{i}$ to $1$ and to [math]. Assume that each $w_{i}^{1}$ satisfies only $p_{i}$ and each $w_{i}^{0}$ satisfies only $q_{i}$.

w_{0}$$p_{1}$$w_{1}^{1}$$q_{1}$$w_{1}^{0}$$\ldots$$p_{n}$$w_{n}^{1}$$q_{n}$$w_{n}^{0}$$\mathtt{a}$$\mathtt{a}$$\ldots$$\mathtt{a}$$\mathtt{a}

Let $\Psi:=Q_{1}x_{1}\mathellipsis Q_{n}x_{n}\Phi(x_{1},\mathellipsis,x_{n})$ be a quantified Boolean formula (so $Q_{i}\in\{\forall,\exists\}$ and $\Phi(x_{1},\mathellipsis,x_{n})$ is Boolean). The formula $\mathit{chosen}_{k}$ below indicates, intuitively, that the values (either 1 or 0) of the first $k$ variables have been chosen.

[TABLE]

Here is, then, a recursive translation from a QBF $\Psi$ to a formula $\psi$ in ${\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$: $\psi_{0}:=\Phi(\mathop{\widehat{\operatorname{K}}_{\mathtt{a}}}p_{1},\mathellipsis,\mathop{\widehat{\operatorname{K}}_{\mathtt{a}}}p_{n})$,

[TABLE]

$\psi:=\psi_{n}$. We need to show that

$Q_{1}x_{1}\mathellipsis Q_{n}x_{n}\Phi(x_{1},\mathellipsis,x_{n})$ is satisfiable  if and only if $(M^{n},w_{0})\Vdash\psi$.

For this, observe that each state in $M^{n}$ can be characterised by a unique formula. Moreover, relation $\mathtt{b}$ is the identity. Therefore, $\mathop{[{\left\{\mathtt{a},\mathtt{b}\right\}{:}\,\ast}!]}$ and $\mathop{\langle{\left\{\mathtt{a},\mathtt{b}\right\}{:}\,\ast}!\rangle}$ can force any restriction of $\mathtt{a}$-arrows from $w_{0}$ to $w_{i}$’s. In the model, states $w^{1}_{i}$ and $w^{0}_{i}$ correspond the truth-value of $x_{i}$. The guard $\mathit{chosen}_{k}$ guarantees that only the truth-values of the first $k$ variables have been chosen, and that they have been chosen unambiguously (i.e. there is exactly one edge from $w_{0}$ to either $w^{1}_{i}$ and $w^{0}_{i}$). Thus, together with $\mathop{[{\left\{\mathtt{a},\mathtt{b}\right\}{:}\,\ast}!]}$ and $\mathop{\langle{\left\{\mathtt{a},\mathtt{b}\right\}{:}\,\ast}!\rangle}$, the guards $\mathit{chosen}_{k}$ emulate $\forall$ and $\exists$. Then, once the values of all $x_{i}$’s have been set, the evaluation of the QBF corresponds to the $\mathtt{a}$-reachability of the corresponding states in $M^{n}$. ∎

4.3. Arbitrary partial communication vs. arbitrary public announcements

The languages $\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$ and $\mathcal{L}_{\xi!}$ are equally expressive (both ‘reduce’ to ${\mathcal{L}}$). As it is shown below, this changes when quantification (over topics and announced formulas, respectively) is added.

Definition \thetheorem.

The language ${\mathcal{L}^{\ast}_{\xi!}}$ extends $\mathcal{L}_{\xi!}$ with a modality $\mathop{[\ast!]}$ such that

[TABLE]

Define $\mathop{\langle\ast!\rangle}\varphi:=\lnot\mathop{[\ast!]}\lnot\varphi$, as usual.

The theorem below shows that ${\mathcal{L}^{\ast}_{\xi!}}$ and ${\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$ are incomparable w.r.t. expressive power (i.e., ${\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}\not\preccurlyeq{\mathcal{L}^{\ast}_{\xi!}}$ and ${\mathcal{L}^{\ast}_{\xi!}}\not\preccurlyeq{\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$). This result is obtained by adapting techniques and models from Balbiani et al. (2008) and van Ditmarsch et al. (2017) to the case of partial communication.888For space reasons, we do not present the whole argument here.

{theorem}

${\mathcal{L}^{\ast}_{\xi!}}$ and ${\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$ are, expressivity-wise, incomparable.

?proofname?.

For ${\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}\not\preccurlyeq{\mathcal{L}^{\ast}_{\xi!}}$, consider $\mathop{\langle{\left\{\mathtt{a},\mathtt{b}\right\}{:}\,\ast}!\rangle}(\mathop{\operatorname{K}_{\mathtt{b}}}p\land\lnot\mathop{\operatorname{K}_{\mathtt{b}}}\mathop{\operatorname{K}_{\mathtt{b}}}p)$ in ${\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$. For a contradiction, assume there is an equivalent $\alpha\in{\mathcal{L}^{\ast}_{\xi!}}$. Since $\alpha$ is finite, there is an atom $q$ that does not occur in it. The strategy consists in building two $\mathtt{P}\setminus\mathopen{\{}{q}\mathclose{\}}$-bisimilar pointed models, then argue that they can be distinguished by $\mathop{\langle{\left\{\mathtt{a},\mathtt{b}\right\}{:}\,\ast}!\rangle}(\mathop{\operatorname{K}_{\mathtt{a}}}p\land\lnot\mathop{\operatorname{K}_{\mathtt{a}}}\mathop{\operatorname{K}_{\mathtt{a}}}p)$ but not by any $\alpha$. Consider the (reflexive and symmetric) models below.

[TABLE]

Note how $(M,w)\not\Vdash\mathop{\langle{\left\{\mathtt{a},\mathtt{b}\right\}{:}\,\ast}!\rangle}(\mathop{\operatorname{K}_{\mathtt{a}}}p\land\lnot\mathop{\operatorname{K}_{\mathtt{a}}}\mathop{\operatorname{K}_{\mathtt{a}}}p)$: making $\mathop{\operatorname{K}_{\mathtt{a}}}p\land\lnot\mathop{\operatorname{K}_{\mathtt{a}}}\mathop{\operatorname{K}_{\mathtt{a}}}p$ true at $w$ requires deleting the symmetric $\mathtt{a}$-edge between $w$ and $u$ (so $\mathop{\operatorname{K}_{\mathtt{a}}}p$ holds), but this makes $u$ inaccessible for $\mathtt{a}$ from $w$ (thus $\lnot\mathop{\operatorname{K}_{\mathtt{a}}}\mathop{\operatorname{K}_{\mathtt{a}}}p$ fails). Yet, $(M^{\prime},w^{\prime}_{1})\Vdash\mathop{\langle{\left\{\mathtt{a},\mathtt{b}\right\}{:}\,\ast}!\rangle}(\mathop{\operatorname{K}_{\mathtt{a}}}p\land\lnot\mathop{\operatorname{K}_{\mathtt{a}}}\mathop{\operatorname{K}_{\mathtt{a}}}p)$: a ‘conversation’ among $\left\{\mathtt{a},\mathtt{b}\right\}$ about $p\leftrightarrow q$ produces the desired result (see Fact 3).

To show that $(M,w)$ and $(M^{\prime},w^{\prime}_{1})$ cannot be distinguished by a $q$-less formula $\alpha$ in ${\mathcal{L}^{\ast}_{\xi!}}$, use structural induction over $\alpha$ and submodels of $M$ and $M^{\prime}$. Both models are collectively $\mathtt{P}\setminus\mathopen{\{}{q}\mathclose{\}}$-bisimilar (witness: $\mathopen{\{}{(w,w^{\prime}_{1}),(w,w^{\prime}_{2}),(u,u^{\prime})}\mathclose{\}}$), so the case for atoms is immediate. As an induction hypothesis, we state that the current submodels of $M$ and $M^{\prime}$ are collectively $\mathtt{P}\setminus\mathopen{\{}{q}\mathclose{\}}$-bisimilar. Boolean, epistemic, and public announcement cases follow from Table 1. Finally, for $\mathop{[\ast!]}$ observe that for each announcement in one submodel we can always find a corresponding announcement in the other submodel such that the resulting updated models are collectively $\mathtt{P}\setminus\mathopen{\{}{q}\mathclose{\}}$-bisimilar. This is due to the fact that each state in both models is uniquely defined by a Boolean formula containing only atoms $p$ and $q$. Moreover, all possible updates of $\mathtt{P}\setminus\mathopen{\{}{q}\mathclose{\}}$-bisimilar submodels are given by the aforementioned witness: $\mathopen{\{}{(w,w^{\prime}_{1}),(w,w^{\prime}_{2}),(u,u^{\prime})}\mathclose{\}}$. E.g. if a submodel of $M^{\prime}$ contains only states $w_{1}^{\prime}$ and $w_{2}^{\prime}$, then the corresponding submodel of $M$ would contain only state $w$.

To show ${\mathcal{L}^{\ast}_{\xi!}}\not\preccurlyeq{\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$, proceed in a similar fashion: consider $\mathop{\langle\ast!\rangle}(\mathop{\operatorname{K}_{\mathtt{b}}}p\land\lnot\mathop{\operatorname{K}_{\mathtt{b}}}\mathop{\operatorname{K}_{\mathtt{b}}}p)$ in ${\mathcal{L}^{\ast}_{\xi!}}$ and assume there is an equivalent $\beta\in{\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$. Let $q$ be an atom not occurring in $\beta$, and consider the (reflexive and symmetric) models below.

[TABLE]

Note how $(M,w_{1})\not\Vdash\mathop{\langle\ast!\rangle}(\mathop{\operatorname{K}_{\mathtt{b}}}p\land\lnot\mathop{\operatorname{K}_{\mathtt{b}}}\mathop{\operatorname{K}_{\mathtt{b}}}p)$ (an announcement preserves transitivity). Yet, $(M^{\prime},w^{\prime}_{1})\Vdash\mathop{\langle\ast!\rangle}(\mathop{\operatorname{K}_{\mathtt{b}}}p\land\lnot\mathop{\operatorname{K}_{\mathtt{b}}}\mathop{\operatorname{K}_{\mathtt{b}}}p)$: the announcement of $q\rightarrow p$ (equivalence classes highlighted) produces the desired result. To show that $(M,w_{1})$ and $(M^{\prime},w^{\prime}_{1})$ cannot be distinguished by a $q$-less formula in ${\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$, use structural induction. For $\mathop{\langle{\mathtt{S}{:}\,\ast}!\rangle}$, observe that the pointed models are collectively $\mathtt{P}\setminus\mathopen{\{}{q}\mathclose{\}}$-bisimilar (witness: $\mathopen{\{}{(w_{1},w^{\prime}_{1}),(w_{2},w^{\prime}_{2}),(u,u^{\prime}_{1}),(u,u^{\prime}_{2})}\mathclose{\}}$) and that, for each update in one model, there is an update in the other that preserves collective $\mathtt{P}\setminus\mathopen{\{}{q}\mathclose{\}}$-bisimilarity. As in the previous case, each state is uniquely characterised by a Boolean formula containing only atoms $p$ and $q$. This allows us to consider all possible bipartitions of the models, and the witness helps to build a corresponding model. E.g., if there is a relation between $w_{1}^{\prime}$ and $u_{1}^{\prime}$, then we need to preserve the same relation between $w_{1}$ and $u$. ∎

5. Discussion

This paper studies further the partial communication framework of Velázquez-Quesada (2022). As such, it makes sense to argue, albeit briefly, for the use of this setting as well as that of its introduced extension.

A first concern might be that, although communication between agents is a crucial form of interaction, the public announcement logic (PAL) framework has been already used for modelling it (e.g., Ågotnes et al. (2010); van Ditmarsch (2014)). Here we argue that this strategy might not be fully suited. A PAL announcement actually requires two parameters: the announcement’s precondition and the information the agents receive. When this announcement is understood as information coming from an external source, it is clear what these two parameters are, and it is clear they are the same: in order to be ‘announced’, $\xi$ must be true, and after the announcement the agents learn that $\xi$ is the case.999More precisely, they learn $\xi$ was the case immediately before its announcement. But when this setting is used for communication between agents, precondition and information content are not straightforward, and they might differ. When an agent $\mathtt{i}$ announces $\xi$, what is the precondition? It cannot be only $\xi$; is it enough that the agent knows $\xi$ (i.e., $\mathop{\operatorname{K}_{\mathtt{i}}}\xi$), or should she be introspective about it (i.e., $\mathop{\operatorname{K}_{\mathtt{i}}}\mathop{\operatorname{K}_{\mathtt{i}}}\xi$)? Analogously, what is what the other agents learn? They learn not only that $\xi$ is true; do they learn that the agent knows $\xi$ (i.e., $\mathop{\operatorname{K}_{\mathtt{i}}}\xi$), or even that she knows that she knows $\xi$ (i.e., $\mathop{\operatorname{K}_{\mathtt{i}}}\mathop{\operatorname{K}_{\mathtt{i}}}\xi$)?

These questions naturally extend to situations of group communication. In group announcement logic Ågotnes et al. (2010), an announcement from a group $\mathtt{S}$ is represented by the public announcement of $\bigwedge_{\mathtt{i}\in\mathtt{S}}\mathop{\operatorname{K}_{\mathtt{i}}}\xi_{\mathtt{i}}$: each agent $\mathtt{i}\in\mathtt{S}$ announces, in parallel with the others, a formula she knows. However, other readings may be more appropriate: the group might announce something that is common knowledge among its members, or even announce something they all know distributively. These alternative readings are more naturally represented by the actions introduced in Baltag (2010); Ågotnes and Wáng (2017); Baltag and Smets (2020), of which partial communication is a novel variation.

Then, in the partial communication setting, although only some of the agents share, this information is received by every agent in the system. One might be interested in more complex ‘private communication’ scenarios, as those in which only some agents receive the shared information (cf., e.g., Baltag and Smets (2020)). Still, this ‘everybody hears’ setting is useful for modelling classroom or meeting-like scenarios in which everybody ‘hears’ but only some get to ‘talk’, or for situations in which the communication channel is insecure, and thus privacy cannot be assumed. Instead of looking at extensions for modelling private communication, this paper has rather focused on the strategic aspects that arise in competitive situations. In such cases, one wonders whether there is a form of partial communication that can achieve a given goal (e.g., van Ditmarsch (2003)). The arbitrary partial communication of section 4 can help to answer such questions.

6. Summary and further work

The focus of this paper is the action of partial communication. Through it, a group of agents $\mathtt{S}$ share, with every agent in the model, all the information they have about the truth-value of a formula $\chi$. Semantically, this is represented by an operation through which the uncertainty of each agent is reduced by removing the uncertainty about $\chi$ some agent in $\mathtt{S}$ has already ruled out. After recalling the basics of this framework, we proved that its language $\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$ is invariant under collective bisimulation, showing also that the complexity of its model checking problem remains in P, as standard epistemic logic Halpern and Moses (1992). It has been also shown that, while the expressivity of $\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$ is exactly that of the language for public announcements (both reducible to ${\mathcal{L}}$), their ‘update expressive power’ are incomparable. The focus has then shifted to a modal operator that quantifies over the topic of the communication: a setting for arbitrary partial communication. We have provided the operator’s semantic interpretation as well as an axiom system and invariance results for the resulting language ${\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$. We have also proved that the model checking problem for the new language ${\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$ is PSPACE-complete, similar to DELs with action models Aucher and Schwarzentruber (2013); de Haan and van de Pol (2021) and logics with quantification over information change Balbiani et al. (2008); Ågotnes et al. (2010); van Ditmarsch et al. (2017); Alechina et al. (2021). Finally, we showed that ${\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$ is, expressivity-wise, incomparable to the language of arbitrary public announcements.

The framework for partial communication provides, arguably, a natural representation of communication between agents. Indeed, it works directly with the information (i.e., uncertainty) the agents have, instead of looking for formulas that are known by the agents, and then using them as announcements (as done, e.g., when dealing with group announcements Ågotnes et al. (2010)). Additionally, the results show that this action is a truly novel epistemic action, different from others as public announcements.

There is still further work to do. In the current version of the setting, some questions still need an answer. An important one is that collective bisimulation is not ‘well-behaved’: a model and its collective bisimulation contraction are not collectively bisimilar Roelofsen (2005). One then wonders whether there is a more adequate notion of structural equivalence for the basic language ${\mathcal{L}}$ and its extensions. Then, with the partial communication setting already compared with that for public announcements (in both their basic and their ‘arbitrary‘ versions), one would like to compare it also with the setting for group announcements Ågotnes et al. (2010), and even with those for more general edge-removing operations (e.g., the arrow update setting Kooi and Renne (2011)). Finally, one can expand the presented framework. For example, one can extend the languages used here by adding a common knowledge operator, a step that requires technical further tools Ågotnes and Wáng (2017); Baltag and Smets (2020); Galimullin and Ågotnes (2021). Equally interesting is a generalisation in which the topic of conversation is rather a set of formulas, together with its connection with other forms of communication (e.g., one in which some agents share all they know with everybody).

?refname?

• (1)
• Ågotnes et al. (2022)

Thomas Ågotnes, Natasha Alechina, and Rustam Galimullin. 2022.

Logics with Group Announcements and Distributed Knowledge: Completeness and Expressive Power.

Journal of Logic, Language and Information 31, 2 (2022), 141–166.

https://doi.org/10.1007/s10849-022-09355-0

• Ågotnes et al. (2010)

Thomas Ågotnes, Philippe Balbiani, Hans van Ditmarsch, and Pablo Seban. 2010.

Group announcement logic.

Journal of Applied Logic 8, 1 (2010), 62–81.

https://doi.org/10.1016/j.jal.2008.12.002

• Ågotnes and Wáng (2017)

Thomas Ågotnes and Yì N. Wáng. 2017.

Resolving distributed knowledge.

Artificial Intelligence 252 (2017), 1–21.

https://doi.org/10.1016/j.artint.2017.07.002

• Alechina et al. (2021)

Natasha Alechina, Hans van Ditmarsch, Rustam Galimullin, and Tuo Wang. 2021.

Verification and Strategy Synthesis for Coalition Announcement Logic.

Journal of Logic, Language and Information 30, 4 (2021), 671–700.

https://doi.org/10.1007/s10849-021-09339-6

• Aucher and Schwarzentruber (2013)

Guillaume Aucher and François Schwarzentruber. 2013.

On the Complexity of Dynamic Epistemic Logic. In Proceedings of the 14th TARK, Burkhard C. Schipper (Ed.).

• Balbiani et al. (2008)

Philippe Balbiani, Alexandru Baltag, Hans van Ditmarsch, Andreas Herzig, Tomohiro Hoshi, and Tiago de Lima. 2008.

’Knowable’ as ’known after an announcement’.

The Review of Symbolic Logic 1, 3 (2008), 305–334.

https://doi.org/10.1017/S1755020308080210

• Balbiani and van Ditmarsch (2015)

Philippe Balbiani and Hans van Ditmarsch. 2015.

A simple proof of the completeness of APAL.

Studies in Logic 8, 2 (2015), 65–78.

• Baltag (2010)

Alexandru Baltag. 2010.

What is DEL good for? (2010).

http://ai.stanford.edu/~epacuit/lograt/esslli2010-slides/copenhagenesslli.pdf

Workshop on Logic, Rationality and Intelligent Interaction.

• Baltag et al. (1998)

Alexandru Baltag, Lawrence S. Moss, and Sławomir Solecki. 1998.

The Logic of Public Announcements and Common Knowledge and Private Suspicions. In Proceedings of the 7th TARK, Itzhak Gilboa (Ed.). Morgan Kaufmann, 43–56.

• Baltag and Smets (2020)

Alexandru Baltag and Sonja Smets. 2020.

Learning What Others Know. In LPAR 2020 (EPiC Series in Computing, Vol. 73), Elvira Albert and Laura Kovács (Eds.). EasyChair, 90–119.

https://doi.org/10.29007/plm4

• Baltag and Smets (2021)

Alexandru Baltag and Sonja Smets. 2021.

Learning What Others Know.

CoRR abs/2109.07255 (2021).

arXiv:2109.07255

https://arxiv.org/abs/2109.07255

• de Bruin (2010)

Boudewijn de Bruin. 2010.

Explaining Games: The Epistemic Programme in Game Theory.

Springer, Dordrecht.

https://doi.org/10.1007/978-1-4020-9906-9

• de Haan and van de Pol (2021)

Ronald de Haan and Iris van de Pol. 2021.

On the Computational Complexity of Model Checking for Dynamic Epistemic Logic with S5 Models.

FLAP 8, 3 (2021), 621–658.

• Fagin et al. (1995)

Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi. 1995.

Reasoning about knowledge.

The MIT Press, Cambridge, Mass.

• Galimullin and Ågotnes (2021)

Rustam Galimullin and Thomas Ågotnes. 2021.

Quantified Announcements and Common Knowledge. In Proceegins of the 20th AAMAS, Frank Dignum, Alessio Lomuscio, Ulle Endriss, and Ann Nowé (Eds.). ACM, 528–536.

https://dl.acm.org/doi/10.5555/3463952.3464018

• Gerbrandy and Groeneveld (1997)

Jelle Gerbrandy and Willem Groeneveld. 1997.

Reasoning about information change.

Journal of Logic, Language, and Information 6, 2 (1997), 147–196.

https://doi.org/10.1023/A:1008222603071

• Goldblatt (1982)

Robert Goldblatt. 1982.

Axiomatising the Logic of Computer Programming. LNCS, Vol. 130.

Springer.

https://doi.org/10.1007/BFb0022481

• Halpern and Moses (1990)

Joseph Y. Halpern and Yoram Moses. 1990.

Knowledge and Common Knowledge in a Distributed Environment.

Journal of the ACM 37, 3 (1990), 549–587.

https://doi.org/10.1145/79147.79161

• Halpern and Moses (1992)

Joseph Y. Halpern and Yoram Moses. 1992.

A Guide to Completeness and Complexity for Modal Logics of Knowledge and Belief.

Artificial Intelligence 54, 2 (1992), 319–379.

https://doi.org/10.1016/0004-3702(92)90049-4

• Hendricks (2006)

Vincent F. Hendricks (Ed.). 2006.

8 Bridges between Formal and Mainstream Epistemology.

Philosophical Studies, 128(1).

• Hintikka (1962)

Jaakko Hintikka. 1962.

Knowledge and Belief.

Cornell University Press, Ithaca, N.Y.

• Kanellakis and Smolka (1990)

Paris C. Kanellakis and Scott A. Smolka. 1990.

CCS Expressions, Finite State Processes, and Three Problems of Equivalence.

Information and Computation 86, 1 (1990), 43–68.

https://doi.org/10.1016/0890-5401(90)90025-D

• Kooi and Renne (2011)

Barteld Kooi and Bryan Renne. 2011.

Arrow Update Logic.

The Review of Symbolic Logic 4, 4 (2011), 536–559.

https://doi.org/10.1017/S1755020311000189

• Kuijer (2015)

Louwe B. Kuijer. 2015.

An Arrow-based Dynamic Logic of Norms. In Proceedings of the 3rd SR, Julian Gutierrez, Fabio Mogavero, Aniello Murano, and Michael Wooldridge (Eds.). 1–11.

• Lutz (2006)

Carsten Lutz. 2006.

Complexity and succinctness of public announcement logic. In Proceedings of the 5th AAMAS, Hideyuki Nakashima, Michael P. Wellman, Gerhard Weiss, and Peter Stone (Eds.). ACM, 137–143.

https://doi.org/10.1145/1160633.1160657

• Meyer and van der Hoek (1995)

John-Jules Ch. Meyer and Wiebe van der Hoek. 1995.

Epistemic Logic for AI and Computer Science.

CUP.

https://doi.org/10.1017/CBO9780511569852

• Plaza (1989)

Jan A. Plaza. 1989.

Logics of public communications. In Proceedings of the 4th International Symposium on Methodologies for Intelligent Systems, M. L. Emrich, M. S. Pfeifer, M. Hadzikadic, and Z. W. Ras (Eds.). 201–216.

• Roelofsen (2005)

Floris Roelofsen. 2005.

Bisimulation and Distributed Knowledge Revisited. (2005).

Available at https://projects.illc.uva.nl/lgc/papers/d-know.pdf.

• Roelofsen (2007)

Floris Roelofsen. 2007.

Distributed knowledge.

Journal of Applied Non-Classical Logics 17, 2 (2007), 255–273.

https://doi.org/10.3166/jancl.17.255-273

• van Benthem (2011)

Johan van Benthem. 2011.

Logical Dynamics of Information and Interaction.

CUP.

• van Benthem and Liu (2007)

Johan van Benthem and Fenrong Liu. 2007.

Dynamic logic of preference upgrade.

Journal of Applied Non-Classical Logics 17, 2 (2007), 157–182.

https://doi.org/10.3166/jancl.17.157-182

• van Ditmarsch (2003)

Hans van Ditmarsch. 2003.

The Russian Cards Problem.

Studia Logica 75, 1 (2003), 31–62.

https://doi.org/10.1023/A:1026168632319

• van Ditmarsch (2014)

Hans van Ditmarsch. 2014.

Dynamics of lying.

Synthese 191, 5 (2014), 745–777.

https://doi.org/10.1007/s11229-013-0275-3

• van Ditmarsch (2020)

Hans van Ditmarsch. 2020.

To Be Announced.

CoRR abs/2004.05802 (2020).

arXiv:2004.05802

https://arxiv.org/abs/2004.05802

• van Ditmarsch et al. (2014)

Hans van Ditmarsch, David Fernández-Duque, and Wiebe van der Hoek. 2014.

On the definability of simulation and bisimulation in epistemic logic.

Journal of Logic and Computation 24, 6 (2014), 1209–1227.

https://doi.org/10.1093/logcom/exs058

• van Ditmarsch et al. (2008)

Hans van Ditmarsch, Wiebe van der Hoek, and Barteld Kooi. 2008.

Dynamic Epistemic Logic.

Springer, Dordrecht, The Netherlands.

https://doi.org/10.1007/978-1-4020-5839-4

• van Ditmarsch et al. (2017)

Hans van Ditmarsch, Wiebe van der Hoek, Barteld Kooi, and Louwe B. Kuijer. 2017.

Arbitrary arrow update logic.

Artificial Intelligence 242 (2017), 80–106.

https://doi.org/10.1016/j.artint.2016.10.003

• Velázquez-Quesada (2022)

Fernando R. Velázquez-Quesada. 2022.

Communication between agents in dynamic epistemic logic.

CoRR abs/2210.04656 (2022).

https://doi.org/10.48550/arXiv.2210.04656 arXiv:2210.04656

• Wang and Cao (2013)

Yanjing Wang and Qinxiang Cao. 2013.

On axiomatizations of public announcement logic.

Synthese 190, Supplement-1 (2013), 103–134.

https://doi.org/10.1007/s11229-012-0233-5

• Wáng and Ågotnes (2013)

Yì N. Wáng and Thomas Ågotnes. 2013.

Public announcement logic with distributed knowledge: expressivity, completeness and complexity.

Synthese 190, Supplement-1 (2013), 135–162.

https://doi.org/10.1007/s11229-012-0243-3

?appendixname? A Appendix

Proof of Table 2

Since $\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$ is the union of $\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}^{i}$ for all $i\in\mathbb{N}$, the proof will proceed by induction on $i$. In fact, the manuscript will prove a stronger statement: for every $\psi\in\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}$ and every $M=\left\langle W,R,V\right\rangle$ and $M^{\prime}=\left\langle W^{\prime},R^{\prime},V^{\prime}\right\rangle$, if $(M,w)\rightleftarrows_{C}(M^{\prime},w^{\prime})$ then

(1) $(M,w)\Vdash\psi$if and only if $(M^{\prime},w^{\prime})\Vdash\psi$, and (2) $({M_{{\mathtt{S}{:}\,\psi}!}},w)\rightleftarrows_{C}({M^{\prime}_{{\mathtt{S}{:}\,\psi}!}},w^{\prime})$ .

Base case.  Take $\psi\in\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}^{0}={\mathcal{L}}$. In this case, (1) is nothing but Theorem 2.7. For (2), suppose $(M,w)\rightleftarrows_{C}(M^{\prime},w^{\prime})$ and let $Z$ be the witness; it will be shown that $Z$ is also a collective $\mathtt{P}$-bisimulation between ${M_{{\mathtt{S}{:}\,\psi}!}}=\langle W,R^{{\mathtt{S}{:}\,\psi}!},V\rangle$ and ${M^{\prime}_{{\mathtt{S}{:}\,\psi}!}}=\langle W^{\prime},R^{\prime{\mathtt{S}{:}\,\psi}!},V^{\prime}\rangle$. Take any $(u,u^{\prime})\in Z$.

• •

Atoms. The operation does not change atomic valuations. Thus, since $Z$ satisfies atoms for $M$ and $M^{\prime}$, it also satisfies it for ${M_{{\mathtt{S}{:}\,\psi}!}}$ and ${M^{\prime}_{{\mathtt{S}{:}\,\psi}!}}$.

• •

Forth. Take any $\mathtt{G}\subseteq\mathtt{A}$ and any $v\in W$ such that ${R^{{\mathtt{S}{:}\,\psi}!}}_{\mathtt{G}}uv$. Since ${R^{{\mathtt{S}{:}\,\psi}!}}_{\mathtt{G}}={R}_{\mathtt{G}\cup\mathtt{S}}\cup({R}_{\mathtt{G}}\cap{\sim^{M}_{\psi}})$ (Footnote 5), then ${R}_{\mathtt{G}\cup\mathtt{S}}uv$ or $({R}_{\mathtt{G}}\cap{\sim^{M}_{\psi}})uv$.

(i) If ${R}_{\mathtt{G}\cup\mathtt{S}}uv$ then, since $Z$ satisfies forth for $M$ and $M^{\prime}$, there is $v^{\prime}\in W^{\prime}$ such that ${R^{\prime}}_{\mathtt{G}\cup\mathtt{S}}u^{\prime}v^{\prime}$ and $(v,v^{\prime})\in Z$. Since ${R^{\prime{\mathtt{S}{:}\,\psi}!}}_{\mathtt{G}}={R^{\prime}}_{\mathtt{G}\cup\mathtt{S}}\cup({R^{\prime}}_{\mathtt{G}}\cap{\sim^{M^{\prime}}_{\psi}})$, the former implies ${R^{\prime{\mathtt{S}{:}\,\psi}!}}_{\mathtt{G}}u^{\prime}v^{\prime}$. Thus, there is $v^{\prime}\in W^{\prime}$ such that ${R^{\prime{\mathtt{S}{:}\,\psi}!}}_{\mathtt{G}}u^{\prime}v^{\prime}$ and $(v,v^{\prime})\in Z$, as required. (ii) If $({R}_{\mathtt{G}}\cap{\sim^{M}_{\psi}})uv$, then both ${R}_{\mathtt{G}}uv$ and $u\sim^{M}_{\psi}v$. From the first and the fact that $Z$ satisfies forth for $M$ and $M^{\prime}$, there is $v^{\prime}\in W^{\prime}$ such that ${R^{\prime}}_{\mathtt{G}}u^{\prime}v^{\prime}$ and $(v,v^{\prime})\in Z$. Now, $u\sim^{M}_{\psi}v$ indicates that $u$ and $v$ agree on $\psi$’s truth-value. But $\psi\in{\mathcal{L}}$. Thus, (1) from this base case indicates that $u$ and $u^{\prime}$ also agree on $\psi$ (from $(u,u^{\prime})\in Z$), and so do $v$ and $v^{\prime}$ (from $(v,v^{\prime})\in Z$). Hence, $u^{\prime}$ and $v^{\prime}$ agree on $\psi$’s truth-value, that is, $u^{\prime}\sim^{M^{\prime}}_{\psi}v^{\prime}$. Therefore, $({R^{\prime}}_{\mathtt{G}}\cap{\sim^{M^{\prime}}_{\psi}})uv$, so ${R^{\prime{\mathtt{S}{:}\,\psi}!}}_{\mathtt{G}}u^{\prime}v^{\prime}$. This means there is $v^{\prime}\in W^{\prime}$ such that ${R^{\prime{\mathtt{S}{:}\,\psi}!}}_{\mathtt{G}}u^{\prime}v^{\prime}$ and $(v,v^{\prime})\in Z$, as required.

• •

Back. As in forth, using the fact that $Z$ satisfies back for $M$ and $M^{\prime}$.

Thus, ${M_{{\mathtt{S}{:}\,\psi}!}}\rightleftarrows_{C}{M^{\prime}_{{\mathtt{S}{:}\,\psi}!}}$. Finally, $(w,w^{\prime})\in Z$, so $({M_{{\mathtt{S}{:}\,\psi}!}},w)$ $\rightleftarrows_{C}$ $({M^{\prime}_{{\mathtt{S}{:}\,\psi}!}},w^{\prime})$.

Inductive case.  Take $\psi\in\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}^{n+1}$ and suppose $(M,w)\rightleftarrows_{C}(M^{\prime},w^{\prime})$. For (1), proceed by structural induction on $\psi$. The cases for atoms, Boolean operators and $\mathop{\operatorname{D}_{\mathtt{G}}}$ are as in Theorem 2.7. The remaining case is for formulas of the form $\mathop{[{\mathtt{S}{:}\,\chi}!]}\varphi$ with $\chi\in\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}^{n}$ and $\varphi\in\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}^{n+1}$. Here, the structural IH states that collectively $\mathtt{P}$-bisimilar pointed models agree on the truth value of the subformula $\varphi$. Note how, since $\chi\in\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}^{n}$ and $(M,w)\rightleftarrows_{C}(M^{\prime},w^{\prime})$, (2) of the (global) IH implies $({M_{{\mathtt{S}{:}\,\chi}!}},w)\rightleftarrows_{C}({M^{\prime}_{{\mathtt{S}{:}\,\chi}!}},w^{\prime})$. Now, from left to right, suppose $(M,w)\Vdash\mathop{[{\mathtt{S}{:}\,\chi}!]}\varphi$. By semantic interpretation, $({M_{{\mathtt{S}{:}\,\chi}!}},w)\Vdash\varphi$; thus, from the structural IH, $({M^{\prime}_{{\mathtt{S}{:}\,\chi}!}},w^{\prime})\Vdash\varphi$, i.e., $(M^{\prime},w^{\prime})\Vdash\mathop{[{\mathtt{S}{:}\,\chi}!]}\varphi$. The right-to-left direction is analogous.

It is only left to prove (2) for $\psi\in\mathcal{L}_{{\mathtt{S}{:}\,\!\chi}!}^{n+1}$. This can be done as in the (global) base case, using (1) from this inductive case instead.

Proposition A.1

Let $M=\left\langle W,R,V\right\rangle$ be a model; let $\xi$ be a formula. Recall (Plaza, 1989) that the world-removing public announcement of $\xi$ on $M$ yields the model M^{\prime}_{\xi!}=\langle\left\llbracket\xi\right\rrbracket^{M},\mathopen{\{}{{R^{\prime}}_{\mathtt{i}}\mid\mathtt{i}\in\mathtt{A}}\mathclose{\}},V^{\prime}\rangle with

[TABLE]

Now, take any $w\in\mathfrak{D}(M^{\prime}_{\xi!})$. Then,

[TABLE]

Proof sketch.

Intuitively, the difference between the world-removing and edge-deleting approaches makes no difference for a collective bisimulation: in both cases, the $\lnot\xi$-partition becomes inaccessible from the $\xi$-partition, where the world $w$ lies. Formally, it is enough to prove that the relation

[TABLE]

is a collective $\mathtt{P}$-bisimulation (between $M_{\xi!}$ and $M^{\prime}_{\xi!}$) containing the pair $(w,w)$. ∎

Theorem A.1

Let $(M,w)$ and $(M^{\prime},w^{\prime})$ be two pointed models. If $(M,w)\rightleftarrows_{C}(M^{\prime},w^{\prime})$ then, for every $\psi\in\mathcal{L}_{\xi!}$,

[TABLE]

?proofname?.

Analogous to the proof of Table 2. ∎

Proof of Table 3

Since ${\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$ is the union of ${\mathcal{L}^{\ast,i}_{{\mathtt{S}{:}\,\!\chi}!}}$ for all $i\in\mathbb{N}$, proceed again by induction on $i$ (as in the proof of Theorem 2.11). Again, one proves a stronger statement: for every $\psi\in{\mathcal{L}^{\ast}_{{\mathtt{S}{:}\,\!\chi}!}}$ and every $M=\left\langle W,R,V\right\rangle$ and $M^{\prime}=\left\langle W^{\prime},R^{\prime},V^{\prime}\right\rangle$, if $(M,w)\rightleftarrows_{C}(M^{\prime},w^{\prime})$ then

(1) $(M,w)\Vdash\psi$if and only if $(M^{\prime},w^{\prime})\Vdash\psi$, and (2) $({M_{{\mathtt{S}{:}\,\psi}!}},w)\rightleftarrows_{C}({M^{\prime}_{{\mathtt{S}{:}\,\psi}!}},w^{\prime})$ .

Base case.  This base case is for formulas in ${\mathcal{L}^{\ast,0}_{{\mathtt{S}{:}\,\!\chi}!}}={\mathcal{L}}^{\ast}$, defined as ${\mathcal{L}}$ plus the modality $\mathop{[{\mathtt{S}{:}\,\ast}!]}$. For (1), proceed by structural induction, with the cases for formulas in ${\mathcal{L}}$ (atoms, Boolean operators and $\mathop{\operatorname{D}_{\mathtt{G}}}$) as in Theorem 2.7. For the remaining case, suppose $(M,w)\rightleftarrows_{C}(M^{\prime},w^{\prime})$. From left to right, if $(M,w)\Vdash\mathop{[{\mathtt{S}{:}\,\ast}!]}\varphi$ then, by semantic interpretation, $({M_{{\mathtt{S}{:}\,\chi}!}},w)\Vdash\varphi$ holds for every $\chi\in{\mathcal{L}}$. But from $(M,w)\rightleftarrows_{C}(M^{\prime},w^{\prime})$ and the fact each $\chi$ is in ${\mathcal{L}}$, it follows that $({M_{{\mathtt{S}{:}\,\chi}!}},w)\rightleftarrows_{C}({M^{\prime}_{{\mathtt{S}{:}\,\chi}!}},w^{\prime})$ for every $\chi\in{\mathcal{L}}$ ((2) in the base case of the proof of Theorem 2.11). Then, by IH, $({M^{\prime}_{{\mathtt{S}{:}\,\chi}!}},w^{\prime})\Vdash\varphi$ for every $\chi\in{\mathcal{L}}$. Hence, $(M^{\prime},w^{\prime})\Vdash\mathop{[{\mathtt{S}{:}\,\ast}!]}\varphi$. The right-to-left direction is analogous.

For (2), proceed as in the same case in the proof of Theorem 2.11 , using now the just proved (1) for formulas in ${\mathcal{L}}^{\ast}$.

Inductive case.  As in the same case in the proof of Table 2.