# Common Knowledge of Abstract Groups

Merlin Humml, Lutz Schröder

###### Abstract

Epistemic logics typically talk about knowledge of individual agents or groups
of explicitly listed agents. Often, however, one wishes to express knowledge
of groups of agents specified by a given property, as in ‘it is common
knowledge among economists’. We introduce such a logic of common knowledge,
which we term _ abstract-group epistemic logic (AGEL)_. That is, AGEL features
a common knowledge operator for groups of agents given by concepts in a
separate agent logic that we keep generic, with one possible agent logic being
$\mathcal{ALC}$. We show that AGEL is ExpTime-complete, with the lower bound
established by reduction from standard group epistemic logic, and the upper
bound by a satisfiability-preserving embedding into the full $\mu$-calculus.
Further main results include a finite model property (not enjoyed by the full
$\mu$-calculus) and a complete axiomatization.

## Introduction

Epistemic (modal) logic is concerned with the individual and collective
knowledge of agents. One of the most important modalities for collective
knowledge is _common knowledge_ : A fact $\phi$ is common knowledge in a given
group of agents if everyone in the group knows $\phi$, and everyone knows that
everyone knows $\phi$, etc. In the present work, our focus of attention is on
the involved notion of group of agents. The most basic variant of the common
knowledge operator, typically written $C$, refers to _all_ agents in a
predetermined finite set $Ag$ that forms a parameter of the logic as a whole
(Fagin et al. 1995). In a more fine-grained variant, $C$ can be annotated with
an explicitly given subset of the set of agents: For $A\subseteq Ag$,
$C_{A}\phi$ says that $\phi$ is common knowledge among the agents in $A$. For
instance, if $\mathsf{Alice}$ and $\mathsf{Bob}$ are legitimate participants
in a communication protocol and $\phi$ is a fact concerning a shared key, then
$\phi$ would ideally be common knowledge of $\mathsf{Alice}$ and
$\mathsf{Bob}$ but not of a malicious third party $\mathsf{Charlie}$ – i.e.
$C_{\\{\mathsf{Alice},\mathsf{Bob}\\}}\phi$ would hold but
$C_{\\{\mathsf{Alice},\mathsf{Bob},\mathsf{Charlie}\\}}\phi$ would not.

Listing agents in a group explicitly is appropriate in well-controlled
settings such as the above, where the participants in the epistemic situation
are fixed and previously known. In other application contexts, however, this
may not always be the case, in particular in statements found in real-world
argumentation. Consider, for example, the sentence ‘Doctors agree that smoking
is bad for your health.’ We take this sentence (maybe debatably) as making a
statement about common knowledge of all doctors. Encoding this claim as a
formula of the form $C_{A}\phi$ where $A$ is a finite set explicitly
enumerating all doctors is clearly neither feasible nor even semantically
desirable, as the statement is presumably meant to hold without regard to
exactly how many, and which, doctors are practising in the world at the
moment. Rather, one would want $A$ to be given by the defining property of
_being a doctor_.

In the present paper, we introduce an epistemic logic that allows precisely
this: _AGEL_ features a common knowledge operator for groups of agents
described by concepts in a dedicated _agent logic_. We keep the technical
development generic in the choice of agent logic, subject to some technical
requirements on the agent logic that are satisfied, for instance, by the
description logic $\mathcal{ALC}$; so we can describe groups of agents such as
‘doctors and pharmacists’ or ‘parents of teenagers’. We note that we treat the
agent logic as rigid, i.e. there is no uncertainty about membership in the
groups it describes. In other words, group descriptions are _de re_ rather
than _de dicto_. We further illustrate the logic on a variant of the muddy
children puzzle where the number of participants is unspecified and
potentially large. Our main results on AGEL are ExpTime-completeness of the
satisfiability problem; a bounded (specifically, doubly exponential) model
property; and a complete axiomatization. Technically, we establish the lower
complexity bound by a satisfiability-preserving translation of standard group
epistemic logic (Fagin et al. 1995) into AGEL, and the upper bound by a
satisfiability-preserving translation of AGEL into the full $\mu$-calculus
(i.e. $\mathcal{ALC}$ with inverse roles and fixpoint operators (Vardi 1998)).
Use of the full $\mu$-calculus avoids the exponential blow-up that would be
incurred by a more naive reverse translation of AGEL into group epistemic
logic. However, the full $\mu$-calculus does not have the finite model
property (Vardi 1998; Streett 1982). Instead, we show the bounded model
property and completeness by means of a filtered model construction that uses
ideas from the finite model construction for propositional dynamic logic
(Fischer and Ladner 1979; Blackburn, de Rijke, and Venema 2001), in particular
transitive closure of (small) canonical pseudo-models.

#### Related Work

There is a line of research on indexing knowledge modalities with _names_ that
designate groups of agents (Grove and Halpern 1993) (Fagin et al. 1995,
Chapter 6). We refer to such groups as _named groups_ ; they are similar to
the atoms of our agent logic but are _non-rigid_ , i.e. their interpretation
depends on the current world, in an approach that is focused on the analysis
of knowledge about the identity of agents. Although common knowledge of such
name-defined groups has been mentioned early on (Grove and Halpern 1993),
results have largely focused on operators of the type ‘every agent / some
agent with name $n$ knows’ (recall that generally, ‘everyone knows $\phi$’
differs from $\phi$ being common knowledge in that it need not imply that
everyone knows that everyone knows $\phi$, etc.). Recently, Bílková,
Christoff, and Roy (2021) have shown completeness and the finite model
property (but no complexity bound) for common knowledge of name-defined
groups. (A different form of common knowledge for non-rigid groups has been
considered earlier, without considering axiomatization (Moses and Tuttle
1988).)

Extending the descriptive means for groups of agents has been considered
already by Grove and Halpern (1993), who give an axiomatization (but no
complexity bound) of a logic that features ‘everyone knows’ and ‘someone
knows’ operators for propositional combinations of names. Additional
expressive means are provided by subsequent first-order extensions of the
logic that allow quantifying over agent names (Grove 1995; Naumov and Tao
2019) in the style of term modal logic (Fitting, Thalmann, and Voronkov 2001).
Quantifying over agents provides a straightforward way of encoding, e.g., the
‘everybody knows operator’; for instance, ‘every doctor knows $\phi$’ would be
expressed as $\forall x.\,\mathsf{doctor}(x)\rightarrow K_{x}\phi$ if $K_{x}$
denotes the usual single-agent knowledge modality ‘$x$ knows’. Common
knowledge, on the other hand, involves transitive closure and as such is not
first-order expressible, hence not easily accommodated in such frameworks.
Also, decidability results in a first-order setting will, of course, require
additional restrictions (e.g. it has recently been shown that the two-variable
fragment of term-modal logic is decidable, with complexity between NExpTime
and 2ExpSpace (Padmanabha and Ramanujam 2019)).

The above logics and ours employ ternary transition relations relating agents
to pairs of worlds. Beyond epistemic logic, ternary relations appear, e.g., in
the logic of Pierce algebras (de Rijke 1993), in arrow logic (Venema 1996),
and in Routley-Meyer-style semantics of _relevance logic_ (Mares 2020). While
such modalities are formally similar to _everyone-knows_ modalities for
abstract groups, the frame conditions imposed on models and, consequently, the
attached meta-theory are quite different from ours.

## Abstract-Group Epistemic Logic

We proceed to introduce the syntax and semantics of _ abstract-group epistemic
logic (AGEL)_.

##### Syntax

We parametrize the logic over the choice of an _agent logic_
${\mathcal{L}_{\mathsf{Ag}}}$ that serves to specify groups of agents. We will
discuss assumptions on the semantics of ${\mathcal{L}_{\mathsf{Ag}}}$ later in
this section. Syntactically, we require only that
${\mathcal{L}_{\mathsf{Ag}}}$ has a formula syntax where formulae are
expressions in some grammar, in particular giving rise to a standard notion of
_subformula_ , and includes propositional atoms from a set
$\mathsf{At}_{\mathsf{Ag}}$, referred to as _agent atoms_ , as well as the
full set of Boolean connectives. Properties of ${\mathcal{L}_{\mathsf{Ag}}}$
needed in our main results will be named explicitly in the respective
theorems. One choice for ${\mathcal{L}_{\mathsf{Ag}}}$ that satisfies all
requisite properties is the standard description logic $\mathcal{ALC}$ (Baader
et al. 2003).

We further assume a set $\mathsf{At}_{\mathsf{W}}$ of _world atoms_. The set
of _(world) formulae_ $\phi,\chi,\dots$ of AGEL is then defined by the grammar

$\phi,\chi:=\bot\mid p\mid\neg\phi\mid\phi\land\chi\mid
C_{\psi}\phi\qquad(p\in\mathsf{At}_{\mathsf{W}},\psi\in{\mathcal{L}_{\mathsf{Ag}}}).$

That is, we include propositional atoms and Boolean connectives; further
Boolean connectives $\lor$, $\rightarrow$, $\leftrightarrow$ are defined as
usual. The key feature is then the common knowledge operator $C_{\psi}$ for
groups of agents defined by an agent formula $\psi$; a formula $C_{\psi}\phi$
is read ‘$\phi$ is common knowledge among agents satisfying $\psi$’, using the
term _common knowledge_ in the sense recalled in the introduction.

######  Example 1.

We may encode the statement ‘parents of teenagers know that education is
pointless’ as the AGEL formula
$C_{\exists\mathsf{hasChild}.\,\mathsf{Teenager}}\,\mathsf{ep}$, using
$\mathcal{ALC}$ as the agent logic and understanding the world atom
$\mathsf{ep}$ as ‘education is pointless’. The even more frustrating fact that
parents know that their offspring know this as well would be captured by the
formula
$C_{\exists\mathsf{hasChild}.\,\mathsf{Teenager}}\,C_{\mathsf{Teenager}}\,\mathsf{ep}$.

##### Semantics

We assume that the agent logic comes with a notion of _agent model_ , and that
every agent model $\mathcal{A}$ is equipped with an underlying set $Ag$ of
_agents_ and a satisfaction relation $\models_{\mathcal{A}}\>\subseteq
Ag\times{\mathcal{L}_{\mathsf{Ag}}}$; we write $\mathcal{A},a\models\psi$ for
$(a,\psi)\in\;\models_{\mathcal{A}}$, and
$\llbracket\phi\rrbracket_{\mathcal{A}}=\\{a\in
Ag\mid\mathcal{A},a\models\psi\\}$. We require that
_${\mathcal{L}_{\mathsf{Ag}}}$ conservatively extends classical propositional
logic_. By this we mean more specifically that ${\mathcal{L}_{\mathsf{Ag}}}$
does not impose restrictions on valuations of agent atoms, i.e. given a set
$Ag$ and a valuation
$V_{\mathsf{Ag}}\colon\mathsf{At}_{\mathsf{Ag}}\to\mathcal{P}(Ag)$, there
always exists an agent model $\mathcal{A}$ with underlying set $Ag$ such that
$\mathcal{A},a\models q$ iff $a\in V_{\mathsf{Ag}}(q)$, for $a\in Ag$ and
$q\in\mathsf{At}_{\mathsf{Ag}}$.

