# Stalnaker’s Epistemic Logic in Isabelle/HOL.††thanks: Supported by NSF
CAREER Award CNS-1552934 and NSF:CCRI Award CNS-2016592.

Laura P. Gamboa Guzman Iowa State University
Ames, IA 50011, USA 11email<EMAIL_ADDRESS>State University
Ames, IA 50011, USA 11email<EMAIL_ADDRESS>Kristin Y. Rozier Iowa State
University
Ames, IA 50011, USA 11email<EMAIL_ADDRESS>
###### Abstract

The foundations of formal models for epistemic and doxastic logics often rely
on certain logical aspects of modal logics such as S4 and S4.2 and their
semantics; however, the corresponding mathematical results are often stated in
papers or books without including a detailed proof, or a reference to it, that
allows the reader to convince themselves about them. We reinforce the
foundations of the epistemic logic S4.2 for countably many agents by
formalizing its soundness and completeness results for the class of all
weakly-directed pre-orders in the proof assistant Isabelle/HOL. This logic
corresponds to the knowledge fragment, i.e., the logic for formulas that may
only include knowledge modalities in Stalnaker’s system for knowledge and
belief. Additionally, we formalize the equivalence between two axiomatizations
for S4, which are used depending on the type of semantics given to the modal
operators, as one is commonly used for the relational semantics, and the other
one arises naturally from the topological semantics.

##  1 Introduction

Epistemic logics are a family of logics that allow us to reason about
knowledge among a group of agents, as well as their knowledge about other’s
knowledge[13]. Reasoning about knowledge is useful for detecting and
identifying faults during the operation of complex critical systems [8, 28],
where important safety properties are formalized using a modal language that
combines temporal, in particular, LTL (Linear Temporal Logic), and epistemic
modal operators, so to verify the correctness of the system using model
checking and related formal fault-detection techniques [10, 22, 25].

When it comes to modal logics for knowledge, most of these logics correspond
to normal logics between S4 and S5 [12, 26]. In particular, we consider
Stalnaker’s epistemic logic, which coincides with the logic S4.2. It is known
that this logic strictly stronger than S4, but weaker than S5 [9]. This logic
is known to be sound and complete with respect to all weakly directed
S4-frames, that is, all frames consisting of reflexive and transitive binary
relations that are confluent [24], but this proof is often omitted in
textbooks where most extensions to system K (the weakest normal modal logic)
are usually treated informally.

Additionally, we encode in Isabelle/HOL the axiomatization of S4 obtained from
the study of the topological interpretation for modal languages, which was
introduced prior to the relational one that is more commonly found in the
literature. This topological interpretation is done by reading the modal
necessity operator as an interior operator on a topological space, for which
is known that the modal logic S4 is complete with respect to all topological
spaces [2]. The preferred axiomatization for the logic of topological spaces
differs from the one presented in [16], not only from the set of axioms, but
also the deductive rules, since it captures the axioms for an interior
operator instead of a reflexive and transitive binary relation. As a
consequence, this makes the topological axiomatization not directly
recognizable as a normal modal logic, since the deduction rules seem to be
weaker at first glance. Since several authors have been recently developing
topological semantics for notions of knowledge and belief [3, 5, 4, 17], we
provide a formalization for this result, which often gets briefly mentioned
and applied without being proved in detail.

### Contributions

We formalize Stalnaker’s epistemic logic, which is expressively equivalent to
S4.2 [26], as well as some intermediate results for the underlying
propositional logic and the modal logics K, .2, and S4 mainly regarding
rewriting rules, properties for maximal consistent sets of formulas, and frame
properties that are induced by the chosen set of axioms in the proof assistant
Isabelle/HOL [18]. Our main result is a formalization of the soundness and
completeness of Stalnaker’s epistemic logic (restricted to countably many
agents) with respect to all weakly directed(also refered to as _confluent_ or
_convergent_ in the literature [23, 24]) S4 frames, this is, all frames
consisting of a non-empty set $W$ and a binary relation $R_{i}$ on $W$, one
for each agent label $i$, that is reflexive, transitive, and that satisfies
the property described by the following condition

$\forall x\,\forall y\,\forall z\,(xR_{i}y\wedge xR_{i}z\implies\exists
w\,yR_{i}w\wedge zR_{i}w).$

The proof uses a Henkin-style completeness method, which is commonly used for
these kinds of logics [6] and was already available on Isabelle’s Archive of
Formal Proofs [15].

As far as we know, all systems corresponding to some multi-agent epistemic
logic already formalized in Isabelle/HOL, which are all contained in [15] (the
ground base for our formalization), were complete with respect to a class of
frames characterized by a universal formula, i.e., a property of frames given
by a first order formula of the form
$\forall\overline{x}\,\phi(\overline{x})$, where $\phi(\overline{x})$ is a
quantifier-free formula with variable symbols in
$\overline{x}=(x_{1},\ldots,x_{n})$. However, the logic S4.2 is complete with
respect to a class of frames that cannot be characterized using a universal
formula; instead it is characterized by a universal-existential formula. This
universal-existential characterization makes it harder to formalize its
completeness result, since one has to show the existence of an object in the
universe of the canonical model satisfying a condition on a union of
consistent sets of formulas. For this, we followed an argument given by
Stalnaker in [27] that includes a set of theorems that are consequences of the
axiom (.2) in K, which imply the consistency of a set obtained by taking the
union of all known facts for an agent in two different worlds that were
accessible from a third one.

Nonetheless, our formalization also includes some intermediate results that
are well-known for all normal modal logics, and that are commonly used when
dealing with formal proofs in Hilbert-style systems. Finally, we formalized
the equivalence between two of the most used axiomatizations of S4, the one
presented in [16] which is commonly used when dealing with the relational
semantics [6], and the one introduced by McKinsey and Tarski for the
topological semantics [2].

### Related work

Our ground base is the Isabelle/HOL theory EpistemicLogic.thy [15], which
contains not only the formalization of other epistemic logics such as S4 and
S5, but also formalizes the definition of an abstract canonical model, as well
as a simple and convenient way to work with any desired normal modal logic by
adding necessary the axioms to the basic system K [16]. A related paper to
this formalization is [29], which contains a broad and updated summary on
formalizations of logical systems and correspondent important results using
different theorem provers. Other ways to formalize logical systems and their
completeness results on Isabelle have also been studied in [11] and [7], which
include (but are not limited to) the use of natural deduction rules, sequent-
style rules, and tableau rules for the formal systems, and coinductive methods
for soundness and completeness results.

However, given the already existent formalization of LTL in Isabelle/HOL [25],
as well as the prevalence of Isabelle as a tool for formal verification of
safety requirements for critical systems, it becomes important to provide this
formalization for this particular proof assistant. In addition to this, in
[20] the authors defined and investigated the notion of $KB_{R}$-structures,
which are used to represent a description of the epistemic status of a
rational agent that is not necessarily aware of their ignorance, and provided
a result that matches them with models of the epistemic logic S4.2. Modal
logics between S4.2 and S5 are of special interest for applications in
epistemic logic, since they allow formalizations of several degrees of
ignorance for each one of the agents [23].

