# Semi-simplicial Set Models for Distributed Knowledge

Éric Goubault1, Roman Kniazev12, Jérémy Ledent3, Sergio Rajsbaum4
1 LIX, CNRS, École Polytechnique, IP-Paris, Palaiseau Cedex, France  2
Université Paris-Saclay, ENS Paris-Saclay, CNRS, LMF, Gif-sur-Yvette, France
3 MSP Group, University of Strathclyde, Glasgow, Scotland  4 Universidad
Nacional Autónoma de México (UNAM), Mexico D.F., Mexico and IRIF, Paris,
France

###### Abstract

In recent years, a new class of models for multi-agent epistemic logic has
emerged, based on simplicial complexes. Since then, many variants of these
simplicial models have been investigated, giving rise to different logics and
axiomatizations. In this paper, we present a further generalization, which
encompasses all previously studied variants of simplicial models.
Geometrically, this is achieved by generalizing beyond simplicial complexes,
and considering instead semi-simplicial sets. By doing so, we define a new
semantics for epistemic logic with distributed knowledge, where a group of
agents may distinguish two worlds, even though each individual agent in the
group is unable to distinguish them. As it turns out, these models are the
geometric counterpart of a generalization of Kripke models, called “pseudo-
models”. We show how to recover the previously defined variants of simplicial
models as sub-classes of our models; and give a sound and complete
axiomatization for each of them††Eric Goubault was partially funded by
AID/CIEDS project FARO. Part of the work of Sergio Rajbaum was performed while
he was an invited professor at IRIF, Université Paris Cité, and at LIX, Ecole
Polytechnique..

###### Index Terms:

Epistemic logic, Simplicial sets, Distributed knowledge

††publicationid: pubid: 979-8-3503-3587-3/23/$31.00 ©2023 IEEE

##  I Introduction

The usual semantics for multi-agent epistemic logic is based on the classic
Kripke _possible worlds_ relational structure [1]. However, the intimate
relationship between distributed computing and algebraic topology [2] showed
the importance of moving from the focus on global states represented by
worlds, to local states, representing perspectives about possible worlds.
Namely, moving from graph structures to simplicial complex structures. A
formal semantics of multi-agent epistemic formulas in terms of simplicial
models was presented [3], and shown to be equivalent to the usual Kripke model
semantics for $\mathbf{S5_{n}}$. Further work explored bisimilarity of
simplicial models [4] and connections with covering spaces [5]. Remarkably, it
has been shown by Yagi and Nishimura [6, 7] that the implicit topological
information in Kripke models, exposed by the simplicial complex point of view,
can be leveraged to produce a logical obstruction to the solvability of
certain distributed computing problems. The notion of _distributed knowledge_
[8] plays a crucial role there: in a sense, it is a higher-dimensional notion
of knowledge.

These first results assumed a finite, fixed set of agents, whose local states
appear in every world. As a consequence, since a world with $n+1$ agents is
represented by a $n$-dimensional simplex, every facet of the simplicial model
is of the same dimension. Such models are called _pure_ simplicial models.
However, in distributed systems, processes may fail, and it may happen that
only a subset of the agents remain in some worlds. To model such situations,
the categorical equivalence of [3] was extended by various authors to include
simplicial models that may not be pure [9, 10, 11]. These situations have been
thoroughly studied since early on in distributed computability, e.g. the
seminal work of Dwork and Moses [12], where a complete characterization of the
number of rounds required to reach simultaneous consensus was given in terms
of common knowledge. By moving away from pure simplicial models, we also move
away from the standard $\mathbf{S5_{n}}$ epistemic logic. Indeed, there are a
number of design choices to be made, both to define the models and their
semantics. Should all simplices represent worlds, or only the facets? Can we
have a world with no agents? How do we deal with formulas involving the
knowledge of agents that are not present in the current world? All these
choices can greatly influence the resulting logic: while [9] drops Axiom T and
works with the logic $\mathbf{KB4_{n}}$ (augmented with some extra axioms),
other authors [11] take a completely different route and define a three-valued
logic (where formulas may be undefined), with an axiom system called
$\textbf{S5}^{\bowtie}$.

In this paper, we aim to bring order to chaos by defining a class of
simplicial models that encompasses all previous variants. Thus, the main
objective of our paper is to unify previous work on simplicial complex models.
For that purpose, we introduce a new class of models called _epistemic
covering models_. As we will see in Section IV-B, the models studied in [3, 9,
10, 15] can all be viewed as sub-classes of epistemic covering models. This
allows us to recover important theoretical results about each of those sub-
classes, by proving them once and for all in our very general setting. Namely,
our paper contains two central results: (i) Theorem 1 shows an equivalence of
categories between epistemic covering models and their Kripke-style
counterpart, called _generalized epistemic models_. Crucially, we also show
(Lemma 3) that this equivalence can safely be restricted to sub-classes of
epistemic covering models; allowing us to recover similar equivalence results
from [3, 9, 10]. (ii) The other essential result of our paper is a sound and
complete axiomatization of epistemic covering models (Corollary 2). Once
again, we are also interested in axiomatizing the various sub-classes of
epistemic covering models, which we do in Section V-C. We show that there is a
close correspondence between structural properties that define a sub-class,
and axioms of the corresponding logic. These results are summed up in Fig. 1
below. The first two columns indicate the correspondence between properties of
epistemic coverings, and axioms of the logic (they will be defined in Sections
IV and V, respectively). The check marks in the other columns indicate how to
recover previously-studied variants of simplicial models. One can check that
the axiomatization provided here matches the one given in each of those papers
(except for [10], which studies a different three-valued semantics).

Covering properties | Axioms | [3] | [9] | [10] | [15]
---|---|---|---|---|---
Proper | ($\mathbf{P}$) | ✓ | ✓ | ✓ | ✓
Pure | ($\mathbf{T}$) | ✓ |  |  | ✓
Minimal | ($\mathbf{Min}$) | ✓ | ✓ |  | ✓
Maximal | ($\mathbf{Max}$) |  |  | ✓ |
No empty world | ($\mathbf{NE}$) | ✓ | ✓ | ✓ | ✓
Simplicial complex | no axiom | ✓ | ✓ | ✓ |
Figure 1:  Sub-classes of epistemic covering models that have been studied in
previous papers, and their associated axioms.

One distinguishing feature of our models, which has not been considered
previously in the literature, is that we generalize beyond simplicial
complexes and consider instead semi-simplicial sets. Geometrically, this means
that simplices (a.k.a. worlds) can be connected in more complex ways; for
instance, two triangles might share two vertices but not the edge between
those vertices (see Fig. 2, which is not a simplicial complex). This new
feature enables us to model situations where a group of agents may distinguish
two worlds, even though each individual agent in the group is unable to
distinguish them.

A toy example of such a situation, in the realm of distributed computing is
the following. Suppose we have three sensors, $s_{1}$, $s_{2}$ and $s_{3}$, in
a sensor network, with overlapping visibility regions of the form of a unit
disk, that can only count the number of targets within their visibility
region. Suppose now that each of these three sensors detects exactly one
target, indicated by a “$\times$” below. There are 5 possible configurations
$w_{1}$, $w_{2}$, $\ldots$, $w_{5}$ (from left to right below), with the total
number of targets, ranging from 1 to 3:

$s_{1}$$s_{2}$$s_{3}$$\times$

$s_{1}$$s_{2}$$s_{3}$$\times$$\times$

$s_{1}$$s_{2}$$s_{3}$$\times$$\times$

$s_{1}$$s_{2}$$s_{3}$$\times$$\times$

$s_{1}$$s_{2}$$s_{3}$$\times$$\times$$\times$

Alone, no sensor can distinguish between these 5 situations. To disambiguate
between configurations, we must indeed use an inclusion-exclusion principle,
so we need to identify if the same target has been detected by different
sensors. For this, we suppose that, jointly, groups of sensors can determine
if a target they saw was seen by all in that group. In this example, $s_{1}$
and $s_{2}$ together can for instance distinguish the worlds $w_{1}$ and
$w_{2}$, but not $w_{1}$ and $w_{4}$. Only the three sensors together can
distinguish between all five worlds. The framework we propose in this paper
allows to formalize such applications.

We show the very important, and surprising fact that every semi-simplicial set
model is bisimilar to a simplicial complex model (leading to Theorem 6). There
are several reasons why, despite this fact, we still believe that semi-
simplicial set models are worth studying. Indeed, some epistemic situations
are described much more naturally and concisely using a semi-simplicial set
model. This is for instance the case of the sensor model described previously.
By turning it into a bisimilar simplicial complex model, we create a tree-like
model with an infinite number of worlds, and where the underlying topology has
disappeared. For some applications (e.g. model-checking), it might be crucial
to keep a model which is as small as possible, let alone infinite. This
situation is akin to classical topology: semi-simplicial sets and simplicial
complexes describe the same spaces up to weak-homotopy. Yet, both structures
are used in algebraic topology in their own right, according to the situation
at hand. For some spaces, e.g. when dealing with the classification of
combinatorial structures (posets, graphs, etc.), the simplicial complex
approach is indeed very practical. However, in other situations (e.g. for non-
triangulable spaces), the semi-simplicial set approach is much more convenient
to use.

##### Plan of the paper

In Section II, we recall various mathematical notions that we will be using in
this paper. In Section III, we define our two notions of models, generalized
epistemic models and epistemic covering models; and prove that they are
equivalent. We define various interesting sub-classes of these models in
Section IV. In Section V, we prove that $\mathbf{EC_{n}}$ is sound and
complete with respect to these models (Theorem 2), and give sound and complete
axiomatizations of interesting sub-classes (Theorems 3, 4, and 5). Finally, we
prove that every simplicial set model is bisimulation equivalent to a
simplicial complex model, bringing interesting questions about the topological
nature of bisimulation (Theorem 6).

##  II Preliminaries

###  II-A Kripke semantics of distributed knowledge

Let $A$ be a finite set of agents, and $\mathsf{At}$ a countable set of atomic
propositions. We consider the language $\mathcal{L}_{D}$ of epistemic logic
with _distributed knowledge_ [1], generated by the following BNF grammar:

$\varphi::=p\mid\neg\varphi\mid\varphi\land\varphi\mid D_{U}\,\varphi\qquad
p\in\mathsf{At},\ U\subseteq A$

The derived operators $\lor,\Rightarrow,\mathsf{true},\mathsf{false}$, are
defined as usual in propositional logic. We also use the following operators:
K_a φ:= D_{a} φ^D_Uφ:= ¬D_U¬φ The operator $D_{U}\varphi$ is read “the group
of agents $U$ (collectively) knows $\varphi$”, while its dual
$\widehat{D}_{U}\varphi$ means that the group $U$ considers possible the
formula $\varphi$. $K_{a}\,\varphi$ is the standard knowledge operator of
epistemic logic, “agent $a$ knows $\varphi$”.

######  Definition 1.

A Kripke model is a structure $\mathcal{M}={\langle M,(\sim_{a})_{a\in
A},L\rangle}$, where:

  * •

$M$ is a set of _possible worlds_ ,

  * •

For every agent $a\in A$, $\sim_{a}$ is an equivalence relation,

  * •

$L:M\to\mathscr{P}(\mathsf{At})$ is a valuation function.

Given a Kripke model, the satisfaction relation $M,w\models\varphi$ is defined
inductively as follows. We write $\sim_{U}\;=\;\bigcap_{a\in U}\sim_{a}$.

$\begin{array}[]{lcl}M,w\models p&\text{iff}&p\in L(w)\\\
M,w\models\neg\varphi&\text{iff}&M,w\not\models\varphi\\\
M,w\models\varphi\land\psi&\text{iff}&M,w\models\varphi\text{ and
}M,w\models\psi\\\ M,w\models
D_{U}\,\varphi&\text{iff}&M,w^{\prime}\models\varphi\text{ for all
}w^{\prime}\in M\\\ &&\text{ such that }w\sim_{U}w^{\prime}\end{array}$

###  II-B Partial Equivalence Relations

######  Definition 2.

A _Partial Equivalence Relation_ (PER) on a set $X$ is a relation ${R\subseteq
X\times X}$ which is symmetric and transitive (but not necessarily reflexive).

The _domain_ of a PER $R$ is the set $\mathsf{dom}(R)=\\{x\in X\mid
R(x,x)\\}\subseteq X$, and it is easy to see that $R$ is an equivalence
relation on its domain, and empty outside of it. Thus, a PER on $X$ is simply
an equivalence relation on a subset of $X$. The _equivalence classes_ of a PER
$R$ are defined as usual, when viewed as an equivalence relation on
$\mathsf{dom}(R)$: for $x\in\mathsf{dom}(R)$, we write $[x]_{R}=\\{y\in X\mid
xRy\\}$ for the equivalence class of $x$, and $X/R$ for the set of equivalence
classes.

###  II-C Semi-simplicial sets

(Semi)-simplicial sets can be viewed as a higher-dimensional generalization of
directed multigraphs, while simplicial complexes are a generalization of
simple graphs. Thus, in dimension $1$, simplicial sets allow loops and
parallel edges; whereas simplicial complexes do not. Similarly, in higher
dimensions, simplicial sets allow simplices to be assembled together in more
complex ways, as in Fig. 2. Standard references for the theory of simplicial
sets and some of their many uses in algebraic topology are [17, 18] and a more
elementary introduction can be found in [19].

Figure 2: A simplicial set which is not a simplicial complex.

Compared to simplicial complexes, simplicial sets exhibit interesting
geometric and categorical features:

  * •

In algebraic topology, they provide a combinatorial model for the homotopy
theory of topological spaces, in fact they are Quillen equivalent to the
standard Quillen model category of topological spaces [17].

  * •

As a presheaf category, simplicial sets form a Grothendieck topos. Still,
simplicial complexes are almost as nice, they are known as forming a
quasitopos, see e.g. [20] for a discussion of the relationship between the
quasitopos of simplicial complexes and the topos of simplicial sets.

Let $\Delta^{+}_{\mathsf{inj}}$ be the category of possibly empty linear
orders with injective maps between them. We write $[n]$ for the
$(n+1)$-element linear order $[n]=\\{0<\ldots<n\\}$, and $[-1]=\varnothing$.
The category of _augmented semi-simplicial sets_ is defined as the presheaf
category $\widehat{\Delta}^{+}_{\mathsf{inj}}$. Thus, its objects are functors
$F:(\Delta^{+}_{\mathsf{inj}})^{\mathsf{op}}\rightarrow\bf Set$, and morphisms
are natural transformations. The elements of $F([n])$ are called
$n$-simplices, and we use the terms vertices, edges, and triangles for
simplices of dimension $0$, $1$ and $2$ respectively.