Then, an _( AGEL) model_ $\mathcal{M}=(X,\mathcal{A},V_{\mathsf{W}},\sim)$
consists of a set $X$ of _worlds_ , an agent model $\mathcal{A}$, a _world
valuation_ $V_{\mathsf{W}}\colon\mathsf{At}_{\mathsf{W}}\to\mathcal{P}(X)$
interpreting the world atoms, and a family $\sim$ of _indistinguishability
relations_ $\sim_{a}\;\subseteq X\times X$ indexed over agents $a\in Ag$. We
require that each $\sim_{a}$ is an equivalence relation (in keeping with the
usual view that epistemic indistinguishability relations should be equivalence
relations); see however Remark 2. For a set $A\subseteq Ag$ of agents, we
write $\sim_{A}=(\bigcup_{a\in A}\sim_{a})^{*}$ 111This should not be confused
with similar notation used to denote the intersection of the $\sim_{a}$ in
work on epistemic logic with quantification over agents (Naumov and Tao 2019)
where $(-)^{*}$ denotes reflexive-transitive closure (note that $\sim_{A}$ is
symmetric, hence an equivalence). We define satisfaction
${\mathcal{M},x\models\psi}$ (_x satisfies $\psi$_) of a formula $\psi$ at a
world $x$ recursively by

$\displaystyle{\mathcal{M},x\not\models\bot}\qquad{\mathcal{M},x\models
p}\text{ iff }x\in V_{\mathsf{W}}(p)$
$\displaystyle{\mathcal{M},x\models\neg\phi}\text{ iff
}{\mathcal{M},x\not\models\phi}$
$\displaystyle{\mathcal{M},x\models\phi\land\chi}\text{ iff
}{\mathcal{M},x\models\phi}\text{ and }{\mathcal{M},x\models\chi}$
$\displaystyle{\mathcal{M},x\models C_{\psi}\phi}\text{ iff whenever
}x\sim_{{\llbracket\psi\rrbracket_{\mathcal{A}}}}y,\text{ then
}{\mathcal{M},y\models\phi};$

that is, $C_{\psi}$ is the standard box modality for
$\sim_{{\llbracket\psi\rrbracket_{\mathcal{A}}}}$. When
${\mathcal{M},x\models\phi}$, then we also say that $(\mathcal{M},x)$ is a
_model of $\phi$_ (and we will use this phrasing in general, also for other
logics). The formula $\phi$ is _satisfiable_ if there is a model of $\phi$,
and _valid_ (notation: $\models\phi$) if $\mathcal{M},x\models\phi$ for all
$\mathcal{M},x$. We write ${\llbracket\phi\rrbracket_{\mathcal{M}}}=\\{x\in
X\mid{\mathcal{M},x\models\phi}\\}$.

We record a fixpoint characterization of $C_{\psi}$: [end]lemma The set
${\llbracket C_{\psi}\phi\rrbracket_{\mathcal{M}}}$ is the greatest fixed
point of the function $F\colon\mathcal{P}(X)\to\mathcal{P}(X)$ given by $F(U)$
being the set of worlds $x$ such that ${\mathcal{M},x\models\phi}$ and
whenever ${\mathcal{A},a\models\psi}$ and $x\sim_{a}y$, then $y\in U$. By the
Knaster-Tarski fixpoint theorem, we can equivalently show that ${\llbracket
C_{\psi}\phi\rrbracket_{\mathcal{M}}}$ is the greatest postfixed point of $F$.
First, it is clear that ${\llbracket C_{\psi}\phi\rrbracket_{\mathcal{M}}}$ is
a postfixed point of $F$: Since $C_{\psi}$ is the box operator for the
transitive and reflexive closure of the $\psi$-successor relation, every world
$x$ in ${\llbracket C_{\psi}\phi\rrbracket_{\mathcal{M}}}$ satisfies $\phi$,
and all $\psi$-successors of $x$ satisfy $C_{\psi}\phi$ again. Second, if
$K\subseteq X$ is another postfixed point of $F$, i.e. $K\subseteq F(K)$, then
every world in $K$ satisfies $\phi$, and $K$ is closed under
$\psi$-successors, so by induction on the formation of $\sim_{\psi}$ as a
reflexive-transitive closure, every world in $K$ is in ${\llbracket
C_{\psi}\phi\rrbracket_{\mathcal{M}}}$.

######  Remark 2.

Since the modality $C_{\psi}$ takes reflexive-transitive closures, it is in
fact immaterial whether the indistinguishability relations $\sim_{a}$ are
individually reflexive and transitive; we impose the corresponding requirement
mainly to ease notation and discussion.

[end, text proof=Details for “autorefthm:prAtEnd]remark In logical settings
with non-rigid (i.e. world-dependent) agent models (e.g. (Grove and Halpern
1993; Grove 1995; Naumov and Tao 2019)), one can accommodate uncertainty about
the identity and properties of agents, and moreover specify agent groups by
their knowledge, as in ‘people who know $\phi$ also know $\psi$’. As indicated
in the introduction, AGEL, which assumes the agent logic to be rigid, trades
this mode of expression for a computationally and axiomatically tractable
treatment of common knowledge. One may still envisage extending AGEL with an
operator $I$, with $I\,\phi$ read as ‘knows about the truth or falsity of
$\phi$’. That is, an agent satisfies $I\,\phi$ if in every world, she knows
either $\phi$ or $\neg\phi$. For instance, if $\phi$ represents the publicly
contested fact whether or not transfer negotiations are under way concerning a
football player $P$, then $I\,\phi$ would hold for the relevant officials of
the involved clubs and maybe for $P$. However, harnessing such an operator
technically is likely to be challenging. To name one potential obstacle, the
first-order translation of $I\,\phi$ would presumably need to involve three
variables (i.e. unlike the translation of most modal logics would not end up
in the two-variable fragment): one for the agent $x$, and two for worlds that
are indistinguishable for $x$, and then required to agree on $\phi$ (see the
appendix). Using notation for models employed in the definition of the
semantics directly in first-order syntax, we translate satisfaction of the
formula $I\,\phi$ by an agent $a$ roughly into

$\forall x,y.\,x\sim_{a}y\to(\bar{\phi}(x)\leftrightarrow\bar{\phi}(y))$

where $\bar{\phi}(-)$ represents a first-order translation of $\phi$. This
formula needs three variables $a,x,y$. (This observation is purely heuristic;
we do not formally claim that use of three variables cannot be avoided, nor
would a two-variable translation directly imply decidability of the extension
of AGEL with $I$, as models are subject to constraints that fail to be first-
order definable.)

######  Remark 3.

Since AGEL is effectively a fixpoint logic, it is expected that compactness
fails. Indeed, given atomic agent concepts $A,B$ and a world atom $p$, the set
consisting of the formula $\neg C_{A\lor B}\>p$ and all formulae of the form
$C_{D_{1}}C_{D_{2}}\dots C_{D_{n}}p$, for $n\geq 0$ and
$D_{1},\dots,D_{n}\in\\{A,B\\}$, is unsatisfiable but all its finite subsets
are satisfiable. It follows that there is no finitary proof system for AGEL
that is _strongly_ complete, i.e. makes all unsatisfiable sets of formulae
inconsistent. We later give a proof system that is _weakly_ complete, i.e.
derives all valid formulae.

## Complexity

We show next that the satisfiability problem of AGEL is ExpTime-complete.

### Lower Bound:
Reduction from Group Epistemic Logic

We prove ExpTime-hardness by a satisfiability-preserving encoding of standard
group epistemic logic (GEL) (with common knowledge), which is known to be
ExpTime-hard (Fagin et al. 1995). (To facilitate the subsequent discussion, we
reduce from a slightly more expressive logic than strictly necessary for the
hardness proof.) We briefly recall the syntax and semantics of GEL: The logic
is parametrized over a finite set $Ag$ of agents and a set
$\mathsf{At}_{\mathsf{W}}$ of (world) atoms. The set of _formulae_
$\phi,\psi,\dots$ of GEL is then given by the grammar

$\phi,\psi::=\bot\mid p\mid\neg\phi\mid\phi\land\psi\mid C_{G}\phi$

where $p\in\mathsf{At}_{\mathsf{W}}$ and $\emptyset\neq G\subseteq Ag$, with
$C_{G}\phi$ read ‘$\phi$ is common knowledge among the agents in $G$’.
(Knowledge operators $K_{a}$ for individual agents $a$ are included as common
knowledge operators $C_{\\{a\\}}$.) As indicated in the introduction, the
difference with AGEL is that in GEL, groups $G$ of agents need to be given as
enumerated finite subsets of a known fixed set of named agents. Models
$\mathcal{M}=(X,V_{\mathsf{W}},\sim)$ consist of a set $X$ of worlds, a
(world) valuation
$V_{\mathsf{W}}\colon\mathsf{At}_{\mathsf{W}}\to\mathcal{P}(X)$, and a family
$\sim$ of indistinguishability relations $\sim_{a}\;\subseteq X\times X$,
indexed over agents $a\in Ag$ and again required to be equivalence relations.
For $G\subseteq Ag$, we write $\sim_{G}:=(\bigcup_{a\in G}\sim_{a})^{*}$.
Then, satisfaction ${\mathcal{M},x\models\phi}$ of a formula $\phi$ at a world
$x$ is defined recursively by the expected clauses for atoms and propositional
connectives, and

${\mathcal{M},x\models C_{G}\phi}\text{ iff whenever }x\sim_{G}y,\text{ then
}{\mathcal{M},y\models\phi}.$

The encoding $q$ of GEL into AGEL is given as follows. We introduce a fresh
agent atom $p_{a}$ for each $a\in Ag$. For a GEL formula $\phi$, $q(\phi)$ is
then defined recursively by

$q(C_{G}\phi):=C_{\bigvee_{a\in G}p_{a}}q(\phi)$