The paper is organized as follows: Section 2 introduces the necessary
background on epistemic logic, including its relational and topological
semantics, and how the syntax and the relational semantics were formalized in
Isabelle/HOL in [15]. Section 3 explains our formalization of Stalnaker’s
epistemic logic, including the intermediate results necessary to prove the
main results, and the limitations of these to only countably many agents.
Section 4 explains our formalization of the equivalence between the two most
common axiomatizations for S4, the one that arises from the topological
semantics, and the one commonly used when working with the relational
semantics. Finally, in Section 5, we conclude with a discussion about the
results, limitations, and future work.

##  2 Background

###  2.1 Stalnaker’s Epistemic logic

We briefly present the axiomatic system developed by R. Stalnaker for both
notions of knowledge and belief, as well as the main result for the “knowledge
formulas” (i.e., for those formulas that do not contain any belief modal
operators), which correspond to the multimodal system S4.2 [26]. We omit the
proof for this result, as the Isabelle theory “Epistemic logic: Completeness
of Modal Logics” [15] does not support belief formulas.

Consider the well-formed formulas obtained from the following grammar, where
$x$ ranges over the set of propositional symbols and $i$ ranges over the set
of agent labels:

$\phi,\psi::=\bot\,|\,x\,|\,\phi\vee\psi\,|\,\phi\wedge\psi\,|\,\phi\to\psi\,|\,K_{i}\phi\,|\,B_{i}\phi.$

The operators $K_{i}$ and $B_{i}$ mean “agent $i$ knows” and “agent $i$
believes,” respectively. Although Stalnaker does not present his logic of
knowledge and belief using this exact set of propositional connectives, but a
proper subset of these, we added the remaining ones given that From’s
formalization includes all of them [16].

Stalnaker’s principles (axioms) for knowledge and belief appear in Table 1,
along with their interpretations in natural language. Stalnaker’s logic for
knowledge and belief corresponds to the formal system obtained by adding these
axioms to the axioms and rules of the multi-modal logic S4, that is, the
smallest logic containing the following axioms:

  * •

all propositional tautologies,

  * •

axiom K: $(K_{i}(\phi\to\psi)\wedge K_{i}\phi)\to K_{i}\psi$,

  * •

axiom T: $K_{i}\phi\to\phi$, and

  * •

axiom 4: $K_{i}\phi\to K_{i}K_{i}\phi$;

and that is closed under Modus Ponens and the Necessitation rule, “from $\phi$
infer $K_{i}\phi$”, where $i$ ranges over the set of agents.

Table 1: Axioms for knowledge and belief. $B_{i}\phi\to K_{i}B_{i}\phi$ | Positive introspection
---|---
$\neg B_{i}\phi\to K_{i}\neg B_{i}\phi$ | Negative introspection
$K_{i}\phi\to B_{i}\phi$ | Knowledge implies belief
$B_{i}\phi\to\neg B_{i}\neg\phi$ | Consistency of belief
$B_{i}\phi\to B_{i}K_{i}\phi$ | Strong belief

The following proposition summarizes some relevant properties of this logic.

######  Proposition 1.

The following are some key properties of Stalnaker’s logic for knowledge and
belief [26].

  1. 1.

The following equivalences, one for each agent label $i$ and formula $\phi$,
are theorems in this logic:

$B_{i}\phi\longleftrightarrow\neg K_{i}\neg K_{i}\phi.$

  2. 2.

As a consequence of the previous property, by replacing ‘$B_{i}$’ with ‘$\neg
K_{i}\neg K_{i}$’ in the _Consistency of belief_ axiom, we get that $\neg
K_{i}\neg K_{i}\phi\to K_{i}\neg K_{i}\neg\phi$ (also known as axiom .2) is a
theorem in this logic. This implies that the knowledge formulas of this logic
correspond exactly to the logic given by the system S4.2, i.e., those that can
be obtained from the rules and axioms of the multi-modal logic S4 in presence
of the axiom .2.

The above proposition allows us to interpret this logic by giving a semantics
only for the propositional variables, Boolean connectives and knowledge
operators. Formally, we use structures $\mathfrak{M}=(\mathcal{F},\pi)$ known
as Kripke models, where the frame $\mathcal{F}=(W,(R_{i})_{i})$ is a pair
consisting of a non-empty set of worlds $W$, a set of binary accessibility
relations $R_{i}\subseteq W\times W$, one for each agent $i$, and
$\pi:\operatorname{Var}\to 2^{W}$ is a valuation of propositional symbols.
Formula satisfiability at a given world $w\in W$ is defined as follows:

$\mathfrak{M},w\not\models\bot$ |  |
---|---|---
$\mathfrak{M},w\models x$ | iff | $w\in\pi(x)$
$\mathfrak{M},w\models\phi\vee\psi$ | iff | $\mathfrak{M},w\models\phi\text{ or }\mathfrak{M},w\models\psi$
$\mathfrak{M},w\models\phi\wedge\psi$ | iff | $\mathfrak{M},w\models\phi\text{ and }\mathfrak{M},w\models\psi$
$\mathfrak{M},w\models\phi\to\psi$ | iff | $\mathfrak{M},w\not\models\phi\text{ or }\mathfrak{M},w\models\psi$
$\mathfrak{M},w\models K_{i}\phi$ | iff | $\forall v\in W\,(wR_{i}v\to\mathfrak{M},v\models\phi)$
$\mathfrak{M},w\models B_{i}\phi$ | iff |  $\mathfrak{M},w\models\neg K_{i}\neg K_{i}\phi$.

One can use functions $\mathcal{K}:W\to 2^{W}$ instead of sets of ordered
pairs $R\subseteq W\times W$, as there is a correspondence between these
objects by setting

$wRv\,\Longleftrightarrow v\in\mathcal{K}(w),$

for all $w,v\in W$.

###  2.2 Epistemic Logic: Completeness of Modal Logics

The “Epistemic Logic: Completeness of Modal Logics” entry on Isabelle’s AFP
[15] contains not only a formalization for the completeness results for some
epistemic logics, but also a formalization of the general strategy for Henkin-
style proofs for completeness. This is what enabled us to formalize a proof
for the completeness result for S4.2. We show here the formalization of the
Kripke models from [15], which are structures consisting of a set of worlds of
type ${}^{\prime}w$, a truth assignment for each propositional variable on
each world given by the function denoted $\pi$, and a set of accessible worlds
from each possible world for each agent ${}^{\prime}i$.

* _datatype_  _$($__$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ i _$\mathord{,}$_  _$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ w _$)$_ kripke  _$=$_

Kripke  _$($__$\mathcal{W}$__$\mathord{:}$_  _‹_ _$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$_ w set _›_ _$)$_  _$($__$\pi$__$\mathord{:}$_
_‹_ _$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ w  _$\Rightarrow$_ id
_$\Rightarrow$_ bool _›_ _$)$_  _$($__$\mathcal{K}$__$\mathord{:}$_  _‹_
_$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ i  _$\Rightarrow$_  _$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$_ w  _$\Rightarrow$_  _$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$_ w set _›_ _$)$_