For example, the simplicial set depicted in Fig. 2 has $4$ vertices, $6$ edges
and $2$ triangles. So, accordingly, the sets $F([0])$, $F([1])$ and $F([2])$
are chosen to have $4$, $6$ and $2$ elements, respectively. There are three
face maps $\partial_{i}:F([2])\to F([1])$ for $i=0,1,2$ which assign to each
triangle its three boundary edges. The maps $\partial_{i}:F([1])\to F([0])$
for $i=0,1$ assign to each edge its source and target vertices.

##  III Generalized epistemic frames and epistemic coverings

In this section, we define two classes of models for distributed knowledge:
one generalizes Kripke frames, and the other generalizes simplicial models. We
show that they are structurally equivalent. In the following sections, we will
show that they subsume previous models found in the literature, and study
their axiomatization.

###  III-A Generalized epistemic frames

As in [9] we will consider Kripke frames where the accessibility relation
$\sim$ is not an equivalence relation but just a partial equivalence relation.
But we generalize one step further by associating an accessibility relation
not only for each agent, but also for any set of agents, making it possible to
interpret distributed knowledge in a very general manner. Such models have
been considered before in the epistemic logic literature, sometimes called
“pseudo-models”, as an intermediate tool in completeness proofs involving
distributed knowledge [13, 14]. One paper that used such models as the main
object of study is [15], in order to model observability in quantum systems.
Still, the models that we present here generalize further, by allowing worlds
where not all agents are necessarily present, and as a consequence condition
(b) below is new.

######  Definition 3.

A _generalized epistemic frame_ is a structure $\mathcal{M}=\langle
M,\sim\rangle$, where:

  * •

$M=\\{w_{0},w_{1},\ldots\\}$ is a set of _possible worlds_ ,

  * •

$\sim$ is a function assigning for every group of agents $U\subseteq A$, a PER
${\sim_{U}\;\subseteq M\times M}$ called the _$U$ -accessibility relation_. We
write $[w]_{U}$ for the equivalence class of $w$ with respect to $\sim_{U}$.

  * •

The PERs $\sim_{U}$ satisfy the following conditions.

    1. (a)

Compatibility:

$\displaystyle\forall U^{\prime}\subseteq U,\ $ $\displaystyle
w\sim_{U}w^{\prime}\Rightarrow w\sim_{U^{\prime}}w^{\prime}$

    2. (b)

Closure under union of the groups of alive agents:

$\displaystyle\forall U,U^{\prime}\subseteq A,\ $
$\displaystyle(w\sim_{U}w\land w\sim_{U^{\prime}}w)\Rightarrow w\sim_{U\cup
U^{\prime}}w.$

The two conditions on $\sim_{U}$ can be interpreted as follows. Condition (a)
means that if a group of agents cannot distinguish between two worlds, all
together, then there is no way a subgroup of agents can distinguish the same
two worlds. Condition (b) implies that in each world $w$, there is a maximal
group of agents $U$ such that $w\sim_{U}w$. We call such a $U$ the group of
_alive agents_ in world $w$, and denote it by $\overline{w}$. We say that an
agent $a$ is _alive_ in $w$ when $a\in\overline{w}$ or, equivalently, when
$w\sim_{\\{a\\}}w$.

Usually, we write $w\sim_{a}w^{\prime}$ as shorthand for
$w\sim_{\\{a\\}}w^{\prime}$. Additionally, we say that a world $w$ is a _sub-
world_ of $w^{\prime}$ when $\overline{w}\subseteq\overline{w^{\prime}}$ and
$w\sim_{\overline{w}}w^{\prime}$. The sub-world relation is a preorder, and is
denoted by $w\leq w^{\prime}$.

######  Example 1.

An example of a generalized epistemic frame is given on Figure 3. It has seven
worlds $M=\\{w_{0},\ldots,w_{5}\\}\cup\\{w_{1}^{\prime}\\}$. Not all relations
are shown, but only the generating ones. Sets of alive agents can be read off
directly on the reflexive loops above a world; in $w_{5}$, no agent is alive,
that is $w_{5}\not\sim_{a}w_{5}$ for all $a\in A$. The empty group can
distinguish $w_{5}$ from other worlds:
$w_{5}\not\sim_{\varnothing}w_{i},i\not=5$. In world $w_{4}$, agents $a$ and
$c$ are alive, and they can distinguish it from all other worlds, but the
empty group cannot. In $w_{2}$ and $w_{3}$ all three agents are alive. Agents
$b$ and $c$ cannot individually distinguish $w_{2}$ from $w_{3}$, however,
together they can: we have $w_{2}\sim_{b}w_{3}$ and $w_{2}\sim_{c}w_{3}$, but
$w_{2}\not\sim_{\\{b,c\\}}w_{3}$. In $w_{1}$ and $w^{\prime}_{1}$, agents $a$
and $b$ are alive, but even together they cannot distinguish them, as we have
$w_{1}\sim_{\\{a,b\\}}w^{\prime}_{1}$. World $w_{0}$ is a sub-world of both
$w_{1}$ and $w^{\prime}_{1}$: only $b$ is alive in $w_{0}$ and it cannot
distinguish $w_{0}$ from $w_{1}$ or $w^{\prime}_{1}$.

$w_{2}$$\\{a,b,c\\}$$w_{3}$$b$$\\{a,b,c\\}$$c$$w_{1}$$w_{4}$$w_{5}$$w^{\prime}_{1}$$w_{0}$$\\{a,b\\}$$\\{a,b\\}$$b$$b$$b$$\\{a,b\\}$$\varnothing$$\\{a,c\\}$$a$$a$
Figure 3: An example of a generalized epistemic frame.

######  Example 2.

In the example of the introduction, $w_{1}$, $\ldots$, $w_{5}$ are worlds,
$s_{1}$, $s_{2}$, $s_{3}$ are agents, representing the sensors. For all
$i,j,k$, we have $w_{i}\sim_{s_{j}}w_{k}$: no individual sensor $s_{j}$ can
distinguish between any pair of worlds $w_{i}$ and $w_{k}$. We also have
$w_{1}\sim_{\\{s_{2},s_{3}\\}}w_{2}$ since in these two worlds, $s_{2}$ and
$s_{3}$ jointly see the same target. More generally,
$w_{1}\sim_{\\{s_{i},s_{j}\\}}w_{k}$ if and only if some target is in
$A_{i}\cap A_{j}$ in world $w_{k}$. But the three sensors together can
distinguish $w_{1}$ from all other worlds. Examining all other intersections
in pairs of worlds gives the epistemic frame on Figure 4.

$w_{2}$$\\{a,b,c\\}$$w_{3}$$b$$\\{a,b,c\\}$$c$$w_{1}$$w_{4}$$w_{5}$$w^{\prime}_{1}$$w_{0}$$\\{a,b\\}$$\\{a,b\\}$$b$$b$$b$$\\{a,b\\}$$\varnothing$$\\{a,c\\}$$a$$a$$w_{1}$$w_{2}$$w_{3}$$w_{5}$$w_{4}$$\\{1,2,3\\}$$1,\\{2,3\\}$$\\{1,2,3\\}$$\\{1,2\\},3$$\\{1,2,3\\}$$1,\\{2,3\\}$$\\{1,2,3\\}$$\\{1,3\\},\\{2,3\\}$$\\{1,2,3\\}$$1,2,3$$\\{1,2\\},\\{1,3\\}$$2,\\{1,3\\}$$\\{1,2\\},\\{2,3\\}$$\\{1,2\\},3$$2,\\{1,3\\}$
Figure 4: Sensor network as an epistemic frame.

Morphisms between epistemic frames are structure-preserving functions between
the sets of worlds.

######  Definition 4.

Let $\mathcal{M}=\langle M,\sim\rangle$ and $\mathcal{N}=\langle
N,\sim^{\prime}\rangle$ be two generalized epistemic frames. A morphism from
$\mathcal{M}$ to $\mathcal{N}$ is a function $f:M\rightarrow N$ such that for
all $U\subseteq A$, for all $u,v\in M$, $u\sim_{U}v$ implies
$f(u)\sim^{\prime}_{U}f(v)$,

We write $\mathbf{GEF}_{A}$ for the category of generalized epistemic frames
with agents $A$. Later, in order to define the semantics of $\mathcal{L}_{D}$
formulas, we will equip these frames with a valuation function, as in Section
II-A. But first, let us first define the geometric counterpart of these
frames: epistemic coverings.

###  III-B Epistemic coverings

####  III-B1 Chromatic augmented semi-simplicial sets

As in the case of simplicial models [3], our first step will be to decorate
the vertices of a simplicial set with colors, representing the names of the
agents in $A$. The resulting structure is called a _chromatic_ augmented semi-
simplicial set, or _cset_ for short. We identify $A$ with the linear order
$[n]=\\{0<\ldots<n\\}$.

Let $S_{A}$ denote the _standard $(|A|-1)$-simplex_, defined by:

  * •

$(S_{A})_{k}=\\{({i_{0}},\ldots,{i_{k}})\mid 0\leq i_{0}<\ldots<i_{k}\leq
n\\}$,

  * •

$\partial_{j}({i_{0}},\ldots,{i_{k}})=(i_{0},\ldots,{i_{j-1}},{i_{j+1}},\ldots,i_{k})\in(S_{A})_{k-1}$.

Given an augmented semi-simplicial set $X$, a coloring of $X$ by the agents in
$A$ is simply a map $f:X\to S_{A}$. Note that, since we work with _semi_
-simplicial sets here, without degeneracy maps, morphisms preserve the
dimension of simplices. Thus, each simplex of $X$ is well-colored, in the
sense that all vertices in a simplex are labelled with distinct agents. We
then define the category of chromatic augmented semi-simplicial sets to be the
slice category $\widehat{\Delta}^{+}_{\mathsf{inj}}/S_{A}$.

For the rest of the paper, we can either see this category as a slice
category, or notice that, by the fundamental theorem of topos theory, the
category of csets is once again a presheaf category on a site $\Gamma$ made of
simplices of the standard $n$-simplex. As with the site of semi-simplicial
sets (see e.g., [21, 22]), $\Gamma$ is the posetal category of subsets of $A$
with the inclusion partial order, defined below.

######  Definition 5.

The category $\Gamma$ is such that:

  * •

Objects are (possibly empty) subsets of $A$.

  * •

There is a unique morphism $\delta_{U,V}:U\to V$ in $\Gamma$ whenever
${U\subseteq V}$. Composition $\delta_{V,W}\circ\delta_{U,V}=\delta_{U,W}$ is
given by the fact that ${U\subseteq V\subseteq W}$ implies $U\subseteq W$.

We write $\mathbf{Cset}_{A}$ for the presheaf category on $\Gamma$. This
category is equivalent to $\widehat{\Delta}^{+}_{\mathsf{inj}}/S_{A}$, hence a
cset can equivalently be viewed as a functor $F:\Gamma^{\mathsf{op}}\to\bf
Set$. Given a cset $F\in\mathbf{Cset}_{A}$, and a group of agents $U\subseteq
A$, the elements of $F(U)$ are called the _$U$ -simplices_. When there is no
ambiguity, we write $\partial_{U,V}:F(V)\to F(U)$ for the boundary operator
$F(\delta_{U,V})$. For $x$ a $V$-simplex, $\partial_{U,V}(x)$ is called the
$U$-face of $x$. If it is clear which $V$ is considered, we simply write
$\partial_{U}(x)$.

Given $U\subseteq A$, the standard $U$-simplex $\Gamma[U]$, is defined as the
representable presheaf $\Gamma(-,U)$, image of $U$ by the Yoneda embedding
$y:\Gamma\to\mathbf{Cset}_{A}$.

######  Example 3.

A cset $X$ is depicted in the figure below. We represent it as a simplicial
set together with colors on the vertices. Elements of $X_{-1}$ are depicted as
dashed regions (and interpreted as generalized connected components). Elements
of $X_{0}$ are depicted as vertices, $X_{1}$ as edges, $X_{2}$ as triangles,
etc. The boundary operators $\partial_{i}$ give the equations that permit to
glue these simplices together, along lower dimensional simplices. The cset in
the picture below is composed of seven vertices (colored with three agents),
eight edges, two triangles, and two $(-1)$-simplices (the annotations will
only be used later).

$w_{2}$$\\{a,b,c\\}$$w_{3}$$b$$\\{a,b,c\\}$$c$$w_{1}$$w_{4}$$w_{5}$$w^{\prime}_{1}$$w_{0}$$\\{a,b\\}$$\\{a,b\\}$$b$$b$$b$$\\{a,b\\}$$\varnothing$$\\{a,c\\}$$a$$a$$w_{2}$$w_{3}$$w_{0}$$w_{4}$$w_{1},w^{\prime}_{1}$$w_{5}$

In the rest of the paper, by a _(chromatic) simplicial complex_ we mean a cset
in which if two simplices share the same set of vertices, then they coincide.
More formally, if for two $U$-simplices $s,s^{\prime}$
$\partial_{a}(s)=\partial_{a}(s^{\prime})$ for all $a\in U$, then
$s=s^{\prime}$.

####  III-B2 Epistemic coverings

In previous papers about simplicial models for epistemic logic, two issues
have arisen:

  1. (i)

We need a way to describe which simplices of the model represent actual
worlds, and which ones do not. Two canonical choices are possible: take all
simplices as worlds, or take only the facets. But one may also want to
consider something in-between.

  2. (ii)

Simplicial models usually correspond to _proper_ Kripke models, because each
individual simplex can represent only a single world.

In this section, we solve both issues by introducing a new notion called
_epistemic coverings_.

The idea is that, lying above the simplicial set $B$ representing the geometry
of the model, we have a projective simplicial set $E$ representing the worlds.
A morphism $f:E\to B$ then maps each world to its representation in the
geometric model. This allows us to (i) freely assign worlds to the simplices
of the model, and (ii) possibly assign several worlds to the same simplex.

In a cset $X$, given a $V$-simplex $t$ and a subset $U\subseteq V$, we say
that $s=\partial_{U}(t)$ is a _subsimplex_ of $t$. We say that $X$ is
_projective_ when for every simplex $s\in X$, there is a unique maximal
simplex $\uparrow\\!s$, such that $s$ is a subsimplex of $\uparrow\\!s$.