and commutation with all other constructs (i.e. $q(\neg\phi)=\neg q(\phi)$
etc.). Using the running assumption that ${\mathcal{L}_{\mathsf{Ag}}}$
conservatively extends classical propositional logic, we obtain

[end]theorem[Lower complexity bound] The satisfiability problem for AGEL is
ExpTime-hard.

###### Proof sketch.

We need to show that $q$ is indeed satisfiability-preserving. A model
$(\mathcal{M},x)$ of a GEL formula $\phi$ over the set $Ag$ of agents, with
$\mathcal{M}=(X,V_{\mathsf{W}},\sim)$, is transformed into a model
$(\mathcal{M}^{\prime},x)$ of the AGEL formula $q(\phi)$, with
$\mathcal{M}^{\prime}=(X,\mathcal{A},V_{\mathsf{W}},\sim^{\prime})$, by taking
$Ag$ to be the underlying set of $\mathcal{A}$, and
$V_{\mathsf{Ag}}(p_{a})=\\{a\\}$ for $a\in Ag$; this uses the running
assumption that ${\mathcal{L}_{\mathsf{Ag}}}$ conservatively extends classical
propositional logic.

Conversely, a model $(\mathcal{M},x)$ of $q(\phi)$, with
$\mathcal{M}=(X,\mathcal{A},V_{\mathsf{W}},\sim)$, is transformed into a model
$(\mathcal{M}^{\prime},x)$ of $\phi$, with
$\mathcal{M}^{\prime}=(X,V_{\mathsf{W}},\sim^{\prime})$, by taking
$\sim^{\prime}_{a}\;=\;\sim_{V_{\mathsf{Ag}}(p_{a})}$ (using notation like in
the formal semantics of AGEL). ∎

By reduction from GEL satisfiability. We show that the translation $q$ given
in the main body of the paper is satisfiability-preserving, i.e. that $\phi$
is satisfiable iff $q(\phi)$ is satisfiable.

_‘If’ :_ Given an AGEL-model
$\mathcal{M}=(X,(Ag,V_{\mathsf{Ag}}),V_{\mathsf{W}},$ ${\sim})$, we construct
a GEL-model $\mathcal{M}^{\prime}=(X,Ag,V_{\mathsf{W}},\sim^{\prime})$ by
taking

$\displaystyle\sim^{\prime}_{a}\;=\;\sim_{{\llbracket
p_{a}\rrbracket_{\mathcal{A}}}}.$

We show by induction on $\phi$ that for all $x\in X$, ${\mathcal{M},x\models
q(\phi)}$ iff ${\mathcal{M}^{\prime},x\models\phi}$. The cases for world atoms
and Boolean operators are trivial; we do the case for $C_{G}\phi$. By
definition, $q(C_{G}\phi)=C_{\bigvee_{a\in G}p_{a}}q(\phi)$. Now
$C_{\bigvee_{a\in G}p_{a}}$ is a standard modal box on the transitive-
reflexive closure of the union of the relations $\sim_{\llbracket
p_{a}\rrbracket_{\mathcal{A}}}$ over all $a\in G$, and by construction of
$\sim^{\prime}$, $C_{G}$ is a standard modal box over the same relation. We
are done by induction.

_‘Only if’ :_ Given a GEL model $\mathcal{M}=(X,V_{\mathsf{W}},\sim)$ over the
set $Ag$ of agents, we construct an AGEL model
$\mathcal{M}^{\prime}=(X,\mathcal{A},V_{\mathsf{W}},\sim^{\prime})$ by taking
$Ag$ to be the underlying set of $\mathcal{A}$, and
$V_{\mathsf{Ag}}(p_{a})=\\{a\\}$ for $a\in Ag$; this uses the running
assumption that ${\mathcal{L}_{\mathsf{Ag}}}$ conservatively extends classical
propositional logic, so an agent model $\mathcal{A}$ with the prescribed
valuation of agent atoms is guaranteed to exist. The truth conditions in the
respective semantics of GEL and AGEL are then literally the same.

######  Remark 4.

Depending on additional restrictions on the agent logic, it will sometimes be
possible to give also a fairly straightforward satisfiability-preserving
translation in the reverse direction, from AGEL to GEL. For instance, if the
agent logic is just classical propositional logic, then we can proceed as
follows: Let $\phi$ be an AGEL formula, and let
$A\subseteq\mathsf{At}_{\mathsf{Ag}}$ be the set of agent atoms mentioned in
$\phi$. Let $Ag$ be the (finite) set of truth valuations $\kappa\colon A\to 2$
in the set $2=\\{\bot,\top\\}$ of Boolean truth values, and write
$\kappa(\psi)$ for the truth value of a propositional formula $\psi$ over $A$
under $\kappa$; then a translation of $\phi$ into a satisfiability-equivalent
GEL formula $s(\phi)$ is defined recursively by

$s(C_{\psi}\chi)=C_{\\{\kappa\in Ag\mid\kappa(\psi)=\top\\}}s(\chi)$

and commutation with all other constructs. However, even in this basic case,
such a translation will be of limited use as it has exponential blowup (the
set ${\\{\kappa\in Ag\mid\kappa(\psi)=\top\\}}$ can be exponentially large).
For more expressive agent logics, e.g. whenever the agent logic extends
$\mathcal{ALC}$, one has (series of) formulae that are satisfiable only over
exponentially large agent models: Given agent formulae $\psi_{n}$ that are of
polynomial size in $n$ but satisfiable only over agent models of exponential
size in $n$ (in $\mathcal{ALC}$, such $\psi_{n}$ exist), the AGEL formulae
$p\land C_{\psi_{n}}\neg p$ are satisfiable only over models whose agent model
components are of exponential size in $n$. Indeed, from a purely computational
point of view (and for suitably restricted agent logics), one may see AGEL as
a way of dealing with exponentially many agents without incurring doubly
exponential computational cost. We realize this by an encoding into a
different target logic, discussed after the next example.

######  Example 5 (Lots of muddy children).

The classical _muddy children_ puzzle with $k$ many children can be seen as
$k$ many agents $A_{i}$ communicating according to a fixed protocol to gain
common knowledge of a length-$k$ bitstring where each agent $A_{i}$ can see
all bits except the one at index $i$ (Pavlovic 2021, Section 4.3).
Specifically, it is commonly known initially that at least one bit is set, and
the protocol then proceeds in rounds in which the agents announce whether they
have learned their missing bit. The full modelling of the puzzle thus requires
a dynamic epistemic logic with common knowledge and public announcements
(Baltag, Moss, and Solecki 1998; Lutz 2006). Here, we concentrate on
modelling, in an extended setting, how knowledge is gained in individual
rounds of the protocol, which does not require public announcements; we
generalize the textbook treatment by Huth and Ryan (2004).

We consider a variant of the puzzle that can essentially be seen as a product
of $n$ copies of the original puzzle. We then have an $n\times k$-matrix of
bits, and each agent has an _invisibility type_ consisting of one
_invisibility index_ per row determining the bit she cannot see in that row
(in the original puzzle, there is only one row, and the invisibility type is
the identity of the agent). We require that every bit of the matrix is seen by
at least one agent. We do not otherwise restrict which invisibility types are
realized; also, a given invisibility type may be realized by more than one
agent. Note that there are exponentially many (viz, $k^{n}$) invisibility
types; the point of these considerations being that the number of
(distinguishable) agents is a) not fixed, and b) potentially large. We
introduce propositional atoms $p_{(j,i)}$ for $1\leq j\leq n$ and $1\leq i\leq
k$ indicating whether the bit at position $(j,i$) in the matrix is _set_
($1$). We use agent atoms $h_{j,i}$ to describe agents who cannot see the
value of the bit at position $(j,i)$ of the matrix, in an agent logic that
extends propositional logic with a propositional background theory, in this
case hardwiring the above description of the scenario (every agent sees all
bits except one per row, and every bit is seen by some agent). The common
knowledge resulting from the visibility conditions is hence

$\textstyle C_{\top}\big{(}\bigwedge_{ij}(p_{j,i}\rightarrow C_{\neg
h_{j,i}}p_{j,i})\land(\neg p_{j,i}\rightarrow C_{\neg h_{j,i}}\neg
p_{j,i})\big{)}.$

We write $\alpha_{j}^{\leq x}$ for the (purely propositional) formula stating
that at most $x$ bits are set in row $j$; that is, $\alpha_{j}^{\leq x}$ is
the disjunction of all conjunctions of the form $\bigwedge_{i\in
H}p_{i,j}\land\bigwedge_{i\in\\{1,\dots,k\\}\setminus H}\neg p_{j,i}$ where
$H\subseteq\\{1,\dots,k\\}$ and $|H|\leq x$. (This formula is of exponential
size in the number $k$ of columns, but note that this happens already in the
original muddy children puzzle, i.e. in the case $n=1$.) The initial knowledge
available to the agents before the first round is that at least one bit is set
in each row:

$\textstyle C_{\top}(\bigwedge_{j}\neg\alpha_{j}^{\leq 0}).$

In each communication round the agents then choose one row, and communicate
whether or not they know the value of the bit they cannot see in that row.
Assuming all agents do not know the value of their respective bit, this
establishes common knowledge about everyone’s uncertainty:

$\textstyle C_{\top}(\bigwedge_{ij}\neg C_{h_{j,i}}p_{j,i}\land\neg
C_{h_{j,i}}\neg p_{j,i}).$

Of course the order of rounds is irrelevant here, and the state of the
protocol can hence simply be represented by a tuple $(x_{i},\dots,x_{n})$
where each $x_{j}$ counts how many communication rounds have taken place for
row $j$ (counting communication of the initial knowledge that at least one bit
is set in each row). The key invariant of the protocol is that if these
counters reach $(x_{1},\dots,x_{n})$ without anyone having learned new bits,
then this results in the accumulated common knowledge

$\textstyle C_{\top}(\bigwedge_{j}\neg\alpha_{j}^{\leq x_{j}}).$

This clearly holds in the beginning of the game due to the initial knowledge.
Then in state $(x_{1},\dots,x_{n})$, after querying row $j$, the common
knowledge increases according to the inference

$\Gamma,C_{\top}(\neg\alpha_{j}^{\leq x_{j}}),\textstyle
C_{\top}(\bigwedge_{i}\neg C_{h_{j,i}}p_{j,i}\land\neg C_{h_{j,i}}\neg
p_{j,i})\\\ \vDash C_{\top}(\neg\alpha_{j}^{\leq x_{j}+1}).$

where $\Gamma$ represents the visibility axioms and $\vDash$ denotes local
(i.e. per-world) consequence.. The formal proof is similar to the textbook
proof for the original puzzle (Huth and Ryan 2004), and sketched as follows:

  * •