Consequently, given a Kripke model $\mathfrak{M}=(W,(\mathcal{K}_{i})_{i\in
I},\pi)$ with accessibility functions $\mathcal{K}_{i}$ for each agent $i$,
formula satisfiability is defined by setting

$\mathfrak{M},w\models K_{i}\phi\quad\text{iff}\quad\forall
v\in\mathcal{K}_{i}(w)\,(\mathfrak{M},v\models\phi).$

Additionally, the _dual_ operator for each knowledge operator $K_{i}$ is
denoted in this formalization as $L_{i}$ and is defined as a short hand for
“agent $i$ does not know if something is false.” In other words,
$L_{i}\phi:=\neg K_{i}(\neg\phi)$, for all formulas $\phi$. The Kripke
semantics for this operator corresponds to [6, 9]

$\mathfrak{M},w\models L_{i}\phi\quad\text{iff}\quad\exists
v\in\mathcal{K}_{i}(w)\,(\mathfrak{M},v\models\phi).$

We show here the corresponding formalization presented in [16] for the Kripke
semantics, which is defined inductively on formulas for each world.

* _primrec_ semantics  _$\mathord{:}$__$\mathord{:}$_  _‹_ _$($__$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ i _$\mathord{,}$_  _$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ w _$)$_ kripke  _$\Rightarrow$_  _$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ w  _$\Rightarrow$_  _$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ i fm  _$\Rightarrow$_ bool _›_

 _$($_ -_$\mathord{,}$_ -  _$\models$_ -  _$[$_ 50 _$\mathord{,}$_ 50 _$]$_ 50
_$)$_  _where_

 _‹_ _$($_ M _$\mathord{,}$_ w  _$\models$_  _$\bot$__$)$_  _$=$_ False _›_

_$\mid$_  _‹_ _$($_ M _$\mathord{,}$_ w  _$\models$_ Pro x _$)$_  _$=$_
_$\pi$_ M w x _›_

_$\mid$_  _‹_ _$($_ M _$\mathord{,}$_ w  _$\models$_  _$($_ p  _$\vee$_ q
_$)$__$)$_  _$=$_  _$($__$($_ M _$\mathord{,}$_ w  _$\models$_ p _$)$_
_$\vee$_  _$($_ M _$\mathord{,}$_ w  _$\models$_ q _$)$__$)$__›_

_$\mid$_  _‹_ _$($_ M _$\mathord{,}$_ w  _$\models$_  _$($_ p  _$\wedge$_ q
_$)$__$)$_  _$=$_  _$($__$($_ M _$\mathord{,}$_ w  _$\models$_ p _$)$_
_$\wedge$_  _$($_ M _$\mathord{,}$_ w  _$\models$_ q _$)$__$)$__›_

_$\mid$_  _‹_ _$($_ M _$\mathord{,}$_ w  _$\models$_  _$($_ p
_$\longrightarrow$_ q _$)$__$)$_  _$=$_  _$($__$($_ M _$\mathord{,}$_ w
_$\models$_ p _$)$_  _$\longrightarrow$_  _$($_ M _$\mathord{,}$_ w
_$\models$_ q _$)$__$)$__›_

_$\mid$_  _‹_ _$($_ M _$\mathord{,}$_ w  _$\models$_ K i p _$)$_  _$=$_
_$($__$\forall\,$_ v  _$\in$_  _$\mathcal{W}$_ M  _$\cap$_  _$\mathcal{K}$_ M
i w _$\mathord{.}$_ M _$\mathord{,}$_ v  _$\models$_ p _$)$__›_

From’s formalization then focuses on proving the soundness and completeness
results for each of the most commonly found normal modal logics in the
literature concerning certain classes of frames [6, 9, 16]. We now summarize
the relevant ones for our formalization.

  1. 1.

The basic logic, K, whose corresponding axiomatic system consists of all
propositional tautologies and the axiom K, and is closed under Modus Ponens
and the Necessitation Rule, is sound and complete with respect to the class of
all frames.

  2. 2.

The logic S4 is sound and complete with respect to the class of all transitive
and reflexive frames.

Notice that From’s formalization does not include modal operators for belief,
this restricts us to the knowledge fragment of the language. However,
Proposition 1 tells us that belief is equivalent to knowledge, thus we do not
lose any information by restricting to the knowledge fragment.

###  2.3 Topological semantics and its axioms

The topological semantics for modal logics was introduced before the
relational semantics that presently dominate the field [2], and the first
semantics completeness proof for S4 was derives from there. Recall the notion
of this topological semantics for a language with a single modal operator
$\square$. Let $\mathcal{L}$ be the language composed of all formulas given by
the following grammar:

$\phi,\psi::=\,x\,|\,\neg\phi\,|\,\phi\wedge\psi\,|\,\phi\vee\psi\,|\,\phi\to\psi\,|\,\square\phi,$

where $x$ ranges over the set of propositional symbols $\operatorname{Var}$.
Formulas in $\mathcal{L}$ are interpreted in a topological model $M=\langle
W,\tau,v\rangle$, consisting of a non-empty set $W$, a topology $\tau$ over
$W$, and a valuation $v:\operatorname{Var}\to 2^{W}$ in the following way:

  * •

$M,w\models x$ iff $x\in v(x)$;

  * •

$M,w\models\neg\phi$ iff $M,x\not\models\phi$;

  * •

$M,w\models\phi\wedge\psi$ iff $M,x\models\phi$ and $M,x\models\psi$;

  * •

$M,w\models\phi\vee\psi$ iff $M,x\models\phi$ or $M,x\models\psi$;

  * •

$M,w\models\phi\to\psi$ iff $M,x\not\models\phi$ or $M,x\models\psi$;

  * •

$M,w\models\square\phi$ iff there exists $U\in\tau$ such that $w\in U$ and
$M,y\models\phi$ for all $y\in U$.

Although there is nothing inherently wrong with using the deductive system
presented in [16] for the logic S4, the following axiomatization is often
preferable when working with the topological semantics, as the meaning of the
axioms and rules under this semantics resembles some well-known properties of
topological spaces [2].

Table 2: Topological S4 axioms and rules. Axiom | Formula | Rule | Formula
---|---|---|---
N | $\square\top$ | MP | $\displaystyle\frac{\phi\to\psi\quad\phi}{\psi}$
R | $\square(\phi\wedge\psi)\leftrightarrow(\square\phi\wedge\square\psi)$
T | $\square\phi\to\psi$ | M | $\displaystyle\frac{\phi\to\psi}{\square\phi\to\square\psi}$
4 | $\square\phi\to\square\square\phi$

Notice that at first it is not obvious weather or not the logic obtained from
this axiomatization is a normal modal logic, often defined as a logic that
_extends_ system K [6], as neither axiom K nor the Necessitation Rule are
present in the list of axioms and rules. However, we formalized a proof for
the equivalence between both axiomatizations in the context of a multi-agent
epistemic logic, as in recent years several authors have been developing
topological semantics for notions of knowledge and belief [3, 5, 4], where
this result is often briefly mentioned and applied, but not proved in detail.
Nonetheless, it is also worth noticing here that the relational semantics of
S4 is no more than a particular case for the topological semantics, as one can
assign a binary relation to each topological space by defining what is known
as the _specialization order_ [2].