######  Definition 6.

An _epistemic covering_ is a morphism $f:E\to B$ in $\mathbf{Cset}_{A}$ such
that $E$ is projective and $f:E\to B$ is surjective. Equivalently, a morphism
$f:E\to B$ is an epistemic covering if $E$ is projective and every maximal
simplex of $B$ has a preimage. We refer to $E$ as _top cset_ and to $B$ as
_base cset_.

Epistemic coverings form a category where morphisms from $f:E\to B$ to
$f^{\prime}:E^{\prime}\to B^{\prime}$ are pairs of morphisms $\alpha_{E}:E\to
E^{\prime},\alpha_{B}:B\to B^{\prime}$, such that the following square
commutes:

$w_{2}$$\\{a,b,c\\}$$w_{3}$$b$$\\{a,b,c\\}$$c$$w_{1}$$w_{4}$$w_{5}$$w^{\prime}_{1}$$w_{0}$$\\{a,b\\}$$\\{a,b\\}$$b$$b$$b$$\\{a,b\\}$$\varnothing$$\\{a,c\\}$$a$$a$$w_{2}$$w_{3}$$w_{0}$$w_{4}$$w_{1},w^{\prime}_{1}$$w_{5}$${E}$${{E^{\prime}}}$${B}$${{B^{\prime}}}$$\scriptstyle{\alpha_{B}}$$\scriptstyle{f}$$\scriptstyle{f^{\prime}}$$\scriptstyle{\alpha_{E}}$

We write this category $\mathbf{eCov}_{A}$. One can see that
$\mathbf{eCov}_{A}$ is a full subcategory of the arrow category of
$\mathbf{Cset}_{A}$.

An epistemic covering $f\\!:\\!E\to B$ can be visually represented as an
annotated cset by taking the base cset $B$ and writing on a simplex $s$ the
set of maximal simplices from $E$ that are mapped on $s$. In particular, as
$f$ is surjective, every maximal simplex in $B$ must have an annotation. For
instance, the annotation on the example of a cset from Example 3 represents an
epistemic covering with the following maximal simplices in $E$: two
$2$-simplices $w_{2},w_{3}$; three $1$-simplices $w_{1},w^{\prime}_{1},w_{4}$
with $f(w_{1})=f(w^{\prime}_{1})$; one $0$-simplex $w_{0}$; one $-1$-simplex
$w_{5}$.

######  Remark 1.

There are two ways to canonically produce an epistemic covering out of a given
cset $X$. We can take $X$ as the base of the covering, but we need to choose
the space $E$. Choosing $E$ amounts to deciding which simplices of $X$
constitute the possible worlds. There are two natural choices: either take all
of the simplices of $X$, or take only the maximal ones (a.k.a. the facets).

The first choice, that we call the “maximal” one, where $E$ is the disjoint
union of all the simplices of $X$, yields a faithful functor from
$\mathbf{Cset}_{A}$ to $\mathbf{eCov}_{A}$. A morphism $g:X\to Y$ is sent to
the morphism of coverings $\langle\alpha_{E},\alpha_{B}\rangle$, where
$\alpha_{B}=g$ and $\alpha_{E}$ sends a simplex $s$ to $t$ if $g$ sends $s$ to
$t$. This functor is injective on objects, so it makes $\mathbf{Cset}_{A}$ a
subcategory of $\mathbf{eCov}_{A}$, though not full. The maximal
interpretation appears (implicitly) in [11] for example, where a formula can
be evaluated in every simplex of a model.

The second choice, where $E$ is the disjoint union of the maximal simplices of
$X$, is the “minimal” one. It is the one that is studied in [3, 9], where a
formula is only evaluated in a facet of a simplicial complex. However, this
construction is not functorial.

###  III-C Isomorphism between epistemic frames and coverings

We want to show that the category of epistemic coverings and the category of
generalized epistemic frames are isomorphic. We first define the functor
$\kappa:\mathbf{eCov}_{A}\to\mathbf{GEF}_{A}$.

Let $f:E\to B$ be an epistemic covering. As $E$ is projective, it can be
represented as a disjoint union of disconnected standard simplices, that is
$E=\bigcup_{U\subseteq A}\bigcup_{E_{U}}\Gamma[U]$, where $E_{U}$ are some
sets. Then the set $W$ of worlds in $\kappa(f)=\langle W,\sim\rangle$ is
exactly $\bigcup_{U\subseteq A}E_{U}$, that is every maximal simplex of $E$ is
interpreted as a world. To define the group indistinguishability relations
${\sim_{U}}$ between the worlds of the corresponding frame, we proceed as
follows. We think of two simplices in $E$ as $U$-indistinguishable, if their
images in $B$ share a $U$-face. Formally, given two worlds
$w_{s},w_{s^{\prime}}$ in $\kappa(f)$, corresponding to two maximal simplices
$s,s^{\prime}$ in $E$, we let $w_{s}\sim_{U}w_{s^{\prime}}$ if
$\partial_{U}(f(s))=\partial_{U}(f(s^{\prime}))$.

Now we define this functor on morphisms. Suppose we are given a morphism of
epistemic coverings $\langle\alpha_{E},\alpha_{B}\rangle$. Then, the morphism
of epistemic frames
$\kappa(\langle\alpha_{E},\alpha_{B}\rangle)\\!:\\!\kappa(f)\to\kappa(f^{\prime})$
sends a world $w_{s}$ to a world $w_{s^{\prime}}$ if the image of the maximal
simplex $s$ in $E$ is included in the maximal simplex $s^{\prime}$ in
$E^{\prime}$.

Next, we construct the inverse functor
$\sigma:\mathbf{GEF}_{A}\to\mathbf{eCov}_{A}$. Given a generalized frame
$\langle M,\sim\rangle$, we need to define two csets $E_{M}$ and $B_{M}$
together with a map $m:E_{M}\to B_{M}$. For every world $w\in M$ we associate
a simplex of type $\overline{w}$ to $E_{M}$, that is $E_{M}=\bigcup_{w\in
M}\Gamma[\overline{w}]$.

It is slightly more intricate to build the base space $B_{M}$ of the covering.
We construct it as a presheaf on $\Gamma$, $B_{M}:\Gamma^{\mathsf{op}}\to\bf
Set$. For every group $U\subseteq A$ of agents, define
$B_{M}(U)=M/_{\sim_{U}}$, the quotient of $M$ with respect to $\sim_{U}$. The
restriction $\partial_{U,V}:M/_{\sim_{V}}\to M/_{\sim_{U}}$ sends the
equivalence class $[w]_{V}$ to $[w]_{U}$. We need to verify that $B_{M}$ is
indeed a cset.

######  Lemma 1.

For any frame $\langle M,\sim\rangle$, $B_{M}$ is a cset.

###### Proof:

First, let us show that restriction maps are correctly defined. Consider
$\partial_{U,V}$ for $U\subseteq V$, and let $w^{\prime}\in[w]_{U}$ be another
representative of the equivalence class $[w]_{U}$. By monotonicity, we have
$w\sim_{V}w^{\prime}\Rightarrow w\sim_{U}w^{\prime}$, so they also belong to
the same equivalence class $[w]_{U}=[w^{\prime}]_{U}$. Thus, the function
$\partial_{U,V}$ is correctly defined. To see that this is functorial, given
sets of agents $U\subseteq V\subseteq W$, we need to prove that
$\partial_{U,V}\circ\partial_{V,W}=\partial_{U,W}$, which is straightforward.
∎

One can see that there is a canonical map ${m:E_{M}\to B_{M}}$ which sends a
maximal simplex $w$ of $E_{M}$, representing a world, to the corresponding
equivalence class $[w]_{\overline{w}}\in B_{M}(\overline{w})$. This describes
$\sigma$ on objects by setting $\sigma(\langle M,\sim\rangle)=m$.

To define $\sigma$ on morphisms, consider a morphism of epistemic frames
$g:\mathcal{M}\to\mathcal{N}$. As both assignments of total spaces
$E_{M},E_{N}$ and base spaces $B_{M},B_{N}$ are functorial one needs to check
that the induced square commutes.

######  Proposition 1.

The functors $\kappa$ and $\sigma$ define an isomorphism of categories:
$\kappa\circ\sigma=\mathsf{id}_{\mathbf{GEF}_{A}}$ and
$\sigma\circ\kappa=\mathsf{id}_{\mathbf{eCov}_{A}}$.

###### Proof:

Consider an epistemic frame $\mathcal{M}$. Then $\kappa\sigma(\mathcal{M})$
has as its worlds the same worlds as in $\mathcal{M}$, as $\kappa$ and
$\sigma$ just transfer this information. The relations $\sim_{U}$ are also
just the same: $w\sim_{U}w^{\prime}$ in $\kappa\sigma(\mathcal{M})$ iff the
simplices $\partial_{U}(w),\partial_{U}(w^{\prime})$ in
$E_{\sigma(\mathcal{M})}$ are sent to the same simplex in
$B_{\sigma(\mathcal{M})}$, but this is the case exactly when
$w\sim_{U}w^{\prime}$ in $\mathcal{M}$. The same line of argument works for
$\sigma\circ\kappa$, and extends to morphisms. ∎

######  Example 4.

Let us illustrate the isomorphism using on the epistemic frame $\mathcal{M}$
of Example 1. We now describe its equivalent representation as an epistemic
covering $\sigma(\mathcal{M})$. In fact, the base $B$ of the covering is the
one depicted in Example 3. Then, we need a projective cset $E$, which can be
thought of as an “exploded view” of $B$, depicted below. Its maximal
simplices, labelled $\\{w_{0},\dots,w_{5}\\}\cup\\{w_{1}^{\prime}\\}$,
correspond to the worlds of the original frame $\mathcal{M}$.

$w_{2}$$\\{a,b,c\\}$$w_{3}$$b$$\\{a,b,c\\}$$c$$w_{1}$$w_{4}$$w_{5}$$w^{\prime}_{1}$$w_{0}$$\\{a,b\\}$$\\{a,b\\}$$b$$b$$b$$\\{a,b\\}$$\varnothing$$\\{a,c\\}$$a$$a$$w_{2}$$w_{3}$$w_{0}$$w_{4}$$w_{1},w^{\prime}_{1}$$w_{5}$$w_{1}$$w_{1}^{\prime}$$w_{2}$$w_{3}$$w_{4}$$w_{5}$$w_{0}$

The covering $f:E\to B$ maps each world of $E$ to its geometric representation
in the base $B$. Note that both $w_{1}$ and $w_{1}^{\prime}$ are mapped to the
same edge of $B$: this is how we model non-proper behavior in epistemic
frames. Moreover, world $w_{0}$ is represented by a single vertex, because
only one agent is alive; it is mapped to the top blue vertex of $B$. This is
how we model sub-worlds: since $w_{0}$ is a sub-world of $w_{1}$ in
$\mathcal{M}$, $f(w_{0})$ is a sub-simplex of $f(w_{1})$ in
$\sigma(\mathcal{M})$.

###  III-D Semantics of distributed knowledge

We now use generalized epistemic frames, and equivalently epistemic coverings,
as a model for the logic of distributed knowledge. The missing piece of data
is to label the worlds with _atomic propositions_ , in order to specify which
facts about the system are either true or false in any given world.

######  Definition 7.

A _(generalized) epistemic model_ $\mathcal{M}={\langle M,\sim,L\rangle}$ over
the set of agents $A$ consists of a generalized frame $\langle M,\sim\rangle$
together with _valuation_ function $L:M\to\mathscr{P}(\mathsf{At})$. A
morphism of epistemic models $f:\mathcal{M}\to\mathcal{N}$ is a morphism of
underlying frames that preserves valuations, that is, if $p\in L_{M}(w)$, then
$p\in L_{N}(f(w))$. The category of generalized epistemic models is denoted
$\mathcal{KM}_{A}$.

######  Remark 2.

Morphisms in $\mathcal{KM}_{A}$ are also known as functional simulations [23].
They are different from the morphisms used in [3]: there the valuations of
atomic propositions were preserved and reflected, that is
$L_{M}(s)=L_{N}(f(s))$, whereas in our definition $L_{M}(s)\subseteq
L_{N}(f(s))$. They are also different from morphisms in [9]: there, morphisms
can be seen as relations, as they are maps $f:M\to\mathscr{P}(N)$.

Given a generalized epistemic model, we can define the satisfaction relation
as we did in Section II-A. Note however that $\sim_{U}$ is now part of the
structure of the model, and might not be equal to $\bigcap_{a\in U}\sim_{a}$
in general.

$\begin{array}[]{lcl}M,w\models
D_{U}\,\varphi&\text{iff}&M,w^{\prime}\models\varphi\text{ for all
}w^{\prime}\in M\\\ &&\text{ such that }w\sim_{U}w^{\prime}\end{array}$

Similarly, we can equip epistemic coverings with a valuation:

######  Definition 8.

An _epistemic covering model_ $X=\langle{f:E\to B},\ell\rangle$ consists of an
epistemic covering $f\\!:\\!E\to B$, together with a labelling
$\ell:\mathsf{max}(E)\to\mathscr{P}(\mathsf{At})$ that associates with each
maximal simplex $s$ of $E$ a set of atomic propositions $\ell(s)$ that hold
there. A morphism of epistemic covering models $\alpha:X\to Y$ is a morphism
of epistemic coverings that preserves the labelling:
$\ell(s)\subseteq\ell^{\prime}(\uparrow\\!\alpha(s))$, where
$\uparrow\\!\alpha(s)$ is the maximal simplex of $E$ that contains
$\alpha(s)$. We denote by $\mathcal{EC}_{A}$ the category of epistemic
covering models.

Given an epistemic covering model $X=\langle f,\ell\rangle$ together with a
maximal simplex $s$ in $E$, we can define the satisfaction relation
$X,s\models\varphi$ by transporting what we did for generalized epistemic
models via the isomophism of Proposition 1.

$\begin{array}[]{lcl}X,s\models
D_{U}\,\varphi&\text{iff}&X,s^{\prime}\models\varphi\text{ for all maximal
}s^{\prime}\in E\\\ &&\text{ such that
}\partial_{U}(f(s^{\prime}))=\partial_{U}(f(s))\end{array}$

Proposition 1 can be readily extended to show that the categories of models
are also isomorphic:

######  Theorem 1.

The category of epistemic covering models $\mathcal{EC}_{A}$ is isomorphic to
the category of generalized epistemic models $\mathcal{KM}_{A}$.

###### Proof:

We provide two functors $\kappa,\sigma$. On the underlying coverings and
frames, they act as in Proposition 1. We just need to extend them to
valuations. For $\kappa:\mathcal{EC}_{A}\to\mathcal{KM}_{A}$, for each maximal
simplex $s$ in $E$, we have an associated world $w_{s}$ in $\kappa(f)$. We set
$L_{\kappa(f)}(w_{s})=\ell(s)$. Similarly, for
${\sigma:\mathcal{KM}_{A}\to\mathcal{EC}_{A}}$, there is an associated maximal
simplex $s_{w}$ for every world $w$. We set $\ell_{\sigma(M)}(s_{w})=L(w)$.
The rest of the proof is the same as in Proposition 1. ∎

As expected, the satisfaction relations for both kinds of models yield the
same result:

######  Lemma 2.

Given a pointed epistemic covering model $(X,s)$, we have $X,s\models\varphi$
iff $\kappa(X),w_{s}\models\varphi$. Conversely, given a pointed generalized
epistemic model $(M,w)$, we have $M,w\models\varphi$ iff
$\sigma(M),s_{w}\models\varphi$.

###### Proof:

We prove the first equivalence by induction on the structure of $\varphi$. The
case of atomic propositions comes from the fact that we keep the labelling
$L(w_{s})=\ell(s)$. The case of boolean connectives is straightforward. For a
formula of the form $D_{U}\varphi$ one can notice that we defined
$w_{s}\sim_{U}w_{s^{\prime}}$ iff
$\partial_{U}(f(s))=\partial_{U}(f(s^{\prime}))$, which coincides with the
semantics of $D_{U}$. The second equivalence follows from the first one,
together with Theorem 1. ∎

##  IV Properties of epistemic models

The models presented in Section III-D are very versatile. Depending on what
kind of applications we have in mind, we might want to impose some extra
properties on the structure of our models. For instance in distributed
computing, the model is usually assumed to be a simplicial complex rather than
a simplicial set, because a global state of the system is merely the sum of
the local states of the agents, without any extra information. In this
section, we define a number of interesting properties of epistemic frames, as
well as their geometric counterpart, epistemic coverings. We will see how some
of the results of previous papers on simplicial models arise as a special case
of Proposition 1.

###  IV-A Properties of epistemic frames and coverings

######  Definition 9.

An epistemic frame $\mathcal{M}=\langle M,\sim\rangle$ is said to

  * •

have _trivial empty-group knowledge_
if $\forall w,w^{\prime}\in M.\ w\sim_{\varnothing}w^{\prime}$;

  * •

have _no empty worlds_ if $\forall w\in M.\ \exists a\in A.\ w\sim_{a}w$;

  * •

be _proper_ if $(\overline{w}=\overline{w^{\prime}}\land
w\sim_{\overline{w}}w^{\prime})\Rightarrow w=w^{\prime}$;

  * •

be _maximal_ if $\forall w\in M.\ \forall U\subseteq\overline{w}.$
$U\neq\varnothing\Rightarrow\exists w^{\prime}\in M.\
(U=\overline{w^{\prime}}\land w^{\prime}\sim_{U}w)$;

  * •

be _minimal_ if $\forall w,w^{\prime}\in M.\
(\overline{w}\subsetneq\overline{w^{\prime}})\Rightarrow
w\not\sim_{\overline{w}}w^{\prime}$;

  * •

be _pure_ if $\forall w\in M.\ \overline{w}=A$;

  * •

have _standard group knowledge_
if $\forall U\\!\subseteq\\!A.\ (\forall a\in U.\
w\sim_{a}w^{\prime})\Rightarrow w\sim_{U}w^{\prime}$.

Let us explain the meaning of these properties. In a frame with trivial empty-
group knowledge, the empty group cannot distinguish any worlds. It models the
idea that an empty group cannot measure anything, so all worlds have the same
properties for it.

If a frame has no empty worlds, then there is an alive agent in every world,
i.e., every possibility is observed by someone.

A frame is proper if every pair of worlds that has the same set of alive
agents is distinguishable by some subgroup of agents. This also corresponds to
the principle of observability: if even a maximal group cannot distinguish
worlds, then they are the same. Notice that this allows sub-worlds.

######  Example 5.

In the figure below, the leftmost frame has trivial empty-group knowledge,
($w_{0}\sim_{\varnothing}w_{1}\sim_{\varnothing}w_{2}$), but also has an empty
world $w_{2}$, and is not proper ($w_{0}\sim_{\\{a,b\\}}w_{1}$). The middle
frame has non-trivial empty-group knowledge
(${w_{1}\not\sim_{\varnothing}w_{2}}$), has no empty worlds, and is not
proper. The rightmost frame has non-trivial empty-group knowledge, has an
empty world, but is proper ($w_{0}\not\sim_{b}w_{1}$).

$w_{2}$$\\{a,b,c\\}$$w_{3}$$b$$\\{a,b,c\\}$$c$$w_{1}$$w_{4}$$w_{5}$$w^{\prime}_{1}$$w_{0}$$\\{a,b\\}$$\\{a,b\\}$$b$$b$$b$$\\{a,b\\}$$\varnothing$$\\{a,c\\}$$a$$a$$w_{2}$$w_{3}$$w_{0}$$w_{4}$$w_{1},w^{\prime}_{1}$$w_{5}$$w_{1}$$w_{1}^{\prime}$$w_{2}$$w_{3}$$w_{4}$$w_{5}$$w_{0}$$w_{0}$$w_{2}$$a,b$$\varnothing$$w_{1}$$\varnothing$$a,b$$a,b$ |  $w_{2}$$\\{a,b,c\\}$$w_{3}$$b$$\\{a,b,c\\}$$c$$w_{1}$$w_{4}$$w_{5}$$w^{\prime}_{1}$$w_{0}$$\\{a,b\\}$$\\{a,b\\}$$b$$b$$b$$\\{a,b\\}$$\varnothing$$\\{a,c\\}$$a$$a$$w_{2}$$w_{3}$$w_{0}$$w_{4}$$w_{1},w^{\prime}_{1}$$w_{5}$$w_{1}$$w_{1}^{\prime}$$w_{2}$$w_{3}$$w_{4}$$w_{5}$$w_{0}$$w_{0}$$w_{2}$$a,b$$\varnothing$$w_{1}$$\varnothing$$a,b$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a,b$$a,b$$a$ | $w_{2}$$\\{a,b,c\\}$$w_{3}$$b$$\\{a,b,c\\}$$c$$w_{1}$$w_{4}$$w_{5}$$w^{\prime}_{1}$$w_{0}$$\\{a,b\\}$$\\{a,b\\}$$b$$b$$b$$\\{a,b\\}$$\varnothing$$\\{a,c\\}$$a$$a$$w_{2}$$w_{3}$$w_{0}$$w_{4}$$w_{1},w^{\prime}_{1}$$w_{5}$$w_{1}$$w_{1}^{\prime}$$w_{2}$$w_{3}$$w_{4}$$w_{5}$$w_{0}$$w_{0}$$w_{2}$$a,b$$\varnothing$$w_{1}$$\varnothing$$a,b$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a,b$$a,b$$a$$w_{0}$$w_{2}$$a,b$$w_{1}$$a$$a,b$
---|---|---

A frame is maximal if every world has a non-empty sub-world. A certain
intuition comes from distributed computing: in a maximal frame, any number of
agents may crash during the execution of a program, as long as at least one of
them remains alive. Moreover, these crashes are undetectable.

A frame is minimal if there are no strict sub-worlds. Once again, this
corresponds to a situation in distributed computing where crashes are
detectable, that is when a process crashes, one of the remaining processes is
aware of it.

A frame is pure if the set of alive agent in every world is the same. In such
a situation, crashes are not allowed at all, and all agents always
participate.

By “standard group knowledge”, we mean that group indistinguishability
relations are generated by individual agents, that is, knowledge of the group
is exactly the sum of individual agents’ knowledge. More formally, when
$\sim_{U}\;=\;\bigcap_{a\in U}\sim_{a}$.

######  Example 6.

In the figure below, the upper left frame is maximal, as it has all sub-
worlds. The upper right frame is minimal as it does not have sub-worlds at
all. The bottom left frame is pure as all its worlds have the same set of
alive agents. The bottom right frame has non-standard group knowledge,
contrary to all previous examples, since $w_{0}\sim_{a}w_{1}$,
$w_{0}\sim_{b}w_{1}$, but $w_{0}\not\sim_{a,b}w_{1}$.

$w_{2}$$\\{a,b,c\\}$$w_{3}$$b$$\\{a,b,c\\}$$c$$w_{1}$$w_{4}$$w_{5}$$w^{\prime}_{1}$$w_{0}$$\\{a,b\\}$$\\{a,b\\}$$b$$b$$b$$\\{a,b\\}$$\varnothing$$\\{a,c\\}$$a$$a$$w_{2}$$w_{3}$$w_{0}$$w_{4}$$w_{1},w^{\prime}_{1}$$w_{5}$$w_{1}$$w_{1}^{\prime}$$w_{2}$$w_{3}$$w_{4}$$w_{5}$$w_{0}$$w_{0}$$w_{2}$$a,b$$\varnothing$$w_{1}$$\varnothing$$a,b$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a,b$$a,b$$a$$w_{0}$$w_{2}$$a,b$$w_{1}$$a$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a$$a$$b$$b$ | $w_{2}$$\\{a,b,c\\}$$w_{3}$$b$$\\{a,b,c\\}$$c$$w_{1}$$w_{4}$$w_{5}$$w^{\prime}_{1}$$w_{0}$$\\{a,b\\}$$\\{a,b\\}$$b$$b$$b$$\\{a,b\\}$$\varnothing$$\\{a,c\\}$$a$$a$$w_{2}$$w_{3}$$w_{0}$$w_{4}$$w_{1},w^{\prime}_{1}$$w_{5}$$w_{1}$$w_{1}^{\prime}$$w_{2}$$w_{3}$$w_{4}$$w_{5}$$w_{0}$$w_{0}$$w_{2}$$a,b$$\varnothing$$w_{1}$$\varnothing$$a,b$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a,b$$a,b$$a$$w_{0}$$w_{2}$$a,b$$w_{1}$$a$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a$$a$$b$$b$$w_{0}$$a,c$$w_{1}$$a$$a,b$
---|---
$w_{2}$$\\{a,b,c\\}$$w_{3}$$b$$\\{a,b,c\\}$$c$$w_{1}$$w_{4}$$w_{5}$$w^{\prime}_{1}$$w_{0}$$\\{a,b\\}$$\\{a,b\\}$$b$$b$$b$$\\{a,b\\}$$\varnothing$$\\{a,c\\}$$a$$a$$w_{2}$$w_{3}$$w_{0}$$w_{4}$$w_{1},w^{\prime}_{1}$$w_{5}$$w_{1}$$w_{1}^{\prime}$$w_{2}$$w_{3}$$w_{4}$$w_{5}$$w_{0}$$w_{0}$$w_{2}$$a,b$$\varnothing$$w_{1}$$\varnothing$$a,b$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a,b$$a,b$$a$$w_{0}$$w_{2}$$a,b$$w_{1}$$a$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a$$a$$b$$b$$w_{0}$$a,c$$w_{1}$$a$$a,b$$w_{0}$$a,b,c$$w_{1}$$b,c$$a,b,c$ | $w_{2}$$\\{a,b,c\\}$$w_{3}$$b$$\\{a,b,c\\}$$c$$w_{1}$$w_{4}$$w_{5}$$w^{\prime}_{1}$$w_{0}$$\\{a,b\\}$$\\{a,b\\}$$b$$b$$b$$\\{a,b\\}$$\varnothing$$\\{a,c\\}$$a$$a$$w_{2}$$w_{3}$$w_{0}$$w_{4}$$w_{1},w^{\prime}_{1}$$w_{5}$$w_{1}$$w_{1}^{\prime}$$w_{2}$$w_{3}$$w_{4}$$w_{5}$$w_{0}$$w_{0}$$w_{2}$$a,b$$\varnothing$$w_{1}$$\varnothing$$a,b$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a,b$$a,b$$a$$w_{0}$$w_{2}$$a,b$$w_{1}$$a$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a$$a$$b$$b$$w_{0}$$a,c$$w_{1}$$a$$a,b$$w_{0}$$a,b,c$$w_{1}$$b,c$$a,b,c$$w_{0}$$a,b$$w_{1}$$a$$a,b$$b$

Similarly, for epistemic coverings:

######  Definition 10.

An epistemic covering $f:E\to B$ is said to

  * •

have _trivial empty-group knowledge_ if there is only one simplex of dimension
$-1$ in $B$;

  * •

have _no empty worlds_ if all maximal simplices of $E$ have dimension $\geq
0$;

  * •

be _proper_ if no two maximal simplices of $E$ have the same image in $B$;

  * •

be _maximal_ if every simplex in $B$ is the image of a maximal simplex of $E$;

  * •

be _minimal_ if the image of a maximal simplex of $E$ is always a maximal
simplex of $B$;

  * •

be _pure_ if all maximal simplices of $E$ have dimension $|A|-1$;

  * •

have _standard group knowledge_ if $B$ is a simplicial complex.

The intuition behind the definitions is exactly the same as in the case of
frames. We give a few illustrative examples. In the picture below, the
leftmost covering has trivial empty-group knowledge as there is only one
$(-1)$-simplex in the base space (one dashed region); but it has empty worlds
because of the maximal $(-1)$-simplex $w_{2}$. The covering depicted in the
middle has no empty worlds since all the maximal simplices have dimension $0$
or $1$. It, however, does not have trivial empty-group knowledge as it has two
$(-1)$-simplices in the base space (depicted as two dashed regions). It is not
proper either because both worlds $w_{0},w_{1}$ label the same edge. The
rightmost covering is proper, as every simplex is annotated with at most one
world. It has an empty world, $w_{2}$, and does not have trivial empty-group
knowledge.

$w_{2}$$\\{a,b,c\\}$$w_{3}$$b$$\\{a,b,c\\}$$c$$w_{1}$$w_{4}$$w_{5}$$w^{\prime}_{1}$$w_{0}$$\\{a,b\\}$$\\{a,b\\}$$b$$b$$b$$\\{a,b\\}$$\varnothing$$\\{a,c\\}$$a$$a$$w_{2}$$w_{3}$$w_{0}$$w_{4}$$w_{1},w^{\prime}_{1}$$w_{5}$$w_{1}$$w_{1}^{\prime}$$w_{2}$$w_{3}$$w_{4}$$w_{5}$$w_{0}$$w_{0}$$w_{2}$$a,b$$\varnothing$$w_{1}$$\varnothing$$a,b$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a,b$$a,b$$a$$w_{0}$$w_{2}$$a,b$$w_{1}$$a$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a$$a$$b$$b$$w_{0}$$a,c$$w_{1}$$a$$a,b$$w_{0}$$a,b,c$$w_{1}$$b,c$$a,b,c$$w_{0}$$a,b$$w_{1}$$a$$a,b$$b$$w_{2}$$w_{0},w_{1}$ |  $w_{2}$$\\{a,b,c\\}$$w_{3}$$b$$\\{a,b,c\\}$$c$$w_{1}$$w_{4}$$w_{5}$$w^{\prime}_{1}$$w_{0}$$\\{a,b\\}$$\\{a,b\\}$$b$$b$$b$$\\{a,b\\}$$\varnothing$$\\{a,c\\}$$a$$a$$w_{2}$$w_{3}$$w_{0}$$w_{4}$$w_{1},w^{\prime}_{1}$$w_{5}$$w_{1}$$w_{1}^{\prime}$$w_{2}$$w_{3}$$w_{4}$$w_{5}$$w_{0}$$w_{0}$$w_{2}$$a,b$$\varnothing$$w_{1}$$\varnothing$$a,b$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a,b$$a,b$$a$$w_{0}$$w_{2}$$a,b$$w_{1}$$a$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a$$a$$b$$b$$w_{0}$$a,c$$w_{1}$$a$$a,b$$w_{0}$$a,b,c$$w_{1}$$b,c$$a,b,c$$w_{0}$$a,b$$w_{1}$$a$$a,b$$b$$w_{2}$$w_{0},w_{1}$$w_{2}$$w_{0},w_{1}$ |  $w_{2}$$\\{a,b,c\\}$$w_{3}$$b$$\\{a,b,c\\}$$c$$w_{1}$$w_{4}$$w_{5}$$w^{\prime}_{1}$$w_{0}$$\\{a,b\\}$$\\{a,b\\}$$b$$b$$b$$\\{a,b\\}$$\varnothing$$\\{a,c\\}$$a$$a$$w_{2}$$w_{3}$$w_{0}$$w_{4}$$w_{1},w^{\prime}_{1}$$w_{5}$$w_{1}$$w_{1}^{\prime}$$w_{2}$$w_{3}$$w_{4}$$w_{5}$$w_{0}$$w_{0}$$w_{2}$$a,b$$\varnothing$$w_{1}$$\varnothing$$a,b$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a,b$$a,b$$a$$w_{0}$$w_{2}$$a,b$$w_{1}$$a$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a$$a$$b$$b$$w_{0}$$a,c$$w_{1}$$a$$a,b$$w_{0}$$a,b,c$$w_{1}$$b,c$$a,b,c$$w_{0}$$a,b$$w_{1}$$a$$a,b$$b$$w_{2}$$w_{0},w_{1}$$w_{2}$$w_{0},w_{1}$$w_{2}$$w_{0}$$w_{1}$
---|---|---

In the examples below, the top left covering is maximal as every simplex is
annotated, that is, every simplex has a maximal simplex that is sent to it.
The top right covering is minimal because only maximal simplices are
annotated. The bottom left covering is pure, as all annotated simplices are of
the same dimension. All of the examples above have standard group knowledge
since their base csets are in fact complexes. The bottom right covering has
non-standard group knowledge as its base cset is not a simplicial complex.

$w_{2}$$\\{a,b,c\\}$$w_{3}$$b$$\\{a,b,c\\}$$c$$w_{1}$$w_{4}$$w_{5}$$w^{\prime}_{1}$$w_{0}$$\\{a,b\\}$$\\{a,b\\}$$b$$b$$b$$\\{a,b\\}$$\varnothing$$\\{a,c\\}$$a$$a$$w_{2}$$w_{3}$$w_{0}$$w_{4}$$w_{1},w^{\prime}_{1}$$w_{5}$$w_{1}$$w_{1}^{\prime}$$w_{2}$$w_{3}$$w_{4}$$w_{5}$$w_{0}$$w_{0}$$w_{2}$$a,b$$\varnothing$$w_{1}$$\varnothing$$a,b$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a,b$$a,b$$a$$w_{0}$$w_{2}$$a,b$$w_{1}$$a$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a$$a$$b$$b$$w_{0}$$a,c$$w_{1}$$a$$a,b$$w_{0}$$a,b,c$$w_{1}$$b,c$$a,b,c$$w_{0}$$a,b$$w_{1}$$a$$a,b$$b$$w_{2}$$w_{0},w_{1}$$w_{2}$$w_{0},w_{1}$$w_{2}$$w_{0}$$w_{1}$$w_{1}$$w_{0}$$w_{2}$ |  $w_{2}$$\\{a,b,c\\}$$w_{3}$$b$$\\{a,b,c\\}$$c$$w_{1}$$w_{4}$$w_{5}$$w^{\prime}_{1}$$w_{0}$$\\{a,b\\}$$\\{a,b\\}$$b$$b$$b$$\\{a,b\\}$$\varnothing$$\\{a,c\\}$$a$$a$$w_{2}$$w_{3}$$w_{0}$$w_{4}$$w_{1},w^{\prime}_{1}$$w_{5}$$w_{1}$$w_{1}^{\prime}$$w_{2}$$w_{3}$$w_{4}$$w_{5}$$w_{0}$$w_{0}$$w_{2}$$a,b$$\varnothing$$w_{1}$$\varnothing$$a,b$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a,b$$a,b$$a$$w_{0}$$w_{2}$$a,b$$w_{1}$$a$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a$$a$$b$$b$$w_{0}$$a,c$$w_{1}$$a$$a,b$$w_{0}$$a,b,c$$w_{1}$$b,c$$a,b,c$$w_{0}$$a,b$$w_{1}$$a$$a,b$$b$$w_{2}$$w_{0},w_{1}$$w_{2}$$w_{0},w_{1}$$w_{2}$$w_{0}$$w_{1}$$w_{1}$$w_{0}$$w_{2}$$w_{1}$$w_{0}$
---|---
$w_{2}$$\\{a,b,c\\}$$w_{3}$$b$$\\{a,b,c\\}$$c$$w_{1}$$w_{4}$$w_{5}$$w^{\prime}_{1}$$w_{0}$$\\{a,b\\}$$\\{a,b\\}$$b$$b$$b$$\\{a,b\\}$$\varnothing$$\\{a,c\\}$$a$$a$$w_{2}$$w_{3}$$w_{0}$$w_{4}$$w_{1},w^{\prime}_{1}$$w_{5}$$w_{1}$$w_{1}^{\prime}$$w_{2}$$w_{3}$$w_{4}$$w_{5}$$w_{0}$$w_{0}$$w_{2}$$a,b$$\varnothing$$w_{1}$$\varnothing$$a,b$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a,b$$a,b$$a$$w_{0}$$w_{2}$$a,b$$w_{1}$$a$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a$$a$$b$$b$$w_{0}$$a,c$$w_{1}$$a$$a,b$$w_{0}$$a,b,c$$w_{1}$$b,c$$a,b,c$$w_{0}$$a,b$$w_{1}$$a$$a,b$$b$$w_{2}$$w_{0},w_{1}$$w_{2}$$w_{0},w_{1}$$w_{2}$$w_{0}$$w_{1}$$w_{1}$$w_{0}$$w_{2}$$w_{1}$$w_{0}$$w_{0}$$w_{1}$ |  $w_{2}$$\\{a,b,c\\}$$w_{3}$$b$$\\{a,b,c\\}$$c$$w_{1}$$w_{4}$$w_{5}$$w^{\prime}_{1}$$w_{0}$$\\{a,b\\}$$\\{a,b\\}$$b$$b$$b$$\\{a,b\\}$$\varnothing$$\\{a,c\\}$$a$$a$$w_{2}$$w_{3}$$w_{0}$$w_{4}$$w_{1},w^{\prime}_{1}$$w_{5}$$w_{1}$$w_{1}^{\prime}$$w_{2}$$w_{3}$$w_{4}$$w_{5}$$w_{0}$$w_{0}$$w_{2}$$a,b$$\varnothing$$w_{1}$$\varnothing$$a,b$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a,b$$a,b$$a$$w_{0}$$w_{2}$$a,b$$w_{1}$$a$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a$$a$$b$$b$$w_{0}$$a,c$$w_{1}$$a$$a,b$$w_{0}$$a,b,c$$w_{1}$$b,c$$a,b,c$$w_{0}$$a,b$$w_{1}$$a$$a,b$$b$$w_{2}$$w_{0},w_{1}$$w_{2}$$w_{0},w_{1}$$w_{2}$$w_{0}$$w_{1}$$w_{1}$$w_{0}$$w_{2}$$w_{1}$$w_{0}$$w_{0}$$w_{1}$$w_{1}$$w_{0}$

As our terminology suggests, these properties of epistemic coverings are the
geometric counterpart of the ones of epistemic frames that we defined
previously.

######  Lemma 3.

The properties of Definition 9 agree with the ones of Definition 10 up to the
equivalence in Proposition 1. Namely, if $f$ is a covering of a certain type,
then $\kappa(f)$ is of the same type, and conversely for $\sigma$.

###### Proof:

We only show two cases, as the proofs are very similar and just a matter of
checking that we correctly translated the notions through the equivalence.

Consider a proper covering $f\\!:\\!E\to B$. In the frame $\kappa(f)$, two
worlds $w_{1},w_{2}$ are indistinguishable by group
$\overline{w_{1}}=\overline{w_{2}}$ if and only if the simplices in $E$ that
correspond to $w_{1}$ and $w_{2}$ are sent to the same simplex in $B$. But, as
$f$ is proper, no two simplices have the same image, thus the frame is proper
too. Now, consider a proper frame $\mathcal{M}$. By construction of the
functor $\sigma$, two simplices $s_{1},s_{2}$ in $E_{M}$ of the same color are
sent to the same simplex in $B_{\sigma(M)}$, if and only for corresponding
worlds $w_{1},w_{2}$ in $\mathcal{M}$ $w_{1}\sim_{\overline{w_{1}}}w_{2}$. But
$\mathcal{M}$ is proper, so it is never the case, thus $\sigma(\mathcal{M})$
is proper too.

Consider a covering $f\\!:\\!E\to B$ with standard group knowledge. Suppose
that for a pair $w_{1},w_{2}$ in the frame $\kappa(f)$, $w_{1}\sim_{a}w_{2}$
for all $a$ in some $U$. It means that
$\partial_{a}(s_{1})=\partial_{a}(s_{2})$, where $s_{1}$ corresponds to
$w_{1}$ and $s_{2}$ to $w_{2}$. As $B$ is a simplicial complex, it follows
that $\partial_{U}(s_{1})=\partial_{U}(s_{2})$, so $\kappa(f)$ has standard
group knowledge. Take now a frame $M$ with standard group knowledge. Suppose
there are two worlds $w_{1},w_{2}$ in $M$ such that
$\overline{w_{1}}=\overline{w_{2}}=U$ and for all $a\in U$,
$[w_{1}]_{a}=[w_{2}]_{a}$. Since $M$ has standard group knowledge,
$[w_{1}]_{U}=\bigcap_{a\in U}[w_{1}]_{a}$. Thus, $[w_{1}]_{U}=[w_{2}]_{U}$,
which means precisely that if two simplices in $B_{\sigma(M)}$ have the same
set of vertices, then they are equal. ∎

###  IV-B Subclasses of epistemic frames and coverings

The properties of epistemic frames (or, equivalently, epistemic coverings)
defined in the previous section can be combined in various ways in order to
define particular sub-classes of interest. The only restriction is that
_minimal_ and _maximal_ are mutually exclusive properties (except in
degenerate cases where the model only has empty worlds). It is also possible,
and perhaps sometimes desirable, to consider models that are neither maximal
nor minimal. Moreover, a frame/covering which is _pure_ must also be minimal
and have no empty world, so there is no need to specify the latter if we
already have the former.

We can recover variants of simplicial models that have been defined in
previous papers. Since they are usually concerned with distributed computing,
where agents represent processes that can reason about the system, there is
little interest in studying empty worlds or empty groups of agents. Thus, they
all have _trivial empty-group knowledge_ and _no empty worlds_. They also have
_standard group knowledge_ since they work with simplicial complexes instead
of semi-simplicial sets. Moreover, all previous instances of simplicial models
were always _proper_ , not out of necessity, but because without the notion of
covering, it is not possible to model non-proper behaviors in the geometric
approach. On top of that:

  * •

The original paper introducing simplicial models [3] was working with _pure_
simplicial models (and thus, minimal).

  * •

In the sequel [9], the “pure” assumption is dropped, but models are still
assumed to be minimal since formulas are only evaluated at the facets.

  * •

On the other hand, [10] and [11] study simplicial models that may not be pure
but are maximal: every simplex is a possible world.

  * •

An example that is not concerned about simplicial models, but which studies
non-standard group knowledge, is [15]. Their models are also pure, proper, and
have trivial empty-group knowledge.

In light of Lemma 3, we can easily restrict the equivalence of categories
proved in Proposition 1 to the various sub-categories of frames and coverings.
For instance, we can reformulate the main result of [3] as follows:

######  Corollary 1 ([3]).

The category of pure proper epistemic frames with standard group knowledge is
isomorphic to the category of pure proper epistemic coverings with standard
group knowledge.

###### Proof:

By Lemma 3, the restrictions of $\kappa$ and $\sigma$ to those sub-categories
is well-defined. Since we still have $\kappa\circ\sigma=\mathsf{id}$ and
$\sigma\circ\kappa=\mathsf{id}$ as proved in Proposition 1, this is still an
isomorphism of categories. ∎

##  V Axiomatization of the various sub-classes

###  V-A Reasoning about alive and dead agents

As in [9], we can express within the language $\mathcal{L}_{D}$ the fact that
agents can be dead or alive. For any agent $a\in A$ and group of agents
$U\subseteq A$, we define the following formulas:

$\displaystyle\mathsf{dead}(a)\,:=\,K_{a}\mathsf{false}$
$\displaystyle\mathsf{alive}(a)\,:=\,\widehat{K}_{a}\mathsf{true}$
$\displaystyle\mathsf{dead}(U)\,:=\,\bigwedge_{a\in U}\mathsf{dead}(a)$
$\displaystyle\mathsf{alive}(U)\,:=\,\widehat{D}_{U}\mathsf{true}$

It is easy to check that they have the expected semantics: for epistemic
frames, we have $M,w\models\mathsf{alive}(U)$ iff $w\sim_{U}w$; and for
epistemic coverings, $X,s\models\mathsf{alive}(U)$ iff $s$ is a $V$-simplex
with $U\subseteq V$.

###  V-B Axiomatization of epistemic covering models

We rely on the usual axiomatization of normal modal logics, with all
propositional tautologies, closure by modus ponens, and the necessitation
rule. On top of that, we add the following five axioms:

  * •

($\mathbf{K}$)
$D_{U}(\varphi\Rightarrow\psi)\Rightarrow(D_{U}\varphi\Rightarrow D_{U}\psi)$

  * •

($\mathbf{4}$) $D_{U}\varphi\Rightarrow D_{U}D_{U}\varphi$

  * •

($\mathbf{B}$) $\varphi\Rightarrow D_{U}\neg D_{U}\neg\varphi$

  * •

($\mathbf{Mono}$) for $U\subseteq U^{\prime}$, $D_{U}\varphi\Rightarrow
D_{U^{\prime}}\varphi$

  * •

($\mathbf{Union}$) for $U,U^{\prime}$,
$\mathsf{alive}(U)\land\mathsf{alive}(U^{\prime})\Rightarrow\mathsf{alive}(U\cup
U^{\prime})$

We abbreviate $\mathbf{KB4_{n}+Mono+Union}$ as $\mathbf{EC_{n}}$, which stands
for the logic of epistemic coverings (as we will see). Notice that the
difference between $\mathbf{KB4_{n}}$ and the more standard multi-agent
epistemic logic $\mathbf{S5_{n}}$ is the absence of axiom $\mathbf{T}$:
$D_{U}\varphi\Rightarrow\varphi$. Here are a few examples of valid formulas in
$\mathbf{EC_{n}}$ related to the life and death of agents.

  * •

$\mathbf{EC_{n}}\vdash\mathsf{dead}(a)\Rightarrow K_{a}\varphi$: dead agents
know everything. More generally, for $a\in U$,
$\mathbf{EC_{n}}\vdash\mathsf{dead}(a)\Rightarrow D_{U}\varphi$.

  * •

$\mathbf{EC_{n}}\vdash\mathsf{alive}(a)\Rightarrow K_{a}\,\mathsf{alive}(a)$:
Alive agents know that they are alive. The same holds for a group $U$ of
agents.

  * •

$\mathbf{EC_{n}}\vdash\mathsf{alive}(U)\Rightarrow(D_{U}\varphi\Rightarrow\varphi)$:
Axiom T is verified when restricted to groups of agents that are alive.

We are going to show soundness and completeness of $\mathbf{EC_{n}}$ with
respect to generalized epistemic models. In order to show completeness, we use
the standard approach: by providing a canonical model, see for example [23].

######  Definition 11.

The _canonical generalized epistemic model_ $M^{\mathrm{c}}=\langle
W^{\mathrm{c}},\sim,L\rangle$ is defined as follows:

  * •

$W^{\mathrm{c}}=\\{\Gamma\mid\Gamma\textup{ is a maximal consistent set of
formulas}\\}$.

  * •

$\Gamma\sim_{U}\Delta$ iff $D_{U}\,\varphi\in\Gamma$ implies
$\varphi\in\Delta$.

  * •

$L(\Gamma)=\Gamma\cap\mathsf{At}$.

######  Lemma 4 (Truth Lemma).

For any formula $\varphi$ and any maximal consistent set of formulas
$\Gamma\in M^{c}$, we have $\varphi\in\Gamma$ iff
$M^{c},\Gamma\models\varphi$.

###### Proof:

We proceed by induction on $\varphi$. The base case of atomic propositions
holds by definition of $M^{c}$. For the boolean connectives, the proof is
trivial.

Let us do the case of $D_{U}\varphi$. Assume that $D_{U}\varphi$ is in
$\Gamma$ and let $\Delta$ be an element of $M^{c}$ such that
$\Gamma\sim_{U}\Delta$. By definition of $\sim$, we have $\varphi\in\Delta$,
so by induction hypothesis $M^{c},\Delta\models\varphi$. As $\Delta$ is
arbitrarily chosen, we have $M^{c},\Gamma\models D_{U}\varphi$. Conversely,
assume that $M^{c},\Gamma\models D_{U}\varphi$ and suppose by contradiction
that $D_{U}\varphi\not\in\Gamma$. Then the set
$\Delta^{-}=\\{\neg\varphi\\}\cup\\{\psi\ |\ D_{U}\psi\in\Gamma\\}$ is
consistent. Indeed, suppose $\Delta^{-}$ is inconsistent. Then we have a proof
of $\vdash\psi_{1}\land\dots\land\psi_{k}\Rightarrow\varphi$, where
$D_{U}\psi_{i}\in\Gamma$ for every $i$. Then, by axiom $\mathbf{K}$, we can
prove $\vdash D_{U}\psi_{1}\land\dots\land D_{U}\psi_{k}\Rightarrow
D_{U}\varphi$. As $\Gamma$ is maximal consistent, this implies that
$D_{U}\varphi\in\Gamma$, which contradicts the assumption. Thus, $\Delta^{-}$
is consistent, and by Lindenbaum’s Lemma, we can extend it to a maximal
consistent set $\Delta\supseteq\Delta^{-}$. By construction,
$\Gamma\sim_{U}\Delta$, and by induction hypothesis,
$M^{c},\Delta\not\models\varphi$. This contradicts the assumption that
$M^{c},\Gamma\models D_{U}\varphi$. Therefore, $D_{U}\varphi\in\Gamma$, and
this concludes the proof. ∎

######  Lemma 5.

In the canonical generalized epistemic model $M^{c}$, for any $\Gamma\in
M^{c}$, $U\subseteq\overline{\Gamma}$ iff $\mathsf{alive}(U)\in\Gamma$.

###### Proof:

Suppose $U\subseteq\overline{\Gamma}$, $\Gamma\sim_{U}\Gamma$. Hence,
$\Gamma\models\widehat{D}_{U}\mathsf{true}$, as there is $\Gamma$ which is
$U$-accessible from $\Gamma$, which means that $\mathsf{alive}(U)$ is in
$\Gamma$ by the Truth Lemma. Conversely, assume $\mathsf{alive}(U)\in\Gamma$.
Then, by Truth Lemma, $\Gamma\models\widehat{D}_{U}\mathsf{true}$, so there is
$\Delta$, such that $\Delta\sim_{U}\Gamma$. By symmetry and transitivity of
$\sim_{U}$, we have $\Gamma\sim_{U}\Gamma$, so $U\subseteq\overline{\Gamma}$.
∎

######  Theorem 2.

The logic $\mathbf{EC_{n}}$ is sound and complete with respect to the family
of generalized epistemic models.

###### Proof:

Soundness is straightforward to check: the axioms $\mathbf{K}$, $\mathbf{B}$
and $\mathbf{4}$ correspond exactly to the fact that the indistinguishability
relations are PERs. Axiom $\mathbf{Mono}$ corresponds to condition (a) and
axiom $\mathbf{Union}$ corresponds to condition (b) in the definition of
generalized epistemic frames.

For completeness, consider the canonical model $M^{c}=\langle
W^{c},\sim,L\rangle$ from Definition 11. Axioms $\mathbf{K,B}$ and
$\mathbf{4}$ ensure that $\sim_{U}$ is a PER, as in the standard treatment of
completeness. Similarly, axiom $\mathbf{Mono}$ ensures that the generated
family of PERs is monotone: assume $U\subseteq U^{\prime}$,
$\Gamma\sim_{U^{\prime}}\Delta$ and $D_{U}\varphi\in\Gamma$, then by
$\mathbf{Mono}$, $D_{U^{\prime}}$ is also in $\Gamma$. As we assumed
$\Gamma\sim_{U^{\prime}}$, $\varphi\in\Delta$, so $\Gamma\sim_{U}\Delta$.
Axiom $\mathbf{Union}$ ensures that the condition $(b)$ is satisfied. Assume
that $\Gamma\sim_{U}\Gamma$, $\Gamma\sim_{U^{\prime}}\Gamma$ and $D_{U\cup
U^{\prime}}\varphi\in\Gamma$. First, we have that if $\Gamma\sim_{U}\Gamma$,
then ${\hat{D}_{U}\mathsf{true}\in\Gamma}$. Indeed, by contraposition we have
that for any $\psi$, $\psi\not\in\Gamma$ entails $D_{U}\psi\not\in\Gamma$. In
particular, as $\Gamma$ is consistent, $\mathsf{false}\not\in\Gamma$, so
$D_{U}\mathsf{false}\not\in\Gamma$. By standard reasoning, $\neg
D_{U}\mathsf{false}\in\Gamma$, as we intended. Hence,
$\mathsf{alive}(U)\land\mathsf{alive}(U^{\prime})\in\Gamma$. By
$\mathbf{Union}$ and modus ponens, $\mathsf{alive}(U\cup
U^{\prime})\in\Gamma$. As the formula
$\mathsf{alive}(V)\Rightarrow(D_{V}\varphi\Rightarrow\varphi)$ is deducible
when $V=U\cup U^{\prime}$, we have $D_{U\cup
U^{\prime}}\varphi\Rightarrow\varphi\in\Gamma$. As we assumed $D_{U\cup
U^{\prime}}\varphi\in\Gamma$, by modus ponens $\varphi\in\Gamma$, which shows
that the canonical model is indeed a generalized epistemic frame.

Applying the Lindenbaum Lemma and the Truth Lemma, any consistent formula
$\varphi$ holds in some state of $W^{c}$, and thus $\varphi$ is satisfiable. ∎

The following corollary follows from Lemma 2.

######  Corollary 2.

The logic $\mathbf{EC_{n}}$ is sound and complete with respect to epistemic
covering models.

###  V-C Axiomatization of other sub-classes

We now show how to axiomatize the various sub-classes of epistemic models, as
discussed in Section IV-B. As in the previous section, we first establish
soundness and completeness for epistemic frames, and then we get the same
result for epistemic coverings thanks to Lemmas 2 and 3. The proof is modular:
each property of the frames (Definition 9) corresponds to an extra axiom. We
denote by $U^{c}$ the complement of the set of agents $U$, that is $A\setminus
U$.

  * •

($\mathbf{NE}$)  $\bigvee_{a\in A}\mathsf{alive}(a)$;

  * •

($\mathbf{P}$)
$\mathsf{alive}(U)\land\mathsf{dead}(U^{c})\land\varphi\Rightarrow
D_{U}(\mathsf{dead}(U^{c})\Rightarrow\varphi)$;

  * •

($\mathbf{Max}$)  for $U\not=\varnothing$, $\mathsf{alive}(U)\Rightarrow\neg
D_{U}\neg\mathsf{dead}(U^{c})$;

  * •

($\mathbf{Min}$)  $\mathsf{alive}(U)\land\mathsf{dead}(U^{c})\Rightarrow
D_{U}\mathsf{dead}(U^{c})$;

  * •

($\mathbf{Pure}$)  $\mathsf{alive}(A)$.

However, there are no axioms related to trivial empty-group knowledge and
standard group knowledge. This is because those two properties cannot be
expressed in the language $\mathcal{L}_{D}$. More formally, we will see in
Theorem 3 and Theorem 6 that $\mathbf{EC_{n}}$ is complete with respect to
both classes of structures. As a consequence, they can be assumed “for free”,
without additional axiom. Indeed, to show that the logic $\mathbf{EC_{n}}$ is
sound and complete with respect to frames with trivial empty-group knowledge,
we can use the strategy from [15]. The proof that standard group knowledge
requires no extra axiom is the subject of Section V-D.

######  Remark 3.

There are several interesting relationships between those axioms. Axiom
$\mathbf{Pure}$, which says that all agents are alive in all worlds, has many
consequences. It entails the axioms $\mathbf{NE}$, $\mathbf{Min}$, and
$\mathbf{Union}$. Axiom $\mathbf{P}$ is greatly simplified and becomes
$\varphi\Rightarrow D_{A}\varphi$, where $A$ is the set of all agents.
Furthermore, $\mathbf{EC_{n}}+\mathbf{Pure}$ together entail Axiom
$\mathbf{T}$, so that the logic $\mathbf{KB4_{n}}$ becomes $\mathbf{S5_{n}}$
when $\mathbf{Pure}$ is assumed. Another possible interaction is
$\mathbf{P}+\mathbf{Min}$, which can be reformulated together as
$\mathsf{alive}(U)\land\mathsf{dead}(U^{c})\land\varphi\Rightarrow
D_{U}\varphi$. This axiom appears in [9], in the particular case of
$U=\\{a\\}$.

Now we prove soundness and completeness.

######  Theorem 3.

The logic $\mathbf{EC_{n}}\mathbf{+NE+P+Max}$ is sound and complete with
respect to proper maximal epistemic models with trivial empty-group knowledge
and no empty worlds.

###### Proof:

For brevity, call an epistemic model with the properties from the theorem
statement a _good maximal_ epistemic model. First, we show soundness. Suppose
we are given a good maximal model $\mathcal{M}$. Axioms of $\mathbf{EC_{n}}$
hold in $\mathcal{M}$ as it is an epistemic model in particular. Axiom
$\mathbf{P}$ holds in $\mathcal{M}$ because it is proper: assume that
$\mathcal{M},w\models\mathsf{alive}(U)\land\mathsf{dead}(U^{c})\land\varphi$,
that is, $\mathcal{M},w\models\varphi$ and $\overline{w}=U$. Let
$w^{\prime}\in M$ such that $w^{\prime}\sim_{U}w$. Assume then that
$\mathcal{M},w^{\prime}\models\mathsf{dead}(U^{c})$, thus
$\overline{w^{\prime}}=U$, and by properness of $\mathcal{M}$, $w=w^{\prime}$
and $\mathcal{M},w^{\prime}\models\varphi$. For axiom $\mathbf{NE}$, as every
world is non-empty, for some $a\in\overline{w}$,
$K_{a}\varphi\Rightarrow\varphi$ holds. For axiom $\mathbf{Max}$, suppose for
some world $w\in M$, $\mathcal{M},w\models\mathsf{alive}(U)$, that is
$U\subseteq\overline{w}$. As $\mathcal{M}$ is maximal, there is always a world
$w^{\prime}$, such that $w^{\prime}\sim_{U}w$ and $\overline{w^{\prime}}=U$.
So $\neg D_{U}\neg\mathsf{dead}(U^{c})$ holds in $w$ since
$\mathsf{dead}(U^{c})$ holds in $w^{\prime}$.

Now we show completeness. We define the canonical model $M^{c}$ as in
Definition 11, except that consistency now refers to the new logic. The proof
of the Truth Lemma (Lemma 4) can easily be adapted. Let $\varphi_{0}$ be a
consistent formula. We shall show that $\varphi_{0}$ is satisfiable in some
good epistemic model. Let $M^{c}$ be the canonical model for the logic, as in
Theorem 2. We need to show that the canonical model is a good model. Recall
that in the canonical model $\Gamma\sim_{U}\Delta$ iff for any $\varphi$,
$D_{U}\varphi\in\Gamma\Rightarrow{\varphi\in\Delta}$. The model $M^{c}$ is:

##### Proper

Suppose $\overline{\Gamma}=\overline{\Delta}=U$ and $\Gamma\sim_{U}\Delta$. We
need to show that $\Gamma=\Delta$, that is for every formula $\varphi$,
$\varphi\in\Gamma$ iff $\varphi\in\Delta$. Suppose $\varphi\in\Gamma$. Then,
by axiom $\mathbf{P}$, $D_{U}(\mathsf{dead}(U^{c})\Rightarrow\varphi)$ is in
$\Gamma$. By the definition of $\sim_{U}$, it means that
$\mathsf{dead}(U^{c})\Rightarrow\varphi\in\Delta$. By modus ponens,
$\varphi\in\Delta$. Similarly, we can show that
$\varphi\in\Delta\Rightarrow\varphi\in\Gamma$. Hence, $\Gamma=\Delta$ and the
canonical model is proper.

##### Maximal

Let $U\subsetneq\overline{\Gamma}$. We want to exhibit a sub-world $\Delta$ of
$\Gamma$, such that $\overline{\Delta}=U$. By Lemma 5,
$\mathsf{alive}(U)\in\Gamma$, so by axiom $\mathbf{Max}$, maximality and
consistency, $\neg D_{U}\neg\mathsf{dead}(U^{c})$ is in $\Gamma$. Then the set
$\Delta^{-}=\\{\mathsf{dead}(U^{c})\\}\cup\\{\psi\ |\ D_{U}\psi\in\Gamma\\}$
is consistent, by the same reasoning as in the proof of the Truth Lemma. By
Lindenbaum’s Lemma, $\Delta^{-}$ can be extended to a maximal consistent set
$\Delta$. Moreover, $\Delta\sim_{U}\Gamma$ by construction, so
$U\subseteq\overline{\Delta}$. Also, as $\mathsf{dead}(U^{c})\in\Delta$,
$\overline{\Delta}\subseteq U$. Hence, $\overline{\Delta}=U$ and $\Delta$ is a
sub-world of $\Gamma$.

##### No empty worlds

By axiom $\mathbf{NE}$, maximality and consistency of any $\Gamma$, there is
an agent $a\in A$, such that $\mathsf{alive}(a)\in\Gamma$. It entails that
$a\in\overline{\Gamma}$.

##### Trivial empty-group knowledge

The canonical model $M^{c}$, however, does not have trivial empty-group
knowledge. Nevertheless, for every $\varphi_{0}$, we can extract a sub-model,
$M^{c}_{0}$, which consists of the set $\\{\Gamma\in M^{c}\ |\
\Gamma\sim_{\varnothing}\Gamma_{0}\\},$ where $\Gamma_{0}$ is some maximal
consistent theory that contains $\varphi_{0}$. By monotonicity of $\sim$, this
restriction preserves all worlds $U$-accessible from $\Gamma_{0}$ and
properties of $\sim$. Moreover, $M^{c}_{0}$ has trivial empty-group knowledge.
Thus, $\varphi_{0}$ holds in at $\Gamma_{0}$ in $M^{c}_{0}$, which is proper,
maximal, has no empty worlds and trivial empty-group knowledge. ∎

Inspecting the proof, one can see that the axioms and properties of the model
are pairwise independent. Hence, any combination of those axioms yields a
sound and complete axiom system for the corresponding class of models. Another
example, with minimal models:

######  Theorem 4.

The logic $\mathbf{EC_{n}}\mathbf{+NE+P}\mathbf{+Min}$ is sound and complete
with respect to proper minimal epistemic models with trivial empty-group
knowledge and no empty worlds.

###### Proof:

Call an epistemic that satisfies properties from the statement of the theorem
a good minimal model. The proof of all clauses, except the correspondence
between axiom $\mathbf{Min}$ and minimality, is the same as in Theorem 3. So
for soundness, let us show the validity of axiom $\mathbf{Min}$ in any good
minimal model. Consider a good minimal model $\mathcal{M}$ and a world
$w\in\mathcal{M}$. Assume that $\mathsf{alive}(U)\land\mathsf{dead}(U^{c})$
holds in $w$. It means that $\overline{w}$ is exactly $U$. Then by minimality
of $\mathcal{M}$, as $w$ is not a subworld of any other world, in any
$w^{\prime}$, such that $w\sim_{U}w^{\prime}$, we have
$\overline{w^{\prime}}=U$. Hence,
$\mathcal{M},w^{\prime}\models\mathsf{dead}(U^{c})$ and $\mathcal{M},w\models
D_{U}\mathsf{dead}(U^{c})$, so axiom $\mathbf{Min}$ is valid.

For completeness, it remains only to verify that the canonical model $M^{c}$
for this logic is minimal. Consider $\Gamma,\Delta\in M^{c}$, such that
$\overline{\Gamma}\subsetneq\overline{\Delta}$ and $\overline{\Gamma}=U$.
Suppose that $\Gamma\sim_{U}\Delta$. By Lemma 5,
$\mathsf{alive}(U)\land\mathsf{dead}(U^{c})$ belongs to $\Gamma$. By modus
ponens and axiom $\mathbf{Min}$, $D_{U}\mathsf{dead}(U^{c})$ is in $\Gamma$.
By definition of $\sim_{U}$, $\mathsf{dead}(U^{c})\in\Delta$. But
$\overline{\Delta}$ is strictly bigger than $U$, thus there $a\in U^{c}$ such
that $a\in\overline{\Delta}$, so $\mathsf{alive}(a)\in\Delta$ which
contradicts with consistency of $\Delta$. Thus, $\Gamma\not\sim_{U}\Delta$ as
required. ∎

For the case of pure models:

######  Theorem 5.

The logic $\mathbf{EC_{n}}\mathbf{+NE+P}\mathbf{+Pure}$ is sound and complete
with respect to proper pure epistemic models with trivial empty-group
knowledge and no empty worlds.

###### Proof:

Extending the previous theorem, for soundness we just need to check validity
of axiom $\mathbf{Pure}$ in a pure model. Take an epistemic model
$\mathcal{M}$ that has properties from the statement of the theorem. The
formula $\hat{D}_{U}\mathsf{true}$ holds in any world $w$ because $w\sim_{a}w$
as $\mathcal{M}$ is pure.

For completeness, we need to verify that the canonical model $M^{c}$ is pure.
As $\mathsf{alive}(A)$ is in any $\Gamma$ in $M^{c}$, by Lemma 5 we have
$\overline{\Gamma}=A$, so $M^{c}$ is pure. ∎

The relationship between all the axiom systems that we consider is summarized
in Figure 5.

scale=0.6
$w_{2}$$\\{a,b,c\\}$$w_{3}$$b$$\\{a,b,c\\}$$c$$w_{1}$$w_{4}$$w_{5}$$w^{\prime}_{1}$$w_{0}$$\\{a,b\\}$$\\{a,b\\}$$b$$b$$b$$\\{a,b\\}$$\varnothing$$\\{a,c\\}$$a$$a$$w_{2}$$w_{3}$$w_{0}$$w_{4}$$w_{1},w^{\prime}_{1}$$w_{5}$$w_{1}$$w_{1}^{\prime}$$w_{2}$$w_{3}$$w_{4}$$w_{5}$$w_{0}$$w_{0}$$w_{2}$$a,b$$\varnothing$$w_{1}$$\varnothing$$a,b$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a,b$$a,b$$a$$w_{0}$$w_{2}$$a,b$$w_{1}$$a$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a$$a$$b$$b$$w_{0}$$a,c$$w_{1}$$a$$a,b$$w_{0}$$a,b,c$$w_{1}$$b,c$$a,b,c$$w_{0}$$a,b$$w_{1}$$a$$a,b$$b$$w_{2}$$w_{0},w_{1}$$w_{2}$$w_{0},w_{1}$$w_{2}$$w_{0}$$w_{1}$$w_{1}$$w_{0}$$w_{2}$$w_{1}$$w_{0}$$w_{0}$$w_{1}$$w_{1}$$w_{0}$
$\mathrm{+Max}$ $\mathrm{+NE}$ $\mathrm{+Max}$ $\mathrm{+NE}$ $\mathrm{+P}$
$\mathrm{+Max}$ $\mathrm{+P}$ ${\mathrm{+Max}}$${\mathrm{+NE}}$ $\mathrm{+NE}$
$\mathrm{+P}$ ${{+\mathrm{P}}}$ $\mathrm{KB4}$ $\mathrm{+Mono}$
$\mathrm{+Union}$ $\mathrm{+Min}$ $\mathrm{+NE}$ $\mathrm{+Min}$
$\mathrm{+NE}$ $\mathrm{+P}$ $\mathrm{+Pure}$ $\mathrm{+NE}$ $\mathrm{+P}$
+$\mathrm{Min}$ $\mathrm{+P}$ ${{\mathrm{+Min}}}$

Figure 5: Variants of epistemic logic

###  V-D Standard group knowledge

The last property that we did not axiomatize is the standard group knowledge,
or, geometrically, the distinction between simplicial sets and simplicial
complexes. In this section, we show that restricting to simplicial complexes
does not require any additional axiom. For that purpose, we use a construction
called _unraveling_ , which turns a generalized epistemic frame $M$ into a new
frame $U(M)$ that is bisimilar to $M$ and has standard group knowledge.

Let $M$ be a generalized epistemic model. A _history_ in $M$ is a finite
sequence of the form $h=(w_{0},U_{1},w_{1},\dots,U_{k},w_{k})$ for some $k\geq
0$, such that $w_{i-1}\sim_{U_{i}}w_{i}$ for all $1\leq i\leq k$ and $U_{i}$
is a maximal such subgroup of agents. Notice that since epistemic models do
not necessarily have standard group knowledge, every pair of worlds
$w,w^{\prime}$ can have several groups $U$ maximal with respect to inclusion
such that $w\sim_{U}w^{\prime}$. For example, if $w\sim_{U}w^{\prime}$,
$w\sim_{U^{\prime}}w^{\prime}$ and both $U,U^{\prime}$ are maximal, then one
has, in particular, two different histories $(w,U,w^{\prime})$ and
$(w,U^{\prime},w^{\prime})$. We write $\mathsf{last}(h)=w_{k}$ for the last
element of a history, and we write $h\to_{U}h^{\prime}$ if
$h^{\prime}=(h,U,w_{k+1})$ with $U\subseteq U^{\prime}$.

######  Definition 12.

The _unraveling_ of $M$ is a generalized epistemic model
$U(M)=(H,\sim^{u},L^{u})$ defined as follows:

  * •

$H$ is the set of histories of $M$,

  * •

$\sim^{u}_{U}$ is the transitive and symmetric closure of $\rightarrow_{U}$,
i.e., $\sim^{u}_{U}\,=\left(\rightarrow_{U}\cup\leftarrow_{U}\right)^{*}$,

  * •

$L^{u}(h)=L(\mathsf{last}(h))$.

The unraveling construction is similar to the tree unraveling from [24],
adjusted to the case of multiple relations related by monotonicity.

######  Lemma 6.

Let $M$ be a generalized epistemic model. Then its unraveling $U(M)$ is a
generalized epistemic model.

###### Proof:

It is easy to see that every $\sim^{u}_{U}$ is a PER, as it is transitive and
symmetric closure. If $U\subseteq U^{\prime}$,
$\rightarrow_{U^{\prime}}\subseteq\rightarrow_{U}$ by definition, so
$\sim^{u}_{U^{\prime}}\subseteq\sim^{u}_{U}$, that is $\sim^{u}$ satisfies the
compatibility condition. Now, suppose that $h\sim^{u}_{U}h$ and
$h\sim^{u}_{U^{\prime}}h$. By definition of $\sim^{u}$, it means that there is
a sequence of worlds in $M$ such that
$\mathsf{last}(h)\sim_{U}\dots\sim_{U}\mathsf{last}(h)$, so, by transitivity
of $\sim_{U}$, $\mathsf{last}(h)\sim_{U}\mathsf{last}(h)$. Similarly,
$\mathsf{last}(h)\sim_{U^{\prime}}\mathsf{last}(h)$. As $M$ is a generalized
epistemic model, it follows that $\mathsf{last}(h)\sim_{U\cup
U^{\prime}}\mathsf{last}(h)$. Thus, there is a history $h^{\prime}=(h,U\cup
U^{\prime},\mathsf{last}(h))$, and $h\sim^{u}_{U\cup U^{\prime}}h^{\prime}$.
By transitivity and symmetry of $\sim^{u}_{U\cup U^{\prime}}$, we have
$h\sim^{u}_{U\cup U^{\prime}}h$, thus concluding that $U(M)$ is closed under
union of the groups of alive agents. ∎

######  Lemma 7.

For every model $M$, its unraveling $U(M)$ has standard group knowledge.

###### Proof:

We need to show that for any two $h,h^{\prime}$ in $U(M)$, if
$h\sim^{u}_{U}h^{\prime}$ and $h\sim^{u}_{U^{\prime}}h^{\prime}$, then
$h\sim^{u}_{U\cup U^{\prime}}h^{\prime}$. There are two cases: if
$h=h^{\prime}$ and $h\not=h^{\prime}$. For the first case, the statement holds
since $U(M)$ is a generalized epistemic model by Lemma 6.

For the second case, notice first that $\to_{V}$ respects the ordering of
histories with respect to the prefix relation: if $h\to_{V}h^{\prime}$, then
$h$ is a prefix of $h^{\prime}$. The prefix relation forms a tree on the set
of histories, and it implies that if $h\sim^{u}_{V}h^{\prime}$, then there is
a unique non-redundant path
$h\leftarrow_{V}\dots\leftarrow_{V}h^{\prime\prime}\rightarrow_{V}\dots\rightarrow_{V}h^{\prime}$
from $h$ to $h^{\prime}$ that witnesses it, where $h^{\prime\prime}$ is the
common prefix of $h$ and $h^{\prime}$. Moreover, this path is the same for any
$V\subseteq A$. We can write
$h=(h^{\prime\prime},V_{1},w_{1},\dots,V_{n},w_{n})$ and
$h^{\prime}=(h^{\prime\prime},V^{\prime}_{1},w^{\prime}_{1},\dots,V^{\prime}_{m},w_{m})$.
As it is the same path for both $U$ and $U^{\prime}$, $U\cup
U^{\prime}\subseteq V_{i}$ and $U\cup U^{\prime}\subseteq V^{\prime}_{j}$ for
all $i,j$. In particular, we have that $\mathsf{last}(h)=w_{n}\sim_{U\cup
U^{\prime}}\dots\sim_{U\cup
U^{\prime}}\mathsf{last}(h^{\prime\prime})\sim_{U\cup
U^{\prime}}\dots\sim_{U\cup
U^{\prime}}w^{\prime}_{m}=\mathsf{last}(h^{\prime})$. Thus, $h\sim^{u}_{U\cup
U^{\prime}}h^{\prime}$, and $U(M)$ has standard group knowledge. ∎

######  Remark 4.

In the proof we have also shown that if ${h\sim^{u}_{U}h^{\prime}}$, then
$\mathsf{last}(h)\sim_{U}\mathsf{last}(h^{\prime})$.

Given two generalized epistemic models $M,N$, we say that morphism $p:M\to N$
is a _functional bisimulation_ if the following conditions hold:

  * •

(atoms) for any $w\in M$, $L_{N}(f(w))=L_{M}(w)$;

  * •

(forth) for all $U\subseteq A$, if $w\sim^{M}_{U}w^{\prime}$, then
$f(w)\sim_{U}f(w^{\prime})$;

  * •

(back) for all $U\subseteq A$, if $f(w)\sim^{N}_{U}v^{\prime}$, then there is
$w^{\prime}\in M$ such that $f(w^{\prime})=v^{\prime}$ and
$w\sim^{M}_{U}w^{\prime}$.

The definition we give is an extension of the standard notion of bisimulation,
which links structural similarity of models with validity of formulas. In
particular, we have the following proposition by adapting the standard
construction (see [23]).

######  Proposition 2.

If $f:M\to N$ is a functional bisimulation, then for any formula $\varphi$, we
have that $M,w\models\varphi$ if and only if $N,f(w)\models\varphi$.

This is the essential proposition that allows us to show that
$\mathbf{EC_{n}}$ is sound and complete with respect to frames with standard
group knowledge.

######  Lemma 8.

For every generalized epistemic model $M$, its unraveling $U(M)$ is bisimilar
to $M$.

###### Proof:

We shall show that $\mathsf{last}:U(M)\to M$ is a functional bisimulation.
First, by the definition of $L^{u}$, $L^{u}(h)=L(\mathsf{last}(h))$, so the
atomic proposition are preserved.

Suppose now that $h\sim^{u}_{U}h^{\prime}$. By Remark 4,
$\mathsf{last}(h)\sim_{U}h^{\prime}$, so (forth) condition is satisfied.

For (back) condition, suppose that $\mathsf{last}(h)\sim_{U}w^{\prime}$. Then
there is a history $h^{\prime}=(h,U^{\prime},w^{\prime})$, such that
$U\subseteq U^{\prime}$. Clearly, $h\to_{U}h^{\prime}$, so
$h\sim^{u}_{U}h^{\prime}$, and the (back) condition holds too, thus concluding
that $\mathsf{last}:U(M)\to M$ is a bisimulation. ∎

######  Theorem 6.

The logic $\mathbf{EC_{n}}$ is sound and complete with respect to models with
standard group knowledge.

###### Proof:

Soundness is straightforward, as models with standard group knowledge are
generalized epistemic models in particular.

Consider the canonical model $M^{c}$ for $\mathbf{EC_{n}}$ from Theorem 2. It
is shown that $M^{c}$ is a generalized epistemic frame. By Lemma 6, $U(M^{c})$
is a generalized epistemic frame, and by Lemma 7 it has standard group
knowledge. For any formula $\varphi$, there is $\Gamma$ in $M^{c}$, such that
$M^{c},\Gamma\models\varphi$. Since $\mathsf{last}:U(M^{c})\to M^{c}$ is a
bisimulation by Lemma 8, for any $h\in U(M^{c})$ such that
$\mathsf{last}(h)=\Gamma$, we have $U(M^{c}),h\models\varphi$. Thus, any
formula $\varphi$ is valid in a model with classic group knowledge, which
concludes completeness. ∎

###  V-E Topological interpretation

The completeness result with respect to models with standard group knowledge
points us towards the study of expressivity of modal logic with respect to
topological properties of csets. In particular, a natural question is what
kind of similarity between csets is induced by a bisimulation? In this
subsection, we give a partial answer to this question.

Let us restrict our attention to good maximal epistemic models. By the
isomorphism we have shown, it is the same as to consider csets where every
simplex is a unique world. Let $\alpha:X\to Y$ be a functional bisimulation.
We can translate the definition of a bisimulation in terms of epistemic
coverings: it means that the valuation of a simplex $s\in X$ coincides with
the valuation of its image $\alpha(s)\in Y$; if two simplices $s,s^{\prime}$
in $X$ have a common $U$-subsimplex, then $\alpha(s)$ and $\alpha(s^{\prime})$
have a common $U$-subsimplex; if $\alpha(s)$ has a common $U$-subsimplex with
$t^{\prime}$ in $Y$, then there is a simplex $s^{\prime}$ in $X$ that shares a
$U$-subsimplex with $s$, and $\alpha(s^{\prime})=t^{\prime}$. The second
condition is always satisfied by any morphism of csets. The last condition is
more interesting, as it can be interpreted as a certain type of _lifting
condition_ that is ubiquitous in topology. This point of view can be traced
back to [25].

Without giving a proof, we remark that the forgetful functor from csets to
simplicial sets (which just forgets colors of vertices) sends functional
bisimulations of csets with _unique_ lifting (corresponding to having a unique
simplex $s^{\prime}$ with $\alpha(s^{\prime})=t^{\prime}$ in the condition
above) to _simplicial coverings_ (see [26]). An example of such a bisimulation
that can be seen as a topological covering is depicted. It represents the
classical example of a covering of a circle by an infinite helix.

$w_{2}$$\\{a,b,c\\}$$w_{3}$$b$$\\{a,b,c\\}$$c$$w_{1}$$w_{4}$$w_{5}$$w^{\prime}_{1}$$w_{0}$$\\{a,b\\}$$\\{a,b\\}$$b$$b$$b$$\\{a,b\\}$$\varnothing$$\\{a,c\\}$$a$$a$$w_{2}$$w_{3}$$w_{0}$$w_{4}$$w_{1},w^{\prime}_{1}$$w_{5}$$w_{1}$$w_{1}^{\prime}$$w_{2}$$w_{3}$$w_{4}$$w_{5}$$w_{0}$$w_{0}$$w_{2}$$a,b$$\varnothing$$w_{1}$$\varnothing$$a,b$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a,b$$a,b$$a$$w_{0}$$w_{2}$$a,b$$w_{1}$$a$$a,b$$w_{0}$$w_{2}$$a,b$$w_{1}$$a$$a$$b$$b$$w_{0}$$a,c$$w_{1}$$a$$a,b$$w_{0}$$a,b,c$$w_{1}$$b,c$$a,b,c$$w_{0}$$a,b$$w_{1}$$a$$a,b$$b$$w_{2}$$w_{0},w_{1}$$w_{2}$$w_{0},w_{1}$$w_{2}$$w_{0}$$w_{1}$$w_{1}$$w_{0}$$w_{2}$$w_{1}$$w_{0}$$w_{0}$$w_{1}$$w_{1}$$w_{0}$

##  VI Conclusions and future work

We have introduced a very general class of epistemic models based on
generalized epistemic frames, and their geometric counterpart based on
simplicial sets, epistemic covering models. These models subsume many variants
of simplicial models found in the literature. We made good use of this
generality by establishing a close connection between properties of the models
and axioms of the logic. This yields soundness and completeness for a variety
of logics (Fig. 5).

A notable fact that we prove is that every model based on simplicial sets is
equivalent modulo bisimulation to a model based on simplicial complexes. This
unveils interesting geometric considerations: epistemic modal logics do not
distinguish simplicial sets from their coverings because of the local nature
of the knowledge operators. Could we define a logic that is able to capture
better the global geometry of the model?

In future work, we aim at putting these logics in action for, in particular,
distributed computing applications such as in e.g. [3, 4, 27, 7], and bridge
the gap between the geometric interpretations [28] of distributed problems
such as sensor networks, as touched upon in Example 2, with their logical
interpretations.

## References

  * [1] R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi, _Reasoning About Knowledge_. Cambridge, MA, USA: MIT Press, 2003.
  * [2] M. Herlihy, D. Kozlov, and S. Rajsbaum, _Distributed Computing Through Combinatorial Topology_. Francisco, CA, USA: Morgan Kaufmann, 2013.
  * [3] É. Goubault, J. Ledent, and S. Rajsbaum, “A simplicial complex model for dynamic epistemic logic to study distributed task computability,” _Inf. Comput._ , vol. 278, 2021.
  * [4] H. v. Ditmarsch, É. Goubault, J. Ledent, and S. Rajsbaum, “Knowledge and simplicial complexes,” in _Philosophy of Computing_ , B. Lundgren and N. A. Nuñez Hernández, Eds., vol. 143. Springer 2022, p. 1–50.
  * [5] H. van Ditmarsch, É. Goubault, M. Lazic, J. Ledent, and S. Rajsbaum, “A dynamic epistemic logic analysis of equality negation and other epistemic covering tasks,” _J. Log. Algebraic Methods Program._ , vol. 121, 2021.
  * [6] K. Yagi and S. Nishimura, “Logical obstruction to set agreement tasks for superset-closed adversaries,” _CoRR_ , vol. abs/2011.13630, 2020.
  * [7] S. Nishimura, “Proving unsolvability of set agreement task with epistemic mu-calculus,” _CoRR_ , vol. abs/2205.06452, 2022.
  * [8] J. Y. Halpern and Y. Moses, “Knowledge and common knowledge in a distributed environment,” _J. ACM_ , vol. 37, no. 3, pp. 549–587, 1990.
  * [9] É. Goubault, J. Ledent, and S. Rajsbaum, “A simplicial model for KB4_n: Epistemic logic with agents that may die,” in STACS 2022, 2022, p. 33:1–33:20.
  * [10] H. van Ditmarsch, “Wanted dead or alive: Epistemic logic for impure simplicial complexes,” in _WoLLIC 2021_ , Lecture Notes in Computer Science, vol. 13038. Springer, 2021, pp. 31–46.
  * [11] R. F. Randrianomentsoa, H. van Ditmarsch, and R. Kuznets, “Impure simplicial complexes: Complete axiomatization,” _CoRR_ , vol. abs/2211.13543, 2022.
  * [12] C. Dwork and Y. Moses, “Knowledge and common knowledge in a byzantine environment: Crash failures,” _Inf. Comput._ , vol. 88, no. 2, pp. 156–186, 1990.
  * [13] J. Gerbrandy, “Distributed knowledge,” in _Formal Semantics and Pragmatics of Dialogue_ , vol. 98, 1998, pp. 111–124.
  * [14] A. Baltag and S. Smets, “Learning what others know,” in _LPAR 2020_ : EPiC Series in Computing, vol. 73, 2020, pp. 90–119.
  * [15] ——, “Correlated Knowledge: An Epistemic-Logic View on Quantum Entanglement,” vol. 49, no. 12, pp. 3005–3021.
  * [16] J. Garson, “Modal Logic,” in _The Stanford Encyclopedia of Philosophy_ , Summer 2021 ed., E. N. Zalta, Ed. Metaphysics Research Lab, Stanford University, 2021.
  * [17] P. Goerss and J. Jardine, _Simplicial Homotopy Theory_ , ser. Modern Birkhäuser Classics. Birkhäuser Basel, 2009.
  * [18] J. May, _Simplicial Objects in Algebraic Topology_ , ser. Chicago Lectures in Mathematics. University of Chicago Press, 1993.
  * [19] G. Friedman, “An elementary illustrated introduction to simplicial sets,” 2008, V7 25 May 2021.
  * [20] J. C. Baez and A. E. Hoffnung, “Convenient categories of smooth spaces,” 2008\.
  * [21] S. Eilenberg and J. A. Zilber, “Semi-simplicial complexes and singular homology,” _Annals of Mathematics_ , pp. 499–513, 1950.
  * [22] E. Riehl, “A leisurely introduction to simplicial sets.”
  * [23] P. Blackburn, M. de Rijke, and Y. Venema, _Modal Logic_ , ser. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press.
  * [24] H. Sahlqvist, “Completeness and Correspondence in the First and Second Order Semantics for Modal Logic,” in _Studies in Logic and the Foundations of Mathematics_ , Elsevier, vol. 82, pp. 110–143.
  * [25] A. Joyal, M. Nielsen, and G. Winskel, “Bisimulation from Open Maps,” vol. 127, no. 2, pp. 164–185.
  * [26] P. Gabriel and M. Zisman, _Calculus of Fractions and Homotopy Theory_ , Ergebnisse Der Mathematik Und Ihrer Grenzgebiete. 2. Folge. Springer-Verlag.
  * [27] É. Goubault, M. Lazic, J. Ledent, and S. Rajsbaum, “Wait-free solvability of equality negation tasks,” in _33rd International Symposium on Distributed Computing, DISC 2019, October 14-18, 2019, Budapest, Hungary_ , LIPIcs, J. Suomela, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019, pp. 21:1–21:16.
  * [28] P. Dlotko, R. Ghrist, M. Juda, and M. Mrozek, “Distributed computation of coverage in sensor networks by homological methods,” _Applicable Algebra in Engineering, Communication and Computing_ , 2012.