# Impure Simplicial Complexes: Complete Axiomatization

Rojo Randrianomentsoa, Hans van Ditmarsch, Roman Kuznets

► To cite this version:

Rojo Randrianomentsoa, Hans van Ditmarsch, Roman Kuznets. Impure Simplicial Complexes: Complete Axiomatization. Logical Methods in Computer Science, 2023, 19 (4), pp.3:1-3:35. 10.46298/lmcs-19(4:3)2023 . hal-04248222

HAL Id: hal-04248222

https://hal.science/hal-04248222v1

Submitted on 8 Jul 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# IMPURE SIMPLICIAL COMPLEXES: COMPLETE AXIOMATIZATION

ROJO RANDRIANOMENTSOA $^{a}$, HANS VAN DITMARSCH $^{b}$, AND ROMAN KUZNETS $^{a}$

$^{a}$TU Wien, Austria

e-mail address: rojorandrianomentsoa@tuwien.ac.at, roman.kuznets@tuwien.ac.at

$^{b}$University of Toulouse, CNRS, IRIT, France

e-mail address: hans.van-ditmarsch@irit.fr

**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 formulae that are undefined, e.g., the knowledge and local propositions of dead agents. In this work we present an axiomatization for the logic of the class of impure complexes and show soundness and completeness. The completeness proof involves the novel construction of the canonical simplicial model and requires a careful manipulation of undefined formulae.

## 1. INTRODUCTION

In this contribution, we present an axiomatization called $S5^{\boxtimes}$ 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, $S5^{\boxtimes}$ is a variant of the well-known multi-agent epistemic logic $S5$ [Hin62]. And in view of that, it may not come as a complete surprise that impure simplicial complexes, a notion from distributed computing [HKR14], correspond to certain multi-agent Kripke models [GLR22, vDK23], 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 [vDK23] (extending [vD21]), 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 $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**,

*Key words and phrases:* simplicial complexes, completeness, canonical model, epistemic logic.

R. Kuznets and R. Randrianomentsoa are funded by the Austrian Science Fund (FWF) ByzDEL project (P33600).

<figure><img src="image_2.png" /></figure>
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 [vDK23], 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 [HKR14] has been used in distributed computing to model concurrency and asynchrony since [FLP85, LA87, BMZ90], with higher-dimensional topological properties entering the picture in [HS99, SZ00]. 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 [Hin62]. Knowledge change was extensively modeled in temporal epistemic logics [Pnu77, HM90, DNR15] and in dynamic epistemic logics [BMS98, vDvdHK07, Mos15].

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 [Led19, GLR21], which was finalized in [vDGL$^+21$]. It is axiomatized by the multimodal logic S5 augmented with the so-called *locality axiom* stating that all agents know their local state, i.e. $K_a p_a \lor K_a \neg p_a$ for all agents $a$ and local propositional 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 [BS20] to the setting of simplicial semantics, exactly in view of describing higher-dimensional topological properties (for example, whether a complex is a manifold) [Led19, vDGLR22].

The dynamics of knowledge was another focus of those works and of additional works [PS18, vDGL$^+21$, VCR21]: the action models of [BMS98] can be used to model distributed computing tasks and algorithms. Action models even appeared in combinatorial topological incarnations as simplicial complexes in [Led19] and in [vDGLR22]. Additionally, [VCR21] proposed novel dynamic objects called communication patterns that represent arbitrary message exchange and are based on similar proposals in dynamic epistemics [ÅW17, BS20]. Communication patterns are different from action models, and their relation is complicated.

Pure complexes and their temporal development describe *asynchronous systems*. All processes then remain potentially active (alive), even when they have crashed: in asynchronous systems [HS99] crashed processes can be modeled as being infinitely slow. In *synchronous systems* [HRT09] 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 [HKR14, Section 13.5.2] (see also [HRT00] for more extended discussion). Impure simplicial complexes are considerably smaller in terms of their number of faces.

Epistemic logics interpreted on impure simplicial complexes were proposed in [vD21], of which the extended version, henceforth the only cited one, is [vDK23],<fnref n="1" /> and also in [GLR22].

In [vDK23], 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 formulae 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 S5 knowledge. No complete axiomatization was given in [vDK23].

In [GLR22], 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 KB4. Exciting further developments of this framework can be found in [GKLR23]: 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.

The works [GLR22, vDK23] 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 S5 knowledge. Consider the **T** axiom $K_a\varphi \rightarrow \varphi$. It is an axiom in S5$\sqsupset$ (and in [vDK23]) but its meaning is ‘known formulae cannot be false’ rather than ‘known formulae must be true’ (because they may be undefined instead). **T** is not an axiom in KB4 [GLR22], but, conveniently, in that work $K_a \perp$ 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 [MS93], knowledge in interpreted systems of [DM90, HM90], distinctions between knowledge and belief presented in [HSS09], and encoding byzantine faults through the hope modality, an epistemic notion weaker than belief [vDFK22], 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 [vDGL+21], we provide some simple examples illustrating how.

Figure 1 depicts some 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

<footnote n="1">¹All statements from [vDK23] we rely on are also present and proved in [vD21], unless stated otherwise.</footnote>
<figure><img src="image_3.png" /><figcaption>Figure 1: Pure simplicial complexes and corresponding Kripke models</figcaption></figure>

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 worlds 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 in a three-agent Kripke model. Together the local states of the triangle determine the world of the Kripke model, and the values of the local state variables together determine the valuation in that world. For example, in worlds labeled $0_a1_b1_c$ in Figure 1 agent *a*'s value is 0, *b*'s is 1, and *c*'s is 1. The single triangle corresponds to the singleton reflexive world 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 (global) 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 world in a Kripke model in order to evaluate propositions. For example, in the leftmost triangle, as well as in the leftmost 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 Figure 2. See [HKR14, Section 13.5.2] for a standard example of an impure simplicial complex from distributed computing.

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 Figure 1. It is merely here for comparison.

The impure complex on the left of Figure 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
<figure><img src="image_4.png" /><figcaption>Figure 2: Impure simplicial complexes and corresponding Kripke models</figcaption></figure>

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 world make explicit who is alive in this world. 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_a1_b0_c$ world and alive in the $0_a1_b1_c$ world, the relation for agent $c$ is restricted to the reflexive arrow from $0_a1_b1_c$ to itself. The Kripke model representation, unlike the impure simplicial complex, contains superfluous information: even though $c$ is dead in the world $0_a1_b0_c$, local variable $p_c$ is false there. Therefore, another representation of the same impure complex is the model $0_a1_b1_c \xrightarrow{a} 0_a1_b1_c$, where again $c$ is dead in $0_a1_b1_c$. (Strictly speaking, the number of such representations depends on how many local variables agent $c$ has.)

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 $S5^{\boxtimes}$ for a three-valued epistemic semantics interpreted on impure complexes. It has some notable differences from the standard multi-agent axiomatization $S5$, such as non-standard axioms $K^{\boxtimes}$ and $\hat{K}K$ instead of $K$ and a non-standard derivation rule $MP^{\boxtimes}$ instead of $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 [vDK23] and obtains additional results for formula definability that are crucial in this three-valued setting. Section 3 presents axiomatization S5$^{[4]}$. Section 4 shows that this axiomatization is sound, and Section 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 [vDK23], 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'_a, q'_a, \dots$$^2$$ 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 ::= p_a \mid \neg \varphi \mid (\varphi \wedge \varphi) \mid K_a \varphi$ where $a \in A$ and $p_a \in P_a$.

Parentheses will be omitted unless confusion results. Connectives $\to$, $\leftrightarrow$, and $\vee$ are defined by abbreviation as usual, as well as $\hat{K}_a\varphi := \neg K_a\neg\varphi$. Expression $K_a\varphi$ stands for ‘agent $a$ knows (that) $\varphi$,’ and $\hat{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 \emptyset$ 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 $\emptyset \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. $\{\{v\} | v \in \mathcal{V}\} \subseteq C$.

* Vertices represent local states of agents, with a chromatic map $\chi: \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) := \{\chi(v) \mid v \in X\} $$

to be the set of agents in simplex $X$.

* A valuation $\ell: \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$. The set of variables that are true in a simplex $X \in C$ is given by

$$ \ell(X) := \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 simplex $X$ is $|X| - 1$, e.g., vertices are of dimension 0, edges are of dimension 1, etc. The dimension of a simplicial

<footnote>$^2$We 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.</footnote>
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 $(C, X)$ where $X \in C$.

**Remarks 2.3.**

(i) It follows from the above definition that for any simplicial complex $C$, its set of vertices $V = \bigcup_{X \in C} X$. Thus, it is not necessary to specify $V$ when defining a complex $C$ or a simplicial model $C = (C, \chi, \ell)$ based on this complex. Further, 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 $V$ explicitly and often specify $\mathcal{F}(C)$ instead of $C$.

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