##  3 Formalization

We now consider the epistemic logic based on the axioms in Table 1 and the
results in Proposition 1 for the knowledge fragment of the language. We prove
the soundness and completeness of the pure epistemic logic obtained from this
system with respect to all frames consisting of weakly directed pre-orders by
combining and applying the results formalized in [16] with some auxiliary
results provided in the Utility section of our Isabelle theory. This allows us
to utilize the canonical model strategy to prove completeness of the obtained
system. We do not formalize a logic for both knowledge and belief, since we
aimed to work on top of the formalization in [15], which considers modalities
only for knowledge. Formalizing the whole logic for both knowledge and belief
will then require developing a new theory almost from scratch that includes
modalities for both notions.

In order to do this, we prove first some intermediate results towards the
completeness of the system obtained by adding axiom .2 to the system K, also
known as system G in the literature [9], including some results about the
underlying propositional logic. This system is known to be complete with
respect to the class of weakly directed frames, and, although we do not
formalize this result completely, we do formalize a version of the Truth lemma
for this system, which is needed so that we can combine it with the results
for system S4 formalized in [16] to achieve our goal of formalizing the
completeness result for the logic S4.2 with respect to all weakly directed
pre-orders.

###  3.1 Rewriting propositional and modal formulas

In the deductive system formalized in [15], deduction from a set of premises
is defined as follows: given a set of formulas $\Gamma\cup\\{\phi\\}$, we say
that “$\phi$ is derived from $\Gamma$” (denoted $\Gamma\vdash\phi$) if there
are formulas $\psi_{1},\ldots,\psi_{k}$ in $\Gamma$ such that the formula
$\psi_{1}\to(\psi_{2}\to\ldots(\psi_{k}\to\phi))$ is a theorem in the system,
where $k$ is a non-negative integer. It is well-known that this formula is
logically equivalent to $(\psi_{1}\wedge\ldots\wedge\psi_{k})\to\phi$ in
classical propositional logic, thus the notion can be defined by requiring the
latter to be a theorem in the system instead. Being able to translate between
these two equivalent formulas in our formal deductive system plays an
important role for the proof of our main result, thus we provided a
formalization of several results of this kind in the Utility section of our
Isabelle theory, which includes some results that were not used later but that
might become handy for the development of the formalizations of other related
theories in the future.

Similarly to the imply function in [15], which produces, from a list of
formulas $[\psi_{1},\ldots,\psi_{k}]$ and a formula $\phi$, the formula
$\psi_{1}\to(\psi_{2}\to\ldots(\psi_{k}\to\phi))$, we introduce the function
conjunct, which takes a list of formulas $[\psi_{1},\ldots,\psi_{k}]$ and
produces the formula $\psi_{1}\wedge\ldots\wedge\psi_{k}\wedge\top$. (Notice
that the input may be an empty list, in which case the output is $\top$.) We
formalized some results about logical equivalences, and derived rules and
maximal consistent sets regarding the imply and conjunct functions that are
well-known for the logic K, some of which are presented in the following
lemmas. These are required to prove in section 3.2 that the axiom .2 induces
the weakly directed property on all frames that satisfy it, following [27]. We
include the proofs for those lemmas that require elaborated arguments.

######  Lemma 2 (Derived rules).

For all formulas $\psi_{1},\ldots,\psi_{k},\phi$, it is the case that
$\vdash(\psi_{1}\wedge\ldots\wedge\psi_{k})\to\phi$ if and only if
$\vdash\psi_{1}\to(\psi_{2}\to\ldots(\psi_{k}\to\phi))$.

######  Lemma 3 (Logical equivalences).

The following two lemmas capture the fact that in system K, hence in any
normal modal logic, the formulas $(K_{i}\psi_{1}\wedge\ldots\wedge
K_{i}\psi_{k})$ and $K_{i}(\psi_{1}\wedge\ldots\wedge\psi_{k})$ are
equivalent, for any finite set of formulas $\psi_{1},\ldots,\psi_{k}$ and any
agent $i$.

######  Lemma 4 (Closure under conjunctions for MCSs).

The following lemma proves that maximal consistent sets of formulas are closed
under conjunctions, that is, if $\Gamma$ is a maximal consistent set of
formulas and $\psi_{1},\ldots,\psi_{k}$ are some formulas in $\Gamma$, then
$\psi_{1}\wedge\ldots\wedge\psi_{k}\in\Gamma$.

