TU Wien<EMAIL_ADDRESS>by
the Austrian Science Fund (FWF) ByzDEL project (P33600). Open University of
the Netherlands0000-0003-4526-8687 TU Wien,
<EMAIL_ADDRESS>by the Austrian Science Fund
(FWF) ByzDEL project (P33600). Rojo Fanamperana Randrianomentsoa, Hans van
Ditmarsch, and Roman Kuznets

# Impure Simplicial Complexes:
Complete Axiomatization

Rojo Fanamperana Randrianomentsoa  Hans van Ditmarsch  Roman Kuznets

###### Abstract

Combinatorial topology is used in distributed computing to model concurrency
and asynchrony. The basic structure in combinatorial topology is the
simplicial complex, a collection of subsets called simplices of a set of
vertices, closed under containment. Pure simplicial complexes describe message
passing in asynchronous systems where all processes (agents) are alive,
whereas impure simplicial complexes describe message passing in synchronous
systems where processes may be dead (have crashed). Properties of impure
simplicial complexes can be described in a three-valued multi-agent epistemic
logic where the third value represents formulas that are undefined, e.g., the
knowledge and local propositions of dead agents. In this work we present the
axiomatization called $\mathsf{S5}^{\bowtie}$ and show that it is sound and
complete for the class of impure complexes. The completeness proof involves
the novel construction of the canonical simplicial model and requires a
careful manipulation of undefined formulas.

###### keywords:

Simplicial complexes, completeness, canonical model, epistemic logic

##  1 Introduction

In this contribution, we present an axiomatization called
$\mathsf{S5}^{\bowtie}$ for an epistemic logic and show that it is sound and
complete for the class of structures known as impure simplicial complexes. Not
surprisingly given its name, $\mathsf{S5}^{\bowtie}$ is a variant of the well-
known multi-agent epistemic logic $\mathsf{S5}$ [22]. And in view of that, it
may not come as a complete surprise that impure simplicial complexes, a notion
from distributed computing [18], correspond to certain multi-agent Kripke
models [10, 15], the usual vehicle to interpret knowledge on. Impure complexes
model that agents (or processes) may have crashed, in other words, may not be
alive but dead. A live agent may be uncertain whether other agents are dead or
alive but may wish to reason about them regardless. In [10] (extending [5]),
it was argued that for a dead agent it should be undefined what it knows or
does not know. This requires a three-valued logical semantics for the
knowledge modality $K_{a}$ (for ‘agent $a$ knows that’) and, consequently, a
variation of the standard axiomatization $\mathsf{S5}$ wherein, for example,
the normality axiom K, i.e.,
$K_{a}(\varphi\rightarrow\psi)\rightarrow(K_{a}\varphi\rightarrow K_{a}\psi)$,
and modus ponens MP, i.e., “from $\varphi$ and $\varphi\rightarrow\psi$, infer
$\psi$,” do not always hold. Still — we do not wish to put off the reader too
much at this stage — the usual three properties of knowledge, i.e., veracity,
positive introspection, and negative introspection, are valid in this three-
valued semantics. In [10], this semantics was extensively motivated. However,
no complete axiomatization was given. The underlying work is a follow-up
investigation providing that axiomatization, and only that, and nothing else.
In order to make the work self-contained we first sketch the area and the
results already obtained in the literature.

### Knowledge and complexes

Combinatorial topology [18] has been used in distributed computing to model
concurrency and asynchrony since [13, 24, 4], with higher-dimensional
topological properties entering the picture in [20, 29]. The basic structure
in combinatorial topology is the _simplicial complex_ , a collection of
subsets called _simplices_ of a set of _vertices_ , closed under containment.
Geometric manipulations such as subdivision have natural combinatorial
counterparts.

Epistemic logic investigates knowledge and belief, and change of knowledge and
belief, in multi-agent systems. A foundational study is [22]. Knowledge change
was extensively modeled in temporal epistemic logics [28, 16, 11] and in
dynamic epistemic logics [2, 9, 26].

A vertex of a complex represents the local state of an agent or process. Given
a complex, an agent may be uncertain about the local state of other agents.
This happens when a vertex for this agent is contained in different simplices
that contain vertices for the other agents but for different local states of
those agents. Similarly, higher-dimensional topological properties involve
higher-order knowledge or group knowledge. There is, therefore, a natural
relation between epistemic reasoning and simplicial complexes.

An epistemic logic interpreted on _pure_ simplicial complexes (i.e., where all
processes are alive) was proposed in [23, 14], which was finalized in [7]. It
is axiomatized by the multimodal logic $\mathsf{S5}$ augmented with the so-
called _locality axiom_ stating that all agents know their local state, i.e.,
$K_{a}p_{a}\vee K_{a}\neg p_{a}$ for all agents $a$ and local variables
$p_{a}$ for that agent.

Common knowledge and distributed knowledge were also considered in these
works, and even the application of novel group epistemic notions such as
common distributed knowledge [3] to the setting of simplicial semantics,
exactly in view of describing higher-dimensional topological properties (for
example, whether a complex is a manifold) [23, 8].

The dynamics of knowledge was another focus of those works and of additional
works [27, 7, 30]: the action models of [2] can be used to model distributed
computing tasks and algorithms. Action models even appeared in combinatorial
topological incarnations as simplicial complexes in [23] and in [8].
Additionally, [30] proposed novel dynamic objects called communication
patterns that represent arbitrary message exchange and are based on similar
proposals in dynamic epistemics [1, 3]. Communication patterns are different
from action models, and their relation is complex.

Pure complexes and their temporal development describe _asynchronous_ systems.
All processes then remain potentially active (alive), even when they have
crashed: in asynchronous systems [20] crashed processes can be modeled as
being infinitely slow. In _synchronous_ systems [19] crashed processes can be
identified — for example, in message passing, with timeouts. This makes it
possible to use _impure_ simplicial complexes, wherein some processes are
dead, to represent them. For a detailed example, see [18, Sect. 13.5.2].
Impure simplicial complexes are considerably smaller in terms of their number
of faces.

Epistemic logics interpreted on impure simplicial complexes were proposed in
[5], of which the extended version, henceforth the only cited one, is
[10],111All statements from [10] we rely on are also present and proved in
[5], unless stated otherwise. and also in [15].

In [10], a three-valued modal logical semantics was proposed for an epistemic
logical language interpreted in faces of impure simplicial complexes that are
decorated with agents and with local propositional variables. The third value
stands for ‘undefined.’ The following are undefined:

  * •

dead processes cannot know or be ignorant of any proposition;

  * •

live processes cannot know or be ignorant of factual propositions involving
processes they know to be dead.

The issue of the definability of formulas has to be handled with care:
standard notions such as validity, equivalence, and the interdefinability of
dual modalities and non-primitive propositional connectives have to be
properly addressed. The epistemic modality is a three-valued version of
$\mathsf{S5}$ knowledge. No complete axiomatization was given in [10].

In [15], a different, classical two-valued modal logical semantics was
proposed, also interpreted in impure simplicial complexes. The authors reduce
the setting to one where processes may not know their local state, and that
can then be treated in standard multi-agent modal logic: they axiomatize the
logic as multimodal $\mathsf{KB4}$. At the workshop CELT2022,222See workshop
website https://easychair.org/cfp/CELT2022. exciting further developments of
this framework were presented: namely, distributed knowledge modalities
interpreted on simplicial sets (also known as pseudo-complexes), a
generalization of simplicial complexes wherein a face may have multiple
occurrences (see [21], or, in the present context, [23, Sect. 3.7] and [8,
Example 25]).

The works [10, 15] also showed that, whereas pure complexes correspond to
Kripke models with equivalence relations, impure complexes correspond to
Kripke models with partial equivalence relations (symmetric and transitive
relations that need not be reflexive).

The novel epistemic notions proposed for impure complexes are akin to
knowledge but are, therefore, not exactly $\mathsf{S5}$ knowledge. Consider
the T axiom $K_{a}\varphi\rightarrow\varphi$. It is an axiom in
$\mathsf{S5}^{\bowtie}$ (and in [10]) but its meaning is ‘known formulas
cannot be false’ rather than ‘known formulas must be true’ (because they may
be undefined instead). T is not an axiom in $\mathsf{KB4}$ [15], but,
conveniently, in that work $K_{a}\bot$ denotes that ‘agent $a$ is dead.’
Various other synchronous and asynchronous epistemic notions have been
proposed in distributed computing, relating in yet other ways to modal logics
of knowledge and belief. We recall ‘belief as defeasible knowledge’ of [25],
knowledge in interpreted systems of [12, 16], distinctions between knowledge
and belief presented in [17], and encoding byzantine faults through the hope
modality, an epistemic notion weaker than belief [6], among others.

### Examples of pure complexes and corresponding Kripke models

Some of our readers may be familiar with simplicial complexes, while other
readers may be familiar with Kripke models. As the correspondence between
these semantic structures has only recently been proposed [7], we provide some
simple examples illustrating how.

Figure 1 depicts some pure simplicial complexes and corresponding Kripke
models:

$1_{b}$$0_{b}$$1_{c}$$1_{c}$$0_{a}$ | $1_{b}$$0_{b}$$1_{c}$$0_{a}$ | $1_{b}$$1_{c}$$0_{a}$
---|---|---
$0_{a}1_{b}1_{c}$$0_{a}0_{b}1_{c}$$a$ | $0_{a}1_{b}1_{c}$$0_{a}0_{b}1_{c}$$ac$ | $0_{a}1_{b}1_{c}$
Figure 1: Pure simplicial complexes and corresponding Kripke models

These simplicial complexes are for three agents $a$, $b$, and $c$. The
vertices of a simplex are required to be labeled, or colored, with different
agents. Therefore, a maximum size simplex, called _facet_ , consists of three
vertices, described as having _dimension $2$_. These are the triangles in the
figure. For two agents we get lines/edges, for four agents we get tetrahedra,
etc. In the figure, the vertices are not named, to simplify the exposition. A
label like $0_{a}$ on a vertex represents that it is a vertex for agent $a$
and that agent $a$’s local state has value $0$, etc. We can see this as the
boolean value of a local proposition, where $0$ means false and $1$ means
true. In other figures (where the value of a proposition is irrelevant) we may
only provide agent labels or vertex names. Simplicial complexes where vertices
are decorated with agents and with propositions will later be called
simplicial _models_.

The Kripke models are also defined for three agents. The states that are
indistinguishable for agent $a$ are connected by an $a$-labeled link; in other
words, for each agent we assume reflexivity, transitivity, and symmetry of the
usual accessibility relations.

A triangle corresponds to a world or state in a three-agent Kripke model.
Together the local states of the triangle determine the (global) state of the
Kripke model, and the values of the local state variables together determine
the valuation in that global state. For example, in states labeled
$0_{a}1_{b}1_{c}$ in Fig. 1 agent $a$’s value is $0$, $b$’s is $1$, and $c$’s
is $1$. The single triangle corresponds to the singleton $\mathcal{S}5$ model
below it. With two triangles, if they intersect only in an $a$-colored vertex,
i.e., are _$a$ -adjacent_, it means that agent $a$ cannot distinguish these
states (as in the corresponding Kripke model), making $a$ uncertain about the
value of $b$. If the triangles intersect in two vertices colored $a$ and $c$,
both $a$ and $c$ are uncertain about the value of $b$.

The current state of the distributed system is represented by a distinguished
facet of the simplicial complex, just as we need a distinguished state in a
Kripke model in order to evaluate propositions. For example, in the leftmost
triangle, as well as in the leftmost state/world, the value of $b$ is $1$ but
$a$ is uncertain whether the value of $b$ is $0$ or $1$. In other words, $a$
does not _know_ whether the value of $b$ is $0$ or $1$. In the same triangle,
$b$ knows that its value is $1$ and all three agents know that the value of
$c$ is $1$.

### Examples of impure complexes and corresponding Kripke models

We continue with several examples of impure complexes, also in relation to
pure complexes we have already seen above. They are depicted in Fig. 2. See
[18, Sect. 13.5.2] for a standard example of an impure simplicial complex from
distributed computing.

$1_{b}$$1_{b}$$1_{c}$$0_{a}$ | $1_{b}$$0_{b}$$1_{c}$$0_{a}$ | $1_{b}$$1_{c}$$0_{a}$
---|---|---
$ab$$abc$$0_{a}1_{b}0_{c}$$0_{a}1_{b}1_{c}$$a$ | $ab$$ac$$0_{a}1_{b}0_{c}$$0_{a}0_{b}1_{c}$$a$ | $0_{a}1_{b}1_{c}$$abc$
Figure 2: Impure simplicial complexes and corresponding Kripke models

The pure complex on the right encodes that all agents know local states of
each other, just as in the same complex on the right of Fig. 1. It is merely
here for comparison.

The impure complex on the left of Fig. 2 encodes that agent $a$ is uncertain
whether agent $c$ is alive. When agent $c$ is dead, in the edge, it does not
have a value and propositions like ‘agent $c$ knows that $p_{b}$ is true’ are
undefined. When agent $c$ is alive, in the triangle, its local variable
$p_{c}$ is true. We, therefore, say that agent $a$ knows that $p_{c}$ is true:
whenever agent $c$ is alive and, therefore, local variable $p_{c}$ is defined
(namely, in the triangle) it is true.

The impure complex in the middle encodes that agent $a$ is uncertain whether
$b$ or $c$ has crashed. Agent $a$ no longer considers it possible that all
processes are alive. In this case, agent $a$ knows that $p_{b}$, justified by
the edge $1_{b}$—$0_{a}$ (where $b$ is alive) and agent $a$ also knows that
$p_{c}$, justified by the edge $0_{a}$—$1_{c}$ (where $c$ is alive). However,
pointedly, agent $a$ does not know that $p_{b}\wedge p_{c}$: for that to be
true we would need a triangle wherein $a$, $b$, and $c$ are all alive. This
example demonstrates that $K_{a}\varphi\wedge K_{a}\psi$ does not imply
$K_{a}(\varphi\wedge\psi)$.

Below the complexes we find the corresponding Kripke models. In this
visualization, the upper indices to a state make explicit who is alive in this
state. It is merely a depiction of models with symmetric and transitive
relations, also known as _partial equivalence relations_. Such a relation is a
partial equivalence in the sense that it is an equivalence relation when
restricted to the worlds where it is not empty, i.e., in our terms, where the
agent is alive.

In the Kripke model on the left, as $c$ is dead in the $0_{a}1_{b}0_{c}$ world
and alive in the $0_{a}1_{b}1_{c}$ world, the relation for agent $c$ is
restricted to the reflexive arrow from $0_{a}1_{b}1_{c}$ to itself. The Kripke
model representation, unlike the impure simplicial complex, contains
superfluous information: even though $c$ is dead in the world
$0_{a}1_{b}0_{c}$, local variable $p_{c}$ is false there. Therefore, another
representation of the same impure complex is the model $0_{a}1_{b}1_{c}$
$\overset{a}{\text{---{}---}}$ $0_{a}1_{b}1_{c}$, where again $c$ is dead in
$0_{a}1_{b}1_{c}$.

Similarly, in the Kripke model in the middle, $c$ is dead on the left and $b$
is dead on the right. Accordingly, there are four different Kripke models
corresponding to the simplicial complex above it.

These are some examples of pure and impure complexes, and how they are used to
model agents’ reasoning about each other.

### Our results

We present a complete axiomatization $\mathsf{S5}^{\bowtie}$ for a three-
valued epistemic semantics interpreted on impure complexes. It has some
notable differences from the standard multi-agent axiomatization
$\mathsf{S5}$, such as non-standard axioms $\mathbf{K}^{\bowtie}$ and
$\mathbf{K\widehat{K}}$ instead of $\mathbf{K}$ and a non-standard derivation
rule $\mathbf{MP}^{\bowtie}$ instead of $\mathbf{MP}$. Some technical features
of the completeness proof may be considered novelties of interest. First,
instead of a canonical Kripke model, we construct a canonical model that is a
canonical simplicial complex. Second, the faces of this canonical simplicial
complex are not maximal consistent sets, but what we call _definability-
maximal consistent sets_ : they need not be maximal and may be contained in
one another, just like the faces of simplicial complexes in general.

### Outline

Section 2 recalls the impure simplicial semantics of [10] and obtains
additional results for formula definability that are crucial in this three-
valued setting. Section 3 presents the axiomatization $\mathsf{S5}^{\bowtie}$.
Section 4 shows that this axiomatization is sound, and Sect. 5 that it is
complete. Section 6 describes some remarkable features of the simplicial
canonical model. Section 7 concludes. Some of the proofs are relegated to
Appendix B, with Appendix A providing auxiliary statements used exclusively in
these proofs.

##  2 Impure Simplicial Models and Definability

We recall the semantics of simplicial complexes from [10], both pure (for
fault-free systems) and impure (for systems where byzantine failures are
restricted to crashes).

We consider a finite set $A$ of _agents_ (or _processes_) $a,b,\dots$ and a
set $P=\bigsqcup_{a\in A}P_{a}$ of _propositional_ _variables_ where sets
$P_{a}$ are countable and mutually disjoint sets of _local variables for agent
$a$_, denoted $p_{a},q_{a},p^{\prime}_{a},q^{\prime}_{a},\dots$333We sometimes
use $\sqcup$ instead of $\cup$ to emphasize that this is a union of mutually
disjoint sets. Similarly, we use $\subseteq$ for inclusion and $\subset$ for
proper inclusion, but may use $\subsetneq$ to emphasize the inclusion
properness. As usual in combinatorial topology, the number $|A|$ of agents is
taken to be $n+1$ for some $n\in\mathbb{N}$, so as to make the dimension of a
simplicial complex (to be defined below), which is one less than the number of
agents, equal to $n$.

######  Definition 2.1 (Language).

The _language of epistemic logic_ is defined by the grammar
$\varphi\coloncolonequals p_{a}\mid\neg\varphi\mid(\varphi\land\varphi)\mid
K_{a}\varphi$ where $a\in A$ and $p_{a}\in P_{a}$.

Parentheses will be omitted unless confusion results. Connectives
$\rightarrow$, $\leftrightarrow$, and $\lor$ are defined by abbreviation as
usual, as well as $\widehat{K}_{a}\varphi:=\neg K_{a}\neg\varphi$. Expression
$K_{a}\varphi$ stands for ‘agent $a$ knows (that) $\varphi$,’ and
$\widehat{K}_{a}\varphi$ stands for ‘agent $a$ considers (it possible that)
$\varphi$.’

######  Definition 2.2 (Simplicial model).

A _simplicial model_ $\mathcal{C}$ is a triple $(C,\chi,\ell)$ consisting of:

  * •

A _(simplicial) complex_ $C\neq\varnothing$ is a collection of _simplices_
that are non-empty finite subsets of a given set $\mathcal{V}$ of vertices
such that $C$ is downward closed (i.e., $X\in C$ and $\varnothing\neq
Y\subseteq X$ imply $Y\in C$). Simplices represent partial global states of a
distributed system.

  * •

It is required that every vertex form a simplex by itself, i.e.,
$\bigl{\\{}\\{v\\}\mid v\in\mathcal{V}\bigr{\\}}\subseteq C$.

  * •

Vertices represent local states of agents, with a _chromatic map_
$\chi\colon\mathcal{V}\to A$ assigning each vertex to one of the agents in
such a way that each agent has at most one vertex per simplex (i.e.,
$\chi(v)=\chi(u)$ for some $v,u\in X\in C$ implies that $v=u$). For $X\in C$,
we define $\chi(X)\colonequals\\{\chi(v)\mid v\in X\\}$ to be the set of
agents in simplex $X$.

  * •

A _valuation_ $\ell\colon\mathcal{V}\to 2^{P}$ assigns to each vertex which
local variables of the vertex’s owner are true in it, i.e., $\ell(v)\subseteq
P_{a}$ whenever $\chi(v)=a$. Variables from $P_{a}\setminus\ell(v)$ are false
in vertex $v$, whereas variables from $P\setminus P_{a}$ do not belong to
agent $a$ and cannot be evaluated in $a$’s vertex $v$. All variables true in a
simplex $X\in C$ are determined by $\ell(X)\colonequals\bigsqcup_{v\in
X}\ell(v)$.