Assume $\alpha_{j}^{\leq x_{j}+1}$.

  * •

From the accumulated knowledge of the previous rounds, the agents already know
that more than $x_{j}$ bits are set in row $j$. From the assumption, they can
conclude that exactly $x_{j}+1$ bits are set.

  * •

Given that nobody knew whether their respective missing bit in row $j$ is set,
the agents can conclude that more than $x_{j}+1$ bits are set in row $j$,
contradicting the assumption. (Otherwise at least one agent whose bit is set
would see only $x_{j}$ many set bits and could hence have deduced that her
missing bit is set.)

Similar reasoning is used to conclude missing bits once enough communication
rounds have been performed.

### Upper Bound: Encoding into the Full $\mu$-Calculus

We establish the ExpTime upper bound on satisfiability checking by a
satisfiability-preserving translation of AGEL into the $\mu$-calculus with
converse, also known as the _full $\mu$-calculus_, whose satisfiability
problem is in ExpTime (Vardi 1998). We emphasize that the full $\mu$-calculus
does not have the finite model property (Vardi 1998; Streett 1982); we
therefore establish a bounded model property separately in the next section.

In the translation, we use fixpoints to take transitive-reflexive closures,
and inverse roles to close under symmetry. The main idea is then to view the
family $\sim$ of per-agent indistinguishability relations $\sim_{a}$ featuring
in the definition of AGEL models as a ternary relation on a single domain, and
to encode this ternary relation as a binary relation between worlds and
(agent, world)-pairs.

In fact, the single-variable fragment of the full $\mu$-calculus suffices for
the translation; we briefly recall its syntax and semantics. The syntax is
parametrized over sets $\mathsf{AP}$ and $\mathsf{Prog}$ of _atomic
propositions_ and _atomic programs_ , respectively. A _program_ is either an
atomic program or a _converse program_ $\alpha^{-}$ of
$\alpha\in\mathsf{Prog}$. Moreover, we fix a single _fixpoint variable_ $z$.
Then, the set of _formulae_ $\phi,\psi,\dots$ is given by the grammar

$\phi,\psi::=\bot\mid p\mid
z\mid\neg\phi\mid\phi\land\psi\mid[\alpha]\phi\mid\nu z.\,\phi$

where $p\in\mathsf{AP}$ and $\alpha$ is a program. The box operator $[\alpha]$
is read ‘for all $\alpha$-successors’. The $\nu z$ operator takes greatest
fixpoints, and binds $z$; that is, an occurrence of $z$ is _free_ if it lies
outside the scope of any $\nu z$. Application of $\nu z$ is restricted to
formulae $\phi$ in which every free occurrence of $z$ is _positive_ , i.e.
lies under an even number of negations $\neg$. Further propositional
connectives $\top$, $\lor$, $\rightarrow$, $\leftrightarrow$ are defined as
usual. Moreover, we define diamond operators as
$\langle\alpha\rangle\phi:=\neg[\alpha]\neg\phi$. (Also, one can define least
fixpoints $\mu z.\,\phi$.)

The semantics is defined over _models_ $\mathcal{M}=(X,R,V)$ that consist of a
domain $X$, an assignment $R$ of a transition relation $R(\alpha)\subseteq
X\times X$ to every atomic program $\alpha\in\mathsf{Prog}$; and a valuation
$V\colon\mathsf{AP}\to\mathcal{P}(X)$ of the atomic propositions. The
interpretation of converse programs is defined by
$R(\alpha^{-})=\\{(e,d)\mid(d,e)\in R(\alpha)\\}$. The semantics of a formula
$\phi$ is then given as a function
$\llbracket\phi\rrbracket_{\mathcal{M}}\colon\mathcal{P}(X)\to\mathcal{P}(X)$
whose argument serves as the extension of $z$, inductively defined by the
expected clauses for Boolean operators, $\llbracket
p\rrbracket_{\mathcal{M}}=V(p)$, and

$\displaystyle\llbracket z\rrbracket_{\mathcal{M}}(U)$ $\displaystyle=U$
$\displaystyle\llbracket[\alpha]\phi\rrbracket_{\mathcal{M}}(U)$
$\displaystyle=\\{w\in X\mid\forall v\in X.\,(w,v)\in R(\alpha)$
$\displaystyle\qquad\qquad\qquad\qquad\qquad\rightarrow
v\in\llbracket\phi\rrbracket_{\mathcal{M}}(U)\\}$ $\displaystyle\llbracket\nu
z.\,\phi\rrbracket_{\mathcal{M}}(U)$ $\displaystyle=\bigcup\\{Z\subseteq X\mid
Z\subseteq\llbracket\phi\rrbracket_{\mathcal{M}}(Z)\\}.$

One shows by induction that when $\nu z.\,\phi$ is well-formed, then
$\llbracket\phi\rrbracket_{\mathcal{M}}$ is monotone w.r.t. set inclusion, so
$\llbracket\nu z.\,\phi\rrbracket_{\mathcal{M}}(U)$ as defined above is, by
the Knaster-Tarski fixpoint theorem, the greatest fixpoint of
$\llbracket\phi\rrbracket_{\mathcal{M}}$.

In detail, the translation is then defined as follows. We assume for the
translation that the agent logic is given as a fragment of the full
$\mu$-calculus. For clarity, we write $u$ for the syntactic embedding; we
assume that each $u(\psi)$ is _closed_ , i.e. does not contain a free
occurrence of $z$. As indicated previously, a typical choice would be
$\mathcal{ALC}$ (modulo the usual slight syntactic shifts), but for purposes
of the complexity analysis, the agent logic could in fact be the full
$\mu$-calculus itself (whereas the axiomatization introduced in the next
section needs assumptions on the agent logic that are not satisfied by the
full $\mu$-calculus, such as the finite model property).

We use three fresh atomic programs $\pi_{1},\pi_{2},\mathsf{edge}$. The
intention is that $\mathsf{edge}$ relates worlds to (agent, world)-pairs, out
of which $\pi_{1}$ extracts the agent component, and $\pi_{2}$ the world
component. Speaking more precisely, we do not insist that $\pi_{1},\pi_{2}$
are functional, so when $(x,r)\in R(\mathsf{edge})$ in a model, then $r$ may
in fact represent several (agent, world) pairs, namely all pairs $(a,y)$ such
that $(r,a)\in R(\pi_{1})$ and $(r,y)\in R(\pi_{2})$ (and indeed it may happen
that $r$ represents no pair at all). As per Remark 2, we do not need to worry
at this point about the fact that the induced indistinguishability relations
are not forced to be equivalence relations. As an intermediate step in the
translation, we introduce forward and backward binary ‘next-step’ modalities
by abbreviation:

$\psi\leadsto\phi:=[\mathsf{edge}](\langle\pi_{1}\rangle\psi\rightarrow[\pi_{2}]\phi),$

is understood as ‘all worlds that are reached by a single forward
indistinguishability step for an agent satisfying $\psi$ satisfy $\phi$’, and

$\phi\mathrel{\reflectbox{$\leadsto$}}\psi:=[\pi_{2}^{-}](\langle\pi_{1}\rangle\psi\rightarrow[\mathsf{edge}^{-}]\phi)$

describes the opposite direction, ‘all worlds that are reached by a single
backward indistinguishability step for an agent satisfying $\psi$ satisfy
$\phi$’. Using these two abbreviations to model a step along the
symmetrization of the indistinguishability relation, we can encode the common
knowledge modality, modelling transitive-reflexive closure via a greatest
fixpoint as indicated above: We define the translation $t$ of a AGEL formula
$\phi$ into a formula $t(\phi)$ in the full $\mu$-calculus recursively by

$t(C_{\psi}\phi)=\nu z.\,t(\phi)\allowbreak\land(u(\psi)\leadsto
z)\allowbreak\land(z\mathrel{\reflectbox{$\leadsto$}}u(\psi))$

and commutation with all other constructs. (Since no recursive calls of $t$
are made on $\psi$, its duplication does not lead to exponential blowup;
recall that by the current assumption, the translation $u$ of agent formulae
does essentially nothing.) We thus obtain the following result.

[end]theorem[Upper complexity bound] If the agent logic is a fragment of the
full $\mu$-calculus, then the satisfiability problem of AGEL is in ExpTime. We
show that the translation $t$ is really satisfiability-preserving, i.e. that
an AGEL formula $\phi$ is satisfiable iff $t(\phi)$ is satisfiable in the full
$\mu$-calculus.

_‘Only if’ :_ Given a AGEL model
$\mathcal{M}=(X,\mathcal{A},V_{\mathsf{W}},\sim)$ we construct a
$\mu$-calculus model $\mathcal{M}^{\prime}=(X^{\prime}=Ag\uplus
X\uplus(Ag\times X),R,V)$ where we interpret the syntactic material (atomic
programs and atomic propositions) mentioned in agent formulae in $\phi$ over
$Ag\subseteq X^{\prime}$ like in the given agent model $\mathcal{A}$,
exploiting that the agent logic is a fragment of the full $\mu$-calculus. We
assume w.l.o.g. that the sets $X$, $Ag$, and $Ag\times X$ are already
disjoint. We define the valuation $V$ as extending the valuation induced by
$\mathcal{A}$ to interpret world atoms via $V_{\mathsf{W}}$, and moreover put

$\displaystyle R(\mathsf{edge})$ $\displaystyle=\\{(x,(a,y))\mid
x\sim_{a}y\text{ in }\mathcal{M}\\}$ $\displaystyle R(\pi_{1})$
$\displaystyle=\\{((a,x),a)\mid(a,x)\in Ag\times X\\}$ $\displaystyle
R(\pi_{2})$ $\displaystyle=\\{((a,x),x)\mid(a,x)\in Ag\times X\\}.$

This model translation encodes the ternary relation into a heterogeneous world
set where edges are encoded as pairs of agents and target states. The agent
and the target state are then extracted from a pair with $\pi_{1}$, $\pi_{2}$
serving as projections.

We show by induction on $\phi$ that $\mathcal{M},x\models\phi$ iff
$\mathcal{M}^{\prime},x\models t(\phi)$, for $x\in X$. Again, the cases for
world atoms and Boolean operators are trivial; we do the case for the common
knowledge operator $C_{\psi}$.

We first note that due to symmetry of $\sim$, we have that for $x,y,a\in
X^{\prime}$,

$(x,(a,y))\in R(\mathsf{edge}),$