Extendmaximal_extensionvalidEpistemic_Logic.thyAx_2Ax_2_weakly_directedmcs_2_weakly_directedimply_completeness_K_2soundness_Ax_2Ax.2
SectionK_conj_imply_factorUtility SectiontopoS4_S4main${}_{\texttt{S4'}}$
Topological S4 Axioms Section
$\vdash_{\texttt{S42}}$AxS4_2soundness_AxS4_2soundness${}_{\texttt{S42}}$imply_completeness_S4_4completeness${}_{\texttt{S42}}$valid${}_{\texttt{S42}}$main${}_{\texttt{S42}}$
System S4.2 Section Figure 1: Dependency graph showing the main results and
the definitions, abbreviations, and intermediate results from their proofs
that require the countable type condition. The dotted lines and the gray text
show the files or sections of the Isabelle theory corresponding to our
formalization where these can be found. Definitions and abbreviations appear
in rounded rectangles, whereas lemmas and theorems appear in rectangles. Those
that explicitly mention the countability condition are colored in blue, and
the color orange means that this result is applied using the set of natural
numbers to label the agents.

######  Lemma 5.

For all formulas $\phi,\psi,\theta$, it is the case that

$\vdash((K_{i}\phi\wedge
K_{i}\psi)\to\theta)\to(K_{i}(\phi\wedge\psi)\to\theta)$

for any agent label $i$, as long as the type of $i$ is countable.

* _lemma_ K-conj-imply-factor _$\mathord{:}$_

 _fixes_ A  _$\mathord{:}$__$\mathord{:}$_  _‹_ _$($__$($__$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$_ i  _$\mathord{:}$__$\mathord{:}$_ countable
_$)$_ fm  _$\Rightarrow$_ bool _$)$__›_

 _shows_  _‹_ A  _$\vdash$_  _$($__$($__$($__$($_ K i p _$)$_  _$\wedge$_
_$($_ K i q _$)$__$)$_  _$\longrightarrow$_ r _$)$_
_$\longrightarrow$__$($__$($_ K i  _$($_ p  _$\wedge$_ q _$)$__$)$_
_$\longrightarrow$_ r _$)$__$)$__›_

The assumption over the set of agent labels for the previous lemma is imposed
by the proof that was formalized for it, as it relies on the proof for the
completeness of K in [15], which requires this condition, as depicted in
Figure 1.

Additionally, we formalize the following lemma, which plays a significant role
in the proof of the completeness result for Stalnaker’s epistemic logic that
follows [27].

######  Lemma 6.

Given any pair of formulas $\phi,\psi$, $(K_{i}\phi\wedge L_{i}\psi)\to
L_{i}(\phi\wedge\psi)$ is a theorem in system K, for every agent label $i$.

###### Proof.

Notice that, for any formulas $\phi$ and $\psi$,
$\vdash\phi\to(\neg(\phi\wedge\psi)\to\neg\psi)$, hence

$\vdash K_{i}\phi\to K_{i}(\neg(\phi\wedge\psi)\to\neg\psi).$

On the other hand, we have that $\vdash
K_{i}(\neg(\phi\wedge\psi)\to\neg\psi)\to((K_{i}\neg(\phi\wedge\psi))\to
K_{i}\neg\psi)$, thus

$\vdash K_{i}\phi\to((K_{i}\neg(\phi\wedge\psi))\to K_{i}\neg\psi).$

This implies that $\vdash K_{i}\phi\to(L_{i}\psi\to L_{i}(\phi\wedge\psi))$,
which is equivalent to

$\vdash(K_{i}\phi\wedge L_{i}\psi)\to L_{i}(\phi\wedge\psi).$

∎

###  3.2 Axiom .2

We formalize axiom schema .2, which when added to the axioms and rules of
system K imposes a structure on the canonical model, namely, we obtain a
weakly directed frame. For this, the inductive command lets us define the
axiom schema in such a way that $i$ and $p$ can be instantiated at will, as
long as the type for the agents labels is countable.

* _inductive_ Ax-2  _$\mathord{:}$__$\mathord{:}$_  _‹_ _$($__$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ i  _$\mathord{:}$__$\mathord{:}$_ countable _$)$_ fm  _$\Rightarrow$_ bool _›_  _where_

 _‹_ Ax-2  _$($__$\neg$_ K i  _$($__$\neg$_ K i p _$)$_  _$\longrightarrow$_ K
i  _$($__$\neg$_ K i  _$($__$\neg$_ p _$)$__$)$__$)$__›_

A frame $\mathcal{F}=(W,(R)_{i\in I})$ is said to be weakly directed if
whenever $vR_{i}w$ and $vR_{i}u$, there exists $x\in W$ such that $wR_{i}x$
and $uR_{i}x$, for each $i\in I$. Accordingly, we formalize this property for
Kripke frames as follows:

* _definition_ weakly-directed  _$\mathord{:}$__$\mathord{:}$_  _‹_ _$($__$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ i _$\mathord{,}$_  _$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ s _$)$_ kripke  _$\Rightarrow$_ bool _›_  _where_

 _‹_ weakly-directed M  _$\equiv$_  _$\forall\,$_ i _$\mathord{.}$_
_$\forall\,$_ s  _$\in$_  _$\mathcal{W}$_ M _$\mathord{.}$_  _$\forall\,$_ t
_$\in$_  _$\mathcal{W}$_ M _$\mathord{.}$_  _$\forall\,$_ r  _$\in$_
_$\mathcal{W}$_ M _$\mathord{.}$_

 _$($_ r  _$\in$_  _$\mathcal{K}$_ M i s  _$\wedge$_ t  _$\in$_
_$\mathcal{K}$_ M i s _$)$__$\longrightarrow$__$($__$\exists\,$_ u  _$\in$_
_$\mathcal{W}$_ M _$\mathord{.}$_  _$($_ u  _$\in$_  _$\mathcal{K}$_ M i r
_$\wedge$_ u  _$\in$_  _$\mathcal{K}$_ M i t _$)$__$)$__›_

The soundness of axiom schema .2 with respect to weakly directed frames is
formalized in our Isabelle theory, and it follows from the definitions for the
semantics and the weakly directed property. However, proving that the property
holds for the canonical model when adding the axiom to a normal modal logic is
non-trivial. Unlike the frame properties imposed by the axioms considered in
the Epistemic Logics formalized in [16], which are all universal properties,
this property is universal-existential, so to prove that the canonical model
has this property means that one has to show the existence of a possible world
satisfying a property under some assumptions.

Recall that the _canonical frame_ ,
$\mathcal{F}^{\operatorname{can}}=\left(W^{\operatorname{can}},(R_{i}^{\operatorname{can}})_{i\in
I}\right)$, consists of the set all maximal consistent sets of formulas (with
respect to K+.2) as the set of possible worlds, $W^{\operatorname{can}}$, and
the accessibility relations $R_{i}^{\operatorname{can}}$ are defined as
follows:

$\Gamma R_{i}^{\operatorname{can}}\Delta\quad\text{ iff
}\quad\\{\phi:\,K_{i}\phi\in\Gamma\\}\subseteq\Delta,$

for each agent $i$. Thus, showing that the canonical frame for a system
including axiom .2 is weakly directed involves verifying that if we have
$\\{\phi:\,K_{i}\phi\in\Gamma\\}\subseteq\Delta_{1}$ and
$\\{\phi:\,K_{i}\phi\in\Gamma\\}\subseteq\Delta_{2}$ for some maximal
consistent sets $\Gamma$, $\Delta_{1}$ and $\Delta_{2}$, then there exists a
maximal consistent set $\Theta$ such that
$\\{\phi:\,K_{i}\phi\in\Delta_{1}\\}\cup\\{\phi:\,K_{i}\phi\in\Delta_{2}\\}\subseteq\Theta$.
We capture this in our formalization by the following lemma.

######  Lemma 7 (Weakly directed property and the axiom .2).

Suppose that $V,U,W$ are three maximal consistent sets with respect to a
normal modal logic containing the axiom .2. If $VR_{i}^{\operatorname{can}}U$
and $VR_{i}^{\operatorname{can}}W$, then there exists a maximal consistent set
$X$ such that $UR_{i}^{\operatorname{can}}X$ and
$WR_{i}^{\operatorname{can}}X$.

###### Proof.

First, fix a set of formulas $A$ and three maximal consistent sets of formulas
$V,U,W$ (with respect to $A$) satisfying the lemma assumptions for some agent
label $i$ of a countable type. Assume towards contradiction that such a set
$X$ does not exist, then

$S:=\\{\phi:\,K_{i}\phi\in W\\}\cup\\{\phi:\,K_{i}\phi\in U\\}$

has to be inconsistent with respect to $A$, hence there are formulas
$\theta_{1},\ldots,\theta_{k}\in\\{\phi:\,K_{i}\phi\in U\\}$ and
$\psi_{1},\ldots,\psi_{m}\in\\{\phi:\,K_{i}\phi\in W\\}$, for some
$k,m\in\mathbb{N}$, such that

$A\vdash(\alpha\wedge\beta)\to\bot,$

where $\alpha=\theta_{1}\wedge\ldots\wedge\theta_{k}$ and
$\beta=\psi_{1}\wedge\ldots\wedge\psi_{m}$. This implies that $A\vdash
K_{i}K_{i}(\neg(\alpha\wedge\beta))$, since $\phi\to\bot$ is equivalent to
$\neg\phi$ for every formula $\phi$, by applying the Necessitation rule twice.
By definition, we have that $K_{i}\theta_{1},\ldots,K_{i}\theta_{k}\in U$ and
$K_{i}\psi_{1},\ldots,K_{i}\psi_{m}\in W$, thus

$K_{i}\theta_{1}\wedge\ldots\wedge K_{i}\theta_{k}\in U\quad\text{ and }\quad
K_{i}\psi_{1}\wedge\ldots\wedge K_{i}\psi_{m}\in W,$

since these sets are closed under logical consequences. We then use the
logical equivalences and properties for maximal consistent sets from the
_Utility section_ (see section 3.1) to obtain that $K_{i}\alpha\in U$ and
$K_{i}\beta\in W$. This implies that the formulas $L_{i}K_{i}\alpha$ and
$L_{i}K_{i}\beta$ are elements of $V$, and so is the formula
$K_{i}L_{i}\alpha$, since $V$ contains every instance of axiom .2 and is
closed under logical consequences. This implies that
$(L_{i}K_{i}\beta)\wedge(K_{i}L_{i}\alpha)\in V$, thus $L_{i}(K_{i}\beta\wedge
L_{i}\alpha)\in V$, so there exists a maximal consistent set $Z$ such that

$VR_{i}^{\operatorname{can}}Z\qquad\text{and}\qquad K_{i}\beta\wedge
L_{i}\alpha\in Z.$

Applying the lemma K-thm we get that $L_{i}(\beta\wedge\alpha)\in Z$, but
notice that $K_{i}\neg(\alpha\wedge\beta)\in Z$, thus
$K_{i}\neg(\beta\wedge\alpha)\in Z$, which is a contradiction because we have
found a formula $\phi$ such that $\phi,\neg\phi\in Z$. ∎

Note that we have restricted ourselves to countable types for the set of agent
labels in formalization of the previous two lemmas, as we are only allowed to
extend a consistent set into a maximal one when the language is countable,
because of a dependency shown in Figure 1. Unlike in the respective result for
each normal modal logic formalized in [16], this restriction to a countable
type was necessary as we were dealing with a universal-existence property and
not with a purely universal one. We then prove a version of the Truth lemma
for the minimal normal modal logic that includes axiom .2, which is the
relevant result about this system that will allow us to prove the completeness
result for system S4.2 in the next section.

######  Lemma 8 (Imply completeness for Axiom .2).

Let $\Gamma\cup\\{\phi\\}$ be a set of formulas. Suppose that, for all weakly
directed Kripke structures $M$, $M,w\models\Gamma$ implies $M,w\models\phi$,
for each world $w\in M$. Then there are formulas
$\gamma_{1},\gamma_{2},\ldots,\gamma_{m}\in\Gamma$ such that

$\vdash_{.2}\gamma_{1}\to(\gamma_{2}\to\ldots(\gamma_{m}\to\phi)\ldots).$

We omit the proof for this lemma, since it follows the same strategy as the
correspondent ones for the systems formalized in [15].

###  3.3 System S4.2

We define system S4.2 as the one obtained by adding to system K the axioms T,
4 and .2, by making use of the abbreviation $\oplus$ introduced in [15] that
allows combining axiom predicates:

* _abbreviation_ SystemS4-2  _$\mathord{:}$__$\mathord{:}$_  _‹_ _$($__$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ i  _$\mathord{:}$__$\mathord{:}$_ countable _$)$_ fm  _$\Rightarrow$_ bool _›_  _$($__$\vdash$__S_ _4_ _2_ -  _$[$_ 50 _$]$_ 50 _$)$_  _where_

 _‹_ _$\vdash$__S_ _4_ _2_ p  _$\equiv$_ AxT  _$\oplus$_ Ax4  _$\oplus$_ Ax-2
_$\vdash$_ p _›_

Recall that axioms T and 4 impose reflexivity and transitivity on the
canonical frame, respectively [6], which was formalized in [15]. This implies
that the composition of these two with axiom .2 imposes all three conditions
on the canonical frame, which leads to the soundness and completeness of S4.2
with respect to all weakly directed pre-orders. To prove the completeness
result, we prove first the analog results to Lemmas 7 and 8 but for S4.2 and
Kripke models based on weakly directed preorders.

######  Lemma 9 (S4.2 and Weakly directed preorders).

Let $\Gamma\cup\\{\phi\\}$ be a set of formulas. Suppose that, for all
countable Kripke structures $M$ based on weakly directed preorders,
$M,w\models\Gamma$ implies $M,w\models\phi$, for each world $w\in M$. Then,
there are formulas $\gamma_{1},\ldots,\gamma_{m}\in\Gamma$ such that

$\vdash_{S42}\gamma_{1}\to(\ldots\to(\gamma_{m}\to\phi)\ldots).$

* _lemma_ imply-completeness-S4-2 _$\mathord{:}$_

 _assumes_ valid _$\mathord{:}$_  _‹_ _$\forall\,$__$($_ M
_$\mathord{:}$__$\mathord{:}$_  _$($__$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_
i  _$\mathord{:}$__$\mathord{:}$_ countable _$\mathord{,}$_  _$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$_ i fm set _$)$_ kripke _$)$__$\mathord{.}$_
_$\forall\,$_ w  _$\in$_  _$\mathcal{W}$_ M _$\mathord{.}$_

w-directed-preorder M  _$\longrightarrow$_  _$($__$\forall\,$_ q  _$\in$_ G
_$\mathord{.}$_ M _$\mathord{,}$_ w  _$\models$_ q _$)$_  _$\longrightarrow$_
M _$\mathord{,}$_ w  _$\models$_ p _›_

 _shows_  _‹_ _$\exists\,$_ qs _$\mathord{.}$_ set qs  _$\subseteq$_ G
_$\wedge$_  _$($_ AxS4-2  _$\vdash$_ imply qs p _$)$__›_

This implies that if a formula is valid in all countable Kripke structures
based on weakly directed preorders, then it is a theorem in S4.2.

* _lemma_ completeness _S_ _4_ _2_ _$\mathord{:}$_

 _assumes_  _‹_ _$\forall\,$__$($_ M  _$\mathord{:}$__$\mathord{:}$_
_$($__$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ i
_$\mathord{:}$__$\mathord{:}$_ countable _$\mathord{,}$_  _$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$_ i fm set _$)$_ kripke _$)$__$\mathord{.}$_
_$\forall\,$_ w  _$\in$_  _$\mathcal{W}$_ M _$\mathord{.}$_ w-directed-
preorder M  _$\longrightarrow$_ M _$\mathord{,}$_ w  _$\models$_ p _›_

 _shows_  _‹_ _$\vdash$__S_ _4_ _2_ p _›_

Our main result follows: the completeness of S4.2 with respect to all frames
consisting of weakly directed pre-orders.

######  Theorem 10 (Completeness of S4.2).

A formula is valid in all countable Kripke structures based on weakly directed
preorders if and only if it is a theorem in S4.2.

* _theorem_ main _S_ _4_ _2_ _$\mathord{:}$_  _‹_ valid _S_ _4_ _2_ p  _$\longleftrightarrow$_  _$\vdash$__S_ _4_ _2_ p _›_

##  4 An alternative axiomatization for System S4

Inspired by the last section of [15], we formalize an alternative
axiomatization for System S4 that is often used when dealing with the
topological semantics [2] for modal operators and we show its equivalence to
the one considered in [16]. We formalize the system corresponding to the
axioms and rules in Table 2 in Isabelle, which we call topoS4, and, if a
formula $\phi$ is a theorem in this system, we denote this by
$\vdash_{Top}\phi$.

* _inductive_ System-topoS4  _$\mathord{:}$__$\mathord{:}$_  _‹_ _$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ i fm  _$\Rightarrow$_ bool _›_  _$($__$\vdash$__T_ _o_ _p_ -  _$[$_ 50 _$]$_ 50 _$)$_  _where_

A1 _$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$__$\mathord{:}$_  _‹_ tautology p
_$\Longrightarrow$_  _$\vdash$__T_ _o_ _p_ p _›_

_$\mid$_ AR _$\mathord{:}$_  _‹_ _$\vdash$__T_ _o_ _p_  _$($__$($_ K i  _$($_
p  _$\wedge$_ q _$)$__$)$_  _$\longleftrightarrow$_  _$($__$($_ K i p _$)$_
_$\wedge$_ K i q _$)$__$)$__›_

_$\mid$_ AT _$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$__$\mathord{:}$_  _‹_
_$\vdash$__T_ _o_ _p_  _$($_ K i p  _$\longrightarrow$_ p _$)$__›_

_$\mid$_ A4 _$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$__$\mathord{:}$_  _‹_
_$\vdash$__T_ _o_ _p_  _$($_ K i p  _$\longrightarrow$_ K i  _$($_ K i p
_$)$__$)$__›_

_$\mid$_ AN _$\mathord{:}$_  _‹_ _$\vdash$__T_ _o_ _p_ K i  _$\top$__›_

_$\mid$_ R1 _$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$__$\mathord{:}$_  _‹_
_$\vdash$__T_ _o_ _p_ p  _$\Longrightarrow$_  _$\vdash$__T_ _o_ _p_  _$($_ p
_$\longrightarrow$_ q _$)$_  _$\Longrightarrow$_  _$\vdash$__T_ _o_ _p_ q _›_

_$\mid$_ RM _$\mathord{:}$_  _‹_ _$\vdash$__T_ _o_ _p_  _$($_ p
_$\longrightarrow$_ q _$)$_  _$\Longrightarrow$_  _$\vdash$__T_ _o_ _p_
_$($__$($_ K i p _$)$_  _$\longrightarrow$_ K i q _$)$__›_

To show that this formulation is equivalent to the one in [16] (which is based
on [6]), we provide derivations of axiom K and the Necessitation Rule (from
$\phi$ deduct $\square\phi$). This is enough as our system already includes
axioms T and 4 in the same fashion as in [16], and is based on the same
propositional logic.

######  Lemma 11.

For all formulas $\phi$ and $\psi$, $\vdash_{top}(K_{i}\phi\wedge
K_{i}(\phi\to\psi))\to K_{i}\psi$ and, if $\vdash_{top}\phi$, then
$\vdash_{top}K_{i}\phi$.

###### Proof.

For the first part, notice that
$\vdash_{top}(\phi\wedge(\phi\to\psi))\to\psi$, since it is an instance of a
propositional tautology. Then, we apply RM to obtain that
$\vdash_{top}K_{i}(\phi\wedge(\phi\to\psi))\to K_{i}\psi$, which implies that
$\vdash_{top}(K_{i}\phi\wedge K_{i}(\phi\to\psi))\to K_{i}\psi$. For the
second one, suppose that $\vdash_{top}\phi$ and notice that
$\vdash_{top}\phi\to(\top\to\phi)$, hence $\vdash_{top}\top\to\phi$. Applying
RM we get that $\vdash_{top}K_{i}\top\to K_{i}\phi$, thus
$\vdash_{top}K_{i}\phi$. ∎

From this it then follows that any formula derivable in the classical S4
system (denoted $\vdash_{S4}$) can be derived in our system as well.

######  Lemma 12.

All S4 theorems are theorems in topoS4.

* _lemma_ S4-topoS4 _$\mathord{:}$_  _‹_ _$\vdash$__S_ _4_ p  _$\Longrightarrow$_  _$\vdash$__T_ _o_ _p_ p _›_

The converse follows by a similar argument, we show that axioms and rules from
our system are all derivable in $\vdash_{S4}$, under the condition that there
are only countably many agents.

######  Lemma 13.

All theorems in topoS4 are theorems in S4, assuming that there are only
countably many agents.

* _lemma_ topoS4-S4 _$\mathord{:}$_

 _fixes_ p  _$\mathord{:}$__$\mathord{:}$_  _‹_ _$($__$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$_ i  _$\mathord{:}$__$\mathord{:}$_ countable
_$)$_ fm _›_

 _shows_  _‹_ _$\vdash$__T_ _o_ _p_ p  _$\Longrightarrow$_  _$\vdash$__S_ _4_
p _›_

By combining the last two results with the main result for S4 in [16], we
obtain formalized soundness and completeness for this alternative
axiomatization of S4 over the class of S4 frames, namely, all reflexive and
transitive frames.

######  Theorem 14 (Soundness and Completeness of topoS4).

A formula is valid in all S4 Kripke models if and only if it is a theorem in
topoS4.

* _theorem_ main _S_ _4_ _$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$__$\mathord{:}$_  _‹_ valid _S_ _4_ p  _$\longleftrightarrow$_  _$($__$\vdash$__T_ _o_ _p_ p _$)$__›_

##  5 Results, Discussion, and Future work

We have formalized the soundness and completeness for Stalnaker’s Epistemic
Logic S4.2 with respect to the class of Kripke frames consisting of weakly-
directed pre-orders for countably many agents, which has not been formalized
before neither in Isabelle, nor in any other publicly available proof
assistant. Additionally, the equivalence between the topological
axiomatization of S4 and the one in [15] is also described in this document.
The proofs for the main result, as well as for many of the intermediate
results, have been sketched before in multiple sources, but we were not able
to find a unique source, making this the first work of its kind. Additionally,
given the recent interest in applications of the topological semantics for
epistemic modal operators [3, 5, 4], some of which coincide with Stalnaker’s
epistemic logic, this provides a reinforcement for the foundations of these
works.

We emphasize on the assumption of the cardinality of the set of agent labels,
as it was necessary to impose such restriction even in some definitions in our
formalization, thus creating a discrepancy with the definitions commonly found
in the literature. We present in Figure 1 a summary of the definitions and
results of our formalization and the one in [15] that rely on this condition,
since the formalization for the general strategy applied to obtain the
completeness results in [15] requires it to be able to obtain maximal
consistent sets. Although, in theory, it is possible to provide an argument
for the general case using Zorn’s lemma (this was also later noted in [16]),
which is available in [14].

Further work in formalizing in Isabelle/HOL of different formal aspects of
modal logics that include S4 operators, as is the case with many temporal
logics like LTL with its _always_ operator, for which a complete
axiomatization is already known [19]; as well as concrete examples of
epistemic scenarios based on Stalnaker’s principles, like the example detailed
in [21]. We hope that this work will facilitate further work in formalizing
different logical systems in Isabelle/HOL.

## References

  * [1]
  * [2] Marco Aiello, Johan van Benthem & Guram Bezhanishvili (2003): _Reasoning About Space: The Modal Way_.  Journal of Logic and Computation 13(6), pp. 889–920, 10.1093/logcom/13.6.889.  arXiv:https://arxiv.org/abs/https://academic.oup.com/logcom/article-pdf/13/6/889/2936128/130889.pdf.
  * [3] Alexandru Baltag, Nick Bezhanishvili & Saúl Fernández González (2022): _Topological Evidence Logics: Multi-agent Setting_.  In Aybüke Özgün & Yulia Zinova, editors: Language, Logic, and Computation, Springer International Publishing, Cham, pp. 237–257, 10.1007/978-3-030-98479-3_12.
  * [4] Alexandru Baltag, Nick Bezhanishvili, Aybüke Özgün & Sonja Smets (2013): _The Topology of Belief, Belief Revision and Defeasible Knowledge_.  In Davide Grossi, Olivier Roy & Huaxin Huang, editors: Logic, Rationality, and Interaction, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 27–40, 10.1007/978-3-642-40948-6_3.
  * [5] Alexandru Baltag, Nick Bezhanishvili, Aybüke Özgün & Sonja Smets (2016): _Justified Belief and the Topology of Evidence_.  In Jouko Väänänen, Åsa Hirvonen & Ruy de Queiroz, editors: Logic, Language, Information, and Computation, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 83–103, 10.1007/978-3-662-52921-8_6.
  * [6] Robert Blackburn, Maarten de Rijke & Yde Venema (2001): _Modal Logic_.  Modal Logic, 10.1017/CBO9781107050884.
  * [7] Jasmin Christian Blanchette, Andrei Popescu & Dmitriy Traytel (2017): _Soundness and Completeness Proofs by Coinductive Methods_.  Journal of Automated Reasoning 58(1), pp. 149 – 179, 10.1007/s10817-016-9391-3.  Available at https://hal.inria.fr/hal-01643157.
  * [8] Marco Bozzano, Alessandro Cimatti, Marco Gario & Stefano Tonetta (2014): _Formal design of fault detection and identification components using temporal epistemic logic_.  In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer, pp. 326–340, 10.1007/978-3-642-54862-8_22.
  * [9] Alexander Chagrov (1997): _Modal Logic_.  Oxford logic guides, Clarendon Press, 10.1093/oso/9780198537793.001.0001.  Available at https://books.google.com/books?id=dhgi5NF4RtcC.
  * [10] Alessandro Cimatti, Marco Gario & Stefano Tonetta (2016): _A Lazy Approach to Temporal Epistemic Logic Model Checking_.  In: Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems, AAMAS ’16, International Foundation for Autonomous Agents and Multiagent Systems, Richland, SC, p. 1218–1226.
  * [11] F Miguel Dionísio, Paula Gouveia & Joao Marcos (2005): _Defining and using deductive systems with Isabelle_.  Computing, Philosophy, and Cognition, pp. 271–293.  Available at http://temporallogic.org/courses/AppliedFormalMethods/DefiningAndUsingDeductiveSystemsWithIsabelle.pdf.
  * [12] Hans van Ditmarsch, Wieve van der Hoek & Barteld Kooi (2008): _Dynamic Epistemic Logic_.  Springer Netherlands, 10.1007/978-1-4020-5839-4.
  * [13] Ronald Fagin, Joseph Y. Halpern, Yoram Moses & Moshe Vardi (1995): _Reasoning About Knowledge_.  MIT Press, London, England.
  * [14] Jacques D. Fleuriot, Tobias Nipkow & Christian Sternagel: _Zorn’s Lemma (ported from Larry Paulson’s Zorn.thy in ZF)._ Available at https://isabelle.in.tum.de/dist/library/HOL/HOL/Zorn.html.
  * [15] Asta Halkjær From (2018): _Epistemic Logic: Completeness of Modal Logics_.  Archive of Formal Proofs.  https://isa-afp.org/entries/Epistemic_Logic.html, Formal proof development.
  * [16] Asta Halkjær From (2021): _Formalized soundness and completeness of epistemic logic_.  In: International Workshop on Logic, Language, Information, and Computation, Springer, pp. 1–15, 10.1007/978-3-030-88853-4_1.
  * [17] Laura P. Gamboa Guzman (2021): _Dynamical operators on models with evidence_.  Master’s thesis, Universidad de los Andes, Bogota, Colombia.  Available at https://repositorio.uniandes.edu.co/handle/1992/55112.
  * [18] Laura P. Gamboa Guzman (2022): _Stalnaker’s Epistemic Logic_.  Archive of Formal Proofs.  https://isa-afp.org/entries/Stalnaker_Logic.html, Formal proof development.
  * [19] Robert Goldblatt (1992): _Logics of Time and Computation_.  CSLI Publications.
  * [20] Costas D. Koutras & Yorgos Zikos (2011): _Relating Truth, Knowledge and Belief in Epistemic States_.  In Weiru Liu, editor: Symbolic and Quantitative Approaches to Reasoning with Uncertainty, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 374–385, 10.1007/978-3-642-22152-1_32.
  * [21] Costas D. Koutras & Yorgos Zikos (2015): _Relating Truth, Knowledge and Belief in epistemic states_.  Online: http://users.uop.gr/~ckoutras/KZ-KBstructures-Dec2015.pdf.
  * [22] Stephan Merz (2005): _TLA: Lamport’s Temporal Logic of Actions_.  Online: https://isabelle.in.tum.de/library/HOL/HOL-TLA/README.html.  Directory in the Isabelle/HOL Library.
  * [23] Leonardo Pacheco & Kazuyuki Tanaka (2022): _On the Degrees of Ignorance: via Epistemic Logic and µ-Calculus_.  In: Proceedings of SOCREAL2022 6th International Workshop on Philosophy and Logic of Social Reality, pp. 74–78.  Available at http://hdl.handle.net/2115/84806.
  * [24] Rasmus Rendsvig & John Symons (2021): _Epistemic Logic_.  In Edward N. Zalta, editor: The Stanford Encyclopedia of Philosophy, Summer 2021 edition, Metaphysics Research Lab, Stanford University.
  * [25] Salomon Sickert (2016): _Linear Temporal Logic_.  Archive of Formal Proofs.  https://isa-afp.org/entries/LTL.html, Formal proof development.
  * [26] Robert Stalnaker (2006): _On logics of knowledge and belief_.  Philosophical Studies 128, pp. 169–199, 10.1007/S11098-005-4062-Y.
  * [27] Robert Stalnaker (2009): _Lecture Notes — Modal Logic — Linguistics and Philosophy — MIT OpenCourseWare_.  Available at https://dspace.mit.edu/bitstream/handle/1721.1/100157/24-244-fall-2009/contents/lecture-notes/index.htm.
  * [28] Stefano Tonetta, Marco Gario, Alessandro Cimatti & Marco Bozzano (2015): _Formal design of asynchronous fault detection and identification components using temporal epistemic logic_.  Logical Methods in Computer Science 11, 10.2168/LMCS-11(4:4)2015.
  * [29] Jørgen Villadsen, Asta Halkjær From, Alexander Birch Jensen & Anders Schlichtkrull (2022): _Interactive Theorem Proving for Logic and Information_ , pp. 25–48.  Springer International Publishing, Cham, 10.1007/978-3-030-90138-7_2.