If $Y\subseteq X$ for $X,Y\in C$, we say that $Y$ is a _face_ of $X$. Since
each simplex is a face of itself, we use ‘simplex’ and ‘face’ interchangeably.
A face $X$ is a _facet_ if it is a maximal simplex in $C$, i.e., $Y\in C$ and
$Y\supseteq X$ imply $Y=X$. Facets represent global states of the distributed
system, and their set is denoted $\mathcal{F}(C)$. The _dimension of a
simplex_ $X$ is $|X|-1$, e.g., vertices are of dimension $0$, edges are of
dimension $1$, etc. The _dimension of a simplicial complex (model)_ is the
largest dimension of its facets. A simplicial complex (model) is _pure_ if all
facets have dimension $n$, i.e., contain vertices for all agents. Otherwise it
is _impure_. A  _pointed simplicial model_ is a pair $(\mathcal{C},X)$ where
$X\in C$.

######  Remark 2.3.

It follows from the above definition that for any simplicial complex $C$, its
set of vertices $\mathcal{V}=\bigcup_{X\in C}X$. Thus, it is not necessary to
specify $\mathcal{V}$ when defining a complex $C$ or a simplicial model
$\mathcal{C}=(C,\chi,\ell)$ based on this complex. Further, a complex $C$ can
be computed from the set $\mathcal{F}(C)$ of its facets by taking the downward
closure with respect to non-empty sets. Thus, we typically forgo defining
$\mathcal{V}$ explicitly and often specify $\mathcal{F}(C)$ instead of $C$.

######  Remark 2.4.

Due to the chromatic-map condition, $|X|\leq n+1$ for all faces $X$ of a
complex and, hence, each face is contained in a facet.

######  Remark 2.5.

It has been common in the literature, including in [10], to consider a more
expansive view of pure simplicial models requiring all the facets to have the
same dimension, rather than the largest possible dimension as we require here.
We believe that the distinction based on the presence of dead agents is more
meaningful than the previously used distinction based on the stability of the
number of dead agents. Indeed, it is the presence of dead agents that poses
the question of what dead agents know. And, as we will see, it is the presence
of dead agents rather than fluctuations of their numbers that separates the
logic of impure simplicial models from the the standard epistemic logic. In
particular, both counterexamples to modus ponens from [10] (not present in
[5]) and in the proof of Lemma 3.3 involve simplicial models with all facets
of the same dimension but with at least one dead agent per facet.

Since simplicial models are an alternative semantics for epistemic logic, it
is useful to understand their relationship to Kripke models. (Global) states
of a Kripke model correspond to facets of a simplicial model. Vertices
represent local states, and, hence, have no direct Kripke representation.
However, they play a crucial role in the simplicial variant of
indistinguishability. Where two Kripke states are indistinguishable for agent
$a$, their corresponding facets $X$ and $Y$ in a simplicial model must have
agent $a$ in the same local state, meaning that $X$ and $Y$ must share an
$a$-colored vertex, i.e., $a\in\chi(X\cap Y)$, and we call them _$a$
-adjacent_. We also apply $a$-adjacency to faces.

The special case of pure simplicial models (of the maximum dimension $n$)
corresponds to the standard epistemic logic $\mathsf{S5}_{n+1}$ (augmented
with the locality axiom to account for variables being local, as mentioned in
the introduction) and is a representation dual to epistemic Kripke models. As
noted in [10], however, the case of impure models introduces a new situation
where formulas may be undefined in a facet. Indeed, if $X$ is a facet with
$b\notin\chi(X)$, which represents a global state where agent $b$ has crashed,
then all local propositional variables of agent $b$ are considered undefined.
This imposes a two-tier system on formulas: one must first determine whether a
formula is defined, before one can probe whether it is true or false. Note
that we do not restrict these definitions to facets only.

######  Definition 2.6 (Definability).

Given a simplicial model $\mathcal{C}=(C,\chi,\ell)$ and its face $X\in C$,
the definability relation $\bowtie$ is defined by recursion on the formula
construction:

$\begin{array}[]{lll}\mathcal{C},X\bowtie p_{a}&\text{ if{f} }&a\in\chi(X);\\\
\mathcal{C},X\bowtie\lnot\varphi&\text{ if{f}
}&\mathcal{C},X\bowtie\varphi;\\\ \mathcal{C},X\bowtie\varphi\land\psi&\text{
if{f} }&\mathcal{C},X\bowtie\varphi\text{ and }\mathcal{C},X\bowtie\psi;\\\
\mathcal{C},X\bowtie K_{a}\varphi&\text{ if{f}
}&\mathcal{C},Y\bowtie\varphi\text{ for some }Y\in C\text{ with
}a\in\chi(X\cap Y).\end{array}$

######  Definition 2.7 (Truth).

Given a simplicial model $\mathcal{C}=(C,\chi,\ell)$ and its face $X\in C$,
the truth relation $\vDash$ is defined by recursion on the formula
construction:

$\begin{array}[]{lll}\mathcal{C},X\vDash p_{a}&\text{ if{f}
}&p_{a}\in\ell(X);\\\ \mathcal{C},X\vDash\lnot\varphi&\text{ if{f}
}&\mathcal{C},X\bowtie\lnot\varphi\text{ and }\mathcal{C},X\nvDash\varphi;\\\
\mathcal{C},X\vDash\varphi\land\psi&\text{ if{f}
}&\mathcal{C},X\vDash\varphi\text{ and }\mathcal{C},X\vDash\psi;\\\
\mathcal{C},X\vDash K_{a}\varphi&\text{ if{f} }&\mathcal{C},X\bowtie
K_{a}\varphi\text{ and }\\\ &&C,Y\vDash\varphi\text{ for all }Y\in C\text{
such that }a\in\chi(X\cap Y)\text{ and
}\mathcal{C},Y\bowtie\varphi.\end{array}$

######  Remark 2.8.

These definitions are equivalent to those from [10], but differ from them as
follows:

  * •

$K_{a}$ is used as the primary connective instead of $\widehat{K}_{a}$ in
[10], which is harmless in light of the duality of $K_{a}$ and
$\widehat{K}_{a}$.

  * •

In [10], $\mathcal{C},X\vDash p_{a}$ additionally requires that $a\in\chi(X)$,
which is redundant because $\ell(X)\cap P_{a}=\varnothing$ if
$a\notin\chi(X)$.

  * •

In [10], $\mathcal{C},X\vDash\lnot\varphi$ requires
$\mathcal{C},X\bowtie\varphi$ instead of the equivalent
$\mathcal{C},X\bowtie\lnot\varphi$ here.

These modifications are primarily to avoid the necessity of changing the
axiomatization of $\mathsf{S5}$ in order to ensure the Replacement Property in
the language based on a $\Diamond$-like modality.

One of the design choices made is that undefined formulas do not have truth
values.444The next few results are from [10], but are reproved here for the
language.

######  Lemma 2.9.

For a simplicial model $\mathcal{C}=(C,\chi,\ell)$, its face $X\in C$, and
formula $\varphi$:

$\mathcal{C},X\vDash\varphi$ $\Longrightarrow$ $\mathcal{C},X\bowtie\varphi$.

$\mathcal{C},X\vDash\lnot\varphi$ $\Longrightarrow$
$\mathcal{C},X\bowtie\varphi$.

It cannot be that both $\mathcal{C},X\vDash\varphi$ and
$\mathcal{C},X\vDash\lnot\varphi$.

######  Proof 2.10.

The proof is by induction on the construction of $\varphi$. For
$\varphi=\lnot\psi$ and $\varphi=K_{a}\psi$, the statement follows directly
from Def. 2.7. If $\mathcal{C},X\vDash p_{a}$, then $p_{a}\in\ell(X)$, hence,
$a\in\chi(X)$, meaning that $\mathcal{C},X\bowtie p_{a}$. If
$\mathcal{C},X\vDash\psi\land\theta$, then $\mathcal{C},X\vDash\psi$ and
$\mathcal{C},X\vDash\theta$. By the induction hypothesis,
$\mathcal{C},X\bowtie\psi$ and $\mathcal{C},X\bowtie\theta$, hence,
$\mathcal{C},X\bowtie\psi\land\theta$.

If $\mathcal{C},X\vDash\lnot\varphi$, then $\mathcal{C},X\bowtie\lnot\varphi$
by clause (2.9). Hence, $\mathcal{C},X\bowtie\varphi$ by Def. 2.6.

This follows directly from Def. 2.7.

Thus, for $\mathcal{C}=(C,\chi,\ell)$, $X\in C$, and $\varphi$, there can be
three mutually exclusive outcomes:

If $\mathcal{C},X\vDash\varphi$, we say that _$\varphi$ is true in $X$_;

If $\mathcal{C},X\not\bowtie\varphi$, we say that _$\varphi$ is undefined in
$X$_, due to crashes;

If $\mathcal{C},X\bowtie\varphi$ and $\mathcal{C},X\nvDash\varphi$, i.e.,
$\mathcal{C},X\vDash\lnot\varphi$, we say that _$\varphi$ is false in $X$_.

The following is easy to obtain from Defs. 2.6 and 2.7 and the abbreviation
$\widehat{K}_{a}\varphi\colonequals\lnot K_{a}\lnot\varphi$.

######  Corollary 2.11.

For a simplicial model $\mathcal{C}=(C,\chi,\ell)$, its face $X\in C$, formula
$\varphi$, and agent $a$:

$\mathcal{C},X\bowtie\widehat{K}_{a}\varphi$ iff $\mathcal{C},Y\bowtie\varphi$
for some $Y\in C$ such that $a\in\chi(X\cap Y)$, i.e., the definability
conditions for $\widehat{K}_{a}\varphi$ and $K_{a}\varphi$ are the same;

$\mathcal{C},X\vDash\widehat{K}_{a}\varphi$ iff $\mathcal{C},Y\vDash\varphi$
for some $Y\in C$ such that $a\in\chi(X\cap Y)$;

$\mathcal{C},X\vDash K_{a}\varphi$ iff

  * •

$\mathcal{C},Y\vDash\varphi$ for some $Y\in C$ such that $a\in\chi(X\cap Y)$
and

  * •

$\mathcal{C},Z\vDash\varphi$ whenever $\mathcal{C},Z\bowtie\varphi$ for any
$Z\in C$ such that $a\in\chi(X\cap Z)$;

$\mathcal{C},X\vDash\lnot K_{a}\varphi$ iff $\mathcal{C},Y\vDash\lnot\varphi$
for some $Y\in C$ such that $a\in\chi(X\cap Y)$.

Definability and truth for other boolean connectives are even easier to
derive. In particular, $\varphi\lor\psi$, $\varphi\to\psi$, and
$\varphi\leftrightarrow\psi$ are defined iff $\varphi\land\psi$ is, i.e., when
both $\varphi$ and $\psi$ are defined.

The proof of the following monotonicity properties from [10] applies as is:

######  Lemma 2.12 (Monotonicity, [10]).

For a simplicial model $\mathcal{C}=(C,\chi,\ell)$, its faces $X,Y\in C$ such
that $X\subseteq Y$, and formula $\varphi$:

$\mathcal{C},X\bowtie\varphi$ $\Longrightarrow$ $\mathcal{C},Y\bowtie\varphi$.

$\mathcal{C},X\vDash\varphi$ $\Longrightarrow$ $\mathcal{C},Y\vDash\varphi$.

$\mathcal{C},Y\vDash\varphi$ and $\mathcal{C},X\bowtie\varphi$
$\Longrightarrow$ $\mathcal{C},X\vDash\varphi$.

Since the standard _modus ponens_ rule is not valid for impure simplicial
models [10] (this result is not present in [5]), the rule has to be weakened
based on the notion of _definability consequence_ that is similar to logical
consequence but with definability in place of truth. Before we state the axiom
system for the logic of impure simplicial models, we formulate this notion and
list its relevant properties.

######  Definition 2.13 (Definability consequence).

A formula $\psi$ is a _definability consequence_ of a set $\Gamma$ of
formulas, notation $\Gamma\mathrel{\ltimes}\psi$, iff there exists a finite
subset $\Gamma^{\prime}\subseteq\Gamma$ such that for any simplicial model
$\mathcal{C}=(C,\chi,\ell)$ and its face $X\in C$,

$(\forall\varphi\in\Gamma^{\prime})\,\mathcal{C},X\bowtie\varphi\qquad\Longrightarrow\qquad\mathcal{C},X\bowtie\psi.$

To simplify notation we omit $\\{$ and $\\}$ for finite sets $\Gamma$, where
we assume w.l.o.g. that $\Gamma^{\prime}=\Gamma$. Note, in particular, that
$\varnothing\not\mathrel{\ltimes}\psi$ for any formula $\psi$. For a set
$\Delta$ of formulas, $\Gamma\mathrel{\ltimes}\Delta$ means that
$\Gamma\mathrel{\ltimes}\psi$ for all $\psi\in\Delta$. Formulas $\varphi$ and
$\psi$ are called _equidefinable_ , written $\varphi\bowtie\psi$, when both
$\varphi\mathrel{\ltimes}\psi$ and $\psi\mathrel{\ltimes}\varphi$.

######  Definition 2.14.

For a set $\Gamma$ of formulas and agent $a$, we define
$K_{a}\Gamma\colonequals\\{K_{a}\theta\mid K_{a}\theta\in\Gamma\\}$.

######  Lemma 2.15 (Properties of definability consequence).

For an agent $a$, propositional variable $p_{a}$, formulas
$\varphi,\psi,\theta,\psi_{1},\dots,\psi_{m}$, and formula sets $\Gamma$ and
$\Delta$:

$\Gamma\mathrel{\ltimes}\varphi$ $\Longrightarrow$
$\Gamma\cup\Delta\mathrel{\ltimes}\varphi$.

$\Gamma\mathrel{\ltimes}\Delta$ and $\Delta\mathrel{\ltimes}\varphi$
$\Longrightarrow$ $\Gamma\mathrel{\ltimes}\varphi$.

$K_{a}\varphi\mathrel{\ltimes}p_{a}$.

$p_{a}\bowtie K_{a}p_{a}$.

$K_{a}\varphi\bowtie K_{a}K_{a}\varphi$.

$K_{a}\varphi\bowtie\lnot K_{a}\varphi\bowtie K_{a}\lnot K_{a}\varphi$.

$K_{a}\theta,\varphi\mathrel{\ltimes}K_{a}\varphi$.

$K_{a}\Gamma,\varphi\mathrel{\ltimes}K_{a}\psi$ $\Longrightarrow$
$K_{a}\Gamma,K_{a}\varphi\mathrel{\ltimes}K_{a}\psi$.

$K_{a}\Gamma,\lnot\varphi\mathrel{\ltimes}K_{a}\psi$ $\Longrightarrow$
$K_{a}\Gamma,\lnot K_{a}\varphi\mathrel{\ltimes}K_{a}\psi$.

$K_{a}(K_{a}\psi_{1}\land\cdots\land K_{a}\psi_{m})\rightarrow
K_{a}\theta\quad\mathrel{\ltimes}\quad
K_{a}\bigl{(}K_{a}\psi_{1}\land\cdots\land
K_{a}\psi_{m}\rightarrow\theta\bigr{)}$.

$K_{a}(K_{a}\psi_{1}\land\cdots\land
K_{a}\psi_{m})\rightarrow\widehat{K}_{a}\theta\quad\mathrel{\ltimes}\quad
K_{a}\bigl{(}K_{a}\psi_{1}\land\cdots\land
K_{a}\psi_{m}\rightarrow\theta\bigr{)}$.

$K_{a}\psi_{1}\land\cdots\land K_{a}\psi_{m}\quad\bowtie\quad
K_{a}(K_{a}\psi_{1}\land\cdots\land K_{a}\psi_{m})$.

######  Proof 2.16.

The proofs are straightforward by using Def. 2.6 and can be found in Appendix
B. Here we only present a proof of clause (2.15) as a sample. Assume
$K_{a}\Gamma,\varphi\mathrel{\ltimes}K_{a}\psi$. It means that there is a
finite subset $\Gamma^{\prime}\subseteq K_{a}\Gamma\cup\\{\varphi\\}$ such
that $K_{a}\psi$ is defined in a face whenever all formulas from
$\Gamma^{\prime}$ are. If $\varphi\notin\Gamma^{\prime}$, then
$\Gamma^{\prime}\subseteq K_{a}\Gamma\subseteq
K_{a}\Gamma\cup\\{K_{a}\varphi\\}$, so we are done. Otherwise, this
$\Gamma^{\prime}=K_{a}\Theta\cup\\{\varphi\\}$ for some finite subset
$\Theta\subseteq\Gamma$. Consider an arbitrary simplicial model
$\mathcal{C}=(C,\chi,\ell)$ and its face $X\in C$ such that
$\mathcal{C},X\bowtie K_{a}\theta$ for all formulas $K_{a}\theta\in
K_{a}\Theta$ and $\mathcal{C},X\bowtie K_{a}\varphi$. The latter means that
there exists a face $Y\in C$ such that $a\in\chi(X\cap Y)$ and
$\mathcal{C},Y\bowtie\varphi$. It follows from the former that, for each
$K_{a}\theta\in K_{a}\Theta$, there exists a face $Z_{\theta}\in C$ such that
$a\in\chi(X\cap Z_{\theta})$ and $\mathcal{C},Z_{\theta}\bowtie\theta$. Since
$X$ cannot have two $a$-vertices, $a\in\chi(Y\cap Z_{\theta})$, making
$\mathcal{C},Y\bowtie K_{a}\theta$ for each $K_{a}\theta\in K_{a}\Theta$.
Recalling $\mathcal{C},Y\bowtie\varphi$, it follows from the assumption that
$\mathcal{C},Y\bowtie K_{a}\psi$. Therefore, there exists $U\in C$ such that
$a\in\chi(Y\cap U)$ and $\mathcal{C},U\bowtie\psi$. The uniqueness of the
$a$-vertex in $Y$ yields once again that $a\in\chi(X\cap U)$, hence,
$\mathcal{C},X\bowtie K_{a}\psi$. We have shown that $K_{a}\psi$ is defined in
a face whenever all formulas from the finite subset
$K_{a}\Theta\cup\\{K_{a}\varphi\\}\subseteq K_{a}\Gamma\cup\\{K_{a}\varphi\\}$
are. Hence, $K_{a}\Gamma,K_{a}\varphi\mathrel{\ltimes}K_{a}\psi$.

A closer observation of impure simplicial models uncovers several
peculiarities that affect not only the logic but also the notion of validity
and even the object language used.

For instance, if boolean constants $\top$ and $\bot$ are not chosen as primary
connectives, it is typically convenient and harmless to add them to the
language as abbreviations by choosing a (fixed but arbitrary) propositional
variable $p$ and using $p\lor\neg p$ for $\top$ and/or $p\land\neg p$ for
$\bot$. This works if $p$ is a global variable. In our agent-oriented
language, however, all propositional variables are local to some agent. Thus,
$p_{a}\lor\neg p_{a}$ is not going to be true in all face(t)s, as one would
expect from boolean constant $\top$. Instead, $p_{a}\lor\neg p_{a}$ is true
whenever agent $a$ is alive and undefined otherwise. We can use such a formula
at most as a local boolean constant $\top_{a}$, which cannot be false but need
not be true.

In fact, no formula is true in all face(t)s. For any formula $\varphi$, it is
not hard to construct a single-vertex simplicial model where $\varphi$ is
undefined. In other words, were we to define validity as truth in all face(t)s
of all models, the set of valid formulas would have been empty. On the other
hand, it is reasonable to consider $\top_{a}$ mentioned above valid in the
sense that it is never false. It is this notion of validity that we axiomatize
in this paper:

######  Definition 2.17 (Validity, [10]).

A formula $\varphi$ is valid in the class of impure simplicial models, written
$\vDash\varphi$, iff $\mathcal{C},X\vDash\varphi$ whenever
$\mathcal{C},X\bowtie\varphi$ for any face $X$ of any simplicial model
$\mathcal{C}$.

One might question why we define validity with respect to all faces even
though it is facets that represent global states. Fortunately, this point is
moot as the logic remains the same if the validity is restricted to facets.

######  Lemma 2.18 (Validity on facets).

A formula $\varphi$ is true in all facets of all impure simplicial models
where it is defined iff $\vDash\varphi$.