(and then $((a,y),a)\in R(\pi_{1})$, $((a,y),y)\in R(\pi_{2})$) exactly when

$((a,x),y)\in R(\mathsf{edge}^{-})$

(and then $((a,x),a)\in R(\pi_{1})$, $(x,(a,x))\in R(\pi_{2}^{-})$), namely,
both hold iff $x\sim_{a}y$, equivalently $y\sim_{a}x$, in $\mathcal{M}$. It is
hence clear that $\psi\leadsto\chi$ and
$\chi\mathrel{\reflectbox{$\leadsto$}}\psi$ are equivalent over the model
$\mathcal{M}^{\prime}$. Over this model, we can thus equivalently modify the
translation to

$t(C_{\psi}\phi)=\nu z.\,\phi\land(\psi\leadsto z);$

also, the above implies that $\psi\leadsto(-)$ acts as a box modality on
$\psi$-successors ($\psi\leadsto\chi$ holds at a world iff $\chi$ holds at all
$\psi$-successors). By Lemma Semantics, the interpretation of $C_{\psi}$ in
$\mathcal{M}$ is a greatest fixpoint involving a box operator for the same
relation $\bigcup_{a\in{\llbracket\psi\rrbracket_{\mathcal{A}}}}\sim_{a}$.
More formally, since $\mathcal{M}$ embeds into $\mathcal{M}^{\prime}$, and the
associated inclusion map is a $p$-morphism (Blackburn, de Rijke, and Venema
2001), i.e. a functional bisimulation, w.r.t. these relations, it follows by
the well-known fact that the (forward) $\mu$-calculus is bisimulation-
invariant that satisfaction of $C_{\psi}\phi$ is preserved.

_‘If’ :_ Given a $\mu$-calculus-model $\mathcal{M}=(X,R,V)$ we construct an
AGEL model $\mathcal{M}^{\prime}=(X,\mathcal{A},V_{\mathsf{W}},\sim)$. We use
the original set $X$ of worlds also as the underlying set $Ag$ of the agent
model $\mathcal{A}$, whose structure we then obtain by just suitably
restricting $\mathcal{M}$. Similarly, we take $V_{\mathsf{W}}$ to be the
restriction of $V$ to world atoms, i.e. we interpret world atoms in
$\mathcal{M}^{\prime}$ like in $\mathcal{M}$. We define the
indistinguishability relation $\sim_{a}$ for $a\in Ag=X$ as the symmetric
closure of the relation

$\\{(x,y)\mid\exists(x,x^{\prime})\in R(\mathsf{edge}).\\\ (x^{\prime},a)\in
R(\pi_{1}),(x^{\prime},y)\in R(\pi_{2})\\},$

exploiting that by Remark 2, we do not actually need to care whether
$\sim_{a}$ is reflexive or transitive. We do enforce symmetry to ensure more
straightforward agreement of the semantics on both sides.

It is then clear that for each $a\in Ag$ and each agent formula $\psi$,
${\mathcal{A},a\models\psi}$ iff
$a\in{\llbracket\psi\rrbracket_{\mathcal{M}}}(U)$, noting that the latter does
not depend on $U$ since agent formulae are assumed to be closed.

Now note that by the above construction of $\sim$, $\psi\leadsto(-)$ and
$(-)\mathrel{\reflectbox{$\leadsto$}}\psi$ jointly act as a box modality on
the $\psi$-successors according to $\sim$, where the symmetric closure is
emulated by considering both $\psi\leadsto(-)$ and
$(-)\mathrel{\reflectbox{$\leadsto$}}\psi$. Replacing the semantic clause for
$C_{\psi}$ by the fixpoint characterization as per Lemma Semantics, we thus
obtain that the truth conditions for $C_{\psi}$ is the same as for its
translation along $t$. As the clauses for Boolean operators agree as well, and
the valuation of world atoms in $\mathcal{M}^{\prime}$ is just inherited from
$\mathcal{M}$, we obtain that for each $x\in X$ and each world formula $\chi$,
$\mathcal{M}^{\prime},x\models\chi$ iff $x\in\llbracket
t(\chi)\rrbracket_{\mathcal{M}}(U)$ (noting again that the latter set does not
depend on $U$ because $t(\chi)$ is closed), so $\mathcal{M}^{\prime}$ serves
as a witness for satisfiability of any formula $\chi$ such that $t(\chi)$ is
satisfied within $\mathcal{M}$.

###### Proof sketch.

We need to show that the translation $t$ is really satisfiability-equivalent.
From a model $\mathcal{M},x_{0}$ of an AGEL formula $\phi$, with
$\mathcal{M}=(X,\mathcal{A},V_{\mathsf{W}},\sim)$, we construct a model
$(\mathcal{M}^{\prime},x_{0})$ of $t(\phi)$, with
$\mathcal{M}^{\prime}=(X^{\prime},R,V)$, as follows. Following the intention
of the translation $t(\phi)$ as indicated above, we take $X^{\prime}$ to be
the union of the set $X$ of worlds, the set $Ag$ of agents (the underlying set
of $\mathcal{A}$), and the set $Ag\times X$ of (agent, world) pairs, assuming
w.l.o.g. that these sets are disjoint. We interpret the syntactic material
(atomic programs and atomic propositions) mentioned in agent formulae in
$\phi$ over $Ag\subseteq X^{\prime}$ like in the given agent model
$\mathcal{A}$, exploiting that the agent logic is a fragment of the full
$\mu$-calculus. Similarly, we interpret world atoms on $X$ in the same way as
in $\mathcal{M}$. Finally, we interpret $\pi_{1},\pi_{2}$ as the expected
projections $R(\pi_{1})=\\{((a,x),a)\mid(a,x)\in Ag\times X\\}$,
$R(\pi_{2})=\\{((a,x),x)\mid(a,x)\in Ag\times X\\}$, and $\mathsf{edge}$ as

$R(\mathsf{edge})=\\{(x,(a,y))\mid x\sim_{a}y\text{ in }\mathcal{M}\\}.$

It is not hard to see that $(\mathcal{M}^{\prime},x)$ is really a model of
$\phi$.

In the converse direction, given a model $(\mathcal{M},x_{0})$ of the
$\mu$-calculus formula $t(\phi)$, with $\mathcal{M}=(X,R,V)$, we construct a
model $(\mathcal{M}^{\prime},x_{0})$ of $\phi$, with
$\mathcal{M}^{\prime}=(X,\mathcal{A},V_{\mathsf{W}},\sim)$, as follows. We use
the original set $X$ of worlds also as the underlying set $Ag$ of the agent
model $\mathcal{A}$, whose structure we then obtain by just suitably
restricting $\mathcal{M}$. Similarly, we take $V_{\mathsf{W}}$ to be the
restriction of $V$ to world atoms, i.e. we interpret world atoms in
$\mathcal{M}^{\prime}$ like in $\mathcal{M}$. Finally, as indicated above, we
define the indistinguishability relation $\sim_{a}$ for $a\in Ag=X$ as the
symmetric closure of the relation

$\\{(x,y)\mid\exists(x,e)\in R(\mathsf{edge}).\\\ (e,a)\in R(\pi_{1}),(e,y)\in
R(\pi_{2})\\}.$

Again, it is not hard to check that $(\mathcal{M},x)$ is really a model of
$\phi$. ∎

In combination with Theorem Lower Bound: Reduction from Group Epistemic Logic,
we thus have

######  Corollary 6 (Complexity of AGEL).

If the agent logic is a fragment of the full $\mu$-calculus, then the
satisfiability problem of AGEL is ExpTime-complete.

######  Remark 7.

Indeed the above encoding implies that one can raise the expressiveness of the
agent logic to extensions of the full $\mu$-calculus that remain decidable in
ExpTime. One candidate is the _full hybrid $\mu$-calculus_ (Sattler and Vardi
2001), which extends the full $\mu$-calculus with _nominals_ , i.e.
propositional atoms denoting single objects. This opens the possibility of
combining explicitly named agents in the standard sense with abstract groups
of agents, as in the formula

$C_{\mathsf{John}\vee\exists\,\mathsf{hasFriend}.\,\\!\mathsf{John}}\,\mathsf{Pub\\_on\\_Wednesdays},$

which says that John and his friends know that their regular pub night is on
Wednesdays.

## Completeness and Bounded Models

We axiomatize AGEL in Hilbert style using the following system $C5$ of axioms
and rules:

$\displaystyle(T)$ $\displaystyle C_{\psi}\phi\rightarrow\phi$
$\displaystyle(\bot)$ $\displaystyle\phi\rightarrow C_{\bot}\phi$
$\displaystyle(K)$ $\displaystyle
C_{\psi}(\phi\rightarrow\gamma)\rightarrow(C_{\psi}\phi\rightarrow
C_{\psi}\gamma)$ $\displaystyle(4)$ $\displaystyle C_{\psi}\phi\rightarrow
C_{\psi}C_{\psi}\phi$ $\displaystyle(5)$ $\displaystyle\neg
C_{\psi}\phi\rightarrow C_{\psi}\neg C_{\psi}\phi$
$\displaystyle(\mathit{Ind})$ $\displaystyle
C_{\psi\lor\chi}(\phi\rightarrow(C_{\psi}\phi\land
C_{\chi}\phi))\rightarrow(\phi\rightarrow C_{\psi\lor\chi}\phi)$
$\displaystyle(\mathit{Nec})$
$\displaystyle\frac{\phi}{C_{\psi}\phi}\qquad(\mathit{AM})\quad\frac{\gamma\rightarrow\psi}{C_{\psi}\phi\rightarrow
C_{\gamma}\phi}$