(iii) It has been common in the literature, including in [vDK23], to consider a more expansive view of pure simplicial models requiring all the facets to have merely the same dimension, without additionally requiring this common dimension to be the largest possible for the given set of agents as we do here. We believe that the distinction based on the presence/absence 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 gives rise to the question of what these 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 standard epistemic logic. In particular, both counterexamples to modus ponens from [vDK23] (not present in [vD21]) and in the proof of Lemma 3.2 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. Worlds 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 worlds 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 $S_5_{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 [vDK23], however, the case of impure models introduces a new situation where formulae 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 formulae: 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.4 (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:

$$ \mathcal{C}, X \bowtie p_a \quad \text{iff} \quad a \in \chi(X); $$

$$ \mathcal{C}, X \bowtie \neg\varphi \quad \text{iff} \quad \mathcal{C}, X \bowtie \varphi; $$

$$ \mathcal{C}, X \bowtie \varphi \wedge \psi \quad \text{iff} \quad \mathcal{C}, X \bowtie \varphi \text{ and } \mathcal{C}, X \bowtie \psi; $$

$$ \mathcal{C}, X \bowtie K_a\varphi \quad \text{iff} \quad \mathcal{C}, Y \bowtie \varphi \text{ for some } Y \in C \text{ with } a \in \chi(X \cap Y). $$

**Definition 2.5 (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:

$$ \mathcal{C}, X \vdash p_a \quad \text{iff} \quad p_a \in \ell(X); $$

$$ \mathcal{C}, X \vdash \neg\varphi \quad \text{iff} \quad \mathcal{C}, X \bowtie \neg\varphi \text{ and } \mathcal{C}, X \not\bowtie \varphi; $$

$$ \mathcal{C}, X \vdash \varphi \wedge \psi \quad \text{iff} \quad \mathcal{C}, X \vdash \varphi \text{ and } \mathcal{C}, X \vdash \psi; $$

$$ \mathcal{C}, X \vdash K_a\varphi \quad \text{iff} \quad \mathcal{C}, X \bowtie K_a\varphi \text{ and } \mathcal{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. $$

**Remark 2.6.** These definitions are equivalent to those from [vDK23], but differ from them as follows:

* $K_a$ is used as the primary connective instead of $\hat{K}_a$ in [vDK23], which is harmless in light of the duality of $K_a$ and $\hat{K}_a$.

* In [vDK23], $\mathcal{C}, X \vdash p_a$ additionally requires that $a \in \chi(X)$, which is redundant because $\ell(X) \cap P_a = \emptyset$ if $a \notin \chi(X)$.

* In [vDK23], $\mathcal{C}, X \vdash \neg\varphi$ requires $\mathcal{C}, X \bowtie \varphi$ instead of the equivalent $\mathcal{C}, X \bowtie \neg\varphi$ here. These modifications are primarily to avoid the necessity of changing the axiomatization of 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 formulae do not have truth values.<fnref n="3" />

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

(a) $\mathcal{C}, X \vdash \varphi \quad \Rightarrow \quad \mathcal{C}, X \bowtie \varphi$.

(b) $\mathcal{C}, X \vdash \neg\varphi \quad \Rightarrow \quad \mathcal{C}, X \bowtie \varphi$.

(c) It cannot be that both $\mathcal{C}, X \vdash \varphi$ and $\mathcal{C}, X \vdash \neg\varphi$.

*Proof.*

(a) The proof is by induction on the construction of $\varphi$. For $\varphi = \neg\psi$ and $\varphi = K_a\psi$, the statement follows directly from Definition 2.5. 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 \wedge \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 \wedge \theta$.

(b) If $\mathcal{C}, X \vdash \neg\varphi$, then $\mathcal{C}, X \bowtie \neg\varphi$ by clause (a). Hence, $\mathcal{C}, X \bowtie \varphi$ by Definition 2.4.

(c) This follows directly from Definition 2.5. □

<figure><img src="image_5.png" /></figure>

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

(i) if $\mathcal{C}, X \vdash \varphi$, we say that $\varphi$ is true in $X$;

(ii) if $\mathcal{C}, X \not\bowtie \varphi$, we say that $\varphi$ is undefined in $X$, due to crashes;

(iii) if $\mathcal{C}, X \bowtie \varphi$ and $\mathcal{C}, X \not\bowtie \varphi$, i.e. $\mathcal{C}, X \vdash \neg\varphi$, we say that $\varphi$ is false in $X$.

The following corollary is easy to obtain from Definitions 2.4 and 2.5 and the abbreviation $\hat{K}_a\varphi := \neg K_a \neg\varphi$:

<footnote n="3">³The next few results are from [vDK23], but are reproved here for this language.</footnote>
**Corollary 2.8.** For a simplicial model $\mathcal{C} = (C, \chi, \ell)$, its face $X \in C$, formula $\varphi$, and agent a:

(a) $\mathcal{C}, X \triangleright \hat{K}_a\varphi$ iff $\mathcal{C}, Y \triangleright \varphi$ for some $Y \in C$ such that $a \in \chi(X \cap Y)$, i.e. the definability conditions for $\hat{K}_a\varphi$ and $K_a\varphi$ are the same.

(b) $\mathcal{C}, X \models \hat{K}_a\varphi$ iff $\mathcal{C}, Y \models \varphi$ for some $Y \in C$ such that $a \in \chi(X \cap Y)$.

(c) $\mathcal{C}, X \models K_a\varphi$ iff

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

• $\mathcal{C}, Z \models \varphi$ whenever $\mathcal{C}, Z \triangleright \varphi$ for any $Z \in C$ such that $a \in \chi(X \cap Z)$.

(d) $\mathcal{C}, X \models \neg K_a\varphi$ iff $\mathcal{C}, Y \models \neg \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 [vDK23] applies as is:

**Lemma 2.9 (Monotonicity [vDK23]).** For a simplicial model $\mathcal{C} = (C, \chi, \ell)$, its faces $X, Y \in C$ such that $X \subseteq Y$, and formula $\varphi$:

(a) $\mathcal{C}, X \triangleright \varphi \implies \mathcal{C}, Y \triangleright \varphi$.

(b) $\mathcal{C}, X \models \varphi \implies \mathcal{C}, Y \models \varphi$.

(c) $\mathcal{C}, Y \models \varphi$ and $\mathcal{C}, X \triangleright \varphi \implies \mathcal{C}, X \models \varphi$.

□

Since the standard *modus ponens* rule is not valid for impure simplicial models [vDK23] (this result is not present in [vD21]), 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.10 (Definability consequence).** A formula $\psi$ is a *definability consequence* of a set $\Gamma$ of formulae, notation $\Gamma \times \psi$, iff there exists a finite subset $\Gamma' \subseteq \Gamma$ such that for any simplicial model $\mathcal{C} = (C, \chi, \ell)$ and its face $X \in C$,

$$ (\forall \varphi \in \Gamma') \mathcal{C}, X \triangleright \varphi \implies \mathcal{C}, X \triangleright \psi. $$

To simplify notation we omit { and } for finite sets $\Gamma$, where we assume without loss of generality that $\Gamma' = \Gamma$. Note, in particular, that $\emptyset \not\subset \psi$ for any formula $\psi$. For a set $\Delta$ of formulae, $\Gamma \times \Delta$ means that $\Gamma \times \psi$ for all $\psi \in \Delta$. Formulae $\varphi$ and $\psi$ are called *equidefinable*, written $\varphi \triangleright \psi$, when both $\varphi \times \psi$ and $\psi \times \varphi$.

**Definition 2.11.** For a set $\Gamma$ of formulae and agent $a$, we define $K_a\Gamma := \{K_a\theta \mid K_a\theta \in \Gamma\}$.

**Lemma 2.12 (Properties of definability consequence).** For an agent $a$, propositional variable $p_a$, formulae $\varphi, \psi, \theta, \psi_1, \dots, \psi_m$, and formula sets $\Gamma$ and $\Delta$:

(a) $\Gamma \times \varphi \implies \Gamma \cup \Delta \times \varphi$.

(b) $\Gamma \times \Delta$ and $\Delta \times \varphi \implies \Gamma \times \varphi$.

(c) $K_a\varphi \times p_a$.

(d) $p_a \triangleright K_a p_a$.

(e) $K_a\varphi \triangleright K_a K_a\varphi$.

(f) $K_a\varphi \triangleright \neg K_a\varphi \triangleright K_a \neg K_a\varphi$.

(g) $K_a\theta, \varphi \times K_a\varphi$.

(h) $K_a\Gamma, \varphi \times K_a\psi \implies K_a\Gamma, K_a\varphi \times K_a\psi$.

(i) $K_a\Gamma, \neg \varphi \times K_a\psi \implies K_a\Gamma, \neg K_a\varphi \times K_a\psi$.

(j) $K_a(K_a\psi_1 \land \dots \land K_a\psi_m) \to K_a\theta \times K_a(K_a\psi_1 \land \dots \land K_a\psi_m \to \theta)$.
$$ (k) K_a(K_a\psi_1 \wedge \dots \wedge K_a\psi_m) \to \hat{K}_a\theta \bowtie K_a(K_a\psi_1 \wedge \dots \wedge K_a\psi_m \to \theta). $$

$$ (l) K_a\psi_1 \wedge \dots \wedge K_a\psi_m \bowtie K_a(K_a\psi_1 \wedge \dots \wedge K_a\psi_m). $$

*Proof.* The proofs are straightforward by using Definition 2.4 and can be found in Appendix B. □

<figure><img src="image_6.png" /></figure>

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 \wedge \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 formulae 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.13 (Validity [vDK23]).** A formula $\varphi$ is valid in the class of impure simplicial models, written $\vdash \varphi$, iff for any face $X$ of any simplicial model $C$,

$$ C, X \bowtie \varphi \implies C, X \vdash \varphi. $$

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.14 (Validity on facets).** A formula $\varphi$ is true in all facets of all impure simplicial models where it is defined iff $\vdash \varphi$.

*Proof.* The “if” direction trivially follows from Definition 2.13 as valid formulae are true in all faces where they are defined, including all facets. For the “only if” direction, assume that $\not\vdash \varphi$, i.e. there exists a face $X$ of a simplicial model $C$ such that $C, X \bowtie \varphi$ but $C, X \not\vdash \varphi$, i.e. $C, X \vdash \neg \varphi$. By Lemma 2.9(b), $C, Y \vdash \neg \varphi$ for any facet $Y \supseteq X$. By Remark 2.3(ii), such a facet exists. In this facet, $C, Y \bowtie \varphi$ but $C, Y \not\vdash \varphi$, meaning that $\varphi$ is not valid with respect to facets either. □

<figure><img src="image_7.png" /></figure>

As a matter of a sanity check, it is easy to see that all propositional tautologies are valid in the class of impure simplicial models. Indeed, whenever such a tautology is defined, boolean connectives behave the same way as in classical propositional logic.

**Comparing three- and two-valued semantics for impure complexes.** Let us explain the difference between our approach and that of [GLR22] by the leftmost model in Figure 2, which we call $C_3$. It consists of two facets, the 1-dimensional edge, let us call it $X$, to the left and the two-dimensional gray triangle, let us call it $Y$, to the right, which are $a$-adjacent, signifying the fact that agent $a$ is not sure whether agent $c$ is alive (even though this cannot be expressed in the object language).
The first observation to make is that our model $\mathcal{C}_3$ corresponds to multiple models in the semantics of [GLR22]. Indeed, where we treat any local propositional variable of agent $c$ as undefined in edge $X$ because $c$ is dead there, the two-valued semantics requires to assign one of two truth values to each of $c$'s variables. This means that for a local state consisting of $n$ local variables, one model $\mathcal{C}_3$ corresponds to $2^n$ two-valued models that differ in the local state of the dead agent (infinitely many local variables would give rise to infinitely many distinct two-valued models).

The differences among these two-valued models go beyond formulae undefined in $\mathcal{C}_3$, however. The objective changes to the truth values of dead-agent variables result in subjective changes to the knowledge of live agents. In $\mathcal{C}_3$, agent $a$ knows that $p_c$ is true, i.e. $\mathcal{C}_3 \models K_a p_c$, because $p_c$ is true whenever defined. In the two-valued semantics of [GLR22], by contrast, $a$ may or may not know $p_c$ to be true depending on whether $p_c$ is true at $X$, i.e. $C'_2 \models K_a p_c$ while $C''_2 \models \neg K_a p_c$ depending on how $p_c$ is evaluated at $X$, where $c$ is dead, in two-valued models $C'_2$ vs. $C''_2$. Thus, a formula valid in three values may be validated or invalidated by the choice of truth values of dead-agent formulae in two values.

It can also happen that a formula valid in three values must be invalid in two values. Consider, for instance, a model $\mathcal{C}_3^{X-b}$ that differs from $\mathcal{C}_3$ only in the value of $p_b$ in edge $X$, i.e. $\mathcal{C}_3, X \models p_b$ but $\mathcal{C}_3^{X-b}, X \not\models p_b$. Then we have $\mathcal{C}_3^{X-b} \models K_a(p_b \wedge p_c)$ because $p_b \wedge p_c$ is true in the only facet it is defined, at $Y$. By contrast, $\mathcal{C}_2^{X-b}, X \not\models p_b \wedge p_c$ no matter how $p_c$ is evaluated, resulting in $\mathcal{C}_2^{X-b} \not\models K_a(p_b \wedge p_c)$ for all two-valued models corresponding to $\mathcal{C}_3^{X-b}$.

### 3. AXIOM SYSTEM S5$^\boxtimes$

The main goal of this paper is to provide a sound and complete axiomatization for the notion of validity from Definition 2.13. Since pure simplicial models correspond to Kripke models with equivalence accessibility relations, their logic is an extension of multimodal S5, the epistemic logic where individual knowledge has both positive and negative introspection (the extension deals with the locality of propositional variables). The susceptibility of agents to crashes can be reasonably expected to weaken the logic somewhat but one could still expect some subsystem of S5.

As we have discovered, the impact of dead agents and undefined formulae is quite drastic and, interestingly, affects the core reasoning, both modal and propositional, rather than the additional epistemic properties. Although these results are from [vDK23], 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 [vDK23]).** In the presence of at least three agents,

$$ \not\models K_a(\varphi \rightarrow \psi) \rightarrow (K_a\varphi \rightarrow K_a\psi). $$

*Proof.* Consider model $\mathcal{C}_K$ with agents $a, b$, and $c$ in Figure 3. Let $\varphi = p_c$ and $\psi = p_b$. Model $\mathcal{C}_K$ has only two facets, $X$ of dimension 1 and $Y$ of the maximal dimension 2. The instance

$$ K_a(p_c \rightarrow p_b) \rightarrow (K_a p_c \rightarrow K_a p_b) \qquad (3.1) $$

of axiom K is defined in both facets because all formulae 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.
<figure><img src="image_8.png" /><figcaption>Figure 3: Counterexample for the unrestricted axiom K</figcaption></figure>

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, $C_K, X \models \neg p_b$ and, hence, $K_a p_b$ is false in both facets. Thus, not only is instance (3.1) of axiom K falsified in this model, but, in fact, its negation is valid in $C_K$. $\square$

Perhaps, even more surprisingly, even the *modus ponens MP* rule, a staple of most logics, does not generally preserve validity. In [vDK23] (though not in [vD21]), 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.2 (Failure of modus ponens).** In the presence of at least three agents, there exist formulae $\varphi$ and $\psi$ such that

$$ \models \varphi \to \psi \quad \text{and} \quad \models \varphi, \quad \text{but} \quad \not\models \psi. $$

*Proof.* Our counterexample to modus ponens preserving validity uses $\varphi = \top_a \wedge \top_b$ and $\psi = \hat{K}_c \hat{K}_a \hat{K}_b p_c \lor \hat{K}_c \hat{K}_b \hat{K}_a \neg p_c$. We will prove the validity of $\varphi$ and of $\varphi \to \psi$, i.e. that

$$ \models \top_a \wedge \top_b, \qquad (3.2) $$

$$ \models \top_a \wedge \top_b \to \hat{K}_c \hat{K}_a \hat{K}_b p_c \lor \hat{K}_c \hat{K}_b \hat{K}_a \neg p_c. \qquad (3.3) $$

but that applying modus ponens to these valid formulae does not produce a valid formula. For the latter part, consider simplicial model $C_{MP}$ with agents $a$, $b$, and $c$ in Figure 4, which has six facets, all of non-maximal dimension 1. To show that $\not\models \hat{K}_c \hat{K}_a \hat{K}_b p_c \lor \hat{K}_c \hat{K}_b \hat{K}_a \neg p_c$, we demonstrate

$$ C_{MP}, X \models \neg (\hat{K}_c \hat{K}_a \hat{K}_b p_c \lor \hat{K}_c \hat{K}_b \hat{K}_a \neg p_c). $$

It remains to prove the former part, i.e. validities (3.2) and (3.3). The validity of formula $\varphi$ in (3.2) immediately follows from our earlier discussion that local boolean constants $\top_e := p_e \lor \neg p_e$ cannot be falsified. Let us show that formula $\varphi \to \psi$ in (3.3) is valid. Assume that $\varphi \to \psi$ is defined in a face $Q$ of a simplicial model $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 $\hat{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 $\hat{K}_c \hat{K}_a \hat{K}_b p_c$, while if $\neg p_c$ is true in $Q$, so is $\hat{K}_c \hat{K}_b \hat{K}_a \neg p_c$. This completes the proof that $\top_a \wedge \top_b \to \hat{K}_c \hat{K}_a \hat{K}_b p_c \lor \hat{K}_c \hat{K}_b \hat{K}_a \neg p_c$ is true whenever defined.

Let us now show that $\psi = \hat{K}_c \hat{K}_a \hat{K}_b p_c \lor \hat{K}_c \hat{K}_b \hat{K}_a \neg p_c$ is invalidated in model $C_{MP}$. For the second disjunct $\hat{K}_c \hat{K}_b \hat{K}_a \neg 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 $\hat{K}_c \hat{K}_b \hat{K}_a \neg p_c$ in $X$ is fully determined by definability/truth of $\hat{K}_b \hat{K}_a \neg 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,
<figure><img src="image_9.png" /><figcaption>Figure 4: Counterexample for the unrestricted modus ponens</figcaption></figure>

the definability/truth of $\hat{K}_b\hat{K}_a\neg p_c$ in $Y$ is fully determined by definability/truth of $\hat{K}_a\neg p_c$ in $V$. Out of three faces a-adjacent to $V$, i.e. $V, U$, and their common vertex, $\neg p_c$ is defined only in $U$, hence, $\hat{K}_a\neg p_c$ is defined at $V$ and its truth is fully determined by the truth of $\neg p_c$ in $U$. Since $\neg p_c$ is false in $U$, it follows that $\hat{K}_a\neg p_c$ is false in $V$, that $\hat{K}_b\hat{K}_a\neg p_c$ is defined and false in $Y$, and that $\hat{K}_c\hat{K}_b\hat{K}_a\neg 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, $\hat{K}_c\hat{K}_a\hat{K}_b p_c \lor \hat{K}_c\hat{K}_b\hat{K}_a\neg p_c$ is defined but false in $X$.

It is interesting to note that implication (3.3) is nowhere defined in $C_{MP}$. $\square$

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.3** (Axioms system S5$^{\boxtimes}$). The axioms and rules of axiom system S5$^{\boxtimes}$ can be found below (non-standard axioms are in the right column):

<table><thead><tr><th>Taut</th><th>prop. tautologies</th><th>L</th><th>K<sub>a</sub>p<sub>a</sub> ∨ K<sub>a</sub>¬p<sub>a</sub></th><th></th></tr></thead><tbody><tr><td>T</td><td>K<sub>a</sub>ϕ → ϕ</td><td>K<sup>Δ</sup></td><td>K<sub>a</sub>(ϕ → ψ) → (K<sub>a</sub>ϕ → K<sub>a</sub>ψ)</td><td>where ψ, K<sub>a</sub>ϕ ≀≀ ϕ</td></tr><tr><td>4</td><td>K<sub>a</sub>ϕ → K<sub>a</sub>K<sub>a</sub>ϕ</td><td>KK̃</td><td>K<sub>a</sub>(ϕ → ψ) → (K<sub>a</sub>ϕ → K̂<sub>a</sub>ψ)</td><td></td></tr><tr><td>5</td><td>¬K<sub>a</sub>ϕ → K<sub>a</sub>¬K<sub>a</sub>ϕ</td><td>MP<sup>Δ</sup></td><td>from ϕ → ψ and ϕ, infer ψ</td><td>where ψ ≀≀ ϕ</td></tr><tr><td>N</td><td>from ϕ, infer K<sub>a</sub>ϕ</td><td></td><td></td><td></td></tr></tbody></table>

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

* taking all axioms and rules of multimodal S5 that are valid for impure simplicial models (see the left column in Definition 3.3),

* adopting the locality axiom **L** used for pure simplicial models,

* restricting **K** and **MP** by imposing definability conditions, and

* adding axiom $KK̃$.

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 $ϕ$ means both truth in *all* adjacent faces where $ϕ$ is defined (universal aspect) and truth in *at least one* adjacent face (existential aspect). Just like its unrestricted variant **K**, axiom $K^{\boxtimes}$ deals only with the universal aspect. The new axiom $KK̃$ is needed to take care of the existential one.

**Remark 3.4.** Logic S5$^{\boxtimes}$ does not satisfy the property of uniform substitution. Note that agent *a*'s local propositional variable $p_a$ in axiom **L** cannot be replaced with propositional variable $q_b$ of some other agent *b*, let alone with an arbitrary formula. Indeed, $K_a q_b \lor K_a \neg q_b$ for $a \neq b$ is not generally valid, and assuming its validity would go against the ideology of
distributed systems where agents are autonomous and do not generally know each other's local state. This lack of closure with respect to substitution is yet another of the multiple ways logic S5<sup>¶</sup> fails to be a normal modal logic, albeit in this case inherited from the logic of pure simplicial complexes.

## 4. SOUNDNESS

**Definition 4.1** (Derivability in S5<sup>¶</sup>). A formula $\varphi$ is derivable in S5<sup>¶</sup>, written $\vdash \varphi$, iff there is a finite sequence $\psi_1, \dots, \psi_k$ of formulae such that $\psi_k = \varphi$ and each formula in the sequence is either an instance of one of the axioms in Definition 3.3 or follows from earlier formulae in the sequence by one of the rules from Definition 3.3. A formula $\varphi$ is derivable in S5<sup>¶</sup> from a set $\Gamma$ of formulae, written $\Gamma \vdash \varphi$, iff either $\vdash \varphi$ or $\vdash \wedge \Gamma_0 \to \varphi$ for some finite non-empty subset $\Gamma_0 \subseteq \Gamma$.

**Remark 4.2.** The proviso that $\Gamma_0 \neq \emptyset$ 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 S5<sup>¶</sup> is sound with respect to impure simplicial models:

$$ \vdash \varphi \qquad \text{implies} \qquad \vdash \varphi. $$

*Proof.* The proof by induction on an S5<sup>¶</sup>-derivation is standard: one shows that all axioms are valid and all rules preserve validity. It has already been shown in [vDK23] that the locality axiom L and all axioms from the left column of Definition 3.3 are valid and that the necessitation rule N preserves validity. For readers' convenience, we reproduce these proofs in Appendix B. Here we provide the argument for the remaining two axioms and rule:

* Axiom $\mathbf{K}\hat{\mathbf{K}}$ is valid. Consider an arbitrary simplicial model $\mathcal{C} = (\mathcal{C}, \chi, \ell)$ and its face $X \in \mathcal{C}$. If one of formulae $K_a(\varphi \to \psi)$ and $K_a\varphi$ is undefined, axiom $\mathbf{K}\hat{\mathbf{K}}$ is undefined. If both formulae are defined but one of them is false, $\mathbf{K}\hat{\mathbf{K}}$ is true. Finally, assume that $\mathcal{C}, X \models K_a(\varphi \to \psi)$ and $\mathcal{C}, X \models K_a\varphi$, Then, $\mathcal{C}, X \bowtie K_a(\varphi \to \psi)$ by Lemma 2.7(a), i.e. $\mathcal{C}, Y \bowtie \varphi \to \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 \models \varphi \to \psi$ and $\mathcal{C}, Y \models \varphi$. Hence, $\mathcal{C}, Y \models \psi$ and $\mathcal{C}, X \models \hat{K}_a\psi$. We conclude that in this final case again $\mathcal{C}, X \models K_a(\varphi \to \psi) \to (K_a\varphi \to \hat{K}_a\psi)$.

* Axiom $\mathbf{K}^{\square}$ is valid, provided $\psi, K_a\varphi \bowtie \varphi$. From now on, we omit all trivial cases and assume that $\mathcal{C}, X \models K_a(\varphi \to \psi)$ and $\mathcal{C}, X \models K_a\varphi$. As already shown for axiom $\mathbf{K}\hat{\mathbf{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}^{\square}$. $\mathcal{C}, X \models 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 \bowtie \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 \models \varphi$ and $\mathcal{C}, Z \models \varphi \to \psi$, meaning that $\mathcal{C}, Z \models \psi$. This concludes the proof that $\mathcal{C}, X \models K_a\psi$ and, hence, of the validity of $\mathbf{K}^{\square}$.
• Rule MP<sup>Δ</sup> preserves validity, provided $\psi \times \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.4.** 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 $C_K$ from Figure 3, $C_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 S5<sup>Δ</sup> as an epistemic logic (see [vDK23] 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.

**Lemma 4.5 (Hypothetical syllogism).** If $\varphi \to \rho \times \psi$, the following rule is derivable:

$$ \frac{\vdash \varphi \to \psi \qquad \vdash \psi \to \rho}{\vdash \varphi \to \rho} $$

*Proof.*

1. $(\varphi \to \psi) \to ((\psi \to \rho) \to (\varphi \to \rho))$ tautology

2. $\varphi \to \psi$ derivable by assumption

3. $\psi \to \rho$ derivable by assumption

4. $(\psi \to \rho) \to (\varphi \to \rho)$ MP<sup>Δ</sup>(1.,2.) as $(\psi \to \rho) \to (\varphi \to \rho) \times \varphi \to \psi$

5. $\varphi \to \rho$ MP<sup>Δ</sup>(3.,4.) as $\varphi \to \rho \times \psi$ and, hence, $\varphi \to \rho \times \psi \to \rho$

□

**Lemma 4.6 (Contraposition).** The following rule is derivable:

$$ \frac{\vdash \varphi \to \psi}{\vdash \neg \psi \to \neg \varphi} $$

*Proof.* See Appendix B. □

□

**Lemma 4.7 (Replacement for $K_a$).** If $\psi, K_a\varphi \times \varphi$, the following rule is derivable:

$$ \frac{\vdash \varphi \to \psi}{\vdash K_a \varphi \to K_a \psi} $$

*Proof.* See Appendix B. □

□

**Lemma 4.8 (Partial normality of $K_a$ with respect to conjunction).**

$$ \vdash K_a \varphi \wedge K_a \psi \to K_a (\varphi \wedge \psi) $$

$$ \vdash K_a (\varphi \wedge \psi) \to K_a \varphi \wedge K_a \psi. $$
*Proof.* See Appendix B.

<figure><img src="image_10.png" /></figure>

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

**Lemma 4.9 (Knowledge of local variables).**

$$ \vdash p_a \rightarrow K_a p_a $$

$$ \vdash \neg p_a \rightarrow K_a \neg p_a. $$

*Proof.*

1. $K_a p_a \rightarrow p_a$

axiom **T**

2. $\neg p_a \rightarrow \neg K_a p_a$

Lemma 4.6(1.)

3. $K_a p_a \lor K_a \neg p_a$

axiom **L**

4. $(K_a p_a \lor K_a \neg p_a) \rightarrow (\neg K_a p_a \rightarrow K_a \neg p_a)$

tautology

5. $\neg K_a p_a \rightarrow K_a \neg p_a$

MP$^{\vdash}$ (3.,4.) as $\neg K_a p_a \rightarrow K_a \neg p_a \lor K_a p_a \lor K_a \neg p_a$

6. $\neg p_a \rightarrow K_a \neg p_a$

Lemma 4.5(2.,5.) as $\neg p_a \rightarrow K_a \neg p_a \lor \neg K_a p_a$

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

<figure><img src="image_11.png" /></figure>

**Theorem 4.10 (Deduction theorem).**

$$ \Gamma, \varphi \vdash \psi \quad \Rightarrow \quad \Gamma \vdash \varphi \rightarrow \psi. $$

*Proof.* See Appendix B.

<figure><img src="image_12.png" /></figure>

The following three lemmatas are used in the completeness proof:

**Lemma 4.11.** For $m \ge 1$,

$$ \vdash K_a \psi_1 \land \dots \land K_a \psi_m \rightarrow K_a (K_a \psi_1 \land \dots \land K_a \psi_m). $$

*Proof.* See Appendix B.

<figure><img src="image_13.png" /></figure>

**Lemma 4.12.** For $m \ge 1$, the following rule is derivable:

$$ \frac{\vdash \neg(\varphi \land K_a \psi_1 \land \dots \land K_a \psi_m)}{\vdash \neg(K_a \varphi \land K_a \psi_1 \land \dots \land K_a \psi_m)} $$

*Proof.* See Appendix B.

<figure><img src="image_14.png" /></figure>

**Lemma 4.13.** For $m \ge 1$, the following rule is derivable:

$$ \frac{\vdash \neg(\neg \varphi \land K_a \psi_1 \land \dots \land K_a \psi_m)}{\vdash \neg(K_a \varphi \land K_a \psi_1 \land \dots \land K_a \psi_m)} $$

*Proof.* See Appendix B.

<figure><img src="image_15.png" /></figure>
## 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} := \{\varphi \mid \mathcal{M}, w \models \varphi\}$ of formulae that are 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 formulae that are true in $w$ provides a complete description of all truth values in $w$: the set of formulae false in $w$ is $\bar{\Gamma}_{\mathcal{M},w}$, the complement of the set of true formulae.

The completeness proof is achieved by combining these syntactic objects (sets of formulae) — 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 \text{ is false at a world } \Gamma \iff \varphi \notin \Gamma \iff \neg \varphi \in \Gamma. \quad (5.1) $$

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 formulae, making the set of worlds of the canonical model a subset of the power set of the set of all formulae. 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 formulae that are true would not be sufficient to represent the distribution of our three truth values. How would we be able to distinguish formulae that are false from those that are undefined? Fortunately, it is possible to do by separating the two descriptions of falsity in (5.1), which were equivalent in the binary semantics. In our three-valued case, we will formulate the truth lemma to associate true formulae with formulae in $\Gamma$, false formulae with formulae whose negation is in $\Gamma$, with all remaining formulae, i.e. formulae $\varphi$ such that both $\varphi \notin \Gamma$ and $\neg \varphi \notin \Gamma$, undefined. This enables us to continue building the canonical model out of sets of formulae rather than pairs of sets or some such.

The next hurdle is that such sets of formulae 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 formulae 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 formulae 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$ alive 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} = \{K_{a_1}\Gamma, K_{a_2}\Gamma, \dots, K_{a_m}\Gamma\}$$

of local states 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 formulae that are true in this facet need not lead to inconsistency. There may well be another facet where $a$ is alive and some previously undefined formulae, including $p_a$, are true there. (It is also possible that adding $p_a$ does lead to inconsistency if, e.g., $K_b \neg 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 \emptyset$ is *definability complete* iff it contains all its definability consequences, i.e. if $\varphi \in \Xi$ whenever $\Xi \times \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 formulae, written $\varphi \in^* \Gamma$, iff either $\varphi \in \Gamma$ or $\neg \varphi \in \Gamma$. Accordingly, a formula is *not determined*, written $\varphi \notin^* \Gamma$, iff $\Gamma \cap \{\varphi, \neg \varphi\} = \emptyset$.

**Definition 5.3 (Consistent sets).** A set $\Gamma$ of formulae is *inconsistent* iff $\vdash \neg \wedge \Gamma_0$ for some finite $\emptyset \neq \Gamma_0 \subseteq \Gamma$. Otherwise, $\Gamma$ is *consistent*. In particular, $\emptyset$ is consistent.

**Remark 5.4.** The non-standard requirement $\Gamma_0 \neq \emptyset$ is due to the lack of boolean constants.

**Definition 5.5 (Definability-maximal consistent (DMC) sets).** A consistent set $\Gamma \neq \emptyset$ is *definability maximal* (a DMC set) iff it determines all its definability consequences:

$$\Gamma \times \varphi \implies \varphi \in^* \Gamma. \qquad (5.2)$$

The following facts 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 formulae $\varphi$ and $\psi$ and a finite set $\Gamma \neq \emptyset$ of formulae:

(a) If $\vdash \neg \wedge \Gamma$, then $\vdash \neg (\varphi \wedge \wedge \Gamma)$.

(b) If $\vdash \wedge \Gamma \rightarrow \psi$, then $\vdash \varphi \wedge \wedge \Gamma \rightarrow \psi$.
*Proof.* See Appendix B. □

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 \emptyset$, the following statements are equivalent:

(i) $\Gamma$ is a DMC set;

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

*Proof.* (i) $\implies$ (ii). Let $\Gamma$ be a DMC set, i.e. let (5.2) hold. We start by showing that set $\Xi := \{\varphi \mid \Gamma \times \varphi\}$ is definability complete. Indeed, if $\Xi \times \psi$, then $\Gamma \times \psi$ by Lemma 2.12(b), and $\psi \in \Xi$ by construction. Since $\Gamma \times \psi$ for any $\psi \in \Gamma$, clearly $\Gamma \subseteq \Xi$, in particular, $\Xi \neq \emptyset$. 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 \times \psi$, which, due to (5.2), would imply that $\neg\psi \in \Gamma$. But then $\vdash \neg(\psi \wedge \neg\psi)$ for $\{\psi, \neg\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$.

(ii) $\implies$ (i). Let $\Xi$ be a definability-complete set, $\Gamma$ be maximal among consistent subsets of $\Xi$, and let $\Gamma \times \varphi$. Then there is some finite subset $\Gamma_0 \subseteq \Gamma$ such that $\varphi$ is defined whenever all formulae from $\Gamma_0$ are. Since $\Gamma_0 \subseteq \Gamma \subseteq \Xi$, we have $\Xi \times \varphi$. Since $\varphi \bowtie \neg\varphi$, also $\Xi \times \neg\varphi$. Due to the definability completeness of $\Xi$, it means that $\{\varphi, \neg\varphi\} \subseteq \Xi$. Suppose towards a contradiction that $\varphi \notin \Gamma$ and $\neg\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 \{\neg\varphi\}$ would be inconsistent. In view of Lemma 5.6(a), without loss of generality, $\vdash \neg(\varphi \wedge \wedge \Gamma_0 \wedge \wedge \Gamma_1)$ and $\vdash \neg(\neg\varphi \wedge \wedge \Gamma_0 \wedge \wedge \Gamma_2)$ for some non-empty finite subsets $\Gamma_1, \Gamma_2 \subseteq \Gamma$. The following is a propositional tautology:

$$ \vdash \neg(\varphi \wedge \wedge \Gamma_0 \wedge \wedge \Gamma_1) \rightarrow \neg(\neg\varphi \wedge \wedge \Gamma_0 \wedge \wedge \Gamma_2) \rightarrow \neg(\wedge \Gamma_0 \wedge \wedge \Gamma_1 \wedge \wedge \Gamma_2). $$

Since it is clear that

$$ \neg(\neg\varphi \wedge \wedge \Gamma_0 \wedge \wedge \Gamma_2) \rightarrow \neg(\wedge \Gamma_0 \wedge \wedge \Gamma_1 \wedge \wedge \Gamma_2) \quad \bowtie \quad \neg(\varphi \wedge \wedge \Gamma_0 \wedge \wedge \Gamma_1), $$

it would follow by $\mathbf{MP}^{\bowtie}$ that

$$ \vdash \neg(\neg\varphi \wedge \wedge \Gamma_0 \wedge \wedge \Gamma_2) \rightarrow \neg(\wedge \Gamma_0 \wedge \wedge \Gamma_1 \wedge \wedge \Gamma_2). $$

Note, additionally, that

$$ \neg(\wedge \Gamma_0 \wedge \wedge \Gamma_1 \wedge \wedge \Gamma_2) \quad \bowtie \quad \neg(\neg\varphi \wedge \wedge \Gamma_0 \wedge \wedge \Gamma_2). $$

Indeed, whenever $\neg(\wedge \Gamma_0 \wedge \wedge \Gamma_1 \wedge \wedge \Gamma_2)$ is defined, all formulae from $\Gamma_2$ and $\Gamma_0$ are defined, the latter implying that $\varphi$ is defined. Hence, $\neg(\neg\varphi \wedge \wedge \Gamma_0 \wedge \wedge \Gamma_2)$ is defined. Thus, another application of $\mathbf{MP}^{\bowtie}$ would yield $\vdash \neg(\wedge \Gamma_0 \wedge \wedge \Gamma_1 \wedge \wedge \Gamma_2)$. 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.8.** For any simplicial model $\mathcal{C} = (C, \chi, \ell)$ and its face $X \in \mathcal{C}$, the truth set

$$ \Gamma_{C,X} := \{\varphi \mid \mathcal{C}, X \models \varphi\} $$

is a DMC set.

*Proof.* It is clear that $\Gamma_{C,X}$ cannot be empty. Hence, to show that $\Gamma_{C,X}$ is consistent, consider any non-empty finite subset $\Gamma_0 \subseteq \Gamma_{C,X}$. We have $C, X \models \bigwedge \Gamma_0$ by construction. Therefore, $C, X \not\models \neg \bigwedge \Gamma_0$ and $X \not\models \neg \bigwedge \Gamma_0$ by the soundness of S5$^{\boxtimes}$ (Theorem 4.3). Since $\Gamma_0$ was chosen arbitrarily, we have established that $\Gamma_{C,X}$ is consistent.

It remains to show that $\Gamma_{C,X}$ is definability maximal (DM). Assume that $\Gamma_{C,X} \times \varphi$, i.e. there is a finite subset $\Gamma_0 \subseteq \Gamma_{C,X}$ such that $\varphi$ is defined whenever all formulae from $\Gamma_0$ are. Since, by construction, $C, X \models \psi$ for all $\psi \in \Gamma_{C,X}$, it follows from Lemma 2.7(a) that $C, X \bowtie \psi$ for all $\psi \in \Gamma_0$. Thus, $C, X \bowtie \varphi$, meaning that either $C, X \models \varphi$ or $C, X \models \neg \varphi$. By construction, either $\varphi$ or $\neg \varphi$ belongs to $\Gamma_{C,X}$, i.e. $\varphi \in^* \Gamma_{C,X}$. $\square$

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

**Lemma 5.9 (Properties of DMC sets).** For DMC sets $\Gamma$ and $\Delta$, an agent $a$, propositional variable $p_a \in P_a$, and formulae $\varphi$, $\varphi_1$, $\varphi_2$, and $\psi$:

(a) $\Gamma \times \varphi$ and $\Gamma \vdash \varphi$ $\Rightarrow$ $\varphi \in \Gamma$.

(b) $\Gamma \times \varphi$ $\Rightarrow$ exactly one of $\varphi \in \Gamma$ and $\neg \varphi \in \Gamma$ holds.

(c) $\varphi_1 \wedge \varphi_2 \in \Gamma$ $\iff$ both $\varphi_1 \in \Gamma$ and $\varphi_2 \in \Gamma$.

(d) $K_a \Gamma \neq \emptyset$ and $\varphi \in^* \Gamma$ $\Rightarrow$ $K_a \varphi \in^* \Gamma$.

(e) $p_a \in \Gamma$ iff $K_a p_a \in \Gamma$, and $\neg p_a \in \Gamma$ iff $K_a \neg p_a \in \Gamma$. Hence, $p_a \in^* \Gamma$ implies $K_a \Gamma \neq \emptyset$.

(f) $K_a \Gamma, \varphi \times K_a \psi$ and $K_a \varphi \in^* \Gamma$ $\Rightarrow$ $K_a \psi \in^* \Gamma$.

(g) $K_a \Gamma \subseteq K_a \Delta$ and $\neg K_a \varphi \in \Gamma$ $\Rightarrow$ $\neg K_a \varphi \in \Delta$.

(h) $K_a \varphi \in \Gamma$ $\Rightarrow$ $\neg \varphi \notin \Gamma$ and $K_a \Gamma \cup \{\varphi\}$ is consistent.

(i) $\neg K_a \varphi \in \Gamma$ $\Rightarrow$ $K_a \Gamma \cup \{\neg \varphi\}$ is consistent.

*Proof.*

(a) Since $\Gamma \vdash \varphi$, we have $\vdash \bigwedge \Gamma_0 \rightarrow \varphi$ for some finite $\emptyset \neq \Gamma_0 \subseteq \Gamma$. Given tautology $\vdash (\bigwedge \Gamma_0 \rightarrow \varphi) \rightarrow (\neg \varphi \wedge \bigwedge \Gamma_0)$, it follows by MP$^{\boxtimes}$ that $\vdash (\neg \varphi \wedge \bigwedge \Gamma_0)$ because $\neg (\neg \varphi \wedge \bigwedge \Gamma_0) \times \bigwedge \Gamma_0 \rightarrow \varphi$. Thus, $\neg \varphi \in \Gamma$ would contradict $\Gamma$'s consistency. On the other hand, either $\varphi \in \Gamma$ or $\neg \varphi \in \Gamma$ because $\Gamma$ is DM and $\Gamma \times \varphi$. Thus, $\varphi \in \Gamma$.

(b) It follows from $\vdash (\neg \varphi \wedge \neg \varphi)$ and $\Gamma$ being DM.

(c) It follows by clause (a) since for $i = 1, 2$ $\varphi_1 \wedge \varphi_2 \vdash \varphi_i$, $\varphi_1 \wedge \varphi_2 \times \varphi_i$, $\varphi_1, \varphi_2 \vdash \varphi_1 \wedge \varphi_2$, and $\varphi_1, \varphi_2 \times \varphi_1 \wedge \varphi_2$.

(d) By Lemma 2.12(g), $\Gamma \times K_a \varphi$. Hence, $K_a \varphi \in^* \Gamma$ because $\Gamma$ is DM.

(e) By Lemma 2.12(d), since $p_a \bowtie \neg p_a$, it follows that $p_a \bowtie K_a p_a$ and $\neg p_a \bowtie K_a \neg p_a$. By Lemma 4.9, $p_a \vdash K_a p_a$ and $\neg p_a \vdash K_a \neg p_a$. By axiom T, $K_a p_a \vdash p_a$ and $K_a \neg p_a \vdash \neg p_a$. Hence, the first two iff claims follow from clause (a). The last claim follows from them.

(f) By Lemma 2.12(h), $K_a \Gamma, K_a \varphi \times K_a \psi$, hence, also $K_a \Gamma, \neg K_a \varphi \times K_a \psi$. Thus, however $\Gamma$ determines $K_a \varphi$, we know that $\Gamma \times K_a \psi$. Now $K_a \psi \in^* \Gamma$ follows from $\Gamma$ being DM.

(g) By clause (a), since $\neg K_a \varphi \times K_a \neg K_a \varphi$ and additionally $\neg K_a \varphi \vdash K_a \neg K_a \varphi$ due to axiom 5, it follows that, if $\neg K_a \varphi \in \Gamma$, then $K_a \neg K_a \varphi \in K_a \Gamma \subseteq K_a \Delta$. Similarly, $K_a \neg K_a \varphi \times \neg K_a \varphi$ by Lemma 2.12(f) and $K_a \neg K_a \varphi \vdash \neg K_a \varphi$ by axiom T. Hence, $\neg K_a \varphi \in \Delta$ by clause (a).

(h) Since $\neg (K_a \varphi \wedge \neg \varphi)$ is equidefinable and equivalent to $K_a \varphi \rightarrow \varphi$, i.e. to axiom T, having $\neg \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 (without loss of generality in view of Lemma 5.6(a)) $\vdash \neg(\varphi \wedge K_a\psi_1 \wedge \dots \wedge K_a\psi_m)$. A contradiction $\vdash \neg(K_a\varphi \wedge K_a\psi_1 \wedge \dots \wedge K_a\psi_m)$ to the consistency of $\Gamma$ would follow by Lemma 4.12.

(i) The argument here is similar to the preceding clause, except that Lemma 4.13 is used in place of Lemma 4.12 and instead of assuming $K_a\Gamma \neq \emptyset$, the non-emptiness is inferred from $K_a\neg K_a\varphi \in \Gamma$, which is obtained by the same argument as in clause (g). $\square$

**Lemma 5.10 (Lindenbaum Lemma).** Any consistent set $\Gamma \neq \emptyset$ can be extended to a DMC set $\Delta \supseteq \Gamma$ such that $\Gamma \times \psi$ for all $\psi \in \Delta$.

*Proof.* Let $\psi_0, \psi_1, \dots$ be an enumeration of the set $\Gamma^{\kappa} := \{\psi \mid \Gamma \succ \psi\}$ of all definability consequences of $\Gamma$. Starting from $\Delta_0 := \Gamma$, add formulae $\psi_i$ one by one, unless doing so would cause inconsistency: $\Delta_{i+1} := \Delta_i \cup \{\psi_i\}$ if that set is consistent or $\Delta_{i+1} := \Delta_i$ otherwise. Define $\Delta := \cup_{i=0}^{\infty} \Delta_i \subseteq \Gamma^{\kappa}$, which is consistent for the same reason as in the standard Lindenbaum construction that enumerates all formulae: were $\Delta$ inconsistent, one of $\Delta_i$ would have been. We now show that $\Delta$ is maximal among consistent subsets of $\Gamma^{\kappa}$. Indeed, any $\psi \in \Gamma^{\kappa} \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^{\kappa}$ is definability complete by Lemma 2.12(b), it follows from Lemma 5.7 that $\Delta$ is a DMC set. $\square$

**Definition 5.11 (Simplicial canonical model).** Let $\mathcal{G}$ denote the collection of all DMC sets. For $\Gamma \in \mathcal{G}$, we define

$$X_{\Gamma} := \{K_{a}\Gamma \mid a \in A, K_{a}\Gamma \neq \emptyset\}.$$

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

* $\mathcal{C}^c := \{X \mid (\exists \Gamma \in \mathcal{G}) (\emptyset \neq X \subseteq X_{\Gamma})\}$. Accordingly, its set of vertices can be computed as $\mathcal{V}^c = \cup_{X \in \mathcal{C}^c} X = \{K_a\Gamma \mid \Gamma \in \mathcal{G}, a \in A, K_a\Gamma \neq \emptyset\}$.

* For $K_a\Gamma \in \mathcal{V}^c$, we define $\chi^c(K_a\Gamma) := a$.

* For $K_a\Gamma \in \mathcal{V}^c$, we define $\ell^c(K_a\Gamma) := \{p_a \in P_a \mid K_a p_a \in K_a\Gamma\}$.

In other words, given $\Gamma \in \mathcal{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 Section 6). The color of vertex $K_a\Gamma$ must obviously be $a$, and the local variables that are true there are those known by this agent $a$.

**Remark 5.12.** Unlike sets $\Gamma \in \mathcal{G}$, sets $K_a\Gamma$ are not DMC sets. For instance, neither $p_a \in K_a\Gamma$ nor $\neg p_a \in K_a\Gamma$ even though either $K_a p_a \in K_a\Gamma$ or $K_a \neg p_a \in K_a\Gamma$ and $p_a$ is a definability consequence of either.

**Lemma 5.13 (Correctness).** The object $\mathcal{C}^c$ constructed in Definition 5.11 is a simplicial model.

*Proof.* The proof is straightforward and can be found in Appendix B. $\square$

<figure><img src="image_16.png" /></figure>

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

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

(ii) 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.14** (Truth Lemma). Let $C^c$ be the canonical simplicial model constructed in Definition 5.11. Then, for any DMC set $\Gamma \in \mathbb{G}$ and any formula $\varphi$,

$$ \varphi \notin^* \Gamma \quad \Rightarrow \quad C^c, X_\Gamma \not\models \varphi, \qquad (5.3) $$

$$ \varphi \in \Gamma \quad \Rightarrow \quad C^c, X_\Gamma \models \varphi, \qquad (5.4) $$

$$ \neg\varphi \in \Gamma \quad \Rightarrow \quad C^c, X_\Gamma \models \neg\varphi. \qquad (5.5) $$

*Proof.* The proof is by induction on the construction of $\varphi$. Note that $X_\Gamma \in C^c$.<fnref n="4" />

**For** $\varphi = p_a$:

(5.3) Assume $p_a \notin^* \Gamma$. Then $\Gamma \not\models p_a$ because $\Gamma$ is DM, hence, $K_a\Gamma = \emptyset$ by Lemma 2.12(c). Therefore, $K_a\Gamma \notin X_\Gamma$, $a \notin \chi^c(X_\Gamma)$, and $C^c, X_\Gamma \not\models p_a$.

(5.4) Assume $p_a \in \Gamma$. Then, $K_a p_a \in K_a \Gamma$ by Lemma 5.9(e). Since $K_a \Gamma \neq \emptyset$, we have $K_a \Gamma \in \mathcal{V}^c$, and $p_a \in \ell^c(K_a \Gamma) \subseteq \ell^c(X_\Gamma)$. Therefore, $C^c, X_\Gamma \models p_a$.

(5.5) Assume $\neg p_a \in \Gamma$. Then, $K_a \neg p_a \in K_a \Gamma$ by Lemma 5.9(e). Again, $K_a \Gamma \neq \emptyset$ implies $K_a \Gamma \in \mathcal{V}^c$ and $a \in \chi^c(X_\Gamma)$. Therefore, $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.9(e). Hence, $p_a \notin \ell^c(X_\Gamma)$ meaning $C^c, X_\Gamma \not\models p_a$. Thus, in summary, $C^c, X_\Gamma \models \neg p_a$.

**For** $\varphi = \neg\psi$:

(5.3) Assume $\neg\psi \notin^* \Gamma$. Then $\psi \notin^* \Gamma$ since $\Gamma$ is DM and $\psi \bowtie \neg\psi$. Then $C^c, X_\Gamma \not\models \psi$ by induction hypothesis (5.3) for $\psi$. Accordingly, $C^c, X_\Gamma \not\models \neg\psi$.

(5.4) Assume $\neg\psi \in \Gamma$. Then, $C^c, X_\Gamma \models \neg\psi$ by induction hypothesis (5.5) for $\psi$.

(5.5) Assume $\neg\neg\psi \in \Gamma$. Then $\psi \in \Gamma$ by Lemma 5.9(a) because $\neg\neg\psi \bowtie \psi$ and $\neg\neg\psi \bowtie \psi$. Thus, $C^c, X_\Gamma \models \psi$ by induction hypothesis (5.4) for $\psi$. Accordingly, $C^c, X_\Gamma \models \neg\neg\psi$.

**For** $\varphi = \psi_1 \wedge \psi_2$:

(5.3) Assume $\psi_1 \wedge \psi_2 \notin^* \Gamma$. Then $\psi_i \notin^* \Gamma$ for at least one of the conjuncts since $\Gamma$ is DM and $\tilde{\psi}_1, \tilde{\psi}_2 \bowtie \psi_1 \wedge \psi_2$ for any $\tilde{\psi}_j \in \{\psi_j, \neg\psi_j\}$. Then $C^c, X_\Gamma \not\models \psi_i$ by induction hypothesis (5.3) for this $\psi_i$. Accordingly, $C^c, X_\Gamma \not\models \psi_1 \wedge \psi_2$.

(5.4) Assume $\psi_1 \wedge \psi_2 \in \Gamma$. Then, $\psi_i \in \Gamma$ for both conjuncts by Lemma 5.9(c). Thus, $C^c, X_\Gamma \models \psi_i$ by induction hypothesis (5.4) for both $\psi_i$. Accordingly, $C^c, X_\Gamma \models \psi_1 \wedge \psi_2$.

(5.5) Assume $\neg(\psi_1 \wedge \psi_2) \in \Gamma$. Then $\psi_j \in^* \Gamma$ since $\Gamma$ is DM and $\neg(\psi_1 \wedge \psi_2) \bowtie \psi_j$ for both conjuncts. Hence, $C^c, X_\Gamma \bowtie \psi_j$ by Lemma 2.7(a)-(b) and induction hypotheses (5.4)-(5.5) for both $\psi_j$. Thus, $C^c, X_\Gamma \bowtie \psi_1 \wedge \psi_2$. On the other hand, $\psi_1 \wedge \psi_2 \notin \Gamma$ by the consistency of $\Gamma$, hence, $\psi_i \notin \Gamma$ for at least one of $\psi_i$ by Lemma 5.9(c). It follows that $\neg\psi_i \in \Gamma$ and $C^c, X_\Gamma \not\models \psi_i$ by induction hypothesis (5.5) for this $\psi_i$. Hence, $C^c, X_\Gamma \not\models \psi_1 \wedge \psi_2$ and, overall, $C^c, X_\Gamma \models \neg(\psi_1 \wedge \psi_2)$.

**For** $\varphi = K_a\psi$:

(5.3) Assume that $K_a\psi \notin^* \Gamma$.

- If $K_a\Gamma = \emptyset$, 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 $C^c, Y \bowtie \psi$. In this case, we have $C^c, X_\Gamma \not\models K_a\psi$.

- If $K_a\Gamma \neq \emptyset$, 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 Definition 5.11, $\emptyset \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 \emptyset$, meaning that $a \in \chi^c(X_\Gamma \cap X_\Delta)$. Since $K_a\psi \in^* \Delta$ iff $K_a\psi \in^* \Gamma$ by Lemma 5.9(g), it follows that $K_a\psi \notin^* \Delta$. By Lemma 5.9(d), $\psi \notin^* \Delta$ and, by induction hypothesis (5.3), $C^c, X_\Delta \not\models \psi$. From Lemma 2.9(a), it follows that $C^c, Y \not\models \psi$. Since face $Y$, which is $a$-adjacent to $X_\Gamma$, was chosen arbitrarily, $C^c, X_\Gamma \not\models K_a\psi$.

<footnote n="4">⁴See the proof of Lemma 5.13 in Appendix B.</footnote>
(5.4) Assume that $K_a\psi \in \Gamma$. Hence, $K_a\Gamma \neq \emptyset$, $K_a\Gamma \in X_\Gamma$, and $a \in \chi^c(X_\Gamma)$. By Corollary 2.8(c), for $C^c$, $X_\Gamma \models K_a\psi$, it is sufficient to show that:

(i) $C^c, Y \bowtie \psi$ implies $C^c, Y \models \psi$ for all $Y \in C^c$ such that $a \in \chi^c(X_\Gamma \cap Y)$, and

(ii) $C^c, Y \models \psi$ for some $Y \in C^c$ with $a \in \chi^c(X_\Gamma \cap Y)$.

To show (i), consider any $Y \in C^c$ such that $a \in \chi^c(X_\Gamma \cap Y)$ and $C^c, Y \bowtie \psi$. It follows from $a \in \chi^c(X_\Gamma \cap Y)$ that $K_a\Gamma \in Y$. By Definition 5.11, $\emptyset \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, $C^c, X_\Delta \bowtie \psi$ by Lemma 2.9(a). It follows from induction hypothesis (5.3) that $\psi \in^* \Delta$. Since $K_a\Delta = K_a\Gamma$ we have $K_a\psi \in \Delta$ and, hence, $\neg\psi \notin \Delta$ by Lemma 5.9(h). Therefore, $\psi \in \Delta$. Thus, $C^c, X_\Delta \models \psi$ by induction hypothesis (5.4), and $C^c, Y \models \psi$ by Lemma 2.9(c). We have shown that $\psi$ is true in all faces a-adjacent to $X_\Gamma$ where it is defined.

To show (ii), consider $K_a\Gamma \cup \{\psi\}$, which is consistent by Lemma 5.9(h). By Lindenbaum Lemma 5.10, there exists a DMC set $\Delta \supseteq K_a\Gamma \cup \{\psi\}$ such that $K_a\Gamma, \psi \times \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, \psi \times K_a\theta$, by Lemma 2.12(h) $K_a\Gamma, K_a\psi \times K_a\theta$, and, hence, $\Gamma \times K_a\theta$. Then $K_a\theta \in^* \Gamma$ because $\Gamma$ is DM. Were $\neg K_a\theta \in \Gamma$, we would have had $\neg K_a\theta \in \Delta$ by Lemma 5.9(g), 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 (5.4) for $\psi$, we have $C^c, X_\Delta \models \psi$, and $X_\Delta$ serves as a face a-adjacent to $X_\Gamma$ where $\psi$ is true.

(5.5) Assume $\neg K_a\psi \in \Gamma$. By Corollary 2.8(d), for $C^c, X_\Gamma \models \neg K_a\psi$, it is sufficient to show that $C^c, Y \models \neg\psi$ for some $Y \in C^c$ with $a \in \chi^c(X_\Gamma \cap Y)$. Consider $K_a\Gamma \cup \{\neg\psi\}$, which is consistent by Lemma 5.9(i). By Lindenbaum Lemma 5.10, there exists a DMC set $\Delta \supseteq K_a\Gamma \cup \{\neg\psi\}$ such that $K_a\Gamma, \neg\psi \times \psi$ for all $\psi \in \Delta$. By construction, $K_a\Gamma \subseteq K_a\Delta$. To prove the opposite inclusion, consider any $K_a\theta \in \Delta$. By Lemma 2.12(i), $K_a\Gamma, \neg K_a\psi \times K_a\theta$, and, hence, $\Gamma \times K_a\theta$. Then $K_a\theta \in^* \Gamma$ because $\Gamma$ is DM. Were $\neg K_a\theta \in \Gamma$, this would have meant that $\neg K_a\theta \in \Delta$ by Lemma 5.9(g), 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 (5.5) for $\psi$, we have $C^c, X_\Delta \models \neg\psi$, and $X_\Delta$ serves as a face a-adjacent to $X_\Gamma$ where $\psi$ is false. $\square$

**Theorem 5.15 (Completeness).** Axiomatization S5$^{\bowtie}$ is complete with respect to impure simplicial models:

$$ \models \varphi \quad \implies \quad \vdash \varphi. $$

*Proof.* We prove the contraposition. Suppose $\not\models \varphi$ for a formula $\varphi$. Then $\{\neg\varphi\}$ is a consistent set. By Lindenbaum Lemma 5.10, $\{\neg\varphi\}$ is a subset of some DMC set $\Gamma$. By Truth Lemma 5.14, $C^c, X_\Gamma \models \neg\varphi$. Thus, $\varphi$ is not valid. $\square$

## 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 $C^c$ constructed in Definition 5.11 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.14 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 $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 $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 $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 $C_{Xmas} = (C, \chi, \ell)$, which we are going to call *Christmas cracker models*,

<figure><img src="image_17.png" /><figcaption>Figure 5: Christmas cracker models</figcaption></figure>

for three agents a, b, and c with

• six **vertices** $V = \{v_a^l, v_a^r, v_b^l, v_b^r, v_c^l, v_c^r\}$,

• four **facets** $\mathcal{F}(C) = \{\{v_a^l, v_b^l, v_c^l\}, \{v_a^r, v_b^r, v_c^r\}, \{v_a^l, v_c^r\}, \{v_c^l, v_a^r\}\}$,

• a **chromatic map** $\chi: 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), \quad \ell(v_b^l) = \ell(v_b^r), \quad \ell(v_c^l) = \ell(v_c^r). \qquad (6.1) $$

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 Figure 5). It immediately follows from the rotational symmetry that, omitting the name of the simplicial model and using

$$ \Gamma_V := \{\varphi \mid C_{Xmas}, V \models \varphi\} \qquad (6.2) $$

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 formulae that are true in a face also provides a complete description of formulae false and undefined in the same face). These sets are DMC sets according to Lemma 5.8.

Accordingly, in the canonical model $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$ and $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 Definitions 2.4 and 2.5 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 formulae $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.* It is sufficient to show that $\Gamma_{Z_l} \subsetneq \Gamma_{U_l}$ in Example 6.1. Note that all formulae 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

$$ C, Z_l \models \varphi \implies C, U_l \models \varphi \quad \text{and} \quad C, Z_l \models \neg\varphi \implies C, U_l \models \neg\varphi. $$

For propositional variables $\varphi = p_a \in P_a$, this is trivial as truth values for them are determined by $\ell(v_a^l)$. For $\varphi = p_c \in P_c$, it follows from (6.1). No $p_b \in P_b$ is defined in $Z_l$.

For $\varphi = \neg\psi$, if $\neg\psi$ is true in $Z_l$, then $\psi$ is false there, hence, $\psi$ is false in $U_l$ by the induction hypothesis, making $\neg\psi$ true in $U_l$. The argument for false $\neg\psi$ in $Z_l$ is analogous.

For $\varphi = \psi_1 \wedge \psi_2$, if $\psi_1 \wedge \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 \wedge \psi_2$ is true in $U_l$. If $\psi_1 \wedge \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 \wedge \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 (6.2). 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 (6.2). 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 $\neg p_b$ must belong to $\Gamma_{U_l}$ (depending on valuation $\ell$), but neither belongs to $\Gamma_{Z_l}$, making the inclusion strict. $\square$

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 $C^c$ is impure.

**Example 6.3.** Given at least three agents $a, b$, and $c$, consider simplicial model $C$ in Figure 6 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 := \{\varphi | C, U \models \varphi\}$ for
$$v_a \frac{U}{v_c}$$

<caption>Figure 6: Simplicial model: agent b is dead</caption>

the set of formulae that are 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 $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 \emptyset$, meaning that $X_\Gamma \subsetneq X_\Delta$ is not a facet. Take any propositional variable $p_b \in P_b$. Since $K_b\varphi \times p_b$ for any formula $\varphi$ by Lemma 2.12(c), it follows that $p_b \in^* \Delta$, i.e. $p_b \in \Delta$ or $\neg p_b \in \Delta$. If $p_b \in \Delta$, then, since $K_a\theta, p_b \times K_a p_b$ for any $\theta$ by Lemma 2.12(g), we conclude that $K_a p_b \in^* \Delta$ because $K_a\Delta = K_a\Gamma \neq \emptyset$. The same applies if $\neg p_b \in \Delta$ since $p_b \bowtie \neg 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, $\neg K_a p_b$ cannot be in $\Delta$ because this would imply that $K_a \neg K_a p_b \in K_a\Delta$ by axiom 5 and, hence, $K_a \neg K_a p_b \in 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 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 S5$^{\bowtie}$ applies to any number of agents, for small numbers of agents, e.g., for one or two agents, simpler axiomatizations should be possible. As follows from Lemmatas 3.1–3.2, 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 would be more expressive. Such more expressive semantics would allow for an embedding into two-valued semantics for impure complexes.

Adding distributed knowledge modalities is a generalization of the semantics, see, for instance, [GKLR23]. This would also increase 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 would come with different axiomatizations, and also promise to address specific modeling issues in distributed computing.

## ACKNOWLEDGMENT

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. We also thank the anonymous reviewers for their comments and remarks.
REFERENCES

[ÅW17] Thomas Ågotnes and Yì N. Wáng. Resolving distributed knowledge. *Artificial Intelligence*, 252:1–21, November 2017. doi:10.1016/j.artint.2017.07.002.

[BMS98] Alexandru Baltag, Lawrence S. Moss, and Slawomir 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, Evanston, Illinois, USA, July 22–24 1998. Morgan Kaufmann. URL: http://www.tark.org/proceedings/tark_jul22_98/p43-baltag.pdf.

[BMZ90] Ofer Biran, Shlomo Moran, and Shmuel Zaks. A combinatorial characterization of the distributed 1-solvable tasks. *Journal of Algorithms*, 11(3):420–440, September 1990. doi:10.1016/0196-6774(90)90020-F.

[BS20] 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.

[DM90] Cynthia Dwork and Yoram Moses. Knowledge and common knowledge in a Byzantine environment: Crash failures. *Information and Computation*, 88(2):156–186, October 1990. doi:10.1016/0890-5401(90)90014-9.

[DNR15] 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.

[FLP85] 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, April 1985. doi:10.1145/3149.214121.

[GKLR23] Éric Goubault, Roman Kniazev, Jérémy Ledent, and Sergio Rajsbaum. Semi-simplicial set models for distributed knowledge. In *2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, Boston, USA, 26–29 June 2023. IEEE. doi:10.1109/LICS56636.2023.10175737.

[GLR21] É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, June 2021. doi:10.1016/j.ic.2020.104597.

[GLR22] Éric Goubault, Jérémy Ledent, and Sergio Rajsbaum. A simplicial model for $KB_4$: 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.

[Hin62] Jaakko Hintikka. *Knowledge and Belief: An Introduction to the Logic of the Two Notions*. Cornell University Press, 1962.

[HKR14] Maurice Herlihy, Dmitry Kozlov, and Sergio Rajsbaum. *Distributed Computing through Combinatorial Topology*. Morgan Kaufmann, 2014. doi:10.1016/C2011-0-07032-1.

[HM90] Joseph Y. Halpern and Yoram Moses. Knowledge and common knowledge in a distributed environment. *Journal of the ACM*, 37(3):549–587, July 1990. doi:10.1145/79147.79161.

[HRT00] Maurice Herlihy, Sergio Rajsbaum, and Mark R. Tuttle. An overview of synchronous message-passing and topology. In *Geometry and Topology in Concurrency theory*, volume 39(2) of *Electronic Notes in Theoretical Computer Science*, PennState, USA, August 21 2000. Elsevier. doi:10.1016/S1571-0661(05)01148-5.

[HRT09] 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.

[HS99] Maurice Herlihy and Nir Shavit. The topological structure of asynchronous computability. *Journal of the ACM*, 46(6):858–923, November 1999. doi:10.1145/331524.331529.
[HSS09] 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, September 2009. doi:10.1017/S1755020309990141.

[LA87] Michael C. Loui and Hosame H. Abu-Amara. Memory requirements for agreement among unreliable asynchronous processes. In Franco P. Preparata, editor, *Parallel and Distributed Computing*, volume 4 of *Advances in Computing Research: A Research Annual*, pages 163–183. JAI Press, 1987.

[Led19] Jérémy Ledent. *Geometric semantics for asynchronous computability*. PhD thesis, Paris-Saclay University, Palaiseau, France, 2019. Prepared at École polytechnique. URL: https://tel.archives-ouvertes.fr/tel-02445180.

[Mos15] 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.

[MS93] Yoram Moses and Yoav Shoham. Belief as defeasible knowledge. *Artificial Intelligence*, 64(2):299–321, December 1993. doi:10.1016/0004-3702(93)90107-M.

[Pnu77] Amir Pnueli. The temporal logic of programs. In *18th Annual Symposium on Foundations of Computer Science (Formerly called the Annual Symposium on Switching and Automata Theory)*, pages 46–57, Providence, Rhode Island, Oct. 31–Nov. 2 1977. IEEE. doi:10.1109/SFCS.1977.32.

[PS18] 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.

[SZ00] 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.

[VCR21] 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*, volume 335 of *Electronic Proceedings in Theoretical Computer Science*, pages 307–321, Beijing, China, June 25–27 2021. Open Publishing Association. doi:10.4204/EPTCS.335.29.

[vD21] 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.

[vDFK22] 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.

[vDGL+21] 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, June 2021. doi:10.1016/j.jlamp.2021.100662.

[vDGLR22] 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.

[vDK23] Hans van Ditmarsch and Roman Kuznets. Wanted dead or alive: Epistemic logic for impure simplicial complexes. Eprint 2103.03032, arXiv, 2023. Accepted to *Journal of Logic and Computation*. doi:10.48550/arXiv.2103.03032.

[vDvdHK07] 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.
# APPENDIX A. AUXILIARY STATEMENTS

**Lemma A.1.** *The following rule is derivable:*

$$ \frac{\vdash \varphi_1 \rightarrow \psi_1 \quad \dots \quad \vdash \varphi_m \rightarrow \psi_m}{\vdash \varphi_1 \wedge \dots \wedge \varphi_m \rightarrow \psi_1 \wedge \dots \wedge \psi_m}. $$

*Proof.* The tautology

$$ (\varphi_1 \rightarrow \psi_1) \rightarrow (\dots \rightarrow (\varphi_m \rightarrow \psi_m) \rightarrow (\varphi_1 \wedge \dots \wedge \varphi_m \rightarrow \psi_1 \wedge \dots \wedge \psi_m)) $$

can be used, followed by $m$ applications of $MP^{\bowtie}$ justified by the fact that the definability of $\varphi_1 \wedge \dots \wedge \varphi_m \rightarrow \psi_1 \wedge \dots \wedge \psi_m$ implies the definability of all $\varphi_i$'s and all $\psi_j$'s, hence, of any other formula in the derivation. $\square$

**Lemma A.2.**

$$ \vdash K_a \psi_1 \wedge \dots \wedge K_a \psi_m \rightarrow K_a(\psi_1 \wedge \dots \wedge \psi_m). $$

*Proof.* Induction on $m$. For $m = 1$, the statement is trivial because $K_a \psi_1 \rightarrow K_a \psi_1$ is a tautology. For $m = 2$, it follows from Lemma 4.8. Assume the statement holds for $m = k$.

1. $K_a \psi_1 \wedge \dots \wedge K_a \psi_k \rightarrow K_a(\psi_1 \wedge \dots \wedge \psi_k)$ induction hypothesis

2. $K_a \psi_{k+1} \rightarrow K_a \psi_{k+1}$ tautology

3. $K_a \psi_1 \wedge \dots \wedge K_a \psi_k \wedge K_a \psi_{k+1} \rightarrow K_a(\psi_1 \wedge \dots \wedge \psi_k) \wedge K_a \psi_{k+1}$ Lemma A.1(1.,2.)

4. $K_a(\psi_1 \wedge \dots \wedge \psi_k) \wedge K_a \psi_{k+1} \rightarrow K_a(\psi_1 \wedge \dots \wedge \psi_k \wedge \psi_{k+1})$ Lemma 4.8

5. $K_a \psi_1 \wedge \dots \wedge K_a \psi_{k+1} \rightarrow K_a(\psi_1 \wedge \dots \wedge \psi_{k+1})$ Lemma 4.5(3.,4.) as $K_a \psi_1 \wedge \dots \wedge K_a \psi_{k+1} \rightarrow K_a(\psi_1 \wedge \dots \wedge \psi_{k+1}) \bowtie K_a(\psi_1 \wedge \dots \wedge \psi_k) \wedge K_a \psi_{k+1}$

$\square$

# APPENDIX B. ADDITIONAL PROOFS

**Lemma 2.12** (Properties of definability consequence). For an agent a, propositional variable $p_a$, formulae $\varphi, \psi, \theta, \psi_1, \dots, \psi_m$, and formula sets $\Gamma$ and $\Delta$:

(a) $\Gamma \bowtie \varphi \Rightarrow \Gamma \cup \Delta \bowtie \varphi$.

(b) $\Gamma \bowtie \Delta$ and $\Delta \bowtie \varphi \Rightarrow \Gamma \bowtie \varphi$.

(c) $K_a \varphi \bowtie p_a$.

(d) $p_a \bowtie K_a p_a$.

(e) $K_a \varphi \bowtie K_a K_a \varphi$.

(f) $K_a \varphi \bowtie \neg K_a \varphi \bowtie K_a \neg K_a \varphi$.

(g) $K_a \theta, \varphi \bowtie K_a \varphi$.

(h) $K_a \Gamma, \varphi \bowtie K_a \psi \Rightarrow K_a \Gamma, K_a \varphi \bowtie K_a \psi$.

(i) $K_a \Gamma, \neg \varphi \bowtie K_a \psi \Rightarrow K_a \Gamma, \neg K_a \varphi \bowtie K_a \psi$.

(j) $K_a(K_a \psi_1 \wedge \dots \wedge K_a \psi_m) \rightarrow K_a \theta \bowtie K_a(K_a \psi_1 \wedge \dots \wedge K_a \psi_m \rightarrow \theta)$.

(k) $K_a(K_a \psi_1 \wedge \dots \wedge K_a \psi_m) \rightarrow \hat{K}_a \theta \bowtie K_a(K_a \psi_1 \wedge \dots \wedge K_a \psi_m \rightarrow \theta)$.

(l) $K_a \psi_1 \wedge \dots \wedge K_a \psi_m \bowtie K_a(K_a \psi_1 \wedge \dots \wedge K_a \psi_m)$.

*Proof.*

(a) $\Gamma \bowtie \varphi$ means that there is a finite subset $\Gamma' \subseteq \Gamma$ such that $\varphi$ is defined whenever all formulae from $\Gamma'$ are. But $\Gamma'$ is also a finite subset of $\Gamma \cup \Delta$. Hence, $\Gamma \cup \Delta \bowtie \varphi$.
(b) Since $\Delta \bowtie \varphi$, there exists a finite subset $\Delta' = \{\psi_1, \dots, \psi_m\} \subseteq \Delta$ such that $\varphi$ is defined whenever all $\psi_i$'s are. Since $\Gamma \bowtie \Delta$, for each $\psi_i$ there must exist a finite subset $\Gamma_i \subseteq \Gamma$ such that $\psi_i$ is defined whenever all formulae from $\Gamma_i$ are. It is now easy to see that $\varphi$ is defined whenever all formulae from the finite subset $\bigcup_{i=1}^m \Gamma_i \subseteq \Gamma$ are. Hence, $\Gamma \bowtie \varphi$.

(c) Starting from this clause, we consider an arbitrary simplicial model $\mathcal{C} = (\mathcal{C}, \chi, \ell)$ and its face $X \in \mathcal{C}$ and assume all formulae to the left of $\bowtie$ to be defined in $X$, e.g., here we assume that $\mathcal{C}, X \bowtie K_a\varphi$. By Definition 2.4, there exists $Y \in \mathcal{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 Definition 2.4.

(d) To show that $p_a \bowtie K_a p_a$, assume that $\mathcal{C}, X \bowtie p_a$. By Definition 2.4, $a \in \chi(X)$. Equivalently, $a \in \chi(X \cap X)$. Hence, $\mathcal{C}, X \bowtie K_a p_a$ by Definition 2.4. The other direction follows from clause (c).

(e) Assume $\mathcal{C}, X \bowtie K_a\varphi$. By Definition 2.4, there exists $Y \in \mathcal{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 Definition 2.4, there exists $Y \in \mathcal{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 \mathcal{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$.

(f) That $K_a\varphi \bowtie \neg K_a\varphi$ follows from Definition 2.4. It remains to prove only that additionally $\neg K_a\varphi \bowtie K_a \neg K_a\varphi$.

Assume $\mathcal{C}, X \bowtie \neg K_a\varphi$. Hence, $\mathcal{C}, X \bowtie K_a\varphi$. By Definition 2.4, there exists $Y \in \mathcal{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 \neg K_a\varphi$. Therefore, $\mathcal{C}, X \bowtie K_a \neg K_a\varphi$.

Assume $\mathcal{C}, X \bowtie K_a \neg K_a\varphi$. By Definition 2.4, there is $Y \in \mathcal{C}$ such that $\mathcal{C}, Y \bowtie \neg 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 \mathcal{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 \neg K_a\varphi$.

(g) Assume $\mathcal{C}, X \bowtie K_a\theta$ and $\mathcal{C}, X \bowtie \varphi$. By Definition 2.4, there exists $Y \in \mathcal{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$.

(h) Assume $K_a\Gamma, \varphi \bowtie K_a\psi$, i.e. there is a finite subset $\Gamma' \subseteq K_a\Gamma \cup \{\varphi\}$ such that $K_a\psi$ is defined whenever all formulae from $\Gamma'$ are. If $\varphi \notin \Gamma'$, then $\Gamma' \subseteq K_a\Gamma \cup \{K_a\varphi\}$, so we are done. Otherwise, $\Gamma' = 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 \mathcal{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 \mathcal{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 \mathcal{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 formulae 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 \bowtie K_a\psi$.

(i) Assume $K_a\Gamma, \neg\varphi \bowtie K_a\psi$. Since $\varphi \bowtie \neg\varphi$, also $K_a\Gamma, \varphi \bowtie K_a\psi$. By clause (h), it follows that $K_a\Gamma, K_a\varphi \bowtie K_a\psi$. Since $K_a\varphi \bowtie \neg K_a\varphi$, we finally obtain $K_a\Gamma, \neg K_a\varphi \bowtie K_a\psi$.

(j) Assume $\mathcal{C}, X \bowtie K_a(K_a\psi_1 \wedge \dots \wedge K_a\psi_m) \to K_a\theta$. Then, $\mathcal{C}, X \bowtie K_a(K_a\psi_1 \wedge \dots \wedge K_a\psi_m)$ and $\mathcal{C}, X \bowtie K_a\theta$. By Definition 2.4, there exists $Y \in \mathcal{C}$ such that $\mathcal{C}, Y \bowtie \theta$ and $a \in \chi(X \cap Y)$ and there exists $Z \in \mathcal{C}$ such that $\mathcal{C}, Z \bowtie K_a\psi_1 \wedge \dots \wedge 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 \mathcal{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 $C, Y \bowtie K_a\psi_i$ for each $i$. Consequently, $C, Y \bowtie K_a\psi_1 \wedge \cdots \wedge K_a\psi_m \to \theta$, and, as required, $C, X \bowtie K_a(K_a\psi_1 \wedge \cdots \wedge K_a\psi_m \to \theta)$.

(k) The proof of this clause is the same as for the preceding clause because $K_a\theta \bowtie \hat{K}_a\theta$.

(l) Assume $C, X \bowtie K_a\psi_1 \wedge \cdots \wedge K_a\psi_m$. Since $C, X \bowtie K_a\psi_1$, there is $Z$ such that $C, Z \bowtie \psi_1$ and $a \in \chi(X \cap Z)$. Thus, $a \in \chi(X \cap X)$. Therefore, $C, X \bowtie K_a(K_a\psi_1 \wedge \cdots \wedge K_a\psi_m)$.

Assume $C, X \bowtie K_a(K_a\psi_1 \wedge \cdots \wedge K_a\psi_m)$. By Definition 2.4, there exists $Y \in C$ such that $C, Y \bowtie K_a\psi_1 \wedge \cdots \wedge K_a\psi_m$ and $a \in \chi(X \cap Y)$. It follows that $C, Y \bowtie K_a\psi_i$ for each $i$, meaning that for each $i$ there exists $Z_i \in C$ such that $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 $C, X \bowtie K_a\psi_i$ for each $i$. Thus $C, X \bowtie K_a\psi_1 \wedge \cdots \wedge K_a\psi_m$. $\square$

**Theorem 4.3 (Soundness).** Axiom system S5$^{\bowtie}$ is sound with respect to impure simplicial models:

$$ \vdash \varphi \quad \text{implies} \quad \vdash \varphi. $$

*Proof.* Additional cases proved earlier in [vDK23].

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

* **Axiom L** is valid. Assume $C, X \bowtie K_a p_a \lor K_a \neg p_a$. Then $C, X \bowtie K_a p_a$, that is, there is a face $Y$ with $a \in \chi(X \cap Y)$ such that $C, Y \bowtie p_a$. Hence, $a \in \chi(X)$ and $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 $C, X \models K_a p_a \lor K_a \neg p_a$. Given $C, X_a \bowtie p_a$, either $C, X_a \models p_a$ or $C, X_a \models \neg p_a$. Since $X_a$ is the only $a$-colored vertex in any face $a$-adjacent to $X_a$, in the former case, $C, X_a \models K_a p_a$ and in the latter case, $C, X_a \models K_a \neg p_a$. Either way, $C, X_a \models K_a p_a \lor K_a \neg p_a$. Since $\{X_a\} \subseteq X$, it now follows from Lemma 2.9(b) that $C, X \models K_a p_a \lor K_a \neg p_a$, as required.

* **Axiom T** is valid. Assume $C, X \bowtie K_a\varphi \to \varphi$. It follows that $C, X \bowtie \varphi$ and $a \in \chi(X)$. If $C, X \models K_a\varphi$, then $C, Y \bowtie \varphi$ implies $C, Y \models \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 $C, X \bowtie \varphi$, we conclude $C, X \models \varphi$. We have shown that $\models K_a\varphi \to \varphi$.

* **Axiom 4** is valid. If $C, X \models K_a\varphi$, then $C, X \bowtie K_a\varphi$ by Lemma 2.7(a). In particular, $C, W \bowtie \varphi$ for some $W$ such that $a \in \chi(X \cap W)$. We also conclude $C, X \bowtie K_a K_a\varphi$ by Lemma 2.12(e) and, hence, $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 $C, X \models 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, $C, Y \bowtie K_a\varphi$. To show that $C, Y \models K_a\varphi$, take an arbitrary face $Z$ such that $a \in \chi(Y \cap Z)$ and $C, Z \bowtie \varphi$. Then $a \in \chi(X \cap Z)$. Thus, $C, Z \bowtie \varphi$ and the assumption $C, X \models K_a\varphi$ yield $C, Z \models \varphi$. We proved that $\varphi$ is true whenever defined in faces $a$-adjacent to $Y$. Hence, $C, Y \models K_a\varphi$. This shows that $K_a\varphi$ is true whenever defined in faces $a$-adjacent to $X$. In addition, $C, X \bowtie K_a\varphi$ and $a \in \chi(X \cap X)$. Hence, $C, X \models K_a K_a\varphi$. We have shown $\models K_a\varphi \to K_a K_a\varphi$.

* **Axiom 5** is valid. If $C, X \models \neg K_a\varphi$, then $C, W \models \neg \varphi$ for some $W$ such that $a \in \chi(X \cap W)$ by Corollary 2.8(d). By Lemma 2.7(a), both $C, X \bowtie \neg K_a\varphi$ and $C, W \bowtie \neg \varphi$. The former implies $C, X \bowtie K_a \neg K_a\varphi$ by Lemma 2.12(f). The latter implies $C, W \bowtie \varphi$ by Definition 2.4. Hence, $C, X \bowtie \neg K_a\varphi \to K_a \neg K_a\varphi$, so that we do not need to assume this separately. In order to prove $C, X \models K_a \neg 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 Corollary 2.8(d) that $C, Y \models \neg K_a\varphi$. Thus, we proved that $\neg K_a\varphi$ is true in all faces $a$-adjacent to $X$. Given that $X$ is one of such faces, $C, X \models K_a \neg K_a\varphi$. We have shown $\models \neg K_a\varphi \to K_a \neg K_a\varphi$.
• Necessitation rule N preserves validity. Assume $\vdash \varphi$ and $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, $C, X \bowtie K_a\varphi$ means that there is a face a-adjacent to X where $\varphi$ is defined. Therefore, $C, X \vdash K_a\varphi$. We have shown that $K_a\varphi$ is true whenever defined, as required. Thus, $\vdash K_a\varphi$. □

**Lemma 4.6 (Contraposition).** *The following rule is derivable:*

$$ \frac{\vdash \varphi \rightarrow \psi}{\vdash \neg \psi \rightarrow \neg \varphi}. $$

*Proof.*

1. $(\varphi \rightarrow \psi) \rightarrow (\neg \psi \rightarrow \neg \varphi)$ tautology

2. $\varphi \rightarrow \psi$ derivable by assumption

3. $\neg \psi \rightarrow \neg \varphi$ $MP^{\bowtie}(1.,2.)$ as $\neg \psi \rightarrow \neg \varphi \bowtie \varphi \rightarrow \psi$ □

**Lemma 4.7 (Replacement for $K_a$).** *If $\psi, K_a\varphi \bowtie \varphi$, the following rule is derivable:*

$$ \frac{\vdash \varphi \rightarrow \psi}{\vdash K_a\varphi \rightarrow K_a\psi}. $$

*Proof.*

1. $\varphi \rightarrow \psi$ derivable by assumption

2. $K_a(\varphi \rightarrow \psi)$ $N(1.)$

3. $K_a(\varphi \rightarrow \psi) \rightarrow (K_a\varphi \rightarrow K_a\psi)$ $K^{\bowtie}$ as $\psi, K_a\varphi \bowtie \varphi$

4. $K_a\varphi \rightarrow K_a\psi$ $MP^{\bowtie}(2.,3.)$ as $K_a\varphi \rightarrow K_a\psi \bowtie K_a(\varphi \rightarrow \psi)$ follows from $\psi, K_a\varphi \bowtie \varphi$ Let us explain why $K_a\varphi \rightarrow K_a\psi \bowtie K_a(\varphi \rightarrow \psi)$ holds in the last step. If $K_a\varphi \rightarrow 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 \bowtie \varphi$ applied to Y yields that $\varphi$, and, hence, $\varphi \rightarrow \psi$, is also defined in Y, making $K_a(\varphi \rightarrow \psi)$ defined in X. □

**Lemma 4.8 (Partial normality of $K_a$ with respect to conjunction).**

$$ \vdash K_a\varphi \wedge K_a\psi \rightarrow K_a(\varphi \wedge \psi) $$

$$ \nvDash K_a(\varphi \wedge \psi) \rightarrow K_a\varphi \wedge K_a\psi. $$

*Proof.*

1. $\varphi \rightarrow (\psi \rightarrow \varphi \wedge \psi)$ tautology

2. $K_a(\varphi \rightarrow (\psi \rightarrow \varphi \wedge \psi))$ $N(1.)$

3. $K_a(\varphi \rightarrow (\psi \rightarrow \varphi \wedge \psi)) \rightarrow (K_a\varphi \rightarrow K_a(\psi \rightarrow \varphi \wedge \psi))$ axiom $K^{\bowtie}$ as $\psi \rightarrow \varphi \wedge \psi \bowtie \varphi$

4. $K_a\varphi \rightarrow K_a(\psi \rightarrow \varphi \wedge \psi)$ as $K_a\varphi \rightarrow K_a(\psi \rightarrow \varphi \wedge \psi) \bowtie K_a(\varphi \rightarrow (\psi \rightarrow \varphi \wedge \psi))$ $MP^{\bowtie}(2.,3.)$

5. $K_a(\psi \rightarrow \varphi \wedge \psi) \rightarrow (K_a\psi \rightarrow K_a(\varphi \wedge \psi))$ axiom $K^{\bowtie}$ as $\varphi \wedge \psi \bowtie \psi$

6. $K_a\varphi \rightarrow (K_a\psi \rightarrow K_a(\varphi \wedge \psi))$ as $K_a\varphi \rightarrow (K_a\psi \rightarrow K_a(\varphi \wedge \psi)) \bowtie K_a(\psi \rightarrow \varphi \wedge \psi)$ Lemma 4.5(4.,5.)

7. $(K_a\varphi \rightarrow (K_a\psi \rightarrow K_a(\varphi \wedge \psi))) \rightarrow (K_a\varphi \wedge K_a\psi \rightarrow K_a(\varphi \wedge \psi))$ tautology

8. $K_a\varphi \wedge K_a\psi \rightarrow K_a(\varphi \wedge \psi)$ as $K_a\varphi \wedge K_a\psi \rightarrow K_a(\varphi \wedge \psi) \bowtie K_a\varphi \rightarrow (K_a\psi \rightarrow K_a(\varphi \wedge \psi))$ $MP^{\bowtie}(6.,7.)$
Figure 3 provides a counterexample to the opposite direction. Indeed, in simplicial model $\mathcal{C}_K$, formula $K_a(p_b \wedge 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). $\square$

**Theorem 4.10 (Deduction theorem).**

$$ \Gamma, \varphi \vdash \psi \quad \Rightarrow \quad \Gamma \vdash \varphi \to \psi. $$

*Proof.*

* Case $\vdash \psi$. Then $\vdash \psi \to (\varphi \to \psi)$ as a tautology, and $\vdash \varphi \to \psi$ is obtained by $\mathbf{MP}^{\bowtie}$ because $\varphi \to \psi \bowtie \psi$. Hence, $\Gamma \vdash \varphi \to \psi$ by Definition 4.1.

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

* Case $\vdash \bigwedge \Gamma_0 \to \psi$ for a finite non-empty subset $\Gamma_0 \subseteq \Gamma$.

1. $\bigwedge \Gamma_0 \to \psi$ assumption

2. $\bigwedge \Gamma_0 \wedge \varphi \to \bigwedge \Gamma_0$ tautology

3. $\bigwedge \Gamma_0 \wedge \varphi \to \psi$ Lemma 4.5(1.,2.) as $\bigwedge \Gamma_0 \wedge \varphi \to \psi \bowtie \bigwedge \Gamma_0$

4. $(\bigwedge \Gamma_0 \wedge \varphi \to \psi) \to (\bigwedge \Gamma_0 \to (\varphi \to \psi))$ tautology

5. $\bigwedge \Gamma_0 \to (\varphi \to \psi)$ $\mathbf{MP}^{\bowtie}(3.,4.)$ as $\bigwedge \Gamma_0 \to (\varphi \to \psi) \bowtie \bigwedge \Gamma_0 \wedge \varphi \to \psi$ Hence, $\Gamma \vdash \varphi \to \psi$ by Definition 4.1 based on $\Gamma_0 \subseteq \Gamma$.

* Case $\vdash \bigwedge \Gamma_0 \wedge \varphi \to \psi$ for a finite subset $\{\varphi\} \sqcup \Gamma_0 \subseteq \Gamma$ such that $\Gamma_0 \neq \emptyset$.

1. $\bigwedge \Gamma_0 \wedge \varphi \to \psi$ assumption

2. $(\bigwedge \Gamma_0 \wedge \varphi \to \psi) \to (\bigwedge \Gamma_0 \to (\varphi \to \psi))$ tautology

3. $\bigwedge \Gamma_0 \to (\varphi \to \psi)$ $\mathbf{MP}^{\bowtie}(1.,2.)$ as $\bigwedge \Gamma_0 \to (\varphi \to \psi) \bowtie \bigwedge \Gamma_0 \wedge \varphi \to \psi$ Hence, $\Gamma \vdash \varphi \to \psi$ by Definition 4.1 based on $\Gamma_0 \subseteq \Gamma$. $\square$

**Lemma 4.11.** For $m \ge 1$,

$$ \vdash K_a \psi_1 \wedge \dots \wedge K_a \psi_m \quad \to \quad K_a(K_a \psi_1 \wedge \dots \wedge K_a \psi_m). $$

*Proof.*

1. $K_a \psi_i \to K_a K_a \psi_i$ for each $i = 1, \dots, m$ axiom 4

2. $K_a \psi_1 \wedge \dots \wedge K_a \psi_m \to K_a K_a \psi_1 \wedge \dots \wedge K_a K_a \psi_m$ Lemma A.1(1.)

3. $K_a K_a \psi_1 \wedge \dots \wedge K_a K_a \psi_m \to K_a(K_a \psi_1 \wedge \dots \wedge K_a \psi_m)$ Lemma A.2

4. $K_a \psi_1 \wedge \dots \wedge K_a \psi_m \to K_a(K_a \psi_1 \wedge \dots \wedge K_a \psi_m)$ as $K_a \psi_1 \wedge \dots \wedge K_a \psi_m \to K_a(K_a \psi_1 \wedge \dots \wedge K_a \psi_m) \bowtie K_a K_a \psi_1 \wedge \dots \wedge K_a K_a \psi_m$ Lemma 4.5(2.,3.)

<figure><img src="image_18.png" /></figure>

**Lemma 4.12.** For $m \ge 1$, the following rule is derivable:

$$ \frac{\vdash \neg(\varphi \wedge K_a \psi_1 \wedge \dots \wedge K_a \psi_m)}{\vdash \neg(K_a \varphi \wedge K_a \psi_1 \wedge \dots \wedge K_a \psi_m)}. $$

*Proof.*

1. $\neg(\varphi \wedge K_a \psi_1 \wedge \dots \wedge K_a \psi_m)$ derivable by assumption

2. $K_a \psi_1 \wedge \dots \wedge K_a \psi_m \to \neg \varphi$ equidefinable and equivalent to 1.

3. $K_a(K_a \psi_1 \wedge \dots \wedge K_a \psi_m \to \neg \varphi)$ $\mathbf{N}(2.)$

4. $K_a(K_a \psi_1 \wedge \dots \wedge K_a \psi_m \to \neg \varphi) \to (K_a(K_a \psi_1 \wedge \dots \wedge K_a \psi_m) \to \hat{K}_a \neg \varphi)$ axiom $\mathbf{K}\hat{\mathbf{K}}$

5. $K_a(K_a \psi_1 \wedge \dots \wedge K_a \psi_m) \to \hat{K}_a \neg \varphi$ $\mathbf{MP}^{\bowtie}(3.,4.)$ as, by Lemma 2.12(k), $K_a(K_a \psi_1 \wedge \dots \wedge K_a \psi_m) \to \hat{K}_a \neg \varphi \bowtie K_a(K_a \psi_1 \wedge \dots \wedge K_a \psi_m \to \neg \varphi)$

6. $K_a \psi_1 \wedge \dots \wedge K_a \psi_m \to K_a(K_a \psi_1 \wedge \dots \wedge K_a \psi_m)$ Lemma 4.11
7. $K_a\psi_1 \wedge \dots \wedge K_a\psi_m \rightarrow \hat{K}_a \neg \varphi$ Lemma 4.5(5.,6.) as, by Lemma 2.12(l),
$K_a\psi_1 \wedge \dots \wedge K_a\psi_m \rightarrow \hat{K}_a \neg \varphi \quad \times \quad K_a(K_a\psi_1 \wedge \dots \wedge K_a\psi_m)$

8. $K_a\psi_1 \wedge \dots \wedge K_a\psi_m \rightarrow \neg K_a \neg \neg \varphi$ from 7. by definition of $\hat{K}_a$

9. $\neg\neg K_a \neg\neg \varphi \rightarrow \neg(K_a\psi_1 \wedge \dots \wedge K_a\psi_m)$ Lemma 4.6(8.)

10. $K_a \neg \neg \varphi \rightarrow \neg (K_a \psi_1 \wedge \dots \wedge K_a \psi_m)$ equidefinable and equivalent to 9.

11. $\varphi \rightarrow \neg\neg\varphi$ tautology

12. $K_a\varphi \rightarrow K_a \neg\neg\varphi$ Lemma 4.7(11.) as $\neg\neg\varphi \times \varphi$

13. $K_a\varphi \rightarrow \neg(K_a\psi_1 \wedge \dots \wedge K_a\psi_m)$ Lemma 4.5(12.,10.)

as $K_a\varphi \rightarrow \neg(K_a\psi_1 \wedge \dots \wedge K_a\psi_m) \quad \times \quad K_a \neg\neg\varphi$

14. $\neg(K_a\varphi \wedge K_a\psi_1 \wedge \dots \wedge K_a\psi_m)$ equidefinable and equivalent to 13.

□

**Lemma 4.13.** For $m \ge 1$, the following rule is derivable:

$$ \frac{\vdash \neg(\neg\varphi \wedge K_a\psi_1 \wedge \dots \wedge K_a\psi_m)}{\vdash \neg(\neg K_a\varphi \wedge K_a\psi_1 \wedge \dots \wedge K_a\psi_m)}. $$

*Proof.*

1. $\neg(\neg\varphi \wedge K_a\psi_1 \wedge \dots \wedge K_a\psi_m)$ derivable by assumption

2. $K_a\psi_1 \wedge \dots \wedge K_a\psi_m \rightarrow \varphi$ equidefinable and equivalent to 1.

3. $K_a(K_a\psi_1 \wedge \dots \wedge K_a\psi_m \rightarrow \varphi)$ N(2.)

4. $K_a(K_a\psi_1 \wedge \dots \wedge K_a\psi_m \rightarrow \varphi) \rightarrow (K_a(K_a\psi_1 \wedge \dots \wedge K_a\psi_m) \rightarrow K_a\varphi)$ K$^{\times}$
as $K_a(K_a\psi_1 \wedge \dots \wedge K_a\psi_m) \quad \times \quad K_a\psi_1 \wedge \dots \wedge K_a\psi_m$ by Lemma 2.12(l)

5. $K_a(K_a\psi_1 \wedge \dots \wedge K_a\psi_m) \rightarrow K_a\varphi$ MP$^{\times}(3.,4.)$ as, by Lemma 2.12(j),
$K_a(K_a\psi_1 \wedge \dots \wedge K_a\psi_m) \rightarrow K_a\varphi \quad \times \quad K_a(K_a\psi_1 \wedge \dots \wedge K_a\psi_m \rightarrow \varphi)$

6. $K_a\psi_1 \wedge \dots \wedge K_a\psi_m \rightarrow K_a(K_a\psi_1 \wedge \dots \wedge K_a\psi_m)$ Lemma 4.11

7. $K_a\psi_1 \wedge \dots \wedge K_a\psi_m \rightarrow K_a\varphi$ Lemma 4.5(5.,6.) as, by Lemma 2.12(l),
$K_a\psi_1 \wedge \dots \wedge K_a\psi_m \rightarrow K_a\varphi \quad \times \quad K_a(K_a\psi_1 \wedge \dots \wedge K_a\psi_m)$

8. $\neg(\neg K_a\varphi \wedge K_a\psi_1 \wedge \dots \wedge K_a\psi_m)$ equidefinable and equivalent to 7.

□

**Lemma 5.6** (Monotonicity of $\vdash$). For formulae $\varphi$ and $\psi$ and a finite set $\Gamma \neq \emptyset$ of formulae:

(a) If $\vdash \neg\neg\Gamma$, then $\vdash \neg(\varphi \wedge \neg\neg\Gamma)$.

(b) If $\vdash \neg\neg\Gamma \rightarrow \psi$, then $\vdash \varphi \wedge \neg\neg\Gamma \rightarrow \psi$.

*Proof.*

(a) $1. \neg\neg\Gamma \rightarrow \neg(\varphi \wedge \neg\neg\Gamma)$ tautology

2. $\neg\neg\Gamma$ derivable by assumption

3. $\neg(\varphi \wedge \neg\neg\Gamma)$ MP$^{\times}(1.,2.)$ as $\neg(\varphi \wedge \neg\neg\Gamma) \times \neg\neg\Gamma$

(b) $1. \varphi \wedge \neg\neg\Gamma \rightarrow \neg\neg\Gamma$ tautology

2. $\neg\neg\Gamma \rightarrow \psi$ derivable by assumption

3. $\varphi \wedge \neg\neg\Gamma \rightarrow \psi$ Lemma 4.5(1.,2.) as $\varphi \wedge \neg\neg\Gamma \rightarrow \psi \times \neg\neg\Gamma$

□

**Lemma 5.13** (Correctness). The object $C^c$ constructed in Definition 5.11 is a simplicial
model.

*Proof.* Since any face of any simplicial model yields a DMC set by Lemma 5.8, $G \neq \emptyset$. DMC sets are not empty by definition. Since $\neg\neg\varphi \times \varphi$ and $\varphi_1 \wedge \varphi_2 \times \varphi_i$ for $i = 1,2$, it follows
that, for each $\Gamma \in \mathbb{G}$, either $p_a \in^* \Gamma$ or $K_a\psi \in^* \Gamma$ for some formula $\psi$ and $a \in A$ because
$\Gamma$ is DM. Since $p_a \ltimes K_a p_a$ by Lemma 2.12(d) and, hence, also $\neg p_a \ltimes K_a p_a$, we conclude
that $K_a\psi \in^* \Gamma$ for some formula $\psi$ and $a \in A$ in either case, from which it follows that
$K_a\Gamma \neq \emptyset$ for this $a$. Hence, $X_\Gamma \neq \emptyset$ for all $\Gamma \in \mathbb{G}$. As a consequence, $C^c \neq \emptyset$ and every
DMC set $\Gamma$ is represented in the canonical model by $X_\Gamma \in C^c$. Set $C^c$ is closed under taking
non-empty subsets and all its faces are non-empty by construction. The faces are finite
because for $X \subseteq X_\Gamma$, we have $|X| \le |X_\Gamma| \le n+1$. Chromatic map $\chi^c$ is defined correctly
because all vertices $K_a\Gamma \in \mathcal{V}^c$ are non-empty by construction and all formulae in $K_a\Gamma$ start
with $K_a$. Thus, it cannot happen that $K_a\Gamma = K_b\Delta \neq \emptyset$ for $a \neq b$, and the definition
of $\chi^c$ is unambiguous. Finally, by construction, each $X_\Gamma$ (and, consequently, any $X \subseteq X_\Gamma$)
has at most one $K_a\Gamma$ per agent $a$. Thus, the chromatic map condition is fulfilled. The
correctness of $\ell^c$ relies on the same argument as that of $\chi^c$, but in addition, by construction,
$\ell^c(K_a\Gamma) \subseteq P_a$ and $\ell^c(K_a\Gamma) = \ell^c(K_a\Delta)$ in case $K_a\Gamma = K_a\Delta \neq \emptyset$ for $\Gamma \neq \Delta$. $\square$