######  Proof 2.19.

The “if” direction trivially follows from Def. 2.17 as valid formulas are true
in all faces where they are defined, including all facets. For the “only if”
direction, assume that $\nvDash\varphi$, i.e., there exists a face $X$ of a
simplicial model $\mathcal{C}$ such that $\mathcal{C},X\bowtie\varphi$ but
$\mathcal{C},X\nvDash\varphi$, i.e., $\mathcal{C},X\vDash\neg\varphi$. By
Lemma 2.12(2.12), $\mathcal{C},Y\vDash\neg\varphi$ for any facet $Y\supseteq
X$. By Remark 2.4, such a facet exists. In this facet,
$\mathcal{C},Y\bowtie\varphi$ but $\mathcal{C},Y\nvDash\varphi$, meaning that
$\varphi$ is not valid with respect to facets either.

##  3 Axiom System $\mathsf{S5}^{\bowtie}$

The main goal of this paper is to provide a sound and complete axiomatization
for the notion of validity from Def. 2.17. Since pure simplicial models
correspond to Kripke models with equivalence accessibility relations, their
logic is an extension of multimodal $\mathsf{S5}$, the epistemic logic with
positively and negatively introspective knowledge (the extension deals with
the locality of propositional variables). The ability of agents to crash can
be reasonably expected to weaken the logic somewhat but one could still expect
some subsystem of $\mathsf{S5}$.

As we have discovered, the impact of dead agents and undefined formulas is
quite drastic and, interestingly, affects the core reasoning, both modal and
propositional, rather than the additional epistemic properties. Although these
results are from [10], we find it instructive to repeat the proofs found there
as it provides insight to the reader on why these axioms/rules are invalid in
their “usual” form.

Firstly, the _normality axiom_ K at the basis of all normal modal logics is
not valid even for the above weaker notion of validity:

######  Lemma 3.1 (Failure of normality, [10]).

In the presence of at least three agents, we have $\nvDash
K_{a}(\varphi\to\psi)\to(K_{a}\varphi\to K_{a}\psi).$

$0_{b}$$1_{b}$$1_{c}$$0_{a}$$Y$$X$$\mathcal{C}_{\mathbf{K}}:$ Figure 3:
Counterexample for the unrestricted axiom K

######  Proof 3.2.

Consider model $\mathcal{C}_{\mathbf{K}}$ with agents $a$, $b$, and $c$ in
Fig. 3. Let $\varphi=p_{c}$ and $\psi=p_{b}$. Model $\mathcal{C}_{\mathbf{K}}$
has only two facets, $X$ of dimension 1 and $Y$ of the maximal dimension 2.
The instance

$K_{a}(p_{c}\to p_{b})\to(K_{a}p_{c}\to K_{a}p_{b})$ (1)

of axiom K is defined in both facets because all formulas are defined in $Y$,
which is $a$-adjacent to all facets. In addition, $p_{c}$ is true wherever it
is defined, making $K_{a}p_{c}$ true in both facets. Similarly, $p_{c}\to
p_{b}$ is true wherever it is defined, i.e., wherever both $b$ and $c$ are
alive, because $p_{b}$ is only false in $X$ where $c$ is dead. This ensures
that $K_{a}(p_{c}\to p_{b})$ is true in both facets. At the same time,
$\mathcal{C}_{\mathbf{K}},X\vDash\neg p_{b}$ and, hence, $K_{a}p_{b}$ is false
in both facets. Thus, not only is instance (1) of axiom K falsified in this
model, but, in fact, its negation is valid in $\mathcal{C}_{\mathbf{K}}$.

Perhaps, even more surprisingly, even the _modus ponens_ MP rule, a staple of
most logics, does not generally preserve validity. In [10] (though not in
[5]), we presented a counterexample to this effect that involved four agents.
Here we offer a mild improvement and demonstrate that already for three
agents, MP does not preserve validity:

######  Lemma 3.3 (Failure of modus ponens).

In the presence of at least three agents, it is possible that
$\vDash\varphi\to\psi$ and $\vDash\varphi$, but $\nvDash\psi$.

######  Proof 3.4.

Let $\varphi=\top_{a}\land\top_{b}$ and
$\psi=\widehat{K}_{c}\widehat{K}_{a}\widehat{K}_{b}p_{c}\lor\widehat{K}_{c}\widehat{K}_{b}\widehat{K}_{a}\lnot
p_{c}$. We will show that

$\displaystyle\vDash\quad$ $\displaystyle{\top_{a}\land\top_{b}},$ (2)
$\displaystyle\vDash\quad$
$\displaystyle\top_{a}\land\top_{b}\rightarrow\widehat{K}_{c}\widehat{K}_{a}\widehat{K}_{b}p_{c}\lor\widehat{K}_{c}\widehat{K}_{b}\widehat{K}_{a}\lnot
p_{c}.$ (3)

To show that modus ponens does not preserve validity, consider simplicial
model $\mathcal{C}_{\mathbf{MP}}$ with agents $a$, $b$, and $c$ in Fig. 4,
which has six facets, all of non-maximal dimension $1$. To show that
$\nvDash\widehat{K}_{c}\widehat{K}_{a}\widehat{K}_{b}p_{c}\lor\widehat{K}_{c}\widehat{K}_{b}\widehat{K}_{a}\lnot
p_{c}$, we demostrate

$\mathcal{C}_{\textbf{MP}},X\vDash\quad\neg\left(\widehat{K}_{c}\widehat{K}_{a}\widehat{K}_{b}p_{c}\lor\widehat{K}_{c}\widehat{K}_{b}\widehat{K}_{a}\lnot
p_{c}\right).$

The validity of formula $\varphi$ in (2) immediately follows from our earlier
discussion that local boolean constants $\top_{e}\colonequals p_{e}\lor\neg
p_{e}$ cannot be falsified. Let us show that formula $\varphi\to\psi$ is
valid. Assume that $\varphi\to\psi$ is defined in a face $Q$ of a simplicial
model $\mathcal{C}$. This necessitates that agents $a$ and $b$ be alive due to
$\top_{a}$ and $\top_{b}$, as well as agent $c$ being alive due to modalities
$\widehat{K}_{c}$. In other words, $\varphi\to\psi$ is only defined in $Q$ if
$Q$ is a face with $a$, $b$, and $c$ all being alive. In particular, variable
$p_{c}$ is defined, i.e., is either true or false in $Q$. Since face $Q$ is
$a$-adjacent, $b$-adjacent, and $c$-adjacent to itself, if $p_{c}$ is true in
$Q$, so is $\widehat{K}_{c}\widehat{K}_{a}\widehat{K}_{b}p_{c}$, while if
$\lnot p_{c}$ is true in $Q$, so is
$\widehat{K}_{c}\widehat{K}_{b}\widehat{K}_{a}\lnot p_{c}$. This completes the
proof that
$\top_{a}\land\top_{b}\rightarrow\widehat{K}_{c}\widehat{K}_{a}\widehat{K}_{b}p_{c}\lor\widehat{K}_{c}\widehat{K}_{b}\widehat{K}_{a}\lnot
p_{c}$ is true whenever defined.

$a$$b$$0_{c}$$1_{c}$$a$$b$$c$$X$$Y$$W$$V$$Z$$U$$\mathcal{C}_{\textbf{MP}}:$
Figure 4: Counterexample for the unrestricted modus ponens

Let us now show that
$\psi=\widehat{K}_{c}\widehat{K}_{a}\widehat{K}_{b}p_{c}\lor\widehat{K}_{c}\widehat{K}_{b}\widehat{K}_{a}\lnot
p_{c}$ is invalidated in model $\mathcal{C}_{\mathbf{MP}}$. For the second
disjunct $\widehat{K}_{c}\widehat{K}_{b}\widehat{K}_{a}\lnot p_{c}$ evaluated
in facet $X$, out of three faces $c$-adjacent to $X$, i.e., $X$, $Y$, and
their common vertex, agent $b$ is alive only in $Y$, hence, the
definability/truth of $\widehat{K}_{c}\widehat{K}_{b}\widehat{K}_{a}\lnot
p_{c}$ in $X$ is fully determined by definability/truth of
$\widehat{K}_{b}\widehat{K}_{a}\lnot p_{c}$ in $Y$. Out of three faces
$b$-adjacent to $Y$, i.e., $Y$, $V$, and their common vertex, agent $a$ is
alive only in $V$, hence, the definability/truth of
$\widehat{K}_{b}\widehat{K}_{a}\lnot p_{c}$ in $Y$ is fully determined by
definability/truth of $\widehat{K}_{a}\lnot p_{c}$ in $V$. Out of three faces
$a$-adjacent to $V$, i.e., $V$, $U$, and their common vertex, $\lnot p_{c}$ is
defined only in $U$, hence, $\widehat{K}_{a}\lnot p_{c}$ is defined at $V$ and
its truth is fully determined by the truth of $\lnot p_{c}$ in $U$. Since
$\lnot p_{c}$ is false in $U$, it follows that $\widehat{K}_{a}\lnot p_{c}$ is
false in $V$, that $\widehat{K}_{b}\widehat{K}_{a}\lnot p_{c}$ is defined and
false in $Y$, and that $\widehat{K}_{c}\widehat{K}_{b}\widehat{K}_{a}\lnot
p_{c}$ is defined and false in $X$. The argument for the first disjunct is
similar, except the chain of faces there is $X$, followed by $X$, followed by
$W$, and finally followed by $Z$. In summary,
$\widehat{K}_{c}\widehat{K}_{a}\widehat{K}_{b}p_{c}\lor\widehat{K}_{c}\widehat{K}_{b}\widehat{K}_{a}\lnot
p_{c}$ is defined but false in $X$.

It is interesting to note that implication (3) is nowhere defined in
$\mathcal{C}_{\mathbf{MP}}$.

Intuitively, the failure of both K and MP can be attributed to the fact that
different instances of modality in impure simplicial models may have different
scope in terms of adjacent faces, which prevents the usual first-order
reasoning about the adjacency. One way to amend this is by imposing
definability restrictions so as to ensure the homogeneity of the scope of
modal operators.

######  Definition 3.5 (Axioms system $\mathsf{S5}^{\bowtie}$).

The axioms and rules of axiom system $\mathsf{S5}^{\bowtie}$ can be found
below (non-standard axioms are in the right column):

$\begin{array}[]{cl|cll}\mathbf{Taut}&\text{prop.
tautologies}&\mathbf{L}&K_{a}p_{a}\lor K_{a}\lnot p_{a}\\\
\mathbf{T}&K_{a}\varphi\rightarrow\varphi&\mathbf{K}^{\bowtie}&K_{a}(\varphi\rightarrow\psi)\rightarrow(K_{a}\varphi\rightarrow
K_{a}\psi)&\text{ where }\psi,K_{a}\varphi\mathrel{\ltimes}\varphi\\\
\mathbf{4}&K_{a}\varphi\rightarrow
K_{a}K_{a}\varphi&\mathbf{K\widehat{K}}&K_{a}(\varphi\rightarrow\psi)\rightarrow(K_{a}\varphi\rightarrow\widehat{K}_{a}\psi)\\\
\mathbf{5}&\lnot K_{a}\varphi\rightarrow K_{a}\lnot
K_{a}\varphi&\mathbf{MP}^{\bowtie}&\text{ from }\varphi\rightarrow\psi\text{
and }\varphi,\text{ infer }\psi&\text{ where }\psi\mathrel{\ltimes}\varphi\\\
\mathbf{N}&\text{ from }\varphi,\text{ infer }K_{a}\varphi\\\ \end{array}$

Thus, axiom system $\mathsf{S5}^{\bowtie}$ is obtained by

  * •

taking all axioms and rules of multimodal $\mathsf{S5}$ that are valid for
impure simplicial models (see the left column in Def. 3.5),

  * •

adopting the locality axiom L used for pure simplicial models,

  * •

restricting K and MP by imposing definability conditions, and

  * •

adding axiom $\mathbf{K\widehat{K}}$.

This last addition is needed for the completeness proof. Intuitively, it can
be explained by the dual universal–existential nature of modalities $K_{a}$.
In impure semantics, knowledge of $\varphi$ means both truth in _all_ adjacent
faces where $\varphi$ is defined (universal aspect) and truth in _at least
one_ adjacent face (existential aspect). Just like its unrestricted variant K,
axiom $\mathbf{K}^{\bowtie}$ deals only with the universal aspect. The new
axiom $\mathbf{K\widehat{K}}$ is needed to take care of the existential one.

##  4 Soundness

######  Definition 4.1 (Derivability in $\mathsf{S5}^{\bowtie}$).

A formula $\varphi$ is _derivable_ in $\mathsf{S5}^{\bowtie}$, written
$\vdash\varphi$, iff there is a finite sequence $\psi_{1},\dots,\psi_{k}$ of
formulas such that $\psi_{k}=\varphi$ and each formula in the sequence is
either an instance of one of the axioms in Def. 3.5 or follows from earlier
formulas in the sequence by one of the rules from Def. 3.5. A formula
$\varphi$ is derivable in $\mathsf{S5}^{\bowtie}$ from a set $\Gamma$ of
formulas, written $\Gamma\vdash\varphi$, iff either $\vdash\varphi$ or
$\vdash\bigwedge\Gamma_{0}\rightarrow\varphi$ for some finite non-empty subset
$\Gamma_{0}\subseteq\Gamma$.

######  Remark 4.2.

The proviso that $\Gamma_{0}\neq\varnothing$ and the special case for
derivations from the empty set are necessary due to the lack of boolean
constants in the language, which makes it problematic to interpret the empty
conjunction.

######  Theorem 4.3 (Soundness).

Axiom system $\mathsf{S5}^{\bowtie}$ is sound with respect to impure
simplicial models, i.e., $\vdash\varphi$ implies $\vDash\varphi$.

######  Proof 4.4.

The proof by induction on an $\mathsf{S5}^{\bowtie}$-derivation is standard:
one shows that all axioms are valid and all rules preserve validity. It has
already been shown in [10] that the locality axiom $\mathbf{L}$ and all axioms
from the left column of Def. 3.5 are valid and that the necessitation rule
$\mathbf{N}$ preserves validity. For the convenience of the readers, we
reproduce these proofs in Appendix B. Here we provide the argument for the
remaining two axioms and rule:

  * •

Axiom $\mathbf{K\widehat{K}}$ is valid. Consider an arbitrary simplicial model
$\mathcal{C}=(C,\chi,\ell)$ and its face $X\in C$. If one of formulas
$K_{a}(\varphi\rightarrow\psi)$ and $K_{a}\varphi$ is undefined, axiom
$\mathbf{K\widehat{K}}$ is undefined. If both formulas are defined but one of
them is false, $\mathbf{K\widehat{K}}$ is true. Finally, assume that
$\mathcal{C},X\vDash K_{a}(\varphi\rightarrow\psi)$ and $\mathcal{C},X\vDash
K_{a}\varphi$, Then, $\mathcal{C},X\bowtie K_{a}(\varphi\rightarrow\psi)$ by
Lemma 2.9(2.9), i.e., $\mathcal{C},Y\bowtie\varphi\rightarrow\psi$ for some
face $Y$ such that $a\in\chi(X\cap Y)$, where $\mathcal{C},Y\bowtie\varphi$
and $\mathcal{C},Y\bowtie\psi$ by the definition of $\bowtie$. Since both
$\varphi\to\psi$ and $\varphi$ are defined in $Y$, they must be true by our
assumptions, i.e., $\mathcal{C},Y\vDash\varphi\to\psi$ and
$\mathcal{C},Y\vDash\varphi$. Hence, $\mathcal{C},Y\vDash\psi$ and
$\mathcal{C},X\vDash\widehat{K}_{a}\psi$. We conclude that in this final case
again $\mathcal{C},X\vDash
K_{a}(\varphi\rightarrow\psi)\rightarrow(K_{a}\varphi\rightarrow\widehat{K}_{a}\psi)$.

  * •

Axiom $\mathbf{K}^{\bowtie}$ is valid provided
$\psi,K_{a}\varphi\mathrel{\ltimes}\varphi$. From now on, we omit all trivial
cases and assume that $\mathcal{C},X\vDash K_{a}(\varphi\rightarrow\psi)$ and
$\mathcal{C},X\vDash K_{a}\varphi$. As already shown for axiom
$\mathbf{K\widehat{K}}$, the former assumption implies that $\psi$ is defined
in some face $a$-adjacent to face $X$. It remains to show that $\psi$ is true
in all such $a$-adjacent faces where it is defined. Consider any face $Z$ such
that $a\in\chi(X\cap Z)$ and $\mathcal{C},Z\bowtie\psi$. Before we can apply
our assumptions to $Z$, we have to make sure that both $\varphi\to\psi$ and
$\varphi$ are defined in $Z$ using the definability provision of
$\mathbf{K}^{\bowtie}$. $\mathcal{C},X\vDash K_{a}\varphi$ means that
$\varphi$ is defined in at least one face $Y$ $a$-adjacent to $X$. But $Y$
being $a$-adjacent to $X$ is equivalent to $Y$ being $a$-adjacent to $Z$
because $a\in\chi(X\cap Z)$. Hence, $\mathcal{C},Z\bowtie K_{a}\varphi$.
Therefore, provision $\psi,K_{a}\varphi\mathrel{\ltimes}\varphi$ ensures that
$\mathcal{C},Z\bowtie\varphi$ and, consequently,
$\mathcal{C},Z\bowtie\varphi\to\psi$. Now we can use the assumptions to obtain
$\mathcal{C},Z\vDash\varphi$ and $\mathcal{C},Z\vDash\varphi\to\psi$, meaning
that $\mathcal{C},Z\vDash\psi$. This concludes the proof that
$\mathcal{C},X\vDash K_{a}\psi$ and, hence, of the validity of
$\mathbf{K}^{\bowtie}$.

  * •

Rule $\mathbf{MP}^{\bowtie}$ preserves validity provided
$\psi\mathrel{\ltimes}\varphi$. We assume that $\vDash\varphi\to\psi$ and
$\vDash\varphi$ and need to show that $\psi$ is true whenever defined. The
definability provision means that $\varphi$ is defined whenever $\psi$ is,
hence, so is $\varphi\to\psi$. Their validity means that $\varphi$ and
$\varphi\to\psi$ are true whenever $\psi$ is defined, and from that we
conclude that $\psi$ is true whenever it is defined.

######  Remark 4.5.

While all the standard epistemic axioms are valid, the meaning of this
validity sometimes defies the usual intuitions. For instance, axiom T is often
called the _factivity of knowledge_ and normally states that whatever is known
must be true. This interpretation is, however, too strong for impure
simplicial models and is not entailed by the validity $\vDash
K_{a}\varphi\to\varphi$. Indeed, for model $\mathcal{C}_{\mathbf{K}}$ from
Fig. 3, $\mathcal{C}_{\mathbf{K}},X\vDash K_{a}p_{c}$ even though formula
$p_{c}$ is undefined rather than true in facet $X$. In our three-valued
semantics, the validity of T means ‘known facts cannot be false’ rather than
‘known facts must be true.’ In this context, perhaps, it is better described
as the _veracity of knowledge_. This is why we may still see logic
$\mathsf{S5}^{\bowtie}$ as an epistemic logic (see [10] for an extensive
discussion on the epistemic interpretation).

In preparation for the completeness proof, we now illustrate how the impurity
and its associated definability restrictions affect standard modal (and
propositional) reasoning techniques, relegating most of the proofs to Appendix
B.

######  Lemma 4.6 (Hypothetical syllogism).

$\displaystyle\frac{\vdash\varphi\rightarrow\psi\hskip
28.45274pt\vdash\psi\rightarrow\rho}{\vdash\varphi\rightarrow\rho}$ is
derivable if $\varphi\rightarrow\rho\mathrel{\ltimes}\psi$.

######  Proof 4.7.

  1. 1.

$(\varphi\rightarrow\psi)\rightarrow\bigl{(}(\psi\rightarrow\rho)\rightarrow(\varphi\rightarrow\rho)\bigr{)}$
tautology

  2. 2.

$\varphi\rightarrow\psi$ derivable by assumption

  3. 3.

$\psi\rightarrow\rho$ derivable by assumption

  4. 4.

$(\psi\rightarrow\rho)\rightarrow(\varphi\rightarrow\rho)$ MP⋈(1.,2.) as
$(\psi\rightarrow\rho)\rightarrow(\varphi\rightarrow\rho)\mathrel{\ltimes}\varphi\rightarrow\psi$

  5. 5.

$\varphi\rightarrow\rho$ MP⋈(3.,4.) as
$\varphi\rightarrow\rho\mathrel{\ltimes}\psi$ and, hence,
$\varphi\rightarrow\rho\mathrel{\ltimes}\psi\rightarrow\rho$

######  Lemma 4.8 (Contraposition).

$\displaystyle\frac{\vdash\varphi\rightarrow\psi}{\vdash\lnot\psi\rightarrow\lnot\varphi}$
is derivable.

######  Lemma 4.9 (Replacement for $K_{a}$).

$\displaystyle\frac{\vdash\varphi\rightarrow\psi}{\vdash
K_{a}\varphi\rightarrow K_{a}\psi}$ is derivable if
$\psi,K_{a}\varphi\mathrel{\ltimes}\varphi$.

######  Lemma 4.10.

$\vdash K_{a}\varphi\land K_{a}\psi\to K_{a}(\varphi\land\psi)$. But $\nvdash
K_{a}(\varphi\land\psi)\to K_{a}\varphi\land K_{a}\psi$.

As desired, in this logic, agents know the truth value of their local
variables:

######  Lemma 4.11.

$\vdash p_{a}\rightarrow K_{a}p_{a}$ and $\vdash\lnot p_{a}\rightarrow
K_{a}\lnot p_{a}$.

######  Proof 4.12.

  1. 1.

$K_{a}p_{a}\to p_{a}$ axiom T

  2. 2.

$\lnot p_{a}\rightarrow\lnot K_{a}p_{a}$ Lemma 4.8(1.)

  3. 3.

$K_{a}p_{a}\lor K_{a}\lnot p_{a}$ axiom L

  4. 4.

$(K_{a}p_{a}\lor K_{a}\lnot p_{a})\rightarrow(\lnot K_{a}p_{a}\rightarrow
K_{a}\lnot p_{a})$ tautology

  5. 5.

$\lnot K_{a}p_{a}\rightarrow K_{a}\lnot p_{a}$ MP⋈(3.,4.) as $\lnot
K_{a}p_{a}\rightarrow K_{a}\lnot p_{a}\mathrel{\ltimes}K_{a}p_{a}\lor
K_{a}\lnot p_{a}$

  6. 6.

$\lnot p_{a}\rightarrow K_{a}\lnot p_{a}$ Lemma 4.6(2.,5.) as $\lnot
p_{a}\rightarrow K_{a}\lnot p_{a}\mathrel{\ltimes}\lnot K_{a}p_{a}$

This derives the second formula. The first one can be derived analogously.

######  Theorem 4.13 (Deduction theorem).

If $\Gamma,\varphi\vdash\psi$, then $\Gamma\vdash\varphi\rightarrow\psi$.

The following three lemmas, proved in Appendix B, are used in the completeness
proof:

######  Lemma 4.14.

$\vdash K_{a}\psi_{1}\land\cdots\land K_{a}\psi_{m}\rightarrow
K_{a}(K_{a}\psi_{1}\land\cdots\land K_{a}\psi_{m})$ for $m\geq 1$.

######  Lemma 4.15.

$\displaystyle\frac{\vdash\lnot(\varphi\land K_{a}\psi_{1}\land\cdots\land
K_{a}\psi_{m})}{\vdash\lnot(K_{a}\varphi\land K_{a}\psi_{1}\land\cdots\land
K_{a}\psi_{m})}$ is derivable for $m\geq 1$.

######  Lemma 4.16.

$\displaystyle\frac{\vdash\lnot(\lnot\varphi\land
K_{a}\psi_{1}\land\cdots\land K_{a}\psi_{m})}{\vdash\lnot(\lnot
K_{a}\varphi\land K_{a}\psi_{1}\land\cdots\land K_{a}\psi_{m})}$ is derivable
for $m\geq 1$.

##  5 Completeness via the Canonical Simplicial Model

In this section, we present the novel construction of the canonical
_simplicial_ model. Our main challenge was that the standard canonical
_Kripke_ model construction, based on maximal consistent sets, builds the
canonical model out of Kripke worlds representing global states, whereas a
simplicial model is built from vertices representing local states, i.e.,
agents’ view of the world.

Before giving the technical account of the necessary changes and a proof of
completeness, we explain the chosen construction on the structural level. To
do that, we briefly recall how standard canonical Kripke models are
constructed and used to prove completeness. A canonical model
$\mathcal{M}^{C}$ for a given logic can be viewed as a universal countermodel,
in the sense that any formula that can be refuted in some world $w$ of some
Kripke model $\mathcal{M}$ can also be refuted in a world of the canonical
model $\mathcal{M}^{C}$. To this effect, for any world $w$ of any Kripke model
$\mathcal{M}$, there is a world in the canonical model that assigns exactly
the same truth values as $w$, which is achieved by using the set
$\Gamma_{\mathcal{M},w}\colonequals\\{\varphi\mid\mathcal{M},w\vDash\varphi\\}$
of formulas true at world $w$ of Kripke model $\mathcal{M}$ as a world in the
canonical model. In fact, the domain of the canonical model consists of all
sets $\Gamma_{\mathcal{M},w}$ over all models $\mathcal{M}$ and worlds $w$.
Note that in the binary boolean semantics the set $\Gamma_{\mathcal{M},w}$ of
formulas true in $w$ provides a complete description of all truth values in
$w$: the set of formulas false in $w$ is $\overline{\Gamma_{\mathcal{M},w}}$,
the complement of the set of true formulas.

The completeness proof is achieved by combining these syntactic objects (sets
of formulas) — via an appropriate valuation and accessibility relations — into
a Kripke model in such a way that semantic truth can be reduced to syntactic
membership. This reduction is termed the _Truth Lemma_ and states that a
formula $\varphi$ is true at a world $\Gamma$ of the canonical model iff
$\varphi\in\Gamma$. Again, the syntactic criterion for falsity at a world of
the canonical model easily follows:

$\text{a formula $\varphi$ is false at a world
$\Gamma$}\qquad\Longleftrightarrow\qquad\varphi\notin\Gamma\qquad\Longleftrightarrow\qquad\lnot\varphi\in\Gamma.$
(4)

Of course, building a model from all worlds of the class of all Kripke models
would have been unwieldy, especially given that all $\Gamma_{\mathcal{M},w}$
are subsets of the set of all formulas, making the set of worlds of the
canonical model a subset of the power set of the set of all formulas. Instead,
the canonical model is built of _maximal consistent sets_ that are
syntactically consistent with respect to the given axiomatization, whereas the
condition of maximality ensures that a set is maximally consistent iff it is
equal to $\Gamma_{\mathcal{M},w}$ for some Kripke model $\mathcal{M}$ and
world $w$.

Our construction of the canonical _simplicial_ model below adapts these ideas
to the semantics of impure simplicial complexes. At first, it might seem that,
unlike in the binary case, knowing the set of formulas that are true would not
be sufficient to represent the distribution of our three truth values. How
would we be able to distinguish formulas that are false from those that are
undefined? Fortunately, it is possible to do by separating the two
descriptions of falsity in (4), which were equivalent in the binary semantics.
In our three-valued case, we will formulate the truth lemma to associate true
formulas with formulas in $\Gamma$, false formulas with formulas _whose
negation_ is in $\Gamma$, with all remaining formulas, i.e., formulas
$\varphi$ such that both $\varphi\notin\Gamma$ and $\lnot\varphi\notin\Gamma$,
undefined. This enables us to continue building the canonical model out of
sets of formulas rather than pairs of sets or some such.

The next hurdle is that such sets of formulas represent a possible
distribution of three truth values in a global state, whereas we need to find
a syntactic representation of local states for each agent $a$. There are two
immediate candidates for formulas belonging to $a$: propositional variables
$p_{a}\in P_{a}$ and knowledge assertions $K_{a}\varphi$. We will show that
the latter are sufficient to describe the local state of $a$ and, hence, each
$a$-colored vertex in our canonical simplicial model will be a set
$K_{a}\Gamma$ of formulas of the form $K_{a}\varphi$. Accordingly, each face
in the canonical simplicial model will be a finite set
$X=\\{K_{a_{1}}\Gamma,K_{a_{2}}\Gamma,\dots,K_{a_{m}}\Gamma\\}$ of sets
$K_{a_{i}}\Gamma$ of knowledge assertions for distinct agents
$a_{1},a_{2},\dots,a_{m}$ in a global state $\Gamma$, and the whole canonical
simplicial model will be a set of such finite sets $X$, supplied with
appropriate valuation and coloring functions.

In the logic of impure simplicial models, it is possible to restore the global
state $\Gamma$ from the collection $X_{\Gamma}$ of local states
$K_{a_{1}}\Gamma,K_{a_{2}}\Gamma,\dots,K_{a_{m}}\Gamma$ for all agents
$a_{1},a_{2},\dots,a_{m}$ alive in $\Gamma$.

There is one final piece of the puzzle before we begin the formal part of the
proof. As discussed above, in the boolean case, _maximal_ consistent sets
represent all possible truth sets across all worlds of all Kripke models. We
need to do the same for all facets of all impure simplicial models, and it is
clear that the absolute maximality condition is too strong for that. In Kripke
models, adding any formula to a truth set of a given world would make the set
inconsistent. If, however, agent $a$ is dead in a given facet, then adding a
propositional variable $p_{a}\in P_{a}$ to the set of formulas true in this
facet need not lead to inconsistency. There may well be another facet where
$a$ is alive and some previously undefined formulas, including $p_{a}$, are
true there. (It is also possible that adding $p_{a}$ does lead to
inconsistency if, i.e., $K_{b}\lnot p_{a}$ is present in the given truth set.)
In our canonical model construction, we replace maximal consistent sets with
maximal consistent subsets of definability-complete sets.

######  Definition 5.1 (Definability completeness).

A set $\Xi\neq\varnothing$ is _definability complete_ iff it contains all its
definability consequences, i.e., if $\varphi\in\Xi$ whenever
$\Xi\mathrel{\ltimes}\varphi$.

To streamline proofs and avoid the reliance on $\Xi$ as an extra parameter, we
use a more direct description of maximal consistent subsets of such $\Xi$’s as
_sets that determine all their definability consequences_.

######  Definition 5.2 (Being determined).

A formula $\varphi$ is _determined_ by a set $\Gamma$ of formulas, written
$\varphi\in^{*}\Gamma$, iff either $\varphi\in\Gamma$ or
$\lnot\varphi\in\Gamma$. Accordingly, a formula is _not determined_ , written
$\varphi\notin^{*}\Gamma$, iff
$\Gamma\cap\\{\varphi,\lnot\varphi\\}=\varnothing$.

######  Definition 5.3 (Consistent sets).

A set $\Gamma$ of formulas is _inconsistent_ iff
$\vdash\lnot\bigwedge\Gamma_{0}$ for some finite
$\varnothing\neq\Gamma_{0}\subseteq\Gamma$. Otherwise, $\Gamma$ is
_consistent_. In particular, $\varnothing$ is consistent.

######  Remark 5.4.

The non-standard requirement $\Gamma_{0}\neq\varnothing$ is due to the lack of
boolean constants.

######  Definition 5.5 (Definability-maximal consistent (DMC) sets).

A consistent set $\Gamma\neq\varnothing$ is _definability maximal (a DMC set)_
iff it determines all its definability consequences:

$\Gamma\mathrel{\ltimes}\varphi\qquad\Longrightarrow\qquad\varphi\in^{*}\Gamma.$
(5)

The following facts, proved in Appendix B, are standard for classical
propositional reasoning but need to be reaffirmed here due to our weaker
version of modus ponens.

######  Lemma 5.6 (Monotonicity of $\vdash$).

For formulas $\varphi$ and $\psi$ and a finite set $\Gamma\neq\varnothing$ of
formulas:

If $\vdash\lnot\bigwedge\Gamma$, then
$\vdash\lnot\left(\varphi\land\bigwedge\Gamma\right)$.

If $\vdash\bigwedge\Gamma\to\psi$, then
$\vdash\varphi\land\bigwedge\Gamma\to\psi$.

Let us justify the term _definability maximal_ by showing that DMC sets are
exactly maximal consistent subsets of definability-complete sets:

######  Lemma 5.7.

For any consistent set $\Gamma\neq\varnothing$, the following statements are
equivalent:

$\Gamma$ is a DMC set;

$\Gamma$ is maximal among consistent subsets of some definability-complete set
$\Xi$.

######  Proof 5.8.

$\eqref{DMC_one}\Longrightarrow\eqref{DMC_two}$. Let $\Gamma$ be a DMC set,
i.e., let (5) hold. We start by showing that set
$\Xi\colonequals\\{\varphi\mid\Gamma\mathrel{\ltimes}\varphi\\}$ is
definability complete. Indeed, if $\Xi\mathrel{\ltimes}\psi$, then
$\Gamma\mathrel{\ltimes}\psi$ by Lemma 2.15(2.15), and $\psi\in\Xi$ by
construction. Since $\Gamma\mathrel{\ltimes}\psi$ for any $\psi\in\Gamma$,
clearly $\Gamma\subseteq\Xi$, in particular, $\Xi\neq\varnothing$. It remains
to show that $\Gamma$ is maximal among consistent subsets of $\Xi$. Suppose,
towards a contradiction, that $\Gamma\cup\\{\psi\\}$ were consistent for some
$\psi\in\Xi\setminus\Gamma$. Then $\psi\notin\Gamma$ but
$\Gamma\mathrel{\ltimes}\psi$, which, due to (5), would imply that
$\lnot\psi\in\Gamma$. But then $\vdash\lnot(\psi\land\lnot\psi)$ for
$\\{\psi,\lnot\psi\\}\subseteq\Gamma\cup\\{\psi\\}$, contradicting the
supposition of consistency for this set. The contradiction shows that $\Gamma$
is maximal among consistent subsets of the definability-complete set $\Xi$.

$\eqref{DMC_two}\Longrightarrow\eqref{DMC_one}$. Let $\Xi$ be a definability-
complete set, $\Gamma$ be maximal among consistent subsets of $\Xi$, and let
$\Gamma\mathrel{\ltimes}\varphi$. Then there is some finite subset
$\Gamma_{0}\subseteq\Gamma$ such that $\varphi$ is defined whenever all
formulas from $\Gamma_{0}$ are. Since $\Gamma_{0}\subseteq\Gamma\subseteq\Xi$,
we have $\Xi\mathrel{\ltimes}\varphi$. Since $\varphi\bowtie\lnot\varphi$,
also $\Xi\mathrel{\ltimes}\lnot\varphi$. Due to the definability completeness
of $\Xi$, it means that $\\{\varphi,\lnot\varphi\\}\subseteq\Xi$. Suppose
towards a contradiction that $\varphi\notin\Gamma$ and
$\lnot\varphi\notin\Gamma$. Due to the maximality of $\Gamma$ among consistent
subsets of $\Xi$, it would mean that both $\Gamma\cup\\{\varphi\\}$ and
$\Gamma\cup\\{\lnot\varphi\\}$ would be inconsistent. In view of Lemma
5.6(5.6), w.l.o.g.,
$\vdash\lnot\bigl{(}\varphi\land\bigwedge\Gamma_{0}\land\bigwedge\Gamma_{1}\bigr{)}$
and
$\vdash\lnot\bigl{(}\lnot\varphi\land\bigwedge\Gamma_{0}\land\bigwedge\Gamma_{2}\bigr{)}$
for some non-empty finite subsets $\Gamma_{1},\Gamma_{2}\subseteq\Gamma$. The
following is a propositional tautology:

$\vdash\lnot\bigl{(}\varphi\land\bigwedge\Gamma_{0}\land\bigwedge\Gamma_{1}\bigr{)}\to\left(\lnot\bigl{(}\lnot\varphi\land\bigwedge\Gamma_{0}\land\bigwedge\Gamma_{2}\bigr{)}\to\lnot\bigl{(}\bigwedge\Gamma_{0}\land\bigwedge\Gamma_{1}\land\bigwedge\Gamma_{2}\bigr{)}\right).$

Since it is clear that
$\lnot\bigl{(}\lnot\varphi\land\bigwedge\Gamma_{0}\land\bigwedge\Gamma_{2}\bigr{)}\to\lnot\bigl{(}\bigwedge\Gamma_{0}\land\bigwedge\Gamma_{1}\land\bigwedge\Gamma_{2}\bigr{)}\mathrel{\ltimes}\lnot\bigl{(}\varphi\land\bigwedge\Gamma_{0}\land\bigwedge\Gamma_{1}\bigr{)}$,
it would follow by $\mathbf{MP}^{\bowtie}$ that

$\vdash\lnot\bigl{(}\lnot\varphi\land\bigwedge\Gamma_{0}\land\bigwedge\Gamma_{2}\bigr{)}\to\lnot\bigl{(}\bigwedge\Gamma_{0}\land\bigwedge\Gamma_{1}\land\bigwedge\Gamma_{2}\bigr{)}.$

Note, additionally, that
$\lnot\bigl{(}\bigwedge\Gamma_{0}\land\bigwedge\Gamma_{1}\land\bigwedge\Gamma_{2}\bigr{)}\mathrel{\ltimes}\lnot\bigl{(}\lnot\varphi\land\bigwedge\Gamma_{0}\land\bigwedge\Gamma_{2}\bigr{)}$.
Indeed, whenever
$\lnot\bigl{(}\bigwedge\Gamma_{0}\land\bigwedge\Gamma_{1}\land\bigwedge\Gamma_{2}\bigr{)}$
is defined, all formulas from $\Gamma_{2}$ and all formulas from $\Gamma_{0}$
are defined. The latter implies that $\varphi$ is defined. Hence, the boolean
combination
$\lnot\bigl{(}\lnot\varphi\land\bigwedge\Gamma_{0}\land\bigwedge\Gamma_{2}\bigr{)}$
is defined. Thus, another application of $\mathbf{MP}^{\bowtie}$ would yield
$\vdash\lnot\bigl{(}\bigwedge\Gamma_{0}\land\bigwedge\Gamma_{1}\land\bigwedge\Gamma_{2}\bigr{)}.$
But $\Gamma_{0}\cup\Gamma_{1}\cup\Gamma_{2}$ is a finite subset of $\Gamma$,
creating a contradiction with the assumption that $\Gamma$ is consistent. This
contradiction shows that $\Gamma$ determines $\varphi$. Since $\varphi$ was
chosen arbitrarily, $\Gamma$ determines all its definability consequences,
i.e., is a DMC set.

We start our formal presentation by showing that DMC sets represent all
possible truth sets across all faces of all simplicial models. This is
slightly more than representing all facets, i.e., all global states, but
creates no additional problems.

######  Lemma 5.9.

For any simplicial model $\mathcal{C}=(C,\chi,\ell)$ and its face $X\in C$,
the truth set
$\Gamma_{\mathcal{C},X}\colonequals\\{\varphi\mid\mathcal{C},X\vDash\varphi\\}$
is a DMC set.

######  Proof 5.10.

It is clear that $\Gamma_{\mathcal{C},X}$ cannot be empty. Hence, to show that
$\Gamma_{\mathcal{C},X}$ is consistent, consider any non-empty finite subset
$\Gamma_{0}\subseteq\Gamma_{\mathcal{C},X}$. We have
$\mathcal{C},X\vDash\bigwedge\Gamma_{0}$ by construction. Therefore,
$\mathcal{C},X\nvDash\lnot\bigwedge\Gamma_{0}$ and
$\nvdash\lnot\bigwedge\Gamma_{0}$ by the soundness of $\mathsf{S5}^{\bowtie}$
(Theorem 4.3). Since $\Gamma_{0}$ was chosen arbitrarily, we have established
that $\Gamma_{\mathcal{C},X}$ is consistent.

It remains to show that $\Gamma_{\mathcal{C},X}$ is definability maximal (DM).
Assume that $\Gamma_{\mathcal{C},X}\mathrel{\ltimes}\varphi$, i.e., there is a
finite subset $\Gamma_{0}\subseteq\Gamma_{\mathcal{C},X}$ such that $\varphi$
is defined whenever all formulas from $\Gamma_{0}$ are. Since, by
construction, $\mathcal{C},X\vDash\psi$ for all
$\psi\in\Gamma_{\mathcal{C},X}$, it follows from Lemma 2.9(2.9) that
$\mathcal{C},X\bowtie\psi$ for all $\psi\in\Gamma_{0}$. Thus,
$\mathcal{C},X\bowtie\varphi$, meaning that either
$\mathcal{C},X\vDash\varphi$ or $\mathcal{C},X\vDash\lnot\varphi$. By
construction, either $\varphi$ or $\lnot\varphi$ belongs to
$\Gamma_{\mathcal{C},X}$, i.e., $\varphi\in^{*}\Gamma_{\mathcal{C},X}$.

Properties of DMC sets differ slightly from those of maximal consistent sets:

######  Lemma 5.11 (Properties of DMC sets).

For DMC sets $\Gamma$ and $\Delta$, an agent $a$, propositional variable
$p_{a}\in P_{a}$, and formulas $\varphi$, $\varphi_{1}$, $\varphi_{2}$, and
$\psi$:

$\Gamma\mathrel{\ltimes}\varphi$ and $\Gamma\vdash\varphi$ $\Longrightarrow$
$\varphi\in\Gamma$.

$\Gamma\mathrel{\ltimes}\varphi$ $\Longrightarrow$ exactly one of
$\varphi\in\Gamma$ and $\lnot\varphi\in\Gamma$ holds.

$\varphi_{1}\land\varphi_{2}\in\Gamma$ $\Longleftrightarrow$ both
$\varphi_{1}\in\Gamma$ and $\varphi_{2}\in\Gamma$.

$K_{a}\Gamma\neq\varnothing$ and $\varphi\in^{*}\Gamma$ $\Longrightarrow$
$K_{a}\varphi\in^{*}\Gamma$.

$p_{a}\in\Gamma$ iff $K_{a}p_{a}\in\Gamma$, and $\lnot p_{a}\in\Gamma$ iff
$K_{a}\lnot p_{a}\in\Gamma$. Hence, $p_{a}\in^{*}\Gamma$ implies
$K_{a}\Gamma\neq\varnothing$.

$K_{a}\Gamma,\varphi\mathrel{\ltimes}K_{a}\psi$ and
$K_{a}\varphi\in^{*}\Gamma$ $\Longrightarrow$ $K_{a}\psi\in^{*}\Gamma$.

$K_{a}\Gamma\subseteq K_{a}\Delta$ and $\lnot K_{a}\varphi\in\Gamma$
$\Longrightarrow$ $\lnot K_{a}\varphi\in\Delta$.

$K_{a}\varphi\in\Gamma$ $\Longrightarrow$ $\lnot\varphi\notin\Gamma$ and
$K_{a}\Gamma\cup\\{\varphi\\}$ is consistent.

$\lnot K_{a}\varphi\in\Gamma$ $\Longrightarrow$
$K_{a}\Gamma\cup\\{\lnot\varphi\\}$ is consistent.

######  Proof 5.12.

Since $\Gamma\vdash\varphi$, we have $\vdash\bigwedge\Gamma_{0}\to\varphi$ for
some finite $\varnothing\neq\Gamma_{0}\subseteq\Gamma$. Given tautology
$\vdash\bigl{(}\bigwedge\Gamma_{0}\to\varphi\bigr{)}\rightarrow\lnot\bigl{(}\lnot\varphi\land\bigwedge\Gamma_{0}\bigr{)}$,
it follows by MP⋈ that
$\vdash\lnot\bigl{(}\lnot\varphi\land\bigwedge\Gamma_{0}\bigr{)}$ because
$\lnot\bigl{(}\lnot\varphi\land\bigwedge\Gamma_{0}\bigr{)}\mathrel{\ltimes}\bigwedge\Gamma_{0}\to\varphi$.
Thus, $\lnot\varphi\in\Gamma$ would contradict $\Gamma$’s consistency. On the
other hand, either $\varphi\in\Gamma$ or $\lnot\varphi\in\Gamma$ because
$\Gamma$ is DM and $\Gamma\mathrel{\ltimes}\varphi$. Thus, $\varphi\in\Gamma$.

It follows from $\vdash\lnot(\varphi\land\lnot\varphi)$ and $\Gamma$ being DM.

It follows by clause (5.11) since for $i=1,2$
$\varphi_{1}\land\varphi_{2}\vdash\varphi_{i}$,
$\varphi_{1}\land\varphi_{2}\mathrel{\ltimes}\varphi_{i}$,
$\varphi_{1},\varphi_{2}\vdash\varphi_{1}\land\varphi_{2}$, and
$\varphi_{1},\varphi_{2}\mathrel{\ltimes}\varphi_{1}\land\varphi_{2}$.

By Lemma 2.15(2.15), $\Gamma\mathrel{\ltimes}K_{a}\varphi$. Hence,
$K_{a}\varphi\in^{*}\Gamma$ because $\Gamma$ is DM.

Since $p_{a}\bowtie\lnot p_{a}$, it follows from Lemma 2.15(2.15) that
$p_{a}\bowtie K_{a}p_{a}$ and $\lnot p_{a}\bowtie K_{a}\lnot p_{a}$. By Lemma
4.11, $p_{a}\vdash K_{a}p_{a}$ and $\lnot p_{a}\vdash K_{a}\lnot p_{a}$. By
axiom T, $K_{a}p_{a}\vdash p_{a}$ and $K_{a}\lnot p_{a}\vdash\lnot p_{a}$.
Hence, the first two iff claims follow from clause (5.11). The last claim
follows from them.

By Lemma 2.15(2.15), $K_{a}\Gamma,K_{a}\varphi\mathrel{\ltimes}K_{a}\psi$,
hence, also $K_{a}\Gamma,\lnot K_{a}\varphi\mathrel{\ltimes}K_{a}\psi$. Thus,
however $\Gamma$ determines $K_{a}\varphi$, we know that
$\Gamma\mathrel{\ltimes}K_{a}\psi$. Now $K_{a}\psi\in^{*}\Gamma$ follows from
$\Gamma$ being DM.

Since $\lnot K_{a}\varphi\mathrel{\ltimes}K_{a}\lnot K_{a}\varphi$ by Lemma
2.15(2.15) and $\lnot K_{a}\varphi\vdash K_{a}\lnot K_{a}\varphi$ by axiom 5,
it follows by clause (5.11) that, if $\lnot K_{a}\varphi\in\Gamma$, also
$K_{a}\lnot K_{a}\varphi\in K_{a}\Gamma\subseteq K_{a}\Delta$. Similarly,
$K_{a}\lnot K_{a}\varphi\mathrel{\ltimes}\lnot K_{a}\varphi$ by Lemma
2.15(2.15) and $K_{a}\lnot K_{a}\varphi\vdash\lnot K_{a}\varphi$ by axiom T.
Hence, $\lnot K_{a}\varphi\in\Delta$ by clause (5.11).

Since $\lnot(K_{a}\varphi\land\lnot\varphi)$ is equidefinable and equivalent
to $K_{a}\varphi\to\varphi$, i.e., to axiom T, having $\lnot\varphi\in\Gamma$
would have contradicted the consistency of $\Gamma$. (Note that, unlike in
traditional modal logic, this does not necessarily mean $\varphi\in\Gamma$.)
We prove the consistency of $K_{a}\Gamma\cup\\{\varphi\\}$ by contradiction.
Were it not, we would have $K_{a}\psi_{1},\dots,K_{a}\psi_{m}\in
K_{a}\Gamma\subseteq\Gamma$ such that (w.l.o.g. in view of Lemma 5.6(5.6))
$\vdash\lnot(\varphi\land K_{a}\psi_{1}\land\dots\land K_{a}\psi_{m})$. A
contradiction $\vdash\lnot(K_{a}\varphi\land K_{a}\psi_{1}\land\dots\land
K_{a}\psi_{m})$ to the consistency of $\Gamma$ would follow by Lemma 4.15.

The argument here is similar to the preceding clause, except that Lemma 4.16
is used instead of Lemma 4.15 and $K_{a}\Gamma\neq\varnothing$ is not assumed
by follows from $K_{a}\lnot K_{a}\varphi\in\Gamma$, obtained by the same
argument as in clause (5.11).

######  Lemma 5.13 (Lindenbaum Lemma).

Any consistent set $\Gamma\neq\varnothing$ can be extended to a DMC set
$\Delta\supseteq\Gamma$ such that $\Gamma\mathrel{\ltimes}\psi$ for all
$\psi\in\Delta$.

######  Proof 5.14.

Let $\psi_{0},\psi_{1},\dots$ be an enumeration of the set
$\Gamma^{\mathrel{\ltimes}}\colonequals\\{\psi\mid\Gamma\mathrel{\ltimes}\psi\\}$
of all definability consequences of $\Gamma$. Starting from
$\Delta_{0}\colonequals\Gamma$, add formulas $\psi_{i}$ one by one, unless
doing so would cause inconsistency:
$\Delta_{i+1}\colonequals\Delta_{i}\cup\\{\psi_{i}\\}$ if that set is
consistent or $\Delta_{i+1}\colonequals\Delta_{i}$ otherwise. Define
$\Delta\colonequals\cup_{i=0}^{\infty}\Delta_{i}\subseteq\Gamma^{\mathrel{\ltimes}}$,
which is consistent for the same reason as in the standard Lindenbaum
construction that enumerates all formulas: were $\Delta$ inconsistent, one of
$\Delta_{i}$ would have been. We now show that $\Delta$ is maximal among
consistent subsets of $\Gamma^{\mathrel{\ltimes}}$. Indeed, any
$\psi\in\Gamma^{\mathrel{\ltimes}}\setminus\Delta$ is one of $\psi_{i}$’s and
was not added to $\Delta_{i}$ due to $\Delta_{i}\cup\\{\psi\\}$ being
inconsistent. Hence, $\Delta\cup\\{\psi\\}$ is also inconsistent. Since
$\Gamma^{\mathrel{\ltimes}}$ is definability complete by Lemma 2.15(2.15), it
follows from Lemma 5.7 that $\Delta$ is a DMC set.

######  Definition 5.15 (Simplicial canonical model).

Let $\mathbb{G}$ denote the collection of all DMC sets. For
$\Gamma\in\mathbb{G}$, we define

$X_{\Gamma}\colonequals\\{K_{a}\Gamma\mid a\in
A,K_{a}\Gamma\neq\varnothing\\}.$

The _simplicial canonical model_ $\mathcal{C}^{c}=(C^{c},\chi^{c},\ell^{c})$
is defined as follows:

  * •

$C^{c}\colonequals\\{X\mid(\exists\Gamma\in\mathbb{G})\,(\varnothing\neq
X\subseteq X_{\Gamma})\\}$.

  * •

Accordingly, its set of vertices $\mathcal{V}^{c}=\bigcup_{X\in
C^{c}}X=\\{K_{a}\Gamma\mid\Gamma\in\mathbb{G},a\in
A,K_{a}\Gamma\neq\varnothing\\}$.

  * •

For $K_{a}\Gamma\in\mathcal{V}^{c}$, we define
$\chi^{c}(K_{a}\Gamma)\colonequals a$.

  * •

For $K_{a}\Gamma\in\mathcal{V}^{c}$, we define
$\ell^{c}(K_{a}\Gamma)\colonequals\\{p_{a}\in P_{a}\mid K_{a}p_{a}\in
K_{a}\Gamma\\}$.

In other words, given $\Gamma\in\mathbb{G}$, non-empty sets $K_{a}\Gamma$ are
vertices of the canonical model $\mathcal{C}^{c}$ and sets $X_{\Gamma}$ are,
in most cases, its facets (but not necessarily, see Sect. 6). The color of
vertex $K_{a}\Gamma$ must obviously be $a$, and the local variables true there
are those known by this agent $a$.

######  Remark 5.16.

Unlike sets $\Gamma\in\mathbb{G}$, sets $K_{a}\Gamma$ are not DMC sets. For
instance, neither $p_{a}\in K_{a}\Gamma$ nor $\lnot p_{a}\in K_{a}\Gamma$ even
though either $K_{a}p_{a}\in K_{a}\Gamma$ or $K_{a}\lnot p_{a}\in K_{a}\Gamma$
and $p_{a}$ is a definability consequence of either.

######  Lemma 5.17 (Correctness).

The object $\mathcal{C}^{c}$ constructed in Def. 5.15 is a simplicial model.

######  Proof 5.18.

The proof is straightforward and can be found in Appendix B.

The Truth Lemma has to be adapted to the logic of impure simplicial models in
two ways:

formulas may be undefined, in addition to being true or false, necessitating
an extra clause (6) in the Truth Lemma;

the Truth Lemma is only proved for faces of the form $X_{\Gamma}$ because
their proper subfaces $X\subsetneq X_{\Gamma}$ do not generally correspond to
DMC sets.

######  Lemma 5.19 (Truth Lemma).

Let $\mathcal{C}^{c}$ be the canonical simplicial model constructed in Def.
5.15. Then, for any DMC set $\Gamma\in\mathbb{G}$ and any formula $\varphi$,

$\displaystyle\varphi\notin^{*}\Gamma\qquad$
$\displaystyle\Longrightarrow\qquad\mathcal{C}^{c},X_{\Gamma}\not\bowtie\varphi,$
(6) $\displaystyle\varphi\in\Gamma\qquad$
$\displaystyle\Longrightarrow\qquad\mathcal{C}^{c},X_{\Gamma}\vDash\varphi,$
(7) $\displaystyle\lnot\varphi\in\Gamma\qquad$
$\displaystyle\Longrightarrow\qquad\mathcal{C}^{c},X_{\Gamma}\vDash\lnot\varphi.$
(8)

######  Proof 5.20.

The proof is by induction on the construction of $\varphi$. Note that
$X_{\Gamma}\in C^{c}$.555See the proof of Lemma 5.17 in Appendix B.

For $\varphi=p_{a}$, first assume $p_{a}\notin^{*}\Gamma$. Then
$\Gamma\not\mathrel{\ltimes}p_{a}$ because $\Gamma$ is DM , hence,
$K_{a}\Gamma=\varnothing$ by Lemma 2.15(2.15). Therefore, $K_{a}\Gamma\notin
X_{\Gamma}$, $a\notin\chi^{c}(X_{\Gamma})$, and
$\mathcal{C}^{c},X_{\Gamma}\not\bowtie p_{a}$.

Assume now $p_{a}\in\Gamma$. Then, $K_{a}p_{a}\in K_{a}\Gamma$ by Lemma
5.11(5.11). Since $K_{a}\Gamma\neq\varnothing$, we have
$K_{a}\Gamma\in\mathcal{V}^{c}$, and
$p_{a}\in\ell^{c}(K_{a}\Gamma)\subseteq\ell^{c}(X_{\Gamma})$. Therefore,
$\mathcal{C}^{c},X_{\Gamma}\vDash p_{a}$.

Finally, assume $\lnot p_{a}\in\Gamma$. Then, $K_{a}\lnot p_{a}\in
K_{a}\Gamma$ by Lemma 5.11(5.11). Again, $K_{a}\Gamma\neq\varnothing$ implies
$K_{a}\Gamma\in\mathcal{V}^{c}$ and $a\in\chi^{c}(X_{\Gamma})$. Therefore,
$\mathcal{C}^{c},X_{\Gamma}\bowtie p_{a}$. On the other hand,
$p_{a}\notin\Gamma$ by the consistency of $\Gamma$ implying $K_{a}p_{a}\notin
K_{a}\Gamma$ by Lemma 5.11(5.11). Hence, $p_{a}\notin\ell^{c}(X_{\Gamma})$
meaning $\mathcal{C}^{c},X_{\Gamma}\nvDash p_{a}$. Thus, in summary,
$\mathcal{C}^{c},X_{\Gamma}\models\lnot p_{a}$.

For $\varphi=\lnot\psi$, first assume $\lnot\psi\notin^{*}\Gamma$. Then
$\psi\notin^{*}\Gamma$ since $\Gamma$ is DM and
$\psi\mathrel{\ltimes}\lnot\psi$. Then
$\mathcal{C}^{c},X_{\Gamma}\not\bowtie\psi$ by induction hypothesis (6) for
$\psi$. Accordingly, $\mathcal{C}^{c},X_{\Gamma}\not\bowtie\lnot\psi$.

Assume now $\lnot\psi\in\Gamma$. Then,
$\mathcal{C}^{c},X_{\Gamma}\models\lnot\psi$ by induction hypothesis (8) for
$\psi$.

Finally, assume $\lnot\lnot\psi\in\Gamma$. Then $\psi\in\Gamma$ by Lemma
5.11(5.11) because $\lnot\lnot\psi\mathrel{\ltimes}\psi$ and
$\lnot\lnot\psi\vdash\psi$. Thus, $\mathcal{C}^{c},X_{\Gamma}\vDash\psi$ by
induction hypothesis (7) for $\psi$. Accordingly,
$\mathcal{C}^{c},X_{\Gamma}\vDash\lnot\lnot\psi$.

For $\varphi=\psi_{1}\land\psi_{2}$, first assume
$\psi_{1}\land\psi_{2}\notin^{*}\Gamma$. Then $\psi_{i}\notin^{*}\Gamma$ for
at least one of the conjuncts since $\Gamma$ is DM and
$\widetilde{\psi_{1}},\widetilde{\psi_{2}}\mathrel{\ltimes}\psi_{1}\land\psi_{2}$
for any $\widetilde{\psi_{j}}\in\\{\psi_{j},\lnot\psi_{j}\\}$. Then
$\mathcal{C}^{c},X_{\Gamma}\not\bowtie\psi_{i}$ by induction hypothesis (6)
for this $\psi_{i}$. Accordingly,
$\mathcal{C}^{c},X_{\Gamma}\not\bowtie\psi_{1}\land\psi_{2}$.

Assume now $\psi_{1}\land\psi_{2}\in\Gamma$. Then, $\psi_{i}\in\Gamma$ for
both conjuncts by Lemma 5.11(5.11). Thus,
$\mathcal{C}^{c},X_{\Gamma}\models\psi_{i}$ by induction hypothesis (7) for
both $\psi_{i}$. Accordingly,
$\mathcal{C}^{c},X_{\Gamma}\vDash\psi_{1}\land\psi_{2}$.

Finally, assume $\lnot(\psi_{1}\land\psi_{2})\in\Gamma$. Then
$\psi_{j}\in^{*}\Gamma$ since $\Gamma$ is DM and
$\lnot(\psi_{1}\land\psi_{2})\mathrel{\ltimes}\psi_{j}$ for both conjuncts.
Hence, $\mathcal{C}^{c},X_{\Gamma}\bowtie\psi_{j}$ by Lemma 2.9(2.9)–(2.9) and
induction hypotheses (7)–(8) for both $\psi_{j}$. Thus,
$\mathcal{C}^{c},X_{\Gamma}\bowtie\psi_{1}\land\psi_{2}$. On the other hand,
$\psi_{1}\land\psi_{2}\notin\Gamma$ by the consistency of $\Gamma$, hence,
$\psi_{i}\notin\Gamma$ for at least one of $\psi_{i}$ by Lemma 5.11(5.11). It
follows that $\lnot\psi_{i}\in\Gamma$ and
$\mathcal{C}^{c},X_{\Gamma}\nvDash\psi_{i}$ by induction hypothesis (8) for
this $\psi_{i}$. Hence,
$\mathcal{C}^{c},X_{\Gamma}\nvDash\psi_{1}\land\psi_{2}$ and, overall,
$\mathcal{C}^{c},X_{\Gamma}\vDash\lnot(\psi_{1}\land\psi_{2})$.

For $K_{a}\varphi$, first assume that $K_{a}\varphi\notin^{*}\Gamma$.

  * •

If $K_{a}\Gamma=\varnothing$, then $K_{a}\Gamma\notin X_{\Gamma}$. Therefore,
$a\notin\chi^{c}(X_{\Gamma})$, and there can be no $Y\in C^{c}$ such that
$a\in\chi^{c}(X_{\Gamma}\cap Y)$ and $\mathcal{C}^{c},Y\bowtie\varphi$. In
this case, we have $\mathcal{C}^{c},X_{\Gamma}\not\bowtie K_{a}\varphi$.

  * •

If $K_{a}\Gamma\neq\varnothing$, then $K_{a}\Gamma\in X_{\Gamma}$. Consider
any $Y\in C^{c}$ such that $a\in\chi^{c}(X_{\Gamma}\cap Y)$. This implies that
$K_{a}\Gamma\in Y$. By Def. 5.15, $\varnothing\neq Y\subseteq X_{\Delta}$ for
some $\Delta\in\mathbb{G}$ and, hence, $K_{a}\Gamma\in X_{\Delta}$. Therefore,
$K_{a}\Delta=K_{a}\Gamma$, and it follows that $K_{a}\Delta\neq\varnothing$,
meaning that $a\in\chi^{c}(X_{\Gamma}\cap X_{\Delta})$. Since
$K_{a}\varphi\in^{*}\Delta$ iff $K_{a}\varphi\in^{*}\Gamma$ by Lemma
5.11(5.11), it follows that $K_{a}\varphi\notin^{*}\Delta$. By Lemma
5.11(5.11), $\varphi\notin^{*}\Delta$ and, by induction hypothesis (6),
$\mathcal{C}^{c},X_{\Delta}\not\bowtie\varphi$. From Lemma 2.12(2.12), it
follows that $\mathcal{C}^{c},Y\not\bowtie\varphi$. Since face $Y$, which is
$a$-adjacent to $X_{\Gamma}$, was chosen arbitrarily,
$\mathcal{C}^{c},X_{\Gamma}\not\bowtie K_{a}\varphi$.

Assume now that $K_{a}\varphi\in\Gamma$. Hence, $K_{a}\Gamma\neq\varnothing$,
$K_{a}\Gamma\in X_{\Gamma}$, and $a\in\chi^{c}(X_{\Gamma})$. By Cor.
2.11(2.11), for $\mathcal{C}^{c},X_{\Gamma}\vDash K_{a}\varphi$, it is
sufficient to show that:

$\mathcal{C}^{c},Y\bowtie\varphi$ implies $\mathcal{C}^{c},Y\vDash\varphi$ for
all $Y\in C^{c}$ such that $a\in\chi^{c}(X_{\Gamma}\cap Y)$, and

$\mathcal{C}^{c},Y\vDash\varphi$ for some $Y\in C^{c}$ with
$a\in\chi^{c}(X_{\Gamma}\cap Y)$. To show (5.20), consider any $Y\in C^{c}$
such that $a\in\chi^{c}(X_{\Gamma}\cap Y)$ and
$\mathcal{C}^{c},Y\bowtie\varphi$. It follows from
$a\in\chi^{c}(X_{\Gamma}\cap Y)$ that $K_{a}\Gamma\in Y$. By Def. 5.15,
$\varnothing\neq Y\subseteq X_{\Delta}$ for some $\Delta\in\mathbb{G}$. Then,
on the one hand, $K_{a}\Gamma\in X_{\Delta}$ which implies that
$K_{a}\Delta=K_{a}\Gamma$, and, on the other hand,
$\mathcal{C}^{c},X_{\Delta}\bowtie\varphi$ by Lemma 2.12(2.12). It follows
from induction hypothesis (6) that $\varphi\in^{*}\Delta$. Since
$K_{a}\Delta=K_{a}\Gamma$ we have $K_{a}\varphi\in\Delta$ and, hence,
$\lnot\varphi\notin\Delta$ by Lemma 5.11(5.11). Therefore, $\varphi\in\Delta$.
Thus, $\mathcal{C}^{c},X_{\Delta}\vDash\varphi$ by induction hypothesis (7),
and $\mathcal{C}^{c},Y\vDash\varphi$ by Lemma 2.12(2.12). We have shown that
$\varphi$ is true in all faces $a$-adjacent to $X_{\Gamma}$ where it is
defined.

To show (5.20), consider $K_{a}\Gamma\cup\\{\varphi\\}$, which is consistent
by Lemma 5.11(5.11). By Lindenbaum Lemma 5.13, there exists a DMC set
$\Delta\supseteq K_{a}\Gamma\cup\\{\varphi\\}$ such that
$K_{a}\Gamma,\varphi\mathrel{\ltimes}\psi$ for all $\psi\in\Delta$. We have
$K_{a}\Gamma\subseteq K_{a}\Delta$ by construction. To prove the opposite
inclusion, consider any $K_{a}\theta\in\Delta$. Since
$K_{a}\Gamma,\varphi\mathrel{\ltimes}K_{a}\theta$, by Lemma 2.15(2.15)
$K_{a}\Gamma,K_{a}\varphi\mathrel{\ltimes}K_{a}\theta$, and, hence,
$\Gamma\mathrel{\ltimes}K_{a}\theta$. Then $K_{a}\theta\in^{*}\Gamma$ because
$\Gamma$ is DM. Were $\lnot K_{a}\theta\in\Gamma$, we would have had $\lnot
K_{a}\theta\in\Delta$ by Lemma 5.11(5.11) making $\Delta$ inconsistent. It
follows that $K_{a}\theta\in\Gamma$ for all $K_{a}\theta\in\Delta$. Thus,
$K_{a}\Gamma=K_{a}\Delta$ and $a\in\chi^{c}(X_{\Gamma}\cap X_{\Delta})$. It
remains to note that, by induction hypothesis (7) for $\varphi$, we have
$\mathcal{C}^{c},X_{\Delta}\vDash\varphi$, and $X_{\Delta}$ serves as a face
$a$-adjacent to $X_{\Gamma}$ where $\varphi$ is true.

Finally, assume $\lnot K_{a}\varphi\in\Gamma$. By Cor. 2.11(2.11), for
$\mathcal{C}^{c},X_{\Gamma}\vDash\lnot K_{a}\varphi$, it is sufficient to show
that $\mathcal{C}^{c},Y\vDash\lnot\varphi$ for some $Y\in C^{c}$ with
$a\in\chi^{c}(X_{\Gamma}\cap Y)$. Consider
$K_{a}\Gamma\cup\\{\lnot\varphi\\}$, which is consistent by Lemma 5.11(5.11).
By Lindenbaum Lemma 5.13, there exists a DMC set $\Delta\supseteq
K_{a}\Gamma\cup\\{\lnot\varphi\\}$ such that
$K_{a}\Gamma,\lnot\varphi\mathrel{\ltimes}\psi$ for all $\psi\in\Delta$. We
have $K_{a}\Gamma\subseteq K_{a}\Delta$ by construction. To prove the opposite
inclusion, consider any $K_{a}\theta\in\Delta$. By Lemma 2.15(2.15),
$K_{a}\Gamma,\lnot K_{a}\varphi\mathrel{\ltimes}K_{a}\theta$, and, hence,
$\Gamma\mathrel{\ltimes}K_{a}\theta$. Then $K_{a}\theta\in^{*}\Gamma$ because
$\Gamma$ is DM. Were $\lnot K_{a}\theta\in\Gamma$, this would have meant that
$\lnot K_{a}\theta\in\Delta$ by Lemma 5.11(5.11) making $\Delta$ inconsistent.
It follows that $K_{a}\theta\in\Gamma$ for all $K_{a}\theta\in\Delta$. Thus,
$K_{a}\Gamma=K_{a}\Delta$ and $a\in\chi^{c}(X_{\Gamma}\cap X_{\Delta})$. It
remains to note that, by induction hypothesis (8) for $\varphi$, we have
$\mathcal{C}^{c},X_{\Delta}\vDash\lnot\varphi$, and $X_{\Delta}$ serves as a
face $a$-adjacent to $X_{\Gamma}$ where $\varphi$ is false.

######  Theorem 5.21 (Completeness).

Axiomatization $\mathsf{S5}^{\bowtie}$ is complete with respect to impure
simplicial models, i.e., $\vDash\varphi$ implies $\vdash\varphi$.

######  Proof 5.22.

We prove the contraposition. Suppose $\nvdash\varphi$ for a formula $\varphi$.
Then $\\{\lnot\varphi\\}$ is a consistent set. By Lindenbaum Lemma 5.13,
$\\{\lnot\varphi\\}$ is a subset of some DMC set $\Gamma$. By Truth Lemma
5.19, $\mathcal{C}^{c},X_{\Gamma}\vDash\lnot\varphi$. Thus, $\varphi$ is not
valid.

##  6 Simplicial Canonical Model Reflections

In most similar papers, the completeness theorem would be the happy ending.
The deed is done, leaving only the conclusions section to summarize the
results and possibly set up a sequel. Here, however, we would like to take a
moment to reflect on the structure of the canonical simplicial model
$\mathcal{C}^{c}$ constructed in Def. 5.15 and how well it matches the class
of all impure simplicial models. As with the normality axiom K and modus
ponens rule MP, there are surprising departures from the properties we are
used to expect, which makes it worthwhile to dispel some possible
misconceptions.

One structural property we have largely ignored until now was the distinction
between facets, i.e., maximal faces, and faces that are not maximal. As
mentioned earlier, it is facets that correspond to global states, i.e., worlds
in Kripke models, whereas other faces are just intermediate constructs. One
can even argue that these non-facet faces are just artifacts of simplicial
complex structure with no significance of their own. It was Lemma 2.18 that
gave us license to ignore this distinction. If the logic does not depend on
whether we look only at global states or additionally allow their partial
shadows, there seemed little reason to bother about separating these shadows
away.

As a result, we constructed canonical simplicial model $\mathcal{C}^{c}$ to
faithfully represent all faces of all simplicial models, which, of course,
includes all facets of all simplicial models. But we did not make an effort to
ensure that those facets are represented by facets in $\mathcal{C}^{c}$. One
might expect the canonicity to take care of that. We now show that such an
expectation would be misplaced, i.e., that there are facets represented in
$\mathcal{C}^{c}$ by non-maximal faces.

######  Example 6.1.

In impure simplicial complexes, the situation when two agents are unsure
whether the third agent is dead or alive is typically represented by
simplicial models of the form $\mathcal{C}_{\mathrm{Xmas}}=(C,\chi,\ell)$,
which we are going to call _Christmas cracker models_ ,

$v_{a}^{l}$$v_{c}^{r}$$v_{a}^{r}$$v_{c}^{l}$$v_{b}^{l}$$v_{b}^{r}$$W_{r}$$Z_{r}$$W_{l}$$Z_{l}$$U_{l}$$U_{r}$$\mathcal{C}_{\mathrm{Xmas}}:$
Figure 5: Christmas cracker models

for three agents $a$, $b$, and $c$ with

  * •

six vertices
$\mathcal{V}=\\{v_{a}^{l},v_{a}^{r},v_{b}^{l},v_{b}^{r},v_{c}^{l},v_{c}^{r}\\}$,

  * •

four facets
$\mathcal{F}(C)=\bigl{\\{}\\{v_{a}^{l},v_{b}^{l},v_{c}^{l}\\},\quad\\{v_{a}^{r},v_{b}^{r},v_{c}^{r}\\},\quad\\{v_{a}^{l},v_{c}^{r}\\},\quad\\{v_{c}^{l},v_{a}^{r}\\}\bigr{\\}}$,

  * •

a chromatic map $\chi\colon v^{*}_{i}\mapsto i$, which maps each vertex to its
subscript, and

  * •

a valuation $\ell$ that must satisfy the following conditions:

$\ell(v_{a}^{l})=\ell(v_{a}^{r}),\qquad\ell(v_{b}^{l})=\ell(v_{b}^{r}),\qquad\ell(v_{c}^{l})=\ell(v_{c}^{r}).$
(9)

Let us use $U_{l}$ and $U_{r}$ for 2-dimensional facets (triangles), $Z_{l}$
and $Z_{r}$ for 1-dimensional facets (edges), and $W_{l}\subset U_{l}$ and
$W_{r}\subset U_{r}$ for the $ac$-colored 1-dimensional faces of the triangles
(see Fig. 5). It immediately follows from the rotational symmetry that,
omitting the name of the simplicial model and using

$\Gamma_{V}\colonequals\\{\varphi\mid\mathcal{C}_{\mathrm{Xmas}},V\vDash\varphi\\}$
(10)

for the truth sets of its faces, we get $\Gamma_{U_{l}}=\Gamma_{U_{r}}$,
$\Gamma_{Z_{l}}=\Gamma_{Z_{r}}$, $\Gamma_{W_{l}}=\Gamma_{W_{r}}$, etc. (recall
that the set of formulas true in a face also provides a complete description
of formulas false and undefined in the same face). These sets are DMC sets
according to Lemma 5.9.

Accordingly, in the canonical model $\mathcal{C}^{c}$, facets $Z_{l}$ and
$Z_{r}$ are represented by the same canonical simplex
$X_{\Gamma_{Z_{l}}}=\\{K_{a}\Gamma_{Z_{l}},K_{c}\Gamma_{Z_{l}}\\}$ of
dimension 1. By the same token, faces $W_{l}$ and $W_{r}$ are represented
there by canonical simplex $\\{K_{a}\Gamma_{U_{l}},K_{c}\Gamma_{U_{l}}\\}$ of
dimension 1, which is a canonical face within canonical facet
$X_{\Gamma_{U_{l}}}=\\{K_{a}\Gamma_{U_{l}},K_{b}\Gamma_{U_{l}},K_{c}\Gamma_{U_{l}}\\}$
of the maximal dimension 2. We will show that
$\\{K_{a}\Gamma_{Z_{l}},K_{c}\Gamma_{Z_{l}}\\}=\\{K_{a}\Gamma_{U_{l}},K_{c}\Gamma_{U_{l}}\\}$,
i.e., both facets $Z_{l}$ an $Z_{r}$ and non-maximal faces $W_{l}$ and $W_{r}$
are represented by the same canonical face that is not a facet.

$K_{a}\Gamma_{Z_{l}}=K_{a}\Gamma_{U_{l}}$ follows directly from Defs. 2.6 and
2.7 because $Z_{l}$ and $U_{l}$ share $a$-colored vertex $v_{a}^{l}$. To show
that $K_{c}\Gamma_{Z_{l}}=K_{c}\Gamma_{U_{l}}$, it is sufficient to note that
the truth values of formulas $K_{c}\varphi$ in $Z_{l}$ are determined by truth
values of $\varphi$ in all simplices $c$-adjacent to $Z_{l}$, i.e., in
$\\{v_{c}^{r}\\},Z_{l},W_{r},\\{v_{c}^{r},v_{b}^{r}\\}$, and $U_{r}$, whereas
the same truth values in $U_{l}$ are determined by truth values of $\varphi$
in all simplices $c$-adjacent to $U_{l}$, i.e., in
$\\{v_{c}^{l}\\},Z_{r},W_{l},\\{v_{c}^{l},v_{b}^{l}\\}$, and $U_{l}$. As
already noted earlier, for every of these five pairs of corresponding
simplices, truth values are identical. Hence, the truth value of each
$K_{c}\varphi$ in $Z_{l}$ and $U_{l}$ is also the same.

This example makes it clear that, while all facets are represented in the
canonical model, they may not be represented by a canonical facet. The same
example demonstrates that definability-maximal consistent sets need not be
maximal consistent in the usual sense but only with respect to subsets of some
definability-complete set.

######  Lemma 6.2.

There exist DMC sets $\Gamma$ and $\Delta$ such that $\Gamma\subsetneq\Delta$.

######  Proof 6.3.

It is sufficient to show that $\Gamma_{Z_{l}}\subsetneq\Gamma_{U_{l}}$ in
Example 6.1. Note that all formulas are defined in $U_{l}$ because all agents
are alive there. We show by mutual induction that any formula that is true
(false) in $Z_{l}$ is true (respectively false) in $U_{l}$, i.e., that

$\mathcal{C},Z_{l}\vDash\varphi\quad\Longrightarrow\quad\mathcal{C},U_{l}\vDash\varphi\qquad\text{and}\qquad\mathcal{C},Z_{l}\vDash\lnot\varphi\quad\Longrightarrow\quad\mathcal{C},U_{l}\vDash\lnot\varphi.$

For propositional variables $\varphi=p_{a}\in P_{a}$, this is trivial as truth
values for them are determined by $\ell(v^{l}_{a})$. For $\varphi=p_{c}\in
P_{c}$, it follows from (9). No $p_{b}\in P_{b}$ is defined in $Z_{l}$.

For $\varphi=\lnot\psi$, if $\lnot\psi$ is true in $Z_{l}$, then $\psi$ is
false there, hence, $\psi$ is false in $U_{l}$ by the induction hypothesis,
making $\lnot\psi$ true in $U_{l}$. The argument for false $\lnot\psi$ in
$Z_{l}$ is analogous.

For $\varphi=\psi_{1}\land\psi_{2}$, if $\psi_{1}\land\psi_{2}$ is true in
$Z_{l}$, then both $\psi_{1}$ and $\psi_{2}$ are true there, hence, both are
true in $U_{l}$ by the induction hypothesis, and $\psi_{1}\land\psi_{2}$ is
true in $U_{l}$. If $\psi_{1}\land\psi_{2}$ is false in $Z_{l}$, then at least
one of the conjuncts is false there. Hence, this conjunct is false in $U_{l}$
by the induction hypothesis. Since $\psi_{1}\land\psi_{2}$ is defined in
$U_{l}$, it can only be false.

No $K_{b}\psi$ is defined in $Z_{l}$. For $\varphi=K_{a}\psi$, if it is true
in $Z_{l}$, then $K_{a}\psi\in K_{a}\Gamma_{Z_{l}}$ according to (10). It was
shown in Example 6.1 that $K_{a}\Gamma_{Z_{l}}=K_{a}\Gamma_{U_{l}}$, i.e.,
$K_{a}\psi$ is also true in $U_{l}$ by (10). If $K_{a}\psi$ is false, then
$K_{a}\psi\notin K_{a}\Gamma_{Z_{l}}=K_{a}\Gamma_{U_{l}}$. Since $K_{a}\psi$
is defined in $U_{l}$, it must be false. The case of $\varphi=K_{c}\psi$ is
analogous.

Thus, $\Gamma_{Z_{l}}\subseteq\Gamma_{U_{l}}$, and it remains to note that
either $p_{b}$ or $\lnot p_{b}$ must belong to $\Gamma_{U_{l}}$ (depending on
valuation $\ell$), but neither belongs to $\Gamma_{Z_{l}}$, making the
inclusion strict.

So far we have shown that facets may be represented by non-facets in the
canonical model and that truth sets of facets may be subsumed by larger facet
truth sets. One might, therefore, ask a question whether it always happens.
Could it be that all DMC sets are embedded into some maximal consistent sets,
in which case the canonical model would be a pure simplicial model? We finish
this section by dispelling this suspicion and showing that canonical
simplicial model $\mathcal{C}^{c}$ is impure.

######  Example 6.4.

Given at least three agents $a$, $b$, and $c$, consider simplicial model
$\mathcal{C}$

$U$$v_{a}$$v_{c}$ Figure 6: Simplicial model: agent $b$ is dead

consisting of one facet $U=\\{v_{a},v_{c}\\}$ of dimension 1. This simplicial
model is impure in our terms because one of the agents, $b$, is dead in its
only facet. Using
$\Gamma\colonequals\\{\varphi\mid\mathcal{C},U\vDash\varphi\\}$ for the set of
formulas true in $U$ and recalling that $\Gamma$ is a DMC set, we are
guaranteed that it is represented by
$X_{\Gamma}=\\{K_{a}\Gamma,K_{c}\Gamma\\}$ in canonical simplicial model
$\mathcal{C}^{c}$. We will now show that this $X_{\Gamma}$ is a canonical
facet.

Suppose towards a contradiction that there exists a DMC set $\Delta$ such that
$K_{a}\Gamma=K_{a}\Delta$, $K_{c}\Gamma=K_{c}\Delta$, but
$K_{b}\Delta\neq\varnothing$, meaning that $X_{\Gamma}\subsetneq X_{\Delta}$
is not a facet. Take any propositional variable $p_{b}\in P_{b}$. Since
$K_{b}\varphi\mathrel{\ltimes}p_{b}$ for any formula $\varphi$ by Lemma
2.15(2.15), it follows that $p_{b}\in^{*}\Delta$, i.e., $p_{b}\in\Delta$ or
$\lnot p_{b}\in\Delta$. If $p_{b}\in\Delta$, then, since
$K_{a}\theta,p_{b}\mathrel{\ltimes}K_{a}p_{b}$ for any $\theta$ by Lemma
2.15(2.15), we conclude that $K_{a}p_{b}\in^{*}\Delta$ because
$K_{a}\Delta=K_{a}\Gamma\neq\varnothing$. The same applies if $\lnot
p_{b}\in\Delta$ since $p_{b}\bowtie\lnot p_{b}$. On the one hand, $K_{a}p_{b}$
cannot be in $K_{a}\Delta=K_{a}\Gamma$ because $K_{a}p_{b}$ is undefined in
$U$ and, hence, cannot be true there. On the other hand, $\lnot K_{a}p_{b}$
cannot be in $\Delta$ because this would imply that $K_{a}\lnot K_{a}p_{b}\in
K_{a}\Delta=K_{a}\Gamma$, which is impossible for the same reason. This
contradiction shows that such a DMC set $\Delta$ does not exist, and
$X_{\Gamma}$ is a canonical facet where agent $b$ is dead.

##  7 Conclusions and Future Work

We presented the axiomatization called $\mathsf{S5}^{\bowtie}$ and showed that
it is sound and complete for the class of impure complexes. The completeness
proof involved the construction of the canonical simplicial model, a novel
kind of a canonical model for a three-valued epistemic semantics where the
third value means ‘undefined.’

We envisage various generalizations and refinements, both concerning
axiomatizations but also concerning epistemic semantics for distributed
computing.

While $\mathsf{S5}^{\bowtie}$ applies to any number of agents, for small
numbers of agents simpler axiomatizations are possible. The full system is
required starting from at least three agents.

Different epistemic semantics can be envisioned wherein, apart from local
variables, there are global variables stating that agents are alive. Those
logics are more expressive. Such more expressive semantics allow for an
embedding into two-valued semantics for impure complexes.

Adding distributed knowledge modalities is a generalization of the semantics.
This also increases the expressivity with respect to impure complexes.
Distributed knowledge can be considered independently from global atoms for
life and death. Finally, one can generalize from simplicial complexes to
simplicial sets.

Such generalizations of the epistemic semantics come with different
axiomatizations, and also promise to address specific modeling issues in
distributed computing.

#### Acknowledgments

The authors would like to thank Marta Bílková, Giorgio Cignarale, Stephan
Felber, Krisztina Fruzsa, Hugo Rincón Galeana, and Thomas Schlögl for many
inspiring discussions and especially Ulrich Schmid for his enthusiasm and
knowledge, which appear to be equally inexhaustible.

## References

  * [1] Thomas Ågotnes and Yì N. Wáng.  Resolving distributed knowledge.  Artificial Intelligence, 252:1–21, 2017.  doi:10.1016/j.artint.2017.07.002.
  * [2] Alexandru Baltag, Lawrence S. Moss, and Sławomir Solecki.  The logic of public announcements, common knowledge, and private suspicions.  In Itzhak Gilboa, editor, Theoretical Aspects of Rationality and Knowledge: Proceedings of the Seventh Conference (TARK 1998), pages 43–56. Morgan Kaufmann, 1998.  Available from: http://www.tark.org/proceedings/tark_jul22_98/p43-baltag.pdf.
  * [3] Alexandru Baltag and Sonja Smets.  Learning what others know.  In Elvira Albert and Laura Kovács, editors, LPAR23. LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 73 of EPiC Series in Computing, pages 90–119. EasyChair, 2020.  doi:10.29007/plm4.
  * [4] Ofer Biran, Shlomo Moran, and Shmuel Zaks.  A combinatorial characterization of the distributed 1-solvable tasks.  Journal of Algorithms, 11(3):420–440, 1990.  doi:10.1016/0196-6774(90)90020-F.
  * [5] Hans van Ditmarsch.  Wanted dead or alive: Epistemic logic for impure simplicial complexes.  In Alexandra Silva, Renata Wassermann, and Ruy de Queiroz, editors, Logic, Language, Information, and Computation: 27th International Workshop, WoLLIC 2021, Virtual Event, October 5–8, 2021, Proceedings, volume 13038 of Lecture Notes in Computer Science, pages 31–46. Springer, 2021.  doi:10.1007/978-3-030-88853-4_3.
  * [6] Hans van Ditmarsch, Krisztina Fruzsa, and Roman Kuznets.  A new hope.  In David Fernández-Duque, Alessandra Palmigiano, and Sophie Pinchinat, editors, Advances in Modal Logic, volume 14, pages 349–369. College Publications, 2022.
  * [7] Hans van Ditmarsch, Éric Goubault, Marijana Lazić, Jérémy Ledent, and Sergio Rajsbaum.  A dynamic epistemic logic analysis of equality negation and other epistemic covering tasks.  Journal of Logical and Algebraic Methods in Programming, 121:100662, 2021.  doi:10.1016/j.jlamp.2021.100662.
  * [8] Hans van Ditmarsch, Éric Goubault, Jérémy Ledent, and Sergio Rajsbaum.  Knowledge and simplicial complexes.  In Björn Lundgren and Nancy Abigail Nuñez Hernández, editors, Philosophy of Computing: Themes from IACAP 2019, volume 143 of Philosophical Studies Series, pages 1–50. Springer, 2022.  doi:10.1007/978-3-030-75267-5_1.
  * [9] Hans van Ditmarsch, Wiebe van der Hoek, and Barteld Kooi.  Dynamic Epistemic Logic, volume 337 of Synthese Library.  Springer, 2007.  doi:10.1007/978-1-4020-5839-4.
  * [10] Hans van Ditmarsch and Roman Kuznets.  Wanted dead or alive: Epistemic logic for impure simplicial complexes.  Eprint 2103.03032, version 2, arXiv, 2022.  doi:10.48550/arXiv.2103.03032.
  * [11] Clare Dixon, Cláudia Nalon, and Ram Ramanujam.  Knowledge and time.  In Hans van Ditmarsch, Joseph Y. Halpern, Wiebe van der Hoek, and Barteld Kooi, editors, Handbook of Epistemic Logic, pages 205–259. College Publications, 2015.
  * [12] Cynthia Dwork and Yoram Moses.  Knowledge and common knowledge in a Byzantine environment: Crash failures.  Information and Computation, 88(2):156–186, 1990.  doi:10.1016/0890-5401(90)90014-9.
  * [13] Michael J. Fischer, Nancy A. Lynch, and Michael S. Paterson.  Impossibility of distributed consensus with one faulty process.  Journal of the ACM, 32(2):374–382, 1985.  doi:10.1145/3149.214121.
  * [14] Éric Goubault, Jérémy Ledent, and Sergio Rajsbaum.  A simplicial complex model for dynamic epistemic logic to study distributed task computability.  Information and Computation, 278:104597, 2021.  doi:10.1016/j.ic.2020.104597.
  * [15] Éric Goubault, Jérémy Ledent, and Sergio Rajsbaum.  A simplicial model for $\mathrm{KB4_{n}}$: Epistemic logic with agents that may die.  In Petra Berenbrink and Benjamin Monmege, editors, 39th International Symposium on Theoretical Aspects of Computer Science: STACS 2022, March 15–18, 2022, Marseille, France (Virtual Conference), volume 219 of Leibniz International Proceedings in Informatics (LIPIcs), pages 33:1–33:20. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2022.  doi:10.4230/LIPIcs.STACS.2022.33.
  * [16] Joseph Y. Halpern and Yoram Moses.  Knowledge and common knowledge in a distributed environment.  Journal of the ACM, 37(3):549–587, 1990.  doi:10.1145/79147.79161.
  * [17] Joseph Y. Halpern, Dov Samet, and Ella Segev.  Defining knowledge in terms of belief: The modal logic perspective.  Review of Symbolic Logic, 2(3):469–487, 2009.  doi:10.1017/S1755020309990141.
  * [18] Maurice Herlihy, Dmitry Kozlov, and Sergio Rajsbaum.  Distributed Computing through Combinatorial Topology.  Morgan Kaufmann, 2013.  doi:10.1016/C2011-0-07032-1.
  * [19] Maurice Herlihy, Sergio Rajsbaum, and Mark Tuttle.  An axiomatic approach to computing the connectivity of synchronous and asynchronous systems (preliminary version).  In E. Goubault, editor, Proceedings of the Workshops on Geometric and Topological Methods in Concurrency Theory (GETCO 2004+2005+2006), volume 230 of Electronic Notes in Theoretical Computer Science, pages 79–102. Elsevier, 2009.  doi:10.1016/j.entcs.2009.02.018.
  * [20] Maurice Herlihy and Nir Shavit.  The topological structure of asynchronous computability.  Journal of the ACM, 46(6):858–923, 1999.  doi:10.1145/331524.331529.
  * [21] P. J. Hilton and S. Wylie.  Homology Theory: An Introduction to Algebraic Topology.  Cambridge University Press, 1960.  doi:10.1017/CBO9780511569289.
  * [22] Jaakko Hintikka.  Knowledge and Belief: An Introduction to the Logic of the Two Notions.  Cornell University Press, 1962.
  * [23] Jérémy Ledent.  Geometric semantics for asynchronous computability.  PhD thesis, Paris-Saclay University, Palaiseau, France, 2019.  Prepared at École polytechnique.  Available from: https://tel.archives-ouvertes.fr/tel-02445180.
  * [24] Michael C. Loui and Hosame H. Abu-Amara.  Memory requirements for agreement among unreliable asynchronous processes.  In Parallel and Distributed Computing, volume 4 of Advances in Computing Research: A research annual, pages 163–183. JAI Press, 1987.
  * [25] Yoram Moses and Yoav Shoham.  Belief as defeasible knowledge.  Artificial Intelligence, 64(2):299–321, 1993.  doi:10.1016/0004-3702(93)90107-M.
  * [26] Lawrence S. Moss.  Dynamic epistemic logic.  In Hans van Ditmarsch, Joseph Y. Halpern, Wiebe van der Hoek, and Barteld Kooi, editors, Handbook of Epistemic Logic, pages 261–312. College Publications, 2015.
  * [27] Daniel Pfleger and Ulrich Schmid.  On knowledge and communication complexity in distributed systems.  In Zvi Lotker and Boaz Patt-Shamir, editors, Structural Information and Communication Complexity: 25th International Colloquium, SIROCCO 2018, Ma’ale HaHamisha, Israel, June 18–21, 2018, Revised Selected Papers, volume 11085 of Lecture Notes in Computer Science, pages 312–330. Springer, 2018.  doi:10.1007/978-3-030-01325-7_27.
  * [28] Amir Pnueli.  The temporal logic of programs.  In 18th Annual Symposium on Foundations of Computer Science, pages 46–57. IEEE, 1977.  doi:10.1109/SFCS.1977.32.
  * [29] Michael Saks and Fotios Zaharoglou.  Wait-free $k$-set agreement is impossible: The topology of public knowledge.  SIAM Journal on Computing, 29(5):1449–1483, 2000.  doi:10.1137/S0097539796307698.
  * [30] Diego A. Velázquez, Armando Castañeda, and David A. Rosenblueth.  Communication pattern models: An extension of action models for dynamic-network distributed systems.  In Joseph Halpern and Andrés Perea, editors, Proceedings Eighteenth Conference on Theoretical Aspects of Rationality and Knowledge: Beijing, China, June 25–27, 2021, volume 335 of Electronic Proceedings in Theoretical Computer Science, pages 307–321. Open Publishing Association, 2021.  doi:10.4204/EPTCS.335.29.

##  Appendix A Auxiliary Statements

######  Lemma A.1.

$\displaystyle\frac{\vdash\varphi_{1}\rightarrow\psi_{1}\qquad\dots\qquad\vdash\varphi_{m}\rightarrow\psi_{m}}{\vdash\varphi_{1}\land\dots\land\varphi_{m}\rightarrow\psi_{1}\land\dots\land\psi_{m}}$
is derivable.

######  Proof A.2.

The tautology
$(\varphi_{1}\rightarrow\psi_{1})\rightarrow\Bigl{(}\dots\rightarrow(\varphi_{m}\rightarrow\psi_{m})\rightarrow(\varphi_{1}\land\dots\land\varphi_{m}\rightarrow\psi_{1}\land\dots\land\psi_{m})\Bigr{)}$
can be used, followed by $m$ applications of MP⋈ justified by the fact that
the definability of
$\varphi_{1}\land\dots\land\varphi_{m}\rightarrow\psi_{1}\land\dots\land\psi_{m}$
implies the definability of all $\varphi_{i}$’s and all $\psi_{j}$’s, hence,
of any other formula in the derivation.

######  Lemma A.3.

$\vdash K_{a}\psi_{1}\land\cdots\land K_{a}\psi_{m}\to
K_{a}(\psi_{1}\land\cdots\land\psi_{m})$.

######  Proof A.4.

Induction on $m$. For $m=1$, the statement is trivial because
$K_{a}\psi_{1}\to K_{a}\psi_{1}$ is a tautology. For $m=2$, it follows from
Lemma 4.10. Assume the statement holds for $m=k$.

  1. 1.

$K_{a}\psi_{1}\land\cdots\land K_{a}\psi_{k}\to
K_{a}(\psi_{1}\land\cdots\land\psi_{k})$ induction hypothesis

  2. 2.

$K_{a}\psi_{k+1}\to K_{a}\psi_{k+1}$ tautology

  3. 3.

$K_{a}\psi_{1}\land\cdots\land K_{a}\psi_{k}\land K_{a}\psi_{k+1}\to
K_{a}(\psi_{1}\land\cdots\land\psi_{k})\land K_{a}\psi_{k+1}$ Lemma A.1(1.,2.)

  4. 4.

$K_{a}(\psi_{1}\land\cdots\land\psi_{k})\land K_{a}\psi_{k+1}\to
K_{a}(\psi_{1}\land\cdots\land\psi_{k}\land\psi_{k+1})$ Lemma 4.10

  5. 5.

$K_{a}\psi_{1}\land\cdots\land K_{a}\psi_{k+1}\to
K_{a}(\psi_{1}\land\cdots\land\psi_{k+1})$ Lemma 4.6(3.,4.)
as $K_{a}\psi_{1}\land\cdots\land K_{a}\psi_{k+1}\to
K_{a}(\psi_{1}\land\cdots\land\psi_{k+1})\mathrel{\ltimes}K_{a}(\psi_{1}\land\cdots\land\psi_{k})\land
K_{a}\psi_{k+1}$

##  Appendix B Additional proofs

See 2.15

######  Proof B.1.

$\Gamma\mathrel{\ltimes}\varphi$ means that there is a finite subset
$\Gamma^{\prime}\subseteq\Gamma$ such that $\varphi$ is defined whenever all
formulas from $\Gamma^{\prime}$ are. But $\Gamma^{\prime}$ is also a finite
subset of $\Gamma\cup\Delta$. Hence,
$\Gamma\cup\Delta\mathrel{\ltimes}\varphi$.

Since $\Delta\mathrel{\ltimes}\varphi$, there exists a finite subset
$\Delta^{\prime}=\\{\psi_{1},\dots,\psi_{m}\\}\subseteq\Delta$ such that
$\varphi$ is defined whenever all $\psi_{i}$’s are. Since
$\Gamma\mathrel{\ltimes}\Delta$, for each $\psi_{i}$ there must exist a finite
subset $\Gamma_{i}\subseteq\Gamma$ such that $\psi_{i}$ is defined whenever
all formulas from $\Gamma_{i}$ are. It is now easy to see that $\varphi$ is
defined whenever all formulas from the finite subset
$\bigcup_{i=1}^{m}\Gamma_{i}\subseteq\Gamma$ are. Hence,
$\Gamma\mathrel{\ltimes}\varphi$.

Starting from this clause, we consider an arbitrary simplicial model
$\mathcal{C}=(C,\chi,\ell)$ and its face $X\in C$ and assume all formulas to
the left of $\mathrel{\ltimes}$ to be defined in $X$, e.g., here we assume
that $\mathcal{C},X\bowtie K_{a}\varphi$. By Def. 2.6, there exists $Y\in C$
such that $\mathcal{C},Y\bowtie\varphi$ and $a\in\chi(X\cap Y)$. Hence,
$a\in\chi(X)$ and the conclusion follows from Def. 2.6.

To show that $p_{a}\mathrel{\ltimes}K_{a}p_{a}$, assume that
$\mathcal{C},X\bowtie p_{a}$. By Def. 2.6, $a\in\chi(X)$. Equivalently,
$a\in\chi(X\cap X)$. Hence, $\mathcal{C},X\bowtie K_{a}p_{a}$ by Def. 2.6. The
other direction follows from clause (2.15).

Assume $\mathcal{C},X\bowtie K_{a}\varphi$. By Def. 2.6, there exists $Y\in C$
such that $\mathcal{C},Y\bowtie\varphi$ and $a\in\chi(X\cap Y)$. Then
$a\in\chi(Y\cap Y)$ so that $\mathcal{C},Y\bowtie K_{a}\varphi$. Therefore,
$\mathcal{C},X\bowtie K_{a}K_{a}\varphi$.

Assume $\mathcal{C},X\bowtie K_{a}K_{a}\varphi$. By Def. 2.6, there exists
$Y\in C$ such that $\mathcal{C},Y\bowtie K_{a}\varphi$ and $a\in\chi(X\cap
Y)$. This in turn implies that there exists $Z\in C$ such that
$\mathcal{C},Z\bowtie\varphi$ and $a\in\chi(Y\cap Z)$. Then $a\in\chi(X\cap
Z)$ and $\mathcal{C},X\bowtie K_{a}\varphi$.

That $K_{a}\varphi\bowtie\lnot K_{a}\varphi$ follows from Def. 2.6. It remains
to prove that that $\lnot K_{a}\varphi\bowtie K_{a}\lnot K_{a}\varphi$.

Assume $\mathcal{C},X\bowtie\lnot K_{a}\varphi$. Hence, $\mathcal{C},X\bowtie
K_{a}\varphi$. By Def. 2.6, there exists $Y\in C$ such that
$\mathcal{C},Y\bowtie\varphi$ and $a\in\chi(X\cap Y)$. Then $a\in\chi(Y\cap
Y)$ so that $\mathcal{C},Y\bowtie K_{a}\varphi$ and $\mathcal{C},Y\bowtie\lnot
K_{a}\varphi$. Therefore, $\mathcal{C},X\bowtie K_{a}\lnot K_{a}\varphi$.

Assume $\mathcal{C},X\bowtie K_{a}\lnot K_{a}\varphi$. By Def. 2.6, there
exists $Y\in C$ such that $\mathcal{C},Y\bowtie\lnot K_{a}\varphi$ and
$a\in\chi(X\cap Y)$, hence, also $\mathcal{C},Y\bowtie K_{a}\varphi$. This in
turn implies that there exists $Z\in C$ such that
$\mathcal{C},Z\bowtie\varphi$ and $a\in\chi(Y\cap Z)$. Then $a\in\chi(X\cap
Z)$ and $\mathcal{C},X\bowtie K_{a}\varphi$, hence, $\mathcal{C},X\bowtie\lnot
K_{a}\varphi$.

Assume $\mathcal{C},X\bowtie K_{a}\theta$ and $\mathcal{C},X\bowtie\varphi$.
By Def. 2.6, there exists $Y\in C$ such that $\mathcal{C},Y\bowtie\theta$ and
$a\in\chi(X\cap Y)$. Then $a\in\chi(X\cap X)$ so that $\mathcal{C},X\bowtie
K_{a}\varphi$.

Assume $K_{a}\Gamma,\varphi\mathrel{\ltimes}K_{a}\psi$, i.e., there is a
finite subset $\Gamma^{\prime}\subseteq K_{a}\Gamma\cup\\{\varphi\\}$ such
that $K_{a}\psi$ is defined whenever all formulas from $\Gamma^{\prime}$ are.
If $\varphi\notin\Gamma^{\prime}$, then $\Gamma^{\prime}\subseteq
K_{a}\Gamma\cup\\{K_{a}\varphi\\}$, so we are done. Otherwise,
$\Gamma^{\prime}=K_{a}\Theta\cup\\{\varphi\\}$ for some finite subset
$\Theta\subseteq\Gamma$. Assume $\mathcal{C},X\bowtie K_{a}\theta$ for all
$K_{a}\theta\in K_{a}\Theta$ and $\mathcal{C},X\bowtie K_{a}\varphi$. The
latter means that there exists $Y\in C$ such that $a\in\chi(X\cap Y)$ and
$\mathcal{C},Y\bowtie\varphi$. It follows from the former that, for each
$K_{a}\theta\in K_{a}\Theta$, there exists $Z_{\theta}\in C$ such that
$a\in\chi(X\cap Z_{\theta})$ and $\mathcal{C},Z_{\theta}\bowtie\theta$. Since
face $X$ cannot have two $a$-vertices, we have $a\in\chi(Y\cap Z_{\theta})$,
making $\mathcal{C},Y\bowtie K_{a}\theta$ for each $K_{a}\theta\in
K_{a}\Theta$. Recalling $\mathcal{C},Y\bowtie\varphi$, we conclude
$\mathcal{C},Y\bowtie K_{a}\psi$. Therefore, there exists $Z\in C$ such that
$a\in\chi(Y\cap Z)$ and $\mathcal{C},Z\bowtie\psi$. The uniqueness of the
$a$-vertex in $Y$ yields once again that $a\in\chi(X\cap Z)$, hence,
$\mathcal{C},X\bowtie K_{a}\psi$. We have shown that $K_{a}\psi$ is defined
whenever all formulas from the finite subset
$K_{a}\Theta\cup\\{K_{a}\varphi\\}\subseteq K_{a}\Gamma\cup\\{K_{a}\varphi\\}$
are. Hence, $K_{a}\Gamma,K_{a}\varphi\mathrel{\ltimes}K_{a}\psi$.

Assume $K_{a}\Gamma,\lnot\varphi\mathrel{\ltimes}K_{a}\psi$. Since
$\varphi\bowtie\lnot\varphi$, also
$K_{a}\Gamma,\varphi\mathrel{\ltimes}K_{a}\psi$. By clause (2.15), it follows
that $K_{a}\Gamma,K_{a}\varphi\mathrel{\ltimes}K_{a}\psi$. Since
$K_{a}\varphi\bowtie\lnot K_{a}\varphi$, we finally obtain $K_{a}\Gamma,\lnot
K_{a}\varphi\mathrel{\ltimes}K_{a}\psi$.

Assume $\mathcal{C},X\bowtie K_{a}(K_{a}\psi_{1}\land\cdots\land
K_{a}\psi_{m})\rightarrow K_{a}\theta$. Then, $\mathcal{C},X\bowtie
K_{a}(K_{a}\psi_{1}\land\cdots\land K_{a}\psi_{m})$ and $\mathcal{C},X\bowtie
K_{a}\theta$. By Def. 2.6, there exists $Y\in C$ such that
$\mathcal{C},Y\bowtie\theta$ and $a\in\chi(X\cap Y)$ and there exists $Z\in C$
such that $\mathcal{C},Z\bowtie K_{a}\psi_{1}\land\cdots\land K_{a}\psi_{m}$
and $a\in\chi(X\cap Z)$. From the latter, we conclude that
$\mathcal{C},Z\bowtie K_{a}\psi_{i}$ for each $i$, meaning that for each $i$
there is $Z_{i}\in C$ such that $\mathcal{C},Z_{i}\bowtie\psi_{i}$ and
$a\in\chi(Z\cap Z_{i})$. Since $a\in\chi(Y\cap Z_{i})$ for each $i$, we have
$\mathcal{C},Y\bowtie K_{a}\psi_{i}$ for each $i$. Consequently,
$\mathcal{C},Y\bowtie K_{a}\psi_{1}\land\cdots\land
K_{a}\psi_{m}\rightarrow\theta$, and, as required, $\mathcal{C},X\bowtie
K_{a}(K_{a}\psi_{1}\land\cdots\land K_{a}\psi_{m}\rightarrow\theta)$.

The proof of this clause is the same as for the preceding clause because
$K_{a}\theta\bowtie\widehat{K}_{a}\theta$.

Assume $\mathcal{C},X\bowtie K_{a}\psi_{1}\land\cdots\land K_{a}\psi_{m}$.
Since $\mathcal{C},X\bowtie K_{a}\psi_{1}$, there is $Z$ such that
$\mathcal{C},Z\bowtie\psi_{1}$ and $a\in\chi(X\cap Z)$. Thus, $a\in\chi(X\cap
X)$. Therefore, $\mathcal{C},X\bowtie K_{a}(K_{a}\psi_{1}\land\cdots\land
K_{a}\psi_{m})$.

Assume $\mathcal{C},X\bowtie K_{a}(K_{a}\psi_{1}\land\cdots\land
K_{a}\psi_{m})$. By Def. 2.6, there exists $Y\in C$ such that
$\mathcal{C},Y\bowtie K_{a}\psi_{1}\land\cdots\land K_{a}\psi_{m}$ and
$a\in\chi(X\cap Y)$. It follows that $\mathcal{C},Y\bowtie K_{a}\psi_{i}$ for
each $i$, meaning that for each $i$ there exists $Z_{i}\in C$ such that
$\mathcal{C},Z_{i}\bowtie\psi_{i}$ and $a\in\chi(Y\cap Z_{i})$. Since we then
have $a\in\chi(X\cap Z_{i})$ for each $i$, we conclude that
$\mathcal{C},X\bowtie K_{a}\psi_{i}$ for each $i$. Thus $\mathcal{C},X\bowtie
K_{a}\psi_{1}\land\cdots\land K_{a}\psi_{m}$.

See 4.3

######  Proof B.2.

Additional cases proved earlier in [10].

  * •

Substitution instances of propositional tautologies are valid because their
truth tables produce truth whenever they produce anything.

  * •

Axiom L is valid. Assume $\mathcal{C},X\bowtie K_{a}p_{a}\lor K_{a}\neg
p_{a}$. Then $\mathcal{C},X\bowtie K_{a}p_{a}$, that is, there is a face $Y$
with $a\in\chi(X\cap Y)$ such that $\mathcal{C},Y\bowtie p_{a}$. Hence,
$a\in\chi(X)$ and $\mathcal{C},X\bowtie p_{a}$. Let $X_{a}\in X$ be the vertex
of $X$ with color $a$, i.e., $\chi(X_{a})=a$. We now show that
$\mathcal{C},X\vDash K_{a}p_{a}\lor K_{a}\neg p_{a}$. Given
$\mathcal{C},X_{a}\bowtie p_{a}$, either $\mathcal{C},X_{a}\vDash p_{a}$ or
$\mathcal{C},X_{a}\vDash\neg p_{a}$. Since $X_{a}$ is the only $a$-colored
vertex in any face $a$-adjacent to $X_{a}$, in the former case,
$\mathcal{C},X_{a}\vDash K_{a}p_{a}$ and in the latter case,
$\mathcal{C},X_{a}\vDash K_{a}\neg p_{a}$. Either way,
$\mathcal{C},X_{a}\vDash K_{a}p_{a}\lor K_{a}\neg p_{a}$. Since
$\\{X_{a}\\}\subseteq X$, it now follows from Lemma 2.12(2.12) that
$\mathcal{C},X\vDash K_{a}p_{a}\lor K_{a}\neg p_{a}$, as required.

  * •

Axiom T is valid. Assume $\mathcal{C},X\bowtie K_{a}\varphi\to\varphi$. It
follows that $\mathcal{C},X\bowtie\varphi$ and $a\in\chi(X)$. If
$\mathcal{C},X\vDash K_{a}\varphi$, then $\mathcal{C},Y\bowtie\varphi$ implies
$\mathcal{C},Y\vDash\varphi$ for all $a$-adjacent faces $Y$, in particular,
for $Y=X$ itself, which is $a$-adjacent because $a\in\chi(X\cap X)$. Since
$\mathcal{C},X\bowtie\varphi$, we conclude $\mathcal{C},X\vDash\varphi$. We
have shown that $\vDash K_{a}\varphi\to\varphi$.

  * •

Axiom 4 is valid. If $\mathcal{C},X\vDash K_{a}\varphi$, then
$\mathcal{C},X\bowtie K_{a}\varphi$ by Lemma 2.9(2.9). In particular,
$\mathcal{C},W\bowtie\varphi$ for some $W$ such that $a\in\chi(X\cap W)$. We
also conclude $\mathcal{C},X\bowtie K_{a}K_{a}\varphi$ by Lemma 2.15(2.15)
and, hence, $\mathcal{C},X\bowtie K_{a}\varphi\to K_{a}K_{a}\varphi$, so that
we do not need to assume this separately. In order to prove
$\mathcal{C},X\vDash K_{a}K_{a}\varphi$, take an arbitrary face $Y$ such that
$a\in\chi(X\cap Y)$. Then $a\in\chi(Y\cap W)$ and, hence,
$\mathcal{C},Y\bowtie K_{a}\varphi$. To show that $\mathcal{C},Y\vDash
K_{a}\varphi$, take an arbitrary face $Z$ such that $a\in\chi(Y\cap Z)$ and
$\mathcal{C},Z\bowtie\varphi$. Then $a\in\chi(X\cap Z)$. Thus,
$\mathcal{C},Z\bowtie\varphi$ and the assumption $\mathcal{C},X\vDash
K_{a}\varphi$ yield $\mathcal{C},Z\vDash\varphi$. We proved that $\varphi$ is
true whenever defined in faces $a$-adjacent to $Y$. Hence,
$\mathcal{C},Y\vDash K_{a}\varphi$. This shows that $K_{a}\varphi$ is true
whenever defined in faces $a$-adjacent to $X$. In addition,
$\mathcal{C},X\bowtie K_{a}\varphi$ and $a\in\chi(X\cap X)$. Hence,
$\mathcal{C},X\vDash K_{a}K_{a}\varphi$. We have shown $\vDash
K_{a}\varphi\rightarrow K_{a}K_{a}\varphi$.

  * •

Axiom 5 is valid. If $\mathcal{C},X\vDash\lnot K_{a}\varphi$, then
$\mathcal{C},W\vDash\lnot\varphi$ for some $W$ such that $a\in\chi(X\cap W)$
by Cor. 2.11(2.11). By Lemma 2.9(2.9), both $\mathcal{C},X\bowtie\lnot
K_{a}\varphi$ and $\mathcal{C},W\bowtie\lnot\varphi$. The former implies
$\mathcal{C},X\bowtie K_{a}\lnot K_{a}\varphi$ by Lemma 2.15(2.15). The latter
implies $\mathcal{C},W\bowtie\varphi$ by Def. 2.6. Hence,
$\mathcal{C},X\bowtie\lnot K_{a}\varphi\to K_{a}\lnot K_{a}\varphi$, so that
we do not need to assume this separately. In order to prove
$\mathcal{C},X\vDash K_{a}\lnot K_{a}\varphi$, take an arbitrary face $Y$ such
that $a\in\chi(X\cap Y)$. Since $a\in\chi(Y\cap W)$, it follows by Cor.
2.11(2.11) that $\mathcal{C},Y\vDash\lnot K_{a}\varphi$. Thus, we proved that
$\lnot K_{a}\varphi$ is true in all faces $a$-adjacent to $X$. Given that $X$
is one of such faces, $\mathcal{C},X\vDash K_{a}\lnot K_{a}\varphi$. We have
shown $\vDash\lnot K_{a}\varphi\rightarrow K_{a}\lnot K_{a}\varphi$.

  * •

Necessitation rule N preserves validity. Assume $\vDash\varphi$ and
$\mathcal{C},X\bowtie K_{a}\varphi$. Validity of $\varphi$ means that it is
true whenever defined. In particular, it is true whenever defined for all
faces $a$-adjacent to $X$. In addition, $\mathcal{C},X\bowtie K_{a}\varphi$
means that there is a face $a$-adjacent to $X$ where $\varphi$ is defined.
Therefore, $\mathcal{C},X\vDash K_{a}\varphi$. We have shown that
$K_{a}\varphi$ is true whenever defined, as required. Thus, $\vDash
K_{a}\varphi$.

See 4.8

######  Proof B.3.

  1. 1.

$(\varphi\to\psi)\to(\lnot\psi\to\lnot\varphi)$ tautology

  2. 2.

$\varphi\to\psi$ derivable by assumption

  3. 3.

$\lnot\psi\to\lnot\varphi$ MP⋈(1.,2.) as
$\lnot\psi\to\lnot\varphi\mathrel{\ltimes}\varphi\to\psi$

See 4.9

######  Proof B.4.

  1. 1.

$\varphi\rightarrow\psi$ derivable by assumption

  2. 2.

$K_{a}(\varphi\rightarrow\psi)$ N(1.)

  3. 3.

$K_{a}(\varphi\rightarrow\psi)\rightarrow(K_{a}\varphi\rightarrow K_{a}\psi)$
K⋈ as $\psi,K_{a}\varphi\mathrel{\ltimes}\varphi$

  4. 4.

$K_{a}\varphi\rightarrow K_{a}\psi$ MP⋈(2.,3.) as $K_{a}\varphi\rightarrow
K_{a}\psi\mathrel{\ltimes}K_{a}(\varphi\rightarrow\psi)$ follows from
$\psi,K_{a}\varphi\mathrel{\ltimes}\varphi$

Let us explain why $K_{a}\varphi\to
K_{a}\psi\mathrel{\ltimes}K_{a}(\varphi\rightarrow\psi)$ holds in the last
step. If $K_{a}\varphi\to K_{a}\psi$ is defined in a face $X$, then both
$K_{a}\varphi$ and $K_{a}\psi$ are defined. The latter implies that there is
an $a$-adjacent face $Y$ where $\psi$ is defined. As before, if $K_{a}\varphi$
is defined in $X$, it is defined in all $a$-adjacent faces, including $Y$.
Hence, the definability provision $\psi,K_{a}\varphi\mathrel{\ltimes}\varphi$
applied to $Y$ yields that $\varphi$, and, hence, $\varphi\to\psi$, is also
defined in $Y$, making $K_{a}(\varphi\to\psi)$ defined in $X$.

See 4.10

######  Proof B.5.

  1. 1.

$\varphi\rightarrow(\psi\rightarrow\varphi\land\psi)$ tautology

  2. 2.

$K_{a}\bigl{(}\varphi\rightarrow(\psi\rightarrow\varphi\land\psi)\bigr{)}$
N(1.)

  3. 3.

$K_{a}\bigl{(}\varphi\rightarrow(\psi\rightarrow\varphi\land\psi)\bigr{)}\rightarrow\bigl{(}K_{a}\varphi\rightarrow
K_{a}(\psi\rightarrow\varphi\land\psi)\bigr{)}$ axiom K⋈ as
$\psi\rightarrow\varphi\land\psi\mathrel{\ltimes}\varphi$

  4. 4.

$K_{a}\varphi\rightarrow K_{a}(\psi\rightarrow\varphi\land\psi)$ MP⋈(2.,3.) as
$K_{a}\varphi\rightarrow
K_{a}(\psi\rightarrow\varphi\land\psi)\mathrel{\ltimes}K_{a}\bigl{(}\varphi\rightarrow(\psi\rightarrow\varphi\land\psi)\bigr{)}$

  5. 5.

$K_{a}(\psi\rightarrow\varphi\land\psi)\rightarrow\bigl{(}K_{a}\psi\rightarrow
K_{a}(\varphi\land\psi)\bigr{)}$ axiom K⋈ as
$\varphi\land\psi\mathrel{\ltimes}\psi$

  6. 6.

$K_{a}\varphi\rightarrow\bigl{(}K_{a}\psi\rightarrow
K_{a}(\varphi\land\psi)\bigr{)}$ Lemma 4.6(4.,5.) as
$K_{a}\varphi\rightarrow\bigl{(}K_{a}\psi\rightarrow
K_{a}(\varphi\land\psi)\bigr{)}\mathrel{\ltimes}K_{a}(\psi\rightarrow\varphi\land\psi)$

  7. 7.

$\Bigl{(}K_{a}\varphi\rightarrow\bigl{(}K_{a}\psi\rightarrow
K_{a}(\varphi\land\psi)\bigr{)}\Bigr{)}\rightarrow\Bigl{(}K_{a}\varphi\land
K_{a}\psi\rightarrow K_{a}(\varphi\land\psi)\Bigr{)}$ tautology

  8. 8.

$K_{a}\varphi\land K_{a}\psi\rightarrow K_{a}(\varphi\land\psi)$ MP⋈(6.,7.) as
$K_{a}\varphi\land K_{a}\psi\rightarrow
K_{a}(\varphi\land\psi)\mathrel{\ltimes}K_{a}\varphi\rightarrow\bigl{(}K_{a}\psi\rightarrow
K_{a}(\varphi\land\psi)\bigr{)}$

Fig. 3 provides a counterexample to the opposite direction. Indeed, in
simplicial model $\mathcal{C}_{\mathbf{K}}$, formula $K_{a}(p_{b}\land p_{c})$
is true, formula $K_{a}p_{c}$ is also true, but $K_{a}p_{b}$ is false because
$p_{b}$ is false in $X$ (where $p_{c}$ is undefined).

See 4.13

######  Proof B.6.

  * •

Case $\vdash\psi$. Then $\vdash\psi\to(\varphi\to\psi)$ as a tautology, and
$\vdash\varphi\to\psi$ is obtained by MP⋈ because
$\varphi\to\psi\mathrel{\ltimes}\psi$. Hence, $\Gamma\vdash\varphi\to\psi$ by
Def. 4.1.

  * •

Case $\vdash\varphi\to\psi$ for the finite subset
$\\{\varphi\\}\subseteq\Gamma\cup\\{\varphi\\}$. Then
$\Gamma\vdash\varphi\to\psi$ by Def. 4.1.

  * •

Case $\vdash\bigwedge\Gamma_{0}\rightarrow\psi$ for a finite non-empty subset
$\Gamma_{0}\subseteq\Gamma$.

    1. 1.

$\bigwedge\Gamma_{0}\rightarrow\psi$ assumption

    2. 2.

$\bigwedge\Gamma_{0}\land\varphi\rightarrow\bigwedge\Gamma_{0}$ tautology

    3. 3.

$\bigwedge\Gamma_{0}\land\varphi\rightarrow\psi$ Lemma 4.6(1.,2.) as
$\bigwedge\Gamma_{0}\land\varphi\rightarrow\psi\mathrel{\ltimes}\bigwedge\Gamma_{0}$

    4. 4.

$(\bigwedge\Gamma_{0}\land\varphi\rightarrow\psi)\rightarrow\bigl{(}\bigwedge\Gamma_{0}\rightarrow(\varphi\rightarrow\psi)\bigr{)}$
tautology

    5. 5.

$\bigwedge\Gamma_{0}\rightarrow(\varphi\rightarrow\psi)$ MP⋈(3.,4.) as
$\bigwedge\Gamma_{0}\rightarrow(\varphi\rightarrow\psi)\mathrel{\ltimes}\bigwedge\Gamma_{0}\land\varphi\rightarrow\psi$

Hence, $\Gamma\vdash\varphi\rightarrow\psi$ by Def. 4.1 based on
$\Gamma_{0}\subseteq\Gamma$.

  * •

Case $\vdash\bigwedge\Gamma_{0}\land\varphi\rightarrow\psi$ for a finite
subset $\\{\varphi\\}\sqcup\Gamma_{0}\subseteq\Gamma$ such that
$\Gamma_{0}\neq\varnothing$.

    1. 1.

$\bigwedge\Gamma_{0}\land\varphi\rightarrow\psi$ assumption

    2. 2.

$(\bigwedge\Gamma_{0}\land\varphi\rightarrow\psi)\rightarrow\bigl{(}\bigwedge\Gamma_{0}\rightarrow(\varphi\rightarrow\psi)\bigr{)}$
tautology

    3. 3.

$\bigwedge\Gamma_{0}\rightarrow(\varphi\rightarrow\psi)$ MP⋈(1.,2.) as
$\bigwedge\Gamma_{0}\rightarrow(\varphi\rightarrow\psi)\mathrel{\ltimes}\bigwedge\Gamma_{0}\land\varphi\rightarrow\psi$

Hence, $\Gamma\vdash\varphi\rightarrow\psi$ by Def. 4.1 based on
$\Gamma_{0}\subseteq\Gamma$.

See 4.14

######  Proof B.7.

  1. 1.