Recall that by our running assumptions, the agent logic
${\mathcal{L}_{\mathsf{Ag}}}$ is closed under all propositional connectives.
We write $C5\vdash\phi$ if an AGEL formula $\phi$ is derivable in this system;
$\phi$ is _consistent_ if $C5\not\vdash\neg\phi$. For a finite set $\Gamma$ of
formulae, we write $\widehat{\Gamma}$ for the conjunction of all formulae in
$\Gamma$, and we say that $\Gamma$ is _consistent_ if $\widehat{\Gamma}$ is
consistent. The system includes the usual $S5$ axioms for common knowledge,
reflecting normality (axiom $(K)$), reflexivity (axiom $(T)$), transitivity
(axiom $(4)$), and Euclideanity (axiom $(5)$), as well as the usual
necessitation rule $(\mathit{Nec})$. As usual, the ($K$) axiom implies
commutation of $C_{\psi}$ with conjunction, and hence, together with the
necessitation rule ($\mathit{Nec}$), monotonicity and replacement of
equivalents for $C_{\psi}$. Specific properties of AGEL are reflected in the
axiom $(\bot)$, which, together with $(T)$, says that $C_{\bot}\phi$ holds
almost vacuously, in the sense that it does not claim any agent to know
anything but requires $\phi$ to be true in the current world; in the rule
$(\mathit{AM})$, which says that $C_{\psi}\phi$ is antimonotone in $\psi$, as
requiring fewer agents to know $\phi$ is a weaker claim; and, centrally, in
the induction axiom $(\mathit{Ind})$, which captures the fact that the
indistinguishability relation $\sim_{A\cup B}$ for a union $A\cup B$ of two
sets $A,B$ of agents is the reflexive-transitive closure of the union of the
indistinguishability relations $\sim_{A}$, $\sim_{B}$ for the original sets.
The rule $(\mathit{AM})$ implies replacement of equivalents in the index of
$C_{\psi}$ (from equivalence of $\psi$ and $\psi^{\prime}$, derive equivalence
of $C_{\psi}\phi$ and $C_{\psi^{\prime}}\phi$). Via $(\mathit{AM})$, the
system depends on reasoning in the agent logic, which we will assume to be
completely axiomatized.

We note first that the induction axiom generalizes to multiple disjuncts:
[end]lemma Every formula of the form

$C_{\bigvee_{i=1}^{n}\psi_{i}}(\phi\rightarrow(\textstyle\bigwedge_{i=1}^{n}C_{\psi_{i}}\phi))\rightarrow(\phi\rightarrow
C_{\bigvee_{i=1}^{n}\psi_{i}}\phi)$

(for $n\geq 0$) is derivable in $C5$. Induction on $n$. We keep use of
monotonicity, replacement of equivalents, and propositional reasoning
implicit. The case $n=0$ is by ($\mathit{Nec}$) and $(\bot)$, and the case
$n=1$ by ($T$). For the inductive step $n\to n+1$, where $n\geq 1$, we note
first that the inductive hypothesis implies derivability of the formula

$C_{\bigvee_{i=1}^{n+1}\psi_{i}}C_{\bigvee_{i=1}^{n}\psi_{i}}(\phi\rightarrow(\textstyle\bigwedge_{i=1}^{n}C_{\psi_{i}}\phi))\rightarrow\\\
C_{\bigvee_{i=1}^{n+1}\psi_{i}}(\phi\rightarrow
C_{\bigvee_{i=1}^{n}\psi_{i}}\phi)$

using ($\mathit{Nec}$) (with $C_{\bigvee_{i=1}^{n+1}\psi_{i}}$) and ($K$).
Using ($\mathit{AM}$),and ($4$), we then derive

$C_{\bigvee_{i=1}^{n+1}\psi_{i}}(\phi\rightarrow(\textstyle\bigwedge_{i=1}^{n}C_{\psi_{i}}\phi))\rightarrow
C_{\bigvee_{i=1}^{n+1}\psi_{i}}(\phi\rightarrow
C_{\bigvee_{i=1}^{n}\psi_{i}}\phi)$

and thus, conjoining both sides of the implication with
$C_{\bigvee_{i=1}^{n+1}\psi_{i}}(\phi\to C_{\psi_{n+1}}\phi)$ and using
commutation of $C_{\bigvee_{i=1}^{n+1}\psi_{i}}$ with conjunction,

$C_{\bigvee_{i=1}^{n+1}\psi_{i}}(\phi\rightarrow(\textstyle\bigwedge_{i=1}^{n+1}C_{\psi_{i}}\phi))\rightarrow\\\
C_{\bigvee_{i=1}^{n+1}\psi_{i}}(\phi\rightarrow(C_{\bigvee_{i=1}^{n}\psi_{i}}\phi\land
C_{\psi_{n+1}}\phi)).$

The inductive claim for $n+1$ then follows by chaining this implication with
an instance of ($\mathit{Ind}$). We explicitly record soundness of the system:
[end]theorem[Soundness] If $C5\vdash\phi$ then $\models\phi$. Soundness of the
axioms $(T)$, $(4)$, $(5)$, $(K)$ and the rule $(\mathit{Nec})$ is standard
for modal logics interpreted over equivalence relations. Soundness of $(\bot)$
and the rule $(\mathit{AM})$ is clear. Soundness of the induction axiom
$C_{\psi\lor\chi}(\phi\rightarrow(C_{\psi}\phi\land
C_{\chi}\phi))\rightarrow(\phi\rightarrow C_{\psi\lor\chi}\phi)$ is seen as
follows. Let $x$ a world in an AGEL-model $\mathcal{M}$ that satisfies
$C_{\psi\lor\chi}(\phi\rightarrow(C_{\psi}\phi\land C_{\chi}\phi))$ and
$\phi$; we have to show that ${\mathcal{M},x\models C_{\psi\lor\chi}\phi}$. We
need to show that ${\mathcal{M},y\models\phi}$ for all worlds $y$ such that
$x\sim_{{\llbracket\psi\lor\chi\rrbracket_{\mathcal{A}}}}y$. Let $y$ be such a
world. Then there exists a finite chain
$x=x_{0}\sim_{a_{1}}x_{1}\sim_{a_{2}}\dots\sim_{a_{m-1}}x_{m-1}\sim_{a_{m}}x_{m}=y$
such that
$a_{1},\dots,a_{m}\in{\llbracket\psi\lor\chi\rrbracket_{\mathcal{A}}}$. By
straightforward induction on $i$, every state $x_{i}$ in this chain satisfies
$C_{\psi}\phi$, $C_{\chi}\phi$, and $\phi$. In particular, $x_{m}$ satisfies
$\phi$, as required. We show completeness via a finite canonical model
construction that is related to the standard treatment of propositional
dynamic logic (PDL) in that it needs to close canonical models under
transitivity (Fischer and Ladner 1979; Blackburn, de Rijke, and Venema 2001).
This construction requires some restrictions on the agent logic:

######  Definition 8.

We say that the agent logic ${\mathcal{L}_{\mathsf{Ag}}}$ has the _filtered
model property_ if, for each finite set $\Sigma_{\mathsf{Ag}}$ of agent
formulae that is closed under subformulae, there is an agent model
$\mathcal{A}(\Sigma_{\mathsf{Ag}})$, with underlying set denoted by
$Ag(\Sigma_{\mathsf{Ag}})$, such that on the one hand any two distinct agents
in $Ag(\Sigma_{\mathsf{Ag}})$ are distinguished by a formula in
$\Sigma_{\mathsf{Ag}}$ (in particular $Ag(\Sigma_{\mathsf{Ag}})$ is finite,
namely at most exponential in $|\Sigma_{\mathsf{Ag}}|$), and on the other hand
for every satisfiable subset $\Gamma\subseteq\Sigma_{\mathsf{Ag}}$, there is
an agent in $Ag(\Sigma_{\mathsf{Ag}})$ that satisfies all formulae in
$\Gamma$. Since the agent logic is closed under propositional connectives, we
then have, for each agent $a\in Ag(\Sigma_{\mathsf{Ag}})$, a _characteristic
agent formula_ $\widehat{a}$ (a propositional combination of
$\Sigma_{\mathsf{Ag}}$-formulae) such that
${\llbracket\widehat{a}\rrbracket_{\mathcal{A}(\Sigma_{\mathsf{Ag}})}}=\\{a\\}$.
We put

$\mathsf{Clo_{\mathsf{Ag}}}(\Sigma_{\mathsf{Ag}})=\Sigma_{\mathsf{Ag}}\cup\\{\widehat{}a\mid
a\in Ag(\Sigma_{\mathsf{Ag}})\\}.$

######  Example 9.

As indicated in the introduction, $\mathcal{ALC}$ has the filtered model
property (and is completely axiomatized), and in fact one can go beyond
$\mathcal{ALC}$ to some degree. In particular, the extension of
$\mathcal{ALC}$ with _nominals_ , $\mathcal{ALCO}$, still has the filtered
model property. (See also comments in Remark 7.)

We _fix from now on a consistent AGEL formula $\rho_{0}$_. We base our
canonical model construction on a suitable notion of closure.

######  Definition 10 (Normalized negation).

We let $\leavevmode\hbox{\smash{$\dot{\neg}$}}\phi=\chi$ if $\phi$ has the
form $\phi=\neg\chi$, and
$\leavevmode\hbox{\smash{$\dot{\neg}$}}\phi=\neg\phi$ otherwise.

######  Definition 11 (Closure).

Let $\Sigma_{\mathsf{Ag}}$ be the closure of the set of agent formulae
occurring in $\rho_{0}$ under taking subformulae. Then the _closure_ $\Sigma$
of $\rho_{0}$ is the least set of world formulae containing $\rho_{0}$ that is
closed under (world) subformulae and normalized negation, and moreover
satisfies

$\text{if }C_{\chi}\phi\in\Sigma\text{ and
}\psi\in\mathsf{Clo_{\mathsf{Ag}}}(\Sigma_{\mathsf{Ag}})\text{, then
}C_{\psi}\phi\in\Sigma$

(with $\mathsf{Clo_{\mathsf{Ag}}}(\Sigma_{\mathsf{Ag}})$ as per Definition 8).

We next construct a weak form of model of $\rho_{0}$ that assigns
indistinguishability relations to sets of agents without regard to their
definition via reflexive-transitive closure; this will be rectified in a
subsequent step.

######  Definition 12 (Pseudo-model).

An AGEL _pseudo-model_
$\mathcal{M}^{p}=(X,\mathcal{A},V_{\mathsf{W}},\sim^{p})$ consists of a set
$X$ of worlds, an agent model $\mathcal{A}$ with underlying set $Ag$ of
agents, a valuation
$V_{\mathsf{W}}\colon\mathsf{At}_{\mathsf{W}}\to\mathcal{P}(X)$ of the world
atoms, and an equivalence relation $\sim^{p}_{A}$ on $X$ for each subset
$A\subset Ag$. The _semantics_ of AGEL over pseudo-models is defined like over
models, except that the interpretation of $C_{\psi}$ uses the relation
$\sim^{p}_{{\llbracket\psi\rrbracket_{\mathcal{A}}}}$ in place of
$\sim_{{\llbracket\psi\rrbracket_{\mathcal{A}}}}$.

We construct a _canonical pseudo-model_
$\mathcal{C}^{p}_{\Sigma}=(X_{\Sigma},\allowbreak\mathcal{A}(\Sigma_{\mathsf{Ag}}),\allowbreak
V_{\mathsf{W}},\sim^{p})$ by taking $X_{\Sigma}$ to consist of the maximal
consistent subsets of $\Sigma$; $\mathcal{A}(\Sigma_{\mathsf{Ag}})$ as per
Definition 8; $V_{\mathsf{W}}(p)=\\{\Gamma\in X_{\Sigma}\mid p\in\Gamma\\}$;
and

$\Gamma\sim^{p}_{\llbracket\psi\rrbracket_{\mathcal{A}}}\Delta\leftrightarrow\widehat{\Gamma}\land
P_{\psi}\widehat{\Delta}\text{ consistent}$

where by $P_{\psi}$ we denote the dual of $C_{\psi}$, i.e. $P_{\psi}\phi:=\neg
C_{\psi}\neg\psi$. Well-definedness is guaranteed by the properties of
$\mathcal{A}(\Sigma_{\mathsf{Ag}})$; indeed we shall often write
$\sim^{p}_{\psi}$ in place of
$\sim^{p}_{\llbracket\psi\rrbracket_{\mathcal{A}}}$ for readability, similarly
for $\sim$. We note that $\Sigma$ inherits exponential size from
$\mathsf{Clo_{\mathsf{Ag}}}(\Sigma_{\mathsf{Ag}})$, so $X_{\Sigma}$ is of
doubly exponential size in the size of $\rho_{0}$.

[end]lemma The relations $\sim^{p}_{\psi}$ are reflexive and symmetric.
_Symmetry:_ Let $\widehat{\Gamma}\land P_{\psi}\widehat{\Delta}$ be
consistent. Then $\widehat{\Delta}\land P_{\psi}\widehat{\Gamma}$ is
consistent; for assume otherwise. Then $\vdash\widehat{\Delta}\rightarrow
C_{\psi}\neg\widehat{\Gamma}$, and hence $\widehat{\Gamma}\land
P_{\psi}C_{\psi}\neg\widehat{\Gamma}$ is consistent. By the contraposition of
axiom $(5)$, we obtain that $\widehat{\Gamma}\land
C_{\psi}\neg\widehat{\Gamma}$ is consistent, which contradicts $(T)$.

_Reflexivity:_ To show that $\Gamma\sim^{p}_{\psi}\Gamma$, suppose otherwise.
Then $\vdash\widehat{\Gamma}\rightarrow C_{\psi}\neg\widehat{\Gamma}$ and via
$(T)$, $\vdash\widehat{\Gamma}\rightarrow\neg\widehat{\Gamma}$, contradicting
consistency of $\Gamma$.

The point of using the canonical pseudo-model is that it allows for a
straightforward proof of the usual existence lemma: [end]lemma[Existence
Lemma] Let $\Gamma\in X_{\Sigma}$ be a world in the canonical pseudo-model
$\mathcal{C}^{p}_{\Sigma}$ such that $\neg C_{\psi}\phi\in\Gamma$. Then there
exists $\Delta\in X_{\Sigma}$ such that $\Gamma\sim^{p}_{\psi}\Delta$ and
$\neg\phi\in\Delta$ Enumerate the formulae
$\sigma_{1},\dots,\sigma_{m}\in\Sigma$. We define sets $\Delta_{n}$
iteratively to make $\widehat{\Gamma}\land P_{\psi}\widehat{\Delta_{n}}$
consistent:

$0$:

$\Delta_{0}=\\{\neg\phi\\}$. Since $\neg C_{\psi}\phi\in\Gamma$, we trivially
have that $\widehat{\Gamma}\land P_{\psi}\neg\phi$ is consistent.

$n\to n+1$:

As $\widehat{\Gamma}\land P_{\psi}\widehat{\Delta_{n}}$ is consistent, so is
$\widehat{\Gamma}\land
P_{\psi}(\widehat{\Delta_{n}}\land(\sigma_{n+1}\lor\leavevmode\hbox{\smash{$\dot{\neg}$}}\sigma_{n+1}))$.
Since $P_{\psi}$ derivably commutes with disjunction, it follows that
$\widehat{\Gamma}\land
P_{\psi}((\widehat{\Delta_{n}}\land\sigma_{n+1})\lor(\widehat{\Delta_{n}}\land\leavevmode\hbox{\smash{$\dot{\neg}$}}\sigma_{n+1}))$
is consistent, i.e. at least one of $\widehat{\Gamma}\land
P_{\psi}(\widehat{\Delta_{n}\cup\\{\sigma_{n+1}\\}})$ or
$\widehat{\Gamma}\land
P_{\psi}(\widehat{\Delta_{n}\cup\\{\leavevmode\hbox{\smash{$\dot{\neg}$}}\sigma_{n+1}\\}})$
is consistent, and correspondingly $\Delta_{n}\cup\\{\sigma_{n+1}\\}$ or
$\Delta_{n}\cup\\{\leavevmode\hbox{\smash{$\dot{\neg}$}}\sigma_{n+1}\\}$ can
then be picked as $\Delta_{n+1}$.

Then, $\Delta_{m}$ serves as the desired $\Delta$. Leveraging characteristic
agent formulae, we can derive a proper AGEL-model, the _canonical model_
$\mathcal{C}_{\Sigma}$, from the canonical pseudo-model
$\mathcal{C}^{p}_{\Sigma}$ by taking

$\sim_{a}\;=\;\sim^{p}_{\widehat{a}},$

where we exploit that by Remark 2, we do not need to care whether $\sim_{a}$
is transitive. The key point is then that the existence lemma survives this
transition thanks to the following fact, which hinges on the induction axiom
$(\mathit{Ind})$: [end]lemma For all formulae
$\psi\in\mathsf{Clo_{\mathsf{Ag}}}(\Sigma_{\mathsf{Ag}})$,
$\sim^{p}_{\psi}\subseteq\sim_{{\llbracket\psi\rrbracket_{\mathcal{A}}}}$ Let
$\Gamma,\Delta\in X_{\Sigma}$, and let
$\psi\in\mathsf{Clo_{\mathsf{Ag}}}(\Sigma_{\mathsf{Ag}})$ be an agent formula
such that $\Gamma\sim^{p}_{\psi}\Delta$. We have to show that there exist a
finite sequence of worlds $C_{0},\dots,C_{n}$ and
$a_{0},\dots,a_{n-1}\in{\llbracket\psi\rrbracket_{\mathcal{A}}}$ such that
$\Gamma=C_{0}\sim_{a_{0}}C_{1},\dots,C_{n-1}\sim_{a_{n-1}}C_{n}=\Delta$. Let
$D$ be the set of all worlds reachable from $\Gamma$ by such a sequence; we
thus have to show that $\Delta\in D$. Define $\delta:=\bigvee_{\Theta\in
D}\widehat{\Theta}$. Note that
$\delta\land\bigvee_{a\in{\llbracket\psi\rrbracket_{\mathcal{A}}}}P_{\widehat{a}}\neg\delta$
is inconsistent, for suppose otherwise. Then (by derivable commutation of $P$
operators with disjunction), $\delta\land P_{\widehat{a}}\widehat{F}$ would be
consistent for some $a\in{\llbracket\psi\rrbracket_{\mathcal{A}}}$ and some
$F_{a}\notin D$. Hence, also $\widehat{C}\land P_{\widehat{a}}\widehat{F_{a}}$
is consistent for at least one $C\in D$. But then
$C\sim^{p}_{\widehat{a}}F_{a}$, i.e. $C\sim_{a}F_{a}$, implying that $F_{a}$
is reachable from $\Gamma$, in contradiction to $F_{a}\notin D$. So,
$\vdash\delta\rightarrow\bigwedge_{a\in{\llbracket\psi\rrbracket_{\mathcal{A}}}}C_{\widehat{a}}\delta$.
By $(\mathit{Nec})$, we obtain $\vdash
C_{\bigvee_{a\in{\llbracket\psi\rrbracket_{\mathcal{A}}}}\widehat{a}}(\delta\rightarrow\bigwedge_{a\in{\llbracket\psi\rrbracket_{\mathcal{A}}}}C_{\widehat{a}}\delta)$,
whence $\vdash\delta\rightarrow
C_{\bigvee_{a\in{\llbracket\psi\rrbracket_{\mathcal{A}}}}\widehat{a}}\delta$
by Lemma Completeness and Bounded Models. From Lemma 12, $\Gamma\in D$ and
hence $\vdash\widehat{\Gamma}\rightarrow
C_{\bigvee_{a\in{\llbracket\psi\rrbracket_{\mathcal{A}}}}\widehat{a}}\delta$.
By the assumptions on $\mathcal{A}(\Sigma_{\mathsf{Ag}})$,
$\vdash\psi\rightarrow\bigvee_{a\in{\llbracket\psi\rrbracket_{\mathcal{A}}}}\widehat{a}$.
Using $(\mathit{AM})$, we obtain $\vdash\widehat{\Gamma}\rightarrow
C_{\psi}\delta$. As $\Gamma\sim^{p}_{\psi}\Delta$, $\widehat{\Gamma}\land
P_{\psi}\widehat{\Delta}$ is consistent, and hence
$P_{\psi}(\widehat{\Delta}\land\delta)$ is consistent by standard reasoning
with the $(K)$ axiom. This means that $\widehat{\Delta}\land\delta$ is
consistent, whence $\widehat{\Theta}\land\widehat{\Delta}$ is consistent for
at least one disjunct $\widehat{\Theta}$ of $\delta$ (with $\Theta\in D$). As
both $\Theta$ and $\Delta$ are maximal consistent subsets of $\Sigma$, we
obtain $\Theta=\Delta$ and hence $\Delta\in D$. It is then straightforward to
establish the expected truth lemma, making use of the fact that
$\mathsf{Clo_{\mathsf{Ag}}}(\Sigma_{\mathsf{Ag}})$ contains all requisite
characteristic agent-formulae: [end]lemma[Truth Lemma] Let $\Gamma$ be a world
in the canonical model $\mathcal{C}_{\Sigma}$. Then for all $\phi\in\Sigma$,

$\phi\in\Gamma\leftrightarrow{\mathcal{C}_{\Sigma},\Gamma\models\phi}.$

Induction on $\phi$. The propositional cases are trivial. In the case for
$\phi=C_{\psi}\chi$, we need to show that $C_{\psi}\chi\in\Gamma$ iff
${\mathcal{C}_{\Sigma},\Gamma\models C_{\psi}\chi}$.

_‘Only if’:_ Suppose that $C_{\psi}\chi\in\Gamma$. We need to show that
${\mathcal{C}_{\Sigma},\Gamma\models C_{\psi}\chi}$, i.e. that all worlds
reachable from $\Gamma$ in finitely many $\psi$-steps satisfy $\chi$. By the
inductive hypothesis, this means that all these worlds contain $\chi$, which
follows by $(T)$ once we show that all these worlds contain $C_{\psi}\chi$; to
this end, it suffices so show that the formula $C_{\psi}\chi$ is inherited
from any world (say, $\Gamma$) to all its $\psi$-successors. Assume the
contrary. Then there exists a world $\Delta$ such that $\widehat{\Gamma}\land
P_{\widehat{a}}\widehat{\Delta}$ is consistent for some
$a\in{\llbracket\psi\rrbracket_{\mathcal{A}}}$ and $\neg
C_{\psi}\chi\in\Delta$. In particular, $\widehat{\Gamma}\land
P_{\widehat{a}}{\neg C_{\psi}\chi}$ is consistent, i.e.
$\widehat{\Gamma}\land\neg C_{\widehat{a}}C_{\psi}\chi$ is consistent. By the
assumptions on $\mathcal{A}(\Sigma_{\mathsf{Ag}})$, and because
$a\in{\llbracket\psi\rrbracket_{\mathcal{A}}}$, we have
$\vdash\widehat{}a\rightarrow\psi$. Using $(\mathit{AM})$, we obtain $\vdash
C_{\psi}C_{\psi}\chi\rightarrow C_{\widehat{a}}C_{\psi}\chi$, and hence
$\vdash\neg C_{\widehat{a}}C_{\psi}\chi\rightarrow\neg C_{\psi}C_{\psi}\chi$.
Thus, $\widehat{\Gamma}\land\neg C_{\psi}C_{\psi}\chi$ is consistent; by (the
contraposition of) $(4)$, it follows that $\widehat{\Gamma}\land\neg
C_{\psi}\chi$ is consistent, in contradiction to $C_{\psi}\chi\in\Gamma$.

_‘If’:_ By contraposition. Suppose that $C_{\psi}\chi\notin\Gamma$, so $\neg
C_{\psi}\chi\in\Gamma$. We need to show that
$\mathcal{C}_{\Sigma},\Gamma\not\models C_{\psi}\chi$. By Lemma 12, we have
$\Gamma\sim^{p}_{\psi}\Delta$ for some $\Delta$ such that $\neg\chi\in\Delta$,
i.e. $\chi\notin\Delta$. By Lemma Completeness and Bounded Models,
$\Gamma\sim_{{\llbracket\psi\rrbracket_{\mathcal{A}}}}\Delta$, and by the
inductive hypothesis, $\mathcal{C}_{\Sigma},\Delta\not\models\chi$, showing
the claim.

Completeness and the bounded model property are then immediate:
[end]corollary[Completeness over finite models] Suppose that
${\mathcal{L}_{\mathsf{Ag}}}$ has the filtered model property and is
completely axiomatized. Then $C5$, together with the axiomatization of
${\mathcal{L}_{\mathsf{Ag}}}$, is weakly complete, i.e. every valid AGEL
formula is derivable. Moreover, AGEL has the _bounded model property_ : if a
formula $\rho_{0}$ is satisfiable, then $\rho_{0}$ has a finite model with at
most doubly exponentially many worlds in the size of $\rho_{0}$. By
contraposition: Let $\rho_{0}$ a formula such that $C5\not\vdash\rho_{0}$,
then $\neg\rho_{0}$ is consistent with $C5$. Let $\Sigma$ be the closure of
$\rho_{0}$ as in Definition 11. Then, there is a world $\Gamma\in X_{\Sigma}$
in the canonical model $\mathcal{C}_{\Sigma}$ such that
$\neg\rho_{0}\in\Gamma$ (since in the finite ordered set of consistent subsets
of $\Sigma$, every element is below a maximal one). By Lemma Completeness and
Bounded Models, ${\mathcal{C}_{\Sigma},\Gamma\models\neg\rho_{0}}$.

## Conclusions

We have introduced _ abstract-group epistemic logic (AGEL)_, a logic for
reasoning about the common knowledge of groups of agents that are described
abstractly via defining properties. We have established ExpTime-completeness,
a bounded model property, and (necessarily weak) completeness of a natural
axiomatization. The ExpTime upper bound holds in spite of the fact that the
expected encoding into standard group epistemic logic (with a common knowledge
operator for enumerated groups of agents) incurs exponential blowup, and
relies instead on a satisfiability-preserving translation into the
$\mu$-calculus with converse. Key directions for future research concern in
particular extensions of the logic by a distributed knowledge operator; by
dynamic epistemic modalities such as public announcements; by expressive means
for describing groups of agents via their individual knowledge; and by
allowing non-rigid agent names and agent atoms to capture knowledge about
agents.

## Acknowledgements

This work was supported by DFG (German Research Foundation) as part of the
Research Training Group 2475 “Cybercrime and Forensic Computing” (grant number
393541319/GRK2475/1-2019) and by DFG project “RAND: Reconstructing Arguments
from Newsworthy Debates” (grant number 377333057). The authors also wish to
thank the anonymous reviewers for their suggestions and feedback.

## References

  * Baader et al. (2003) Baader, F.; Calvanese, D.; McGuinness, D.; Nardi, D.; and Patel-Schneider, P., eds. 2003.  _The Description Logic Handbook_.  Cambridge University Press.  ISBN 0-521-78176-0.
  * Baltag, Moss, and Solecki (1998) Baltag, A.; Moss, L. S.; and Solecki, S. 1998.  The Logic of Public Announcements and Common Knowledge and Private Suspicions.  In Gilboa, I., ed., _Theoretical Aspects of Rationality and Knowledge, TARK-1998_ , 43–56. Morgan Kaufmann.
  * Bílková, Christoff, and Roy (2021) Bílková, M.; Christoff, Z.; and Roy, O. 2021.  Revisiting Epistemic Logic with Names.  In _Theoretical Aspects of Rationality and Knowledge, TARK 2021_ , volume 335 of _EPTCS_ , 39–54.
  * Blackburn, de Rijke, and Venema (2001) Blackburn, P.; de Rijke, M.; and Venema, Y. 2001.  _Modal Logic_.  Cambridge Tracts in Theoretical Computer Science. Cambridge University Press.
  * de Rijke (1993) de Rijke, M. 1993.  _Extending Modal Logic_.  Ph.D. thesis, Universiteit van Amsterdam Institute for Logic, Language and Computation.
  * Fagin et al. (1995) Fagin, R.; Halpern, J. Y.; Moses, Y.; and Vardi, M. Y. 1995.  _Reasoning About Knowledge_.  MIT Press.  ISBN 9780262562003.
  * Fischer and Ladner (1979) Fischer, M. J.; and Ladner, R. E. 1979.  Propositional Dynamic Logic of Regular Programs.  _J. Comput. Syst. Sci._ , 18(2): 194–211.
  * Fitting, Thalmann, and Voronkov (2001) Fitting, M.; Thalmann, L.; and Voronkov, A. 2001.  Term-Modal Logics.  _Stud Logica_ , 69(1): 133–169.
  * Grove (1995) Grove, A. J. 1995.  Naming and Identity in Epistemic Logic Part II: A First-Order Logic for Naming.  _Artif. Intell._ , 74(2): 311–350.
  * Grove and Halpern (1993) Grove, A. J.; and Halpern, J. Y. 1993.  Naming and Identity in Epistemic Logics Part I: The Propositional Case.  _J. Log. Comput._ , 3(4): 345–378.
  * Huth and Ryan (2004) Huth, M.; and Ryan, M. D. 2004.  _Logic in Computer Science - Modelling and Reasoning about Systems (2. ed.)_.  Cambridge University Press.  ISBN 9780511264016.
  * Lutz (2006) Lutz, C. 2006.  Complexity and succinctness of public announcement logic.  In _Autonomous Agents and Multiagent Systems, AAMAS 2006_ , 137–143. ACM.
  * Mares (2020) Mares, E. 2020.  Relevance Logic.  In _The Stanford Encyclopedia of Philosophy_. Metaphysics Research Lab, Stanford University, Winter 2020 edition.
  * Moses and Tuttle (1988) Moses, Y.; and Tuttle, M. 1988.  Programming Simultaneous Actions Using Common Knowledge.  _Algorithmica_ , 3: 121–169.
  * Naumov and Tao (2019) Naumov, P.; and Tao, J. 2019.  Everyone Knows that someone Knows: Quantifiers over Epistemic Agents.  _Rev. Symb. Log._ , 12(2): 255–270.
  * Padmanabha and Ramanujam (2019) Padmanabha, A.; and Ramanujam, R. 2019.  Two variable fragment of Term Modal Logic.  In _Mathematical Foundations of Computer Science, MFCS 2019_ , volume 138 of _LIPIcs_ , 30:1–30:14. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.
  * Pavlovic (2021) Pavlovic, D. 2021.  Probabilistic Annotations for Protocol Models.  In Dougherty, D.; Meseguer, J.; Mödersheim, S.; and Rowe, P., eds., _Protocols, Strands, and Logic_ , volume 13066 of _LNCS_ , 332–347. Springer.
  * Sattler and Vardi (2001) Sattler, U.; and Vardi, M. 2001.  The Hybrid $\mathrm{\mu}$-Calculus.  In _Automated Reasoning, IJCAR 2001_ , volume 2083 of _LNCS_ , 76–91. Springer.
  * Streett (1982) Streett, R. 1982.  Propositional Dynamic Logic of Looping and Converse Is Elementarily Decidable.  _Inf. Control._ , 54(1/2): 121–141.
  * Vardi (1998) Vardi, M. 1998.  Reasoning about The Past with Two-Way Automata.  In _Automata, Languages and Programming, ICALP 1998_ , volume 1443 of _LNCS_ , 628–641. Springer.
  * Venema (1996) Venema, Y. 1996.  A Crash Course in Arrow Logic.  In _Arrow Logic and Multi-Modal Logic_ , Studies in Logic, Language, and Information. European Association of Logic, Language and Information (FoLLI).  ISBN 9781575869858.

##  Appendix A Details and Full Proofs

We give details and full proofs where these have been omitted in the main body
of the paper; for the convenience of the reader, we restate the relevant
claims. When discussing AGEL models, we use the following additional
terminology: When $x\sim_{a}y$ and ${\mathcal{A},a\models\psi}$, we call $y$ a
_$\psi$ -successor of $x$_.

  *[AGEL]: abstract-group epistemic logic
  *[ AGEL]: abstract-group epistemic logic
  *[GEL]: group epistemic logic
  *[PDL]: propositional dynamic logic