# Base-extension Semantics for S5 Modal Logic

Timo Eckhardt  UCL Computer Science
London WC1E 6BT, UK<EMAIL_ADDRESS>David Pym  UCL Computer Science and
Philosophy & Institute of Philosophy
London WC1E 6BT, UK<EMAIL_ADDRESS>
###### Abstract

We develop a proof-theoretic semantics — in particular, a base-extension
semantics — for multi-agent $S5$ modal logic (and hence also for the usual
unindexed $S5$). Following the inferentialist interpretation of logic, this
gives us a semantics in which validity is based on proof rather than truth. In
base-extension semantics, the validity of formulae is generated by provability
in a ‘base’ of atomic rules and an inductive definition of the validity of the
connectives. Base-extension semantics for many interesting logics has been
explored by several authors and, in particular, a base-extension semantics for
the modal logics $K$, $KT$, $K4$, and $S4$ has been developed by the present
authors. Here, we give a base-extension semantics for multi-agent $S5$ with
$\square_{a}$, for an agent $a$, as our primary operators, framed as the
knowledge operator $K_{a}$. Similarly to Kripke semantics, we make use of
relational structure between bases, allowing us to establish a correspondence
between certain bases and worlds. We use this to establish the appropriate
soundness and completeness results. We conclude by discussing how this
semantics can be extended to Dynamic Epistemic Logics (DEL) starting with
Public Announcement Logic (PAL).

###### keywords:

Proof-theoretic semantics, base-extension semantics, modal logic, (multi-
agent) S5 modal logic, epistemic logic

##  1 Introduction

In proof-theoretic semantics (Pt-S), meaning is based on inference. It is a
logical realization of the philosophical position known as inferentialism [2].
It provides a universal approach to the meaning of the operators of logical
systems: their meaning is given in terms of their use. By contrast, in model-
theoretic semantics (Mt-S) meaning is determined relative to a choice of
abstract (model) structure (see, for example, [20]).

Current research in Pt-S largely follows two different approaches. The first
is proof-theoretic validity, following Dummett [3] and Prawitz [14, 15]. It
aims to define what makes a proof valid. Dummett’s _The Logical Basis of
Metaphysics_ [3] develops a philosophical interpretation of the normality
results for the natural deduction rules of intuitionistic propositional logic
(IPL). A valid proof is then one that can, by certain fixed operations, be
transformed into a proof without unnecessary detours called a canonical proof.
This approach is closely related to the Brouwer-Heyting-Kolmogorov
interpretation of IPL. For a more in-depth explanation see [19, 20, 21].

The second approach to proof-theoretic semantics is base-extension semantics
(B-eS), as developed in, for example, [11, 13, 16, 17, 18, 12].In B-eS, sets
of atomic rules, called bases, establish the validity of atoms and the meaning
of the logical connectives is then inductively defined relative to these
bases. The choice of the form of atomic rules has profound repercussions: In
the usual set-up of B-eS as stated above, limiting the atomic rules to simple
production rules yields semantics for classical logic (see [16, 17]), while
allowing for the discharging of atoms as assumptions, and taking care of the
treatment of disjunction, results in intuitionistic semantics [18]. However,
see [7, 22] for alternative approaches that are related to Kripke semantics.
Deep connections between B-eS and the least fixed point semantics for logic
programming in IPL, based on the proof-theoretic operational semantics of
proof-search over hereditary Harrop formulae, have been described in [6, 21].
In this setting, definite formulae and negation-as-failure (for intuitionistic
propositional logic) are key ideas [6, 21].

The standard M-tS for modal logic is Kripke semantics [8, 9]. In this
semantics, the validity of formulae is defined by reference to sets of
possible worlds and a relation over those worlds. A necessitated formula (a
formula of the form $\square\phi$) is true at a world if it holds at all the
worlds reachable via the relation. In multi-agent modal logics, relations are
indexed by agents and provide models that are able to interpret modalities
index by agents. Different modal logics arise according to different
restrictions on relations.

The goal of this paper is to give a Pt-S for Multi-agent $S5$ modal logics
with $\square_{a}$, for an agent $a$, as our primary operators, framed as the
knowledge operator $K_{a}$, by adapting the Be-S for the modal logics
$K,KT,K4,$ and $S4$ given in [5]. Similarly to Kripke semantics, relations
between bases are used and validity is defined by validity at a base given a
relation. The specific set-up of the semantics proved to be incomplete with
respect to Euclidean models. We address this issue by changing which relations
between bases we consider. In future work, this will provide the basis for a
base-extension semantics for (static) epistemic logic, as used to develop
Dynamic Epistemic Logics (DEL) such as Public Announcement Logic (PAL).

In Section 2, we revisit the relational structures required to give Kripke
semantics for modal logics. In Section 3, we summarize our recent work,
building on Sandqvist’s [16, 17] and Makinson’s [11] work on treatments of
classical propositional logic, on the B-eS for modal logics $K$, $KT$, $K4$,
and $S4$. The ideas of these sections will be required for Section 4, in which
we give a B-eS for (multi-agent) $S5$. Here, the main challenge is to handle
the Euclidean axiom. In Section 5 we show this semantics to be sound and
complete. In Section 6, we conclude with a discussion of how to extend our
results to Dynamic Epistemic Logics (DEL), beginning with Public Announcement
Logic (PAL). We provide some technical proofs in an appendix.

##  2 Kripke semantics

We define a multi-agent Kripke semantics for $S5$ modal logic and give the
axioms that constitute sound and complete proof systems. We take $\square$ to
be the principle modal operator and use $K_{a}$ for some agent $a$, in
deference to convention. A single-agent modal logic with $\square$ can be
obtained by restricting the set of agents $A$ to a single agent. We also give
a sound and complete axiomatic proof system (taken from [1]).

A formula $K_{a}\phi$ holds at a world $w$ iff it also holds at all worlds $v$
such that $R_{a}wv$, where $R_{a}$ is a (reflexive, transitive and Euclidean)
relation between worlds. The natural reading for such a formula in an
epistemic logic is as ‘the agent $a$ knows property $\phi$’ and,
correspondingly, the relation $R_{a}$ is interpreted as indistinguishability
for $a$, that is $R_{a}wv$ iff at worlds $w$ agent $a$ cannot distinguish
between $w$ and $v$. So, a formula $K_{a}\phi$ holds at a world $w$ iff at all
the worlds that the agent $a$ finds indistinguishable to the world $w$ $\phi$
holds; that is that every world $a$ thinks is possible is a $\phi$ world.

The Kripke semantics and proof system established in this section will be used
in Section 5 to establish the soundness and completeness of the base-extension
semantics of Section 4.

######  Definition 2.1.

For atomic propositions $p$ and an agent $a$, the language for modal logic
$S5$ is generated by the following grammar:

$\phi::=p\mid\bot\mid\neg\phi\mid\phi\to\phi\mid K_{a}\phi$

######  Definition 2.2.

A frame is a pair $F=\langle W,R^{A}\rangle$, in which $W$ is a set of
possible worlds, $R^{A}$ a set of binary relation on $W$, one for each agent
$a\in A$. A model $M=\langle F,V\rangle$ is a pair of a frame $F$ and a
valuation function $V$ giving the set of worlds in which $p$ is true s.t.
$V(p)\subseteq W$ for every $p$.

######  Definition 2.3.

$S5$-frames are those frames whose relations satisfy the frame conditions in
Table 1 and $S5$-models are those models constructed from $S5$-frames. Frames
and models for other modal logics are obtained by only using the corresponding
frame conditions (e.g., $KT$-frames are the reflexive and transitive frames).

######  Definition 2.4.

Let $F=\langle W,R^{A}\rangle$ be a $S5$-frame, $M=\langle F,V\rangle$ a
$S5$-model and $w\in W$ a world. That a formula $\phi$ is true at
$(M,w)$—denoted $M,w\vDash\phi$—as follows:

$\begin{array}[]{l@{\quad}c@{\quad}l}M,w\vDash p&\mbox{iff}&w\in V(p)\\\
M,w\vDash\phi\to\psi&\mbox{iff}&\mbox{if $M,w\vDash\phi$, then
$M,w\vDash\psi$}\\\ M,w\vDash\neg\phi&\mbox{iff}&\mbox{$M,w\not\vDash\phi$}\\\
M,w\vDash\bot&\mbox{never}&\\\ M,w\vDash K_{a}\phi&\mbox{iff}&\mbox{for all
$v$ s.t. $R_{a}wv$, $M,v\vDash^{\gamma}\phi$}\\\ \end{array}$

If a formula $\phi$ is true at all worlds in a model $M$, we say $\phi$ is
true in $M$. A formula is valid in a model logic $\gamma$ iff it is true in
all $\gamma$-models.

$\begin{array}[]{|l@{\quad}|l@{\quad}|l|}\hline\cr\mbox{Name}&\mbox{Frame
condition}&\mbox{Modal axiom}\\\ \hline\cr
K&\mbox{None}&K_{a}(K_{a}\phi\to\psi)\to(K_{a}\phi\to K_{a}\psi)\\\
T&\mbox{Reflexivity}&K_{a}\phi\to\phi\\\ 4&\mbox{Transitivity}&K_{a}\phi\to
K_{a}K_{a}\phi\\\ 5&\mbox{Euclidean}&\neg K_{a}\phi\to K_{a}\neg K_{a}\phi\\\
\hline\cr\end{array}$
Table 1:  Frame conditions and the corresponding modal axioms

######  Definition 2.5.

The proof system for the modal logic $S5$, with $a\in A$ is given by the
following axioms and rules:

  * •

_(1)_ : $\phi\to(\psi\to\phi)$

  * •

_(2)_ : $(\phi\to(\psi\to\chi))\to((\phi\to\psi)\to(\phi\to\chi))$

  * •

_(3)_ : $(\neg\phi\to\neg\psi)\to(\psi\to\phi)$

  * •

_(K)_ : $K_{a}(\phi\to\psi)\to(K_{a}\phi\to K_{a}\psi)$

  * •

_(T)_ : $K_{a}\phi\to\phi$

  * •

_(4)_ : $K_{a}\phi\to K_{a}K_{a}\phi$

  * •

_(5)_ : $\neg K_{a}\phi\to K_{a}\neg K_{a}\phi$

  * •

_(MP)_ : If $\phi$ and $\phi\to\psi$, then $\psi$

  * •

_(NEC)_ : If $\phi$ is a theorem, so is $K_{a}\phi$.

The axioms _(1)-(3)_ together with the rule _(MP)_ constitute a proof system
for classical logic. Proof systems for the other modal logics are obtained by
taking only the corresponding axioms from Table 1 (e.g., modal logic $KT$
results from adding _(K)_ , _(T)_ , and _(NEC)_ to the classical proof
system).

Given the Kripke semantics and the corresponding axiomatic proof system we can
state the following, well-known, result.

######  Theorem 2.6.

The proof system for a multi-agent modal logic $S5$ is sound and complete with
respect to the validity given by $S5$-models.

##  3 Preliminary base-extension semantics

We define the base-extension semantics for classical logic that will form the
foundation for our modal semantics. Our presentation of classical base-
extension semantics follows the versions given in [16, 17] and [11]. We also
briefly introduce the modal base-extension semantics for the single-agent
modal logics $K$, $KT$, $K4$, and $S4$ we developed in [5].

We define base rules and bases to give the underlying atomic system. We then
inductively define the other classical connectives based on top of that. We
also define the notion of maximally-consistent bases. For the single-agent
modal base-extension semantics for non-Euclidean systems, we add a relation
between bases and define the appropriate relations necessary, called modal
relations. We then define validity based on holding at a base given a modal
relation. The notion of modal relation is especially important as, in [5], we
have shown that it results in incomplete semantics for Euclidean modal logics
and so will have to be changed for the $S5$ modal logic in Section 4.

###  3.1 Classical base-extension semantics

We start our presentation of classical base-extension semantics by defining
the language.

######  Definition 3.1.

For atomic propositions $p$, the language for classical logic is generated by
the following grammar:

$\phi::=p\mid\bot\mid\phi\to\phi$

The negation symbol $\neg\phi$ is defined as $\phi\to\bot$. All other
connectives can be obtained from $\to$ and $\bot$ in the usual manner.

As base rules and bases build the foundation of validity, we have to define
them before moving to validity conditions.

######  Definition 3.2.

A base rule is a pair $(L_{j},p)$ where $L_{j}=\\{p_{1},\dots,p_{n}\\}$ is a
finite (possibly empty) set of sentence letters and $p$ is also a sentence
letter. Generally, a base rule will be written as
$p_{1},\dots,p_{n}\Rightarrow p$. A base $\mathscr{B}$ is any countable
collection of base rules. We call the set of all bases $\Omega$ and
$\overline{\mathscr{B}}$ is the closure of the empty set under the rules in
$\mathscr{B}$.

Given those definitions we can now give validity. We give a condition for when
a connective is valid given a base. Validity (generally) is then defined by
being valid at all bases.

######  Definition 3.3.

Classical validity is defined as follows:

$\begin{array}[]{l@{\quad}c@{\quad}l}\Vdash_{\mathscr{B}}p&\mbox{iff}&\mbox{$p$
is in every set of basic sentences closed under $\mathscr{B}$}\\\
&&\mbox{(i.e., iff $p\in\overline{\mathscr{B}}$)}\\\
\Vdash_{\mathscr{B}}\phi\to\psi&\mbox{iff}&\mbox{$\phi\Vdash_{\mathscr{B}}\psi$}\\\
\Vdash_{\mathscr{B}}\bot&\mbox{iff}&\mbox{$\Vdash_{\mathscr{B}}p$ for every
basic sentence $p$.}\\\ &&\\\ \mbox{For non empty $\Gamma$:}&&\\\
\Gamma\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\phi&\mbox{iff}&\mbox{for all
$\mathscr{C}\supseteq\mathscr{B}$, if
$\Vdash_{\mathscr{C},\mathfrak{R}^{A}}\psi$ for all $\psi\in\Gamma$, then
$\Vdash_{\mathscr{C},\mathfrak{R}^{A}}\phi$}\\\ \end{array}$

A formula $\phi$ is valid iff $\Vdash_{\mathscr{B}}\phi$ for every base
$\mathscr{B}$. A base $\mathscr{B}$ is inconsistent iff
$\Vdash_{\mathscr{B}}\bot$ and consistent otherwise.

For classical base-extension semantics [11] has shown that maximally-
consistent bases correspond to valuations in classical semantics. In [5], we
have shown that the same holds true between maximally-consistent bases in
modal base-extension semantics and worlds in Kripke semantics. For that reason
we define maximally-consistent bases here.

######  Definition 3.4.

A base $\mathscr{B}$ is maximally-consistent iff it is consistent and for
every base rule $\delta$, either $\delta\in\mathscr{B}$ or
$\mathscr{B}\cup\\{\delta\\}$ is inconsistent.

Further we show that if a formula does not hold at some base, there also has
to be a maximally-consistent base at which it is not valid. This will proof
useful in our proof of soundness later.

######  Lemma 3.5.

For every propositional formula $\phi$, if there is a base $\mathscr{B}$ s.t.
$\nVdash_{\mathscr{B}}\phi$, then there is a maximally-consistent base
$\mathscr{B}^{*}\supseteq\mathscr{B}$ with $\nVdash_{\mathscr{B}^{*}}\phi$.

A proof of Lemma 3.5 can be found in [11].

###  3.2 Single-agent non-Euclidean modal logic

For our modal language we extend the language for classical base-extension
semantics with a $\square$ operator.

######  Definition 3.6.

For atomic propositions $p$, the language for a modal logic $\gamma$ is
generated by the following grammar:

$\begin{array}[]{rcl}\phi&:=&p\mid\bot\mid\phi\rightarrow\phi\mid\square\phi\end{array}$

Importantly, we do not change the make-up of our base rules and bases and so
the definitions of those terms from Definition 3.2 remain unchanged.

The fundamental difference between the classical and the modal account lies in
the definition of validity. We no longer define validity at a base but rather
validity at a base given a relation over the set of bases. So before moving to
validity we have to define exactly the type of relations between bases we
require.

######  Definition 3.7.

A relation $\mathfrak{R}$ on the set of bases $\Omega$ is called a modal
relation iff, for all $\mathscr{B}$,

  1. (a)

if $\Vdash_{\mathscr{B}}\bot$, then there is a $\mathscr{C}$ s.t.
$\mathfrak{R}\mathscr{B}\mathscr{C}$ and $\Vdash_{\mathscr{C}}\bot$ and, for
all $\mathscr{D}$, if $\mathfrak{R}\mathscr{B}\mathscr{D}$, then
$\Vdash_{\mathscr{D}}\bot$

  2. (b)

if $\nVdash_{\mathscr{B}}\bot$, then, for all $\mathscr{C}$, s.t.
$\mathfrak{R}\mathscr{B}\mathscr{C}$, $\nVdash_{\mathscr{C}}\bot$

  3. (c)

for all $\mathscr{C}$, if $\mathscr{B}$ is consistent and
$\mathfrak{R}\mathscr{B}\mathscr{C}$, then either $\mathscr{B}$ is maximally-
consistent or there is a $\mathscr{D}\supset\mathscr{B}$ s.t.
$\mathfrak{R}\mathscr{D}\mathscr{C}$

  4. (d)

for all $\mathscr{C}$, if $\mathfrak{R}\mathscr{B}\mathscr{C}$, then, for all
$\mathscr{D}\subseteq\mathscr{B}$, $\mathfrak{R}\mathscr{D}\mathscr{C}$.

Given a modal logic $\gamma=K,K4,KT$, or $S4$, a modal relation $\mathfrak{R}$
is called a $\gamma$-modal relation iff $\mathfrak{R}$ satisfies the frame
conditions corresponding to $\gamma$.

Conditions (a) and (b) make sure that inconsistent and consistent worlds are
not connected via $\mathfrak{R}$ and conditions (c) and (d) guarantee that the
structure of $\mathfrak{R}$ is preserved when going from a base to its super-
and subsets, respectively. For a more in-depth discussion of this definition
see [5].

We can now give a general definition of validity for the modal logics
$K,KT,K4$ and $S4$, as they share the same validity conditions and only differ
in the modal relations they consider.

######  Definition 3.8.

We define validity at a base $\mathscr{B}$ given a $\gamma$-modal relation
$\mathfrak{R}$ for a modal logic $\gamma$ as follows:

$\begin{array}[]{l@{\quad}c@{\quad}l}\Vdash^{\gamma}_{\mathscr{B},\mathfrak{R}}p&\mbox{iff}&\mbox{$p$
is in every set of basic sentences closed under $\mathscr{B}$}\\\
&&\mbox{(i.e., iff $p\in\overline{\mathscr{B}}$)}\\\
\Vdash^{\gamma}_{\mathscr{B},\mathfrak{R}}\phi\to\psi&\mbox{iff}&\mbox{$\phi\Vdash^{\gamma}_{\mathscr{B},\mathfrak{R}}\psi$}\\\
\Vdash^{\gamma}_{\mathscr{B},\mathfrak{R}}\bot&\mbox{iff}&\mbox{$\Vdash^{\gamma}_{\mathscr{B},\mathfrak{R}}p$
for every basic sentence $p$}\\\
\Vdash^{\gamma}_{\mathscr{B},\mathfrak{R}}\square\phi&\mbox{iff}&\mbox{for all
$\mathscr{C}\supseteq\mathscr{B}$ and $\mathscr{C^{\prime}}$ s.t.
$\mathfrak{R}\mathscr{C}\mathscr{C^{\prime}}$,
$\Vdash^{\gamma}_{\mathscr{C^{\prime}},\mathfrak{R}}\phi$}\\\ &&\\\ \mbox{For
non empty $\Gamma$:}&&\\\
\Gamma\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\phi&\mbox{iff}&\mbox{for all
$\mathscr{C}\supseteq\mathscr{B}$, if
$\Vdash_{\mathscr{C},\mathfrak{R}^{A}}\psi$ for all $\psi\in\Gamma$, then
$\Vdash_{\mathscr{C},\mathfrak{R}^{A}}\phi$}\\\ \end{array}$

A formula $\phi$ is $\gamma$-valid, written as $\Vdash^{\gamma}\phi$, iff
$\Vdash^{\gamma}_{\mathscr{B},\mathfrak{R}}\phi$ for all modal bases
$\mathscr{B}$ and $\gamma$-modal relations $\mathfrak{R}$. The definition of
inconsistent base remains unchanged from the classical base-extension
semantics in Definition 3.3. A base $\mathscr{B}$ is inconsistent iff
$\Vdash_{\mathscr{B}}\bot$.

##  4 Bases-extension semantics for $S5$

Our presentation of modal base-extension semantics for the epistemic logic
only differs in a few key places from the base-extension semantics for modal
logics given above. In our presentation, perhaps the most obvious difference
is that we use, in deference to convention, $K_{a}$ as the knowledge operator
for an agent $a$ to replace $\square$. As we want to consider the knowledge of
multiple agents, we add a modal operator $K_{a}$ for every agent $a$ in a
given set of agents $A$, as we did for Kripke semantics. Correspondingly, we
consider relations between bases $\mathfrak{R}_{a}$ for each agent $a$. Again
this relation can be interpreted as indistinguishability so that
$\mathfrak{R}_{a}\mathscr{B}\mathscr{C}$ iff agent $a$ cannot distinguish
between bases $\mathscr{B}\mathscr{C}$.

For single agent $a$, so that the relation is just an unindexed $R$, this
modality reduces to the usual S5 necessitation, $\square$. It follows that our
analysis incorporates this case.

The remainder of this section develops a base-extension semantics for multi-
agent $S5$ by adapting the definitions from Section 3. We begin by setting up
validity in a base and give a definition of modal relation capable of handling
$S5$. We proceed to establish completeness and soundness in Section 5.

######  Definition 4.1.

For atomic propositions $p$ and agents $a$, the language for the epistemic
modal logic is generated by the following grammar:

$\phi:=p\mid\bot\mid\phi\to\phi\mid K_{a}\phi$

Importantly, the definitions for base rules and bases remain unchanged from
the classical semantics and the modal semantics presented above as given in
Definition 3.2. We now no longer need to simply consider a single model
relation $\mathfrak{R}$ but rather a $\mathfrak{R}_{a}$ for every agent $a\in
A$. So, we start by defining validity at a base given a set of relations and
give validity (proper) based on this notion. We write $\Vdash$ instead of
$\Vdash^{S5}$ as we do not consider any other modal logic in the rest of this
paper.

######  Definition 4.2.

For the epistemic modal logic, we define validity at a base $\mathscr{B}$
given a set of agents $A$ and a set of $S5$-modal relations
$\mathfrak{R}_{a}$, one for every agent $a\in A$, denoted by
$\mathfrak{R}^{A}$ as follows:

$\begin{array}[]{l@{\quad}c@{\quad}l}\Vdash_{\mathscr{B},\mathfrak{R}^{A}}p&\mbox{iff}&\mbox{$p$
is in every set of basic sentences closed under $\mathscr{B}$}\\\
&&\mbox{(i.e., iff $p\in\overline{\mathscr{B}}$)}\\\
\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\phi\to\psi&\mbox{iff}&\mbox{$\phi\Vdash_{\mathscr{B},\\{\mathfrak{R}\\}}\psi$}\\\
\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\bot&\mbox{iff}&\mbox{$\Vdash_{\mathscr{B},\mathfrak{R}^{A}}p$
for every basic sentence $p$}\\\
\Vdash_{\mathscr{B},\mathfrak{R}^{A}}K_{a}\phi&\mbox{iff}&\mbox{for all
$\mathscr{C}$ s.t. $\mathfrak{R}_{a}\mathscr{B}\mathscr{C}$,
$\Vdash_{\mathscr{C^{\prime}},\mathfrak{R}^{A}}\phi$}\\\ &&\\\ \mbox{For non
empty $\Gamma$:}&&\\\
\Gamma\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\phi&\mbox{iff}&\mbox{for all
$\mathscr{C}\supseteq\mathscr{B}$, if
$\Vdash_{\mathscr{C},\mathfrak{R}^{A}}\psi$ for all $\psi\in\Gamma$, then
$\Vdash_{\mathscr{C},\mathfrak{R}^{A}}\phi$}\\\ \end{array}$

Given a set of agents $A$, a formula $\phi$ is valid, written as
$\Vdash^{A}\phi$, iff $\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\phi$ for all
modal bases $\mathscr{B}$ and set of modal relations $\mathfrak{R}^{A}$. A
base $\mathscr{B}$ is inconsistent, given a set of agents $A$, iff
$\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\bot$ for any $\mathfrak{R}^{A}$.

As one might expect, the definition of validity for the classical connectives
remains unchanged. The new case for $K_{a}\phi$ is defined in much the same
way as it is in Kripke semantics: by universal quantification over the bases
that are in relation to the base we started at. There are, however, two
differences in our presentation. As mentioned above, we have a $K_{a}$
operator for every agents $a\in A$ and so have different $\mathfrak{R}_{a}$ to
consider. Additionally, in Definition 3.8 we required the validity condition
for $\square$ as it is here to hold for all supersets of $\mathscr{B}$ but, as
follows, we also change the definition of modal relation from Definition 3.7
and it is no longer required.

This is due to the conditions we require to hold for the relation between base
$\mathfrak{R}$, we give below in Definition 4.3. We can not just allow for any
relation on the set of bases to be a modal relation $\mathfrak{R}$.

First, as in Kripke semantics, putting restrictions in form of the well-known
frame conditions of modal logic on $\mathfrak{R}$ will allow us to model
different modal logics.

Here we want to give a base-extension semantics for $S5$ modal logic as our
starting off point for PAL. As might be expected, requiring $\mathfrak{R}$ to
be reflexive, transitive, and Euclidean will be necessary to get a base-
extension semantics for $S5$ modal logic. We show this below as part of our
completeness proof.

There are, however, a couple more restrictions that need to be put on
$\mathfrak{R}$, regardless of the specific modal logic. In comparison to
Kripke models, there is more inherent structure embedded into base-extension
semantics. We now have two types of relations between bases: $\subseteq$ and
$\mathfrak{R}_{a}$ and we have inconsistent bases to deal with. These
conditions make sure that these behave appropriately.

For this we give the conditions (a)-(d). Conditions (c) and (d) are the big
difference from the presentation in Definition 3.7. The idea was that if a
base considers a base possible, at least one of its supersets has to still
think it’s possible. We require that $\mathfrak{R}_{a}\mathscr{B}\mathscr{C}$
and this means that there is a $\mathscr{B}^{\prime}\supset\mathscr{B}$ s.t.
we also have $\mathfrak{R}_{a}\mathscr{B}^{\prime}\mathscr{C}$ and,
conversely, that for all $\mathscr{B}^{\prime\prime}\subset\mathscr{B}$ we
have $\mathfrak{R}_{a}\mathscr{B}^{\prime\prime}\mathscr{C}$. This causes the
$5$ axiom and Euclidean to no longer coincide, as we have shown in [5].

In fact, given an equivalence relation such a relation will collapse to a
universal relation between bases as every base $\mathscr{D}$, we have
$\mathfrak{R}\mathscr{D}\mathscr{D}$, by reflexivity, and so
$\mathfrak{R}\emptyset\mathscr{D}$ and $\mathfrak{R}\mathscr{D}\emptyset$ by
symmetry. So for any two bases $\mathscr{D}_{1}$ and $\mathscr{D}_{2}$ we get
$\mathfrak{R}\mathscr{D}_{1}\mathscr{D}_{2}$ by transitivity.

We present the following new conditions for a modal relation to address this
issue.

######  Definition 4.3.

A relation $\mathfrak{R}_{a}$ on the set bases $\Omega$ is called a $S5$-modal
relation iff, for all $\mathscr{B}$,

  1. (a)

if $\Vdash_{\mathscr{B}}\bot$, there is a $\mathscr{C}$ s.t.
$\mathfrak{R}_{a}\mathscr{B}\mathscr{C}$ and $\Vdash_{\mathscr{C}}\bot$ and,
for all $\mathscr{D}$, if $\mathfrak{R}_{a}\mathscr{B}\mathscr{D}$, then
$\Vdash_{\mathscr{D}}\bot$

  2. (b)

if $\nVdash_{\mathscr{B}}\bot$, then for all $\mathscr{C}$, s.t.
$\mathfrak{R}_{a}\mathscr{B}\mathscr{C}$, $\nVdash_{\mathscr{C}}\bot$

  3. (c)

for all $\mathscr{C}$, if $\mathfrak{R}_{a}\mathscr{B}\mathscr{C}$, then, for
all consistent $\mathscr{D}\supseteq\mathscr{B}$, there is an
$\mathscr{E}\supseteq\mathscr{C}$ s.t.
$\mathfrak{R}_{a}\mathscr{D}\mathscr{E}$

  4. (d)

for all consistent $\mathscr{C}$, if $\mathfrak{R}_{a}\mathscr{B}\mathscr{C}$,
then, for all $\mathscr{D}\subseteq\mathscr{B}$, there are
$\mathscr{E}\subseteq\mathscr{C}$ s.t.
$\mathfrak{R}_{a}\mathscr{D}\mathscr{E}$.

A modal relation $\mathfrak{R}$ is called a $S5$-modal relation iff
$\mathfrak{R}$ is reflexive, transitive, and Euclidean.

Conditions (a) and (b) govern inconsistent bases by making sure that
inconsistent bases all have access to each other (thereby forcing $K_{a}\bot$
and $\neg K_{a}\neg\bot$ at them) and that no consistent base can have access
to an inconsistent one, much like no world in Kripke semantics can have access
to an inconsistent world (see Figure 1).

$\mathscr{B}$$\bot$$\mathscr{C}$$\bot$$\mathscr{D}$$\cancel{\bot}$at least one $\xcancel{\>\;}$ |  $\mathscr{B}$$\cancel{\bot}$$\mathscr{C}$$\bot$$\xcancel{\>\;}$
---|---
Figure 1:  Illustration of Definition 4.3 (a) on the left and (b) on the right

Additionally, we need conditions that ensure that the structure of
$\mathfrak{R}_{a}$ is preserved to super- and subset bases. The conditions (c)
and (d), as they are given here, directly correspond to the _zig and zag_
conditions for bisimulation (see, for example [1]). This makes them obvious
candidates for restrictions to put on modal relations as zig and zag similarly
guarantee that the structure of a relation is preserved when going back or
forth on the bisimulation.

Given the reading of our logic as an epistemic logic, there is another
potential reading of (c) and (d). In game theory [10] and dynamic logics [23]
there are two related notions that formally coincide with zig and zag:
_perfect recall_ and _no learning_. Perfect recall expresses the idea that no
information is lost from previous states. If we interpret a superset bases as
one that has more information in it, because it has more rules in it, (d)
ensures that no bases are considered that were not already considered before
and so that nothing that was previously known becomes lost by adding those new
rules. No learning is the dual of perfect recall and expresses the idea that
no information about the possibility of bases is gained by adding these rules
and so directly corresponds to (c). Perfect recall and _no miracles_ , a
weaker version of no learning that expresses that no learning of unrelated
information can occur, are inherent to updates in PAL and DEL [24, 4].

$\mathscr{B}$$\mathscr{C}$$\mathscr{D}$$\cancel{\bot}$ |  $\Longrightarrow$ | $\mathscr{B}$$\mathscr{C}$$\mathscr{D}$$\mathscr{E}$
---|---|---
Figure 2:  Illustration of Definition 4.3 (c) with dotted lines representing the subset relation $\mathscr{D}$$\mathscr{B}$$\mathscr{C}$ |  $\Longrightarrow$ | $\mathscr{D}$$\mathscr{E}$$\mathscr{B}$$\mathscr{C}$
---|---|---
Figure 3:  Illustration of Definition 4.3 (d) with dotted lines representing
the subset relation

We can now show that some of the most important properties of base-extension
semantics can be generalized to our new system. The end goal is to show that
our semantics is in fact sound and complete with respect to different
Euclidean modal logics. The general idea for this will, again, be close to
what was shown for the non-Euclidean base-extension semantics in [5] but given
our changed definition of modal relation we have to make sure that all steps
of these proofs still hold. Additionally, as the axiomatic systems for modal
logic are easier to work with, we showed that the modal axioms are valid but
followed [16, 17] in showing the classical fragment with respect to a natural
deduction proof system in [5]. Here we show completeness with respect to the
axiomatic systems for modal logic rather than the natural deduction system.

As mentioned above, we no longer require to consider superset bases for the
validity of $K$-formulae (as we did in [5]). This is because the condition (c)
guarantees that if a $K$-formula holds, it also holds at its supersets. We
show this as part of Lemma 4.4. Since the method of appealing to the superset
bases are meant to deal with hypothetical formulae (like implications), this
points to our approach here to be more in-line with the ideas behind base-
extension semantics.

######  Lemma 4.4.

If $\Gamma\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\phi$ and
$\mathscr{B}\subseteq\mathscr{C}$, then
$\Gamma\Vdash_{\mathscr{C},\mathfrak{R}^{A}}\phi$.

######  Proof 4.5.

This proof goes by induction on the complexity of $\phi$. If $\Gamma$ is not
empty, this follows immediately from the validity conditions.

For empty $\Gamma$, the propositional cases remain unchanged from the proof
for classical propositional logic in [17]. The new case is the case in which
$\phi=K_{a}\psi$. In order for
$\Vdash_{\mathscr{B},\mathfrak{R}^{A}}K_{a}\psi$, at all $\mathscr{D}$ s.t.
$\mathfrak{R}_{a}\mathscr{B}\mathscr{D}$,
$\Vdash_{\mathscr{D},\mathfrak{R}^{A}}\psi$. By condition (d) of Definition
4.3, we know that for every $\mathscr{E}$ s.t.
$\mathfrak{R}_{a}\mathscr{C}\mathscr{E}$, there is such a $\mathscr{D}$ with
$\mathscr{D}\subseteq\mathscr{E}$. By induction hypothesis
$\Vdash_{\mathscr{E},\mathfrak{R}^{A}}\psi$ and, since this holds for all
$\mathscr{E}$ s.t. $\mathfrak{R}_{a}\mathscr{C}\mathscr{E}$, we conclude
$\Vdash_{\mathscr{C},\mathfrak{R}^{A}}K_{a}\psi$.

Additionally, the conditions of Definition 4.3 guarantees ex falso quod libet
in the sense that any formula $\phi$ follows from $\bot$.

######  Lemma 4.6.

For all inconsistent bases $\mathscr{B}$ and $\mathfrak{R}^{A}$,
$\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\phi$ for all $\phi$.

######  Proof 4.7.

This proof goes by induction on the complexity of the formula $\phi$. For
propositional $\phi$ this follows immediately from the validity conditions in
Definition 4.2. For the case in which $\phi=K_{a}\psi$, the condition (a)
ensures that any inconsistent base can only have access to other inconsistent
bases and, by induction hypothesis, $\psi$ holds at these bases.

In Definition 3.4, we defined what it means for a base to be maximally-
consistent. In [5] we used maximally-consistent bases to proof soundness for a
variety of modal base-extension semantics and we follow this strategy again
here. This is because, if we carefully pick a $\mathfrak{R^{A}}$, maximally-
consistent bases closely correspond to worlds in Kripke semantics.

In [11], Makinson shows that for classical propositional base-extension
semantics formulae on maximally-consistent bases can be evaluated using their
classical valuations. In Lemma 4.8 This result can be straightforwardly
generalised to show that formulae on maximally-consistent bases can be
evaluated using validity conditions that directly correspond to truth
condition in Kripke semantics in our modal base-extension semantics.

######  Lemma 4.8.

For any set of $S5$-modal relations $\mathfrak{R}^{A}$ and maximally-
consistent base $\mathscr{B}$, the following hold:

  * •

$\nVdash_{\mathscr{B},\mathfrak{R}^{A}}\bot$, and

  * •

$\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\phi\to\psi$ iff
$\nVdash_{\mathscr{B},\mathfrak{R}^{A}}\phi$ or
$\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\psi$.

######  Proof 4.9.

As the validity conditions for $\to$ and $\bot$ do not depend on
$\mathfrak{R}^{A}$ the proof remains unchanged from [11].

From this it follows, maybe unsurprisingly, that the law of excluded middle
holds at maximally-consistent bases.

######  Lemma 4.10.

For every formula $\phi$, maximally-consistent base $\mathscr{B}$, and set of
$S5$-modal relation $\mathfrak{R}^{A}$, either
$\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\phi$ or
$\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\phi\to\bot$.

######  Proof 4.11.

Consider the case in which $\nVdash_{\mathscr{B},\mathfrak{R}^{A}}\phi$. Any
base $\mathscr{C}$ s.t. $\mathscr{C}\supseteq\mathscr{B}$ is inconsistent and
so $\Vdash_{\mathscr{C},\mathfrak{R}^{A}}\bot$ and so
$\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\phi\to\bot$.

Before moving to our completeness and soundness proofs, we show some more
useful properties of maximally-consistent bases. If a formula is not valid at
a particular base, then there is a maximally-consistent superset of that base
at which it does not hold either. In other words, if something holds at all
maximally-consistent supersets of a base, it also has to hold at that base.

######  Lemma 4.12.

For every formula $\phi$, if there is a base $\mathscr{B}$ s.t.
$\nVdash_{\mathscr{B},\mathfrak{R}^{A}}\phi$, then there is a maximally-
consistent base $\mathscr{C}\supseteq\mathscr{B}$ with
$\nVdash_{\mathscr{C},\mathfrak{R}^{A}}\phi$.

######  Proof 4.13.

The proof goes by induction on the complexity of the formula $\phi$. The proof
for the classical cases follows the proof of Lemma 3.3 and 3.4 in [11].

We consider the case in which $\phi=K_{a}\psi$. Since
$\nVdash_{\mathscr{B},\mathfrak{R}^{A}}K_{a}\psi$, there is a $\mathscr{C}$
s.t. $\mathfrak{R}_{a}\mathscr{B}\mathscr{C}$ and
$\nVdash_{\mathscr{C},\mathfrak{R}^{A}}\psi$. By our induction hypothesis, we
know that there is a maximally-consistent
$\mathscr{C}^{*}\supseteq\mathscr{C}$. By symmetry,
$\mathfrak{R}_{a}\mathscr{C}\mathscr{B}$ and so, by condition (c) of
Defintition 4.3, there is a $\mathscr{B}^{\prime}\supseteq\mathscr{B}$ s.t.
$\mathfrak{R}_{a}\mathscr{C}^{*}\mathscr{B}^{\prime}$. Again by symmetry, we
have $\mathfrak{R}_{a}\mathscr{B}^{\prime}\mathscr{C}^{*}$. If
$\mathscr{B}^{\prime}$ is maximally-consistent, let $\mathscr{B}^{\prime}$ be
our $\mathscr{B}^{*}$. Otherwise note that for any maximally-consistent
$\mathscr{B}^{*}\supseteq\mathscr{B}^{\prime}$ we have
$\mathfrak{R}_{a}\mathscr{B}^{*}\mathscr{C}^{*}$ because of condition (c)
again and because $\mathscr{C}^{*}$ is maximally-consistent. Finally, since
$\nVdash_{\mathscr{C}^{*},\mathfrak{R}^{A}}\psi$, we have
$\nVdash_{\mathscr{B}^{*},\mathfrak{R}^{A}}K_{a}\psi$.111It might be of
interest to note here that this proof relies on $\mathfrak{R}_{a}$ being
symmetric. This suggests that it cannot be used to show that this property
holds for arbitrary modal relations. More conditions might be required for
this lemma to hold for non-symmetric modal relations.

The following interesting corollary follows immediately from the special case
in which $\mathscr{B}$ is the empty base.

######  Corollary 1.

Any formula $\phi$ that is valid at all maximally-consistent bases for all
$\mathfrak{R}^{A}$, is valid.

##  5 Soundness and completeness

We show completeness between our semantics and the axiomatic system for
$S5$-modal logic step-by-step. We first show that the axioms and rules of
classical logic are valid in our semantics and then add the modal axioms and
necessitation. This method of proving completeness differs from the methods
generally used in the literature (see, for example, [16, 18]) in which
completeness is shown between a natural deduction proof system and the base-
extension semantics222The result we call completeness is called soundness in
the cited papers.. We believe it is fitting to focus on the axiomatic system
in the case of modal logics because of the close connection between a modal
logic and it’s corresponding modal axiom(s). We follow the same approach as in
the appendix of [5], in which we have shown the completeness of our base-
extension semantics for single-agent modal logics up to $S4$ with respect to
their corresponding axiomatic proof systems.

######  Lemma 5.1.

The following axioms hold:

  1. (1)

$\phi\Vdash^{A}\psi\to\phi$

  2. (2)

$\phi\to(\psi\to\chi)\Vdash^{A}(\phi\to\psi)\to(\phi\to\chi)$

  3. (3)

$(\phi\to\bot)\to(\psi\to\bot)\Vdash^{A}\psi\to\phi$.

Additionally, the following rule holds for any $\mathscr{B}$ and
$\mathfrak{R}^{A}$:

  1. (MP)

If $\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\phi\to\psi$ and
$\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\phi$,
$\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\psi$.

######  Proof 5.2.

The detailed proof can be found in the appendix. We give a sketch here.

The proof of _(MP)_ is a direct proof using the validity condition of $\to$
from Definition 4.2.

The proofs of _(1)_ and _(2)_ follow the same strategy: For an arbitrary base
$\mathscr{B}$ and set of relations $\mathfrak{R}^{A}$, we assume that the
formula on the left of the turnstyle holds and show that the formula on the
right follows. As we are trying to show conditional formulae, we additionally
assume the antecedent and show that the consequent has to hold at all
supersets of $\mathscr{B}$ using Lemma 4.4.

For the proof of _(3)_ , we show that at any maximally-consistent superset
base of $\mathscr{B}$, called $\mathscr{C}$, at which either $\phi$ or
$\phi\to\psi$ holds, $\psi\to\phi$ follows. Given Lemma 4.10, we know that
$\phi$ or $\phi\to\psi$ has to hold for all maximally-consistent bases and so
$\psi\to\phi$ holds at all $\mathscr{C}$. From the contrapositive of Lemma
4.12, it follows that $\psi\to\phi$ holds at $\mathscr{B}$ as well.

Lemma 5.1 tells us that all classical tautologies will also be valid in our
base-extension semantics. This gives us completeness of our system to
classical logic. What is left to show is that the same holds for the
corresponding $S5$ modal formulae. We proof this analogously by showing that
the axioms and rules of our modal logic hold at our bases.

######  Lemma 5.3.

Given $a\in A$. the following axioms hold:

  1. (K) $K_{a}(\phi\to\psi)\Vdash^{A}K_{a}\phi\to K_{a}\psi$

  2. (T) $K_{a}\phi\Vdash^{A}\phi$

  3. (4) $K_{a}\phi\Vdash^{A}K_{a}K_{a}\phi$.

  4. (5) $\neg K_{a}\phi\Vdash^{A}K_{a}\neg K_{a}\phi$

Additionally, the following rule holds for any $\mathscr{B}$ and
$\mathfrak{R}^{A}$:

  1. (NEC) If $\Vdash^{A}\phi$, then $\Vdash^{A}K_{a}\phi$

######  Proof 5.4.

The detailed proof can be found in the appendix. We give a sketch here.

The proof of these goes via contradiction with the exception of _(T)_ , which
can be straightforwardly proven to follow directly from the reflexivity of
$\mathfrak{R}_{a}$.

For the other cases, we take some base $\mathscr{B}$ and set of relations
$\mathfrak{R}^{A}$ and assume the formula to the left of the turnstyle. We
then show that the right’s not holding leads to a contradiction given that
$\mathfrak{R}_{a}$ is a $S5$-modal relation. The arguments used closely mirror
equivalent arguments in Kripke semantics.

From the Lemmas 5.1 and 5.3, our completeness result follows immediately.

######  Theorem 5.5 (Completeness).

If $\phi$ is a theorem of $S5$ modal logic, then $\phi$ is valid in the base-
extension semantics for $S5$.

We show soundness with respect to the Kripke semantics for epistemic logic
rather than the axiomatic system as we did for completeness. We take a formula
that is not valid in Kripke semantics and show that is also not valid on the
corresponding base-extension semantics. This suffices as the Kripke semantics
is sound and complete with respect to the axiomatic system.

This proof-strategy is the same as the one used to show soundness in [5].

######  Theorem 5.6 (Soundness).

If $\phi$ is valid in the base-extension semantics for multi-agent modal logic
$S5$, then $\phi$ is a theorem of multi-agent modal logic $S5$.

######  Proof 5.7.

The detailed proof can be found in the appendix. We give a sketch here.

Take some $\phi$ that is not valid in the Kripke semantics of multi-agent
$S5$, we know that there is a model and a world s.t. $M,w\nvDash\phi$. We
would like to use that model to create bases and a set of modal relations by
taking the maximally-consistent bases that correspond to those worlds. However
this would not work, because it is possible that $M$ contains multiple worlds
with the same valuation, but we cannot have multiple maximally-consistent
bases for which the same formulae hold. So, first we tweak $M$ to create a
model $M^{\prime}$ s.t. no two worlds in $M^{\prime}$ have the same valuation
but for which we still have $M^{\prime},w\nvDash\phi$ by changing the
valuations for propositional formulae that do not appear in $\phi$. We then
use $M^{\prime}$ and methods from [11] to construct maximally-consistent bases
from the worlds in $M^{\prime}$ by choosing our base rules in a way that
guarantees that all non-modal formulae are valid at the bases iff they are
true at the worlds. Next we construct a set of relations $\mathfrak{R}^{A}$ on
our set of bases that, for the bases corresponding to worlds, mimics the
relation $R$ of $M^{\prime}$. This concludes the construction of our
counterexample.

What is left is to show that it is in fact the counterexample we need. To do
so we show that the relations in $\mathfrak{R}^{A}$ are $S5$-modal relations
(i.e., they are reflexive, transitive, and Euclidean, and that the conditions
of Definition 4.3 hold) and that, for the base $\mathscr{B}_{w}$ that
corresponds to $w$ in $M^{\prime}$, any formula that holds at
$\mathscr{B}_{w}$ iff they are true at $w$ Since $\mathscr{B}_{w}$ is a
maximally-consistent base we can use Lemma 4.8. From this and
$M,w\nvDash\phi$, it follows that
$\nVdash_{\mathscr{B}_{w},\mathfrak{R}^{A}}\phi$ and so, we can conclude that
$\phi$ is not valid in base-extension semantics.

Here is a list of the steps of the proof (adapted from [5]):

  1. (1)

Construct $M^{\prime}$ from $M$ s.t. there are no two worlds with the same
valuation.

  2. (2)

Construct maximally-consistent bases corresponding to the worlds in
$M^{\prime}$.

  3. (3)

Define a relation $\mathfrak{R}^{A}$ on the set of bases using
$\\{R\\}^{\prime}$ of $M^{\prime}$

  4. (4)

Prove that the members of $\mathfrak{R}^{A}$ are $S5$-modal relations

  5. (5)

Prove that $\Vdash_{\mathscr{B}_{w},\mathfrak{R}^{A}}\psi$ iff
$M^{\prime},w\vDash\psi$, for all $\psi$

  6. (6)

Since $M,w\nvDash\phi$, it follows that
$\nVdash_{\mathscr{B}_{w},\mathfrak{R}^{A}}\phi$. So, $\phi$ is not valid in
the base-extension semantics for epistemic logic.

##  6 Discussion

We have developed a base-extension semantics for the multi-agent modal logic
$S5$. In [5], a base-extension semantics for modal logic has been given that
is not complete with respect to Euclidean models. We have generalized the
semantics to multiple agents and adapted the conditions for modal relations. A
modal semantics with an unindexed $\square$ can be retrieved simply by
considering the case in which we only have a single agent. We have established
that the resulting semantics is sound and complete.

The semantics for multi-agent $S5$ modal logic provides the semantics for
static epistemic logic from which, in future work, the authors plan to
establish a semantics for PAL. In Kripke semantics, PAL is given in terms of
an update semantics that takes an epistemic model and updates it corresponding
to the information obtained from a certain announcement. In base-extension
semantics, however, such an update has to be restricted to the modal
relations.

For a simple example, take an $S5$-model with two worlds $w$ and $v$ and a
single agent $a$ s.t. $R_{a}wv$. Let some formula $\phi$ hold at $w$ but not
at $v$. An announcement of $\phi$ should result in a model in which $R_{a}wv$
is no longer the case as $a$ no longer considers non-$\phi$ worlds possible.
Similarly, in base-extension semantics an announcement of $\phi$ should change
$\mathfrak{R}_{a}$ to no longer hold between $\phi$ and non-$\phi$ bases. This
would, however, potentially cause $\mathfrak{R}_{a}$ to no longer be a modal
relation, as non-$\phi$ bases can have superset bases on which $\phi$ holds
and, conversely, non-$\phi$ be the case on subset bases of $\phi$ bases.

We explore an approach that ensures that the resulting relations are modal
relations by differentiating at which base an announcement has been taken: If
an announcement of $\phi$ at a base $\mathscr{B}$ causes $\mathscr{B}$ to no
longer have access to a non-$\phi$ base $\mathscr{C}$, then all sub- and
supersets of $\mathscr{B}$ do not have access to those sub- and supersets of
the $\mathscr{C}$ that they had access to before. The details of this approach
remain future work.

This provides the first step into the broader world of dynamic epistemic
logics.

## References

  * [1] Patrick Blackburn, Maarten de Rijke, and Yde Venema.  Modal Logic.  Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001.
  * [2] Robert Brandom.  Articulating reasons: An introduction to inferentialism.  Harvard University Press, 2009.
  * [3] Michael Dummett.  The logical basis of metaphysics.  Duckworth, London, 1991.
  * [4] Timo Eckhardt.  Extended Model Semantics and Forgetting in Dynamic Epistemic Logic.  PhD thesis, The University of Melbourne, 2021.
  * [5] Timo Eckhardt and David J. Pym.  Base-extension semantics for modal logic.  Logic Journal of the IGPL, https://doi.org/10.1093/jigpal/jzae004, 2024.
  * [6] Alexander Gheorghiu and David J. Pym.  Definite formulae, negation-as-failure, and the base-extension semantics of intuitionistic propositional logic.  Bulletin of the Section of Logic, in press, 2023.  Manuscript: http://www0.cs.ucl.ac.uk/staff/D.Pym/NaFP-tS.pdf.
  * [7] Warren Goldfarb.  On Dummett’s “Proof-Theoretic Justifications of Logical Laws”.  In Thomas Piecha and Peter Schroeder-Heister, editors, Advances in Proof-Theoretic Semantics, pages 195–210. Springer International Publishing, Cham, 2016.
  * [8] Saul A Kripke.  A completeness theorem in modal logic1.  The journal of symbolic logic, 24(1):1–14, 1959.
  * [9] Saul A Kripke.  Semantical analysis of modal logic i normal modal propositional calculi.  Mathematical Logic Quarterly, 9(5-6):67–96, 1963.
  * [10] Harold W. Kuhn.  Extensive games and the problem of information.  Princeton University Press, Princeton, NJ, 1953.
  * [11] David Makinson.  On an inferential semantics for classical logic.  Logic Journal of the IGPL, 22(1):147–154, 2014.
  * [12] Thomas Piecha and Peter Schroeder-Heister.  Atomic systems in proof-theoretic semantics: Two approaches.  In Ángel Nepomuceno Fernández, Olga Pombo Martins, and Juan Redmond, editors, Epistemology, Knowledge and the Impact of Interaction, pages 47–62. Springer Verlag, 04 2016.
  * [13] Thomas Piecha and Peter Schroeder-Heister.  The definitional view of atomic systems in proof-theoretic semantics.  In The Logica Yearbook 2016. Universität Tübingen, 2017\.
  * [14] Dag Prawitz.  Ideas and results in proof theory.  In J.E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, volume 63 of Studies in Logic and the Foundations of Mathematics, pages 235–307. Elsevier, 1971.
  * [15] Dag Prawitz.  Meaning approached via proofs.  Synthese, 148:507–524, 2006.
  * [16] Tor Sandqvist.  An Inferentialist Interpretation of Classical Logic.  Uppsala prints and preprints in philosophy. Univ., Department of Philosophy, 2005.
  * [17] Tor Sandqvist.  Classical logic without bivalence.  Analysis, 69(2):211–218, 2009.
  * [18] Tor Sandqvist.  Base-extension semantics for intuitionistic sentential logic.  Logic Journal of the IGPL, 23(5):719–731, 2015.
  * [19] Peter Schroeder-Heister.  Validity concepts in proof-theoretic semantics.  Synthese, 148(3):525–571, 2006.
  * [20] Peter Schroeder-Heister.  Proof-Theoretic versus Model-Theoretic Consequence.  In Michal Pelis, editor, The Logica Yearbook 2007. Filosofia, 2008\.
  * [21] Peter Schroeder-Heister.  Proof-theoretic versus model-theoretic consequence.  In Michal Pelis, editor, The Logica Yearbook 2007, 2008.
  * [22] Will Stafford and Victor Nascimento.  Following all the rules: intuitionistic completeness for generalized proof-theoretic validity.  Analysis, page anac100, 07 2023.
  * [23] Johan van Benthem.  Games in dynamic‐epistemic logic.  Bulletin of Economic Research, 53:219 – 248, 10 2001.
  * [24] Yanjing Wang and Qinxiang Cao.  On axiomatizations of public announcement logic.  Synthese, 190(S1), 2013.

##  Appendix A Proof Details Elided in Main Text

Lemma 5.1 _The following axioms hold:_

  * _(1)_

$\phi\Vdash^{A}\psi\to\phi$

  * _(2)_

$\phi\to(\psi\to\chi)\Vdash^{A}(\phi\to\psi)\to(\phi\to\chi)$

  * _(3)_

$(\phi\to\bot)\to(\psi\to\bot)\Vdash^{A}\psi\to\phi$.

_Additionally, the following rule holds for any $\mathscr{B}$ and
$\mathfrak{R}^{A}$:_

  1. $(MP)$

_If $\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\phi\to\psi$ and
$\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\phi$,
$\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\psi$._

######  Proof A.1.

We start by showing _(MP)_ as it is helpful in establishing the other results.
Simply note that because $\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\phi\to\psi$,
we have for all $\mathscr{C}\supseteq\mathscr{B}$, if
$\Vdash_{\mathscr{C},\mathfrak{R}^{A}}\phi$, then
$\Vdash_{\mathscr{C},\mathfrak{R}^{A}}\psi$. By assumption,
$\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\phi$ and so
$\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\psi$.

By Definition 4.2, for _(1)_ we need to show that for any $\mathscr{B}$, if
$\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\phi$, then
$\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\psi\to\phi$. By Lemma 4.4, for any
$\mathscr{C}\supseteq\mathscr{B}$ s.t.
$\Vdash_{\mathscr{C},\mathfrak{R}^{A}}\psi$ we also have
$\Vdash_{\mathscr{C},\mathfrak{R}^{A}}\phi$ and so
$\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\psi\to\phi$.

For _(2)_ we follow the same strategy of showing that if the formula on the
left of the turnstyle holds at a base, so does the right. To show that
$\Vdash_{\mathscr{B},\mathfrak{R}^{A}}(\phi\to\psi)\to(\phi\to\chi)$, we need
to show that for all $\mathscr{C}\supseteq\mathscr{B}$, if
$\Vdash_{\mathscr{C},\mathfrak{R}^{A}}\phi\to\psi$, then
$\Vdash_{\mathscr{C},\mathfrak{R}^{A}}\phi\to\chi$. Take some
$\mathscr{D}\supseteq\mathscr{C}$ s.t.
$\Vdash_{\mathscr{D},\mathfrak{R}^{A}}\phi\to(\psi\to\chi)$,
$\Vdash_{\mathscr{D},\mathfrak{R}^{A}}\phi\to\psi$ and
$\Vdash_{\mathscr{D},\mathfrak{R}^{A}}\phi$. By _(MP)_ , we get
$\Vdash_{\mathscr{D},\mathfrak{R}^{A}}\chi$ and so,
$\Vdash_{\mathscr{C},\mathfrak{R}^{A}}\phi\to\chi$ and, finally,
$\Vdash_{\mathscr{B},\mathfrak{R}^{A}}(\phi\to\psi)\to(\phi\to\chi)$.

For _(3)_ we take some $\mathscr{B}$ with
$\Vdash_{\mathscr{B},\mathfrak{R}^{A}}(\phi\to\bot)\to(\psi\to\bot)$. To show
that $\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\psi\to\phi$, we show that for all
$\mathscr{C}\supseteq\mathscr{B}$ s.t.
$\Vdash_{\mathscr{C},\mathfrak{R}^{A}}\psi$ we also have
$\Vdash_{\mathscr{C},\mathfrak{R}^{A}}\phi$. Assume
$\nVdash_{\mathscr{C},\mathfrak{R}^{A}}\phi$ for contradiction. By Lemma 4.10,
all maximally-consistent $\mathscr{C}^{*}\supseteq\mathscr{C}$ either
$\Vdash_{\mathscr{C}^{*},\mathfrak{R}^{A}}\phi$ or
$\Vdash_{\mathscr{C}^{*},\mathfrak{R}^{A}}\phi\to\bot$. By Lemma 4.4, we know
that $\Vdash_{\mathscr{C}^{*},\mathfrak{R}^{A}}(\phi\to\bot)\to(\psi\to\bot)$
and $\Vdash_{\mathscr{C}^{*},\mathfrak{R}^{A}}\psi$. So, if
$\Vdash_{\mathscr{C}^{*},\mathfrak{R}^{A}}\phi\to\bot$, then, by _(MP)_ ,
$\Vdash_{\mathscr{C}^{*},\mathfrak{R}^{A}}\psi\to\bot$ and
$\Vdash_{\mathscr{C}^{*},\mathfrak{R}^{A}}\bot$. This is a contradiction as
$\mathscr{C}^{*}$ is, by assumption, consistent. So, $\phi$ holds at all
maximally-consistent superset bases of $\mathscr{C}$ and so, by the
contrapositive of Lemma 4.12, $\Vdash_{\mathscr{C},\mathfrak{R}^{A}}\phi$.

Lemma 5.2 _Given $a\in A$. the following axioms hold:_

  1. $(K)$ $K_{a}(\phi\to\psi)\Vdash^{A}K_{a}\phi\to K_{a}\psi$

  2. $(T)$ $K_{a}\phi\Vdash^{A}\phi$

  3. $(4)$ $K_{a}\phi\Vdash^{A}K_{a}K_{a}\phi$.

  4. $(5)$ $\neg K_{a}\phi\Vdash^{A}K_{a}\neg K_{a}\phi$

_Additionally, the following rule holds for any $\mathscr{B}$ and
$\mathfrak{R}^{A}$:_

  1. $(NEC)$ _If $\Vdash^{A}\phi$, then $\Vdash^{A}K_{a}\phi$_

######  Proof A.2.

For _(K)_ , we show the contrapositive and assume
$\nVdash_{\mathscr{B},\mathfrak{R}^{A}}K_{a}\phi\to K_{a}\psi$ for an
arbitrary $\mathscr{B}$ and $\mathfrak{R}^{A}$. So, there is a
$\mathscr{C}\supseteq\mathscr{B}$ s.t.
$\Vdash_{\mathscr{C},\mathfrak{R}^{A}}K_{a}\phi$ and
$\nVdash_{\mathscr{C},\mathfrak{R}^{A}}K_{a}\psi$. So, there are
$\mathscr{D}\supseteq\mathscr{C}$ and $\mathscr{E}$ s.t.
$\mathfrak{R}_{a}\mathscr{D}\mathscr{E}$ with
$\Vdash_{\mathscr{E},\mathfrak{R}^{A}}\phi$ but
$\nVdash_{\mathscr{E},\mathfrak{R}^{A}}\psi$ and so
$\nVdash_{\mathscr{E},\mathfrak{R}^{A}}\phi\to\psi$ and
$\Vdash_{\mathscr{D},\mathfrak{R}^{A}}K_{a}(\phi\to\psi)$. Finally, as
$\mathscr{D}\supseteq\mathscr{B}$,
$\nVdash_{\mathscr{B},\mathfrak{R}^{A}}K_{a}(\phi\to\psi)$.

For _(T)_ , take some $\Vdash_{\mathscr{B},\mathfrak{R}^{A}}K_{a}\phi$. By the
reflexivity of $\mathfrak{R}_{a}$, $\mathfrak{R}_{a}\mathscr{B}\mathscr{B}$
and so $\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\phi$.

For _(4)_ , we, without loss of generality, assume some $\mathscr{B}$ and
$\mathfrak{R}^{A}$ s.t. $\Vdash_{\mathscr{B},\mathfrak{R}^{A}}K_{a}\phi$. For
contradiction, we also assume
$\nVdash_{\mathscr{B},\mathfrak{R}^{A}}K_{a}K_{a}\phi$. So, there are
$\mathscr{C}\supseteq\mathscr{B}$ and $\mathscr{D}$ s.t.
$\mathfrak{R}_{a}\mathscr{C}\mathscr{D}$ and
$\nVdash_{\mathscr{D},\mathfrak{R}^{A}}K_{a}\phi$. This means there have to be
$\mathscr{E}\supseteq\mathscr{D}$ and $\mathscr{F}$ s.t.
$\mathfrak{R}_{a}\mathscr{E}\mathscr{F}$ and
$\nVdash_{\mathscr{F},\mathfrak{R}^{A}}\phi$. By Definition 4.3 $(d)$, we know
there is a $\mathscr{G}\subseteq\mathscr{F}$ and
$\mathfrak{R}_{a}\mathscr{D}\mathscr{G}$ and, by transitivity,
$\mathfrak{R}_{a}\mathscr{C}\mathscr{G}$. Obviously,
$\nVdash_{\mathscr{G},\mathfrak{R}^{A}}\phi$ and so
$\nVdash_{\mathscr{B},\mathfrak{R}^{A}}K_{a}\phi$, which contradicts our
assumption.

For _(5)_ , we assume, without loss of generality, some $\mathscr{B}$ and
$\mathfrak{R}^{A}$ s.t. $\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\neg K_{a}\phi$
and, for contradiction, $\nVdash_{\mathscr{B},\mathfrak{R}^{A}}K_{a}\neg
K_{a}\phi$. So, there is $\mathscr{C}$ s.t.
$\mathfrak{R}_{a}\mathscr{B}\mathscr{C}$ and
$\nVdash_{\mathscr{C},\mathfrak{R}^{A}}\neg K_{a}\phi$. So, there is a
$\mathscr{D}\supseteq\mathscr{C}$ s.t $\mathscr{D}$ is consistent and
$\Vdash_{\mathscr{D},\mathfrak{R}^{A}}K_{a}\phi$.

From $\Vdash_{\mathscr{B},\mathfrak{R}^{A}}\neg K_{a}\phi$ it follows that for
all consistent $\mathscr{E}\supseteq\mathscr{B}$, we have
$\nVdash_{\mathscr{B},\mathfrak{R}^{A}}K_{a}\phi$. So there is a $\mathscr{F}$
s.t. $\mathfrak{R}_{a}\mathscr{E}\mathscr{F}$ and
$\nVdash_{\mathscr{F},\mathfrak{R}^{A}}\phi$.

By symmetry, we have $\mathfrak{R}_{a}\mathscr{C}\mathscr{B}$ and so, by
condition (c) of Definition 4.3, for one of these
$\mathscr{E}\supseteq\mathscr{B}$ we have
$\mathfrak{R}_{a}\mathscr{D}\mathscr{E}$ and, again by symmetry,
$\mathfrak{R}_{a}\mathscr{E}\mathscr{D}$. By Euclidean and
$\mathfrak{R}_{a}\mathscr{E}\mathscr{F}$, we have
$\mathfrak{R}_{a}\mathscr{D}\mathscr{F}$ which gives us our contradiction: We
have $\Vdash_{\mathscr{D},\mathfrak{R}^{A}}K_{a}\phi$ and
$\nVdash_{\mathscr{F},\mathfrak{R}^{A}}\phi$.

We show _(NEC)_ via the contrapositive. If $\nVdash^{A}K_{a}\phi$, then
$\nVdash^{A}\phi$. Suppose $\nVdash^{A}K_{a}\phi$. So, there is a
$\mathscr{B}$ and an $\mathfrak{R}^{A}$ s.t.
$\nVdash_{\mathscr{B},\mathfrak{R}^{A}}K_{a}\phi$. Therefore, there are
$\mathscr{C}\supseteq\mathscr{B}$ and $\mathscr{D}$ s.t.
$\mathfrak{R}_{a}\mathscr{C}\mathscr{D}$ and
$\nVdash_{\mathscr{D},\mathfrak{R}^{A}}\phi$ and, so, $\nVdash^{A}\phi$.

Theorem 5.4 (Soundness) _If $\phi$ is valid in the base-extension semantics
for multi-agent modal logic $S5$, then $\phi$ is a theorem of multi-agent
modal logic $S5$._

######  Proof A.3.

We assume an $S5$ model $M=\langle F,V\rangle$ and a world $w$ s.t.
$M,w\nvDash\phi$. We begin by step (i) from the proof sketch above.

We can have worlds with the same valuation but not maximally-consistent bases
that agree on all propositional atoms. So we need to adapt our $M$ so that
every world disagrees on some propositional formulae that are not relevant to
$\phi$. We do so by assigning a different propositional atom $q$ that does not
appear in $\phi$ to each world. This is possible as we have infinitely many
propositional sentences. For every $v\in W$, let $q_{v}$ be some propositional
sentence s.t. it does not appear in $\phi$ and, for all worlds $u$, if $u\neq
v$, then $q_{v}\neq q_{u}$.

Let $M^{\prime}=\langle F,V^{\prime}\rangle$ be s.t. for all $v\in W$,
$V^{\prime}(q_{v})=W\setminus\\{v\\}$ and $V^{\prime}(p)=V(p)$ for all other
propositional atoms $p$. Note that $M^{\prime},w\nvDash\phi$. This concludes
our first step.

In step (ii), this model is now used to construct bases that correspond to its
worlds. For every world $w\in W$, we define a base $\mathscr{A}_{w}$ in the
following way:

$\begin{split}\mathscr{A}_{w}:=&\\{\Rightarrow p:M^{\prime},w\vDash
p\\}\cup\\\ &\\{\Rightarrow q_{v}:v\in W\text{ and }v\neq w\\}\cup\\\
&\\{p\Rightarrow q_{w},q_{w}\Rightarrow p:M^{\prime},w\nvDash p\\}\\\
\end{split}$

By Lemma 3.5, we know there is a maximally-consistent
$\mathscr{C}\supseteq\mathscr{A}_{w}$ s.t. $\Vdash_{\mathscr{C}}q_{w}$, so we
can let $\mathscr{B}_{w}$ be that $\mathscr{C}$.

This gives us the bases we require, but we still need to define a set of
relations $\mathfrak{R}^{A}$ between them. This is step (iii).

We consider the relations such that, for every agent $a\in A$
$\mathfrak{R}_{a}\mathscr{B}\mathscr{C}$ only by the following:

  1. (1)

if $R_{a}wv$, then $\mathfrak{R}_{a}\mathscr{B}_{w}\mathscr{B}_{v}$

  2. (2)

if $\mathscr{B}$ and $\mathscr{C}$ are inconsistent, then
$\mathfrak{R}_{a}\mathscr{B}\mathscr{C}$

  3. (3)

    1. (a)

for all $\mathscr{B}$ and $\mathscr{C}$ s.t. there are exactly one maximally-
consistent $\mathscr{B}^{\prime}\supset\mathscr{B}$ and one maximally-
consistent $\mathscr{C}^{\prime}\supset\mathscr{C}$ and there are $w,v\in W$
s.t. $\mathscr{B}^{\prime}=\mathscr{B}_{w}$ and
$\mathscr{C}^{\prime}=\mathscr{B}_{v}$, if $R_{a}wv$, then
$\mathfrak{R}_{a}\mathscr{B}\mathscr{C}$,

    2. (b)

for all $\mathscr{B}$, $\mathscr{C}$ s.t. there are $w,v\in W$ and
$\mathscr{B}_{w}\supset\mathscr{B}$ and $\mathscr{B}_{v}\supset\mathscr{B}$,
if $R_{a}wv$ and there are maximally-consistent
$\mathscr{B}^{\prime}\supset\mathscr{B}$ and
$\mathscr{C}^{\prime}\supset\mathscr{C}$ and
$\mathscr{B}^{\prime}\neq\mathscr{B}_{w}$ and
$\mathscr{C}^{\prime}\neq\mathscr{B}_{v}$, then
$\mathfrak{R}_{a}\mathscr{B}\mathscr{C}$,

    3. (c)

for all consistent $\mathscr{B}$, if there are no $w,v\in W$ with
$\mathscr{B}_{w}\supseteq\mathscr{B}$ and
$\mathscr{B}_{v}\supseteq\mathscr{C}$, then
$\mathfrak{R}_{a}\mathscr{B}\mathscr{C}$,

  4. (4)

reflexivity: for all bases $\mathscr{B}$,
$\mathfrak{R}_{a}\mathscr{B}\mathscr{B}$,

  5. (5)

transitivity: if $\mathfrak{R}_{a}\mathscr{B}\mathscr{C}$ and
$\mathfrak{R}_{a}\mathscr{C}\mathscr{D}$, then
$\mathfrak{R}_{a}\mathscr{B}\mathscr{D}$

  6. (6)

Euclidean: if $\mathfrak{R}_{a}\mathscr{B}\mathscr{C}$ and
$\mathfrak{R}_{a}\mathscr{B}\mathscr{D}$, then
$\mathfrak{R}_{a}\mathscr{C}\mathscr{D}$.

We have now constructed the bases and the relation required, but we have not
yet shown that the relations are in fact $S5$-modal relations. This is step
(iv).

It is easy to see that any $\mathfrak{R}_{a}$ is an equivalence relation by
(4), (5), and (6). We still need to show that the conditions (a)-(d) from
Definition 4.3 hold (i.e., that it is a modal relation). Since (2) simply
connects all inconsistent bases with each other, condition $(a)$ holds
straightforwardly. Any step that can connect a base to an inconsistent base
can only do so if the initial base is itself inconsistent. So, $(b)$ follows.

To show (c), we have to consider all steps of the construction of
$\mathfrak{R}_{a}$ that introduce new connections. (1) only applies for
maximally-consistent bases and (2) only for inconsistent ones, so (c) holds
for those trivially.

For (3c), note that all $\mathscr{D}\supseteq\mathscr{B}$ are also do not have
any $w$ s.t. $\mathscr{B}_{w}\supseteq\mathscr{D}$ and so
$\mathfrak{R}_{a}\mathscr{D}\mathscr{C}$. For
$\mathfrak{R}_{a}\mathscr{B}\mathscr{C}$ added by (3a), there are
$\mathscr{B}_{w}\supset\mathscr{B}$ and $\mathscr{B}_{v}\supset\mathscr{C}$
with $\mathfrak{R}_{a}\mathscr{B}_{w}\mathscr{B}_{v}$ and for all
$\mathscr{B}\subseteq\mathscr{B}^{\prime}\subset\mathscr{B}_{w}$ we have
$\mathfrak{R}_{a}\mathscr{B}^{\prime}\mathscr{C}$.

For (3b), if there are $w,v\in W$ and $\mathscr{B}_{w}\supseteq\mathscr{B}$
and $\mathscr{B_{v}}\supseteq\mathscr{B}$ and there are maximally-consistent
$\mathscr{B}^{\prime}\supseteq\mathscr{B}$ and
$\mathscr{C}^{\prime}\supseteq\mathscr{C}$ and
$\mathscr{B}^{\prime}\neq\mathscr{B}_{w}$ and
$\mathscr{C}^{\prime}\neq\mathscr{B}_{v}$, then we have a couple of cases to
consider for $\mathscr{D}$:

If $\mathscr{D}$ has $\mathscr{B}_{w}$ and another maximally-consistent base
$\mathscr{D}^{\prime}$ as their supersets, we get
$\mathfrak{R}_{a}\mathscr{D}\mathscr{C}$ by (3b).

If $\mathscr{D}=\mathscr{B}_{w}$ for some $w$, then there is a
$\mathscr{B}_{v}\supset\mathscr{C}$ and
$\mathfrak{R}_{a}\mathscr{B}_{w}\mathscr{B}_{v}$.

If there is a $w$ and exactly one maximally-consistent
$\mathscr{D}^{\prime}\supset\mathscr{D}$ s.t.
$\mathscr{D}^{\prime}=\mathscr{B}_{w}$, then there is also a $v$ s.t.
$\mathfrak{R}_{a}\mathscr{B}_{w}\mathscr{B}_{v}$ and
$\mathscr{B}_{v}\supset\mathscr{C}$. By (3a), for all
$\mathscr{E}\supset\mathscr{C}$ s.t. $\mathscr{B}_{v}$ is the only maximally-
consistent superset of $\mathscr{E}$, we have
$\mathfrak{R}_{a}\mathscr{D}\mathscr{E}$.

If $\mathscr{D}$ has no $w$ s.t. $\mathscr{B}_{w}\supseteq\mathscr{D}$, then
we have $\mathfrak{R}_{a}\mathscr{D}\mathscr{E}$ for all
$\mathscr{E}\supset\mathscr{C}$ s.t. there are no $v$ with
$\mathscr{B}_{v}\supset\mathscr{E}$.

For (4), simply note that if $\mathfrak{R}_{a}\mathscr{B}\mathscr{B}$, then
for all consistent $\mathscr{C}\supset\mathscr{B}$, we have
$\mathfrak{R}_{a}\mathscr{C}\mathscr{C}$. For (5), take some
$\mathfrak{R}_{a}$ with $\mathfrak{R}_{a}\mathscr{B}\mathscr{C}$ and
$\mathfrak{R}_{a}\mathscr{C}\mathscr{D}$ for which (c) holds. We show that is
still holds when we add $\mathfrak{R}_{a}\mathscr{B}\mathscr{D}$. By
assumption we know that for all $\mathscr{B}^{\prime}\supseteq\mathscr{B}$
there are $\mathscr{C}^{\prime}\supseteq\mathscr{C}$ s.t.
$\mathfrak{R}_{a}\mathscr{B}^{\prime}\mathscr{C}^{\prime}$ by (c). Similarly,
we know that there is a $\mathscr{D}^{\prime}\supseteq\mathscr{D}$ and that
$\mathfrak{R}_{a}\mathscr{C}^{\prime}\mathscr{D}^{\prime}$. So, by
transitivity, $\mathfrak{R}_{a}\mathscr{B}^{\prime}\mathscr{D}^{\prime}$. For
(6), we follow the same strategy. Suppose
$\mathfrak{R}_{a}\mathscr{B}\mathscr{C}$ and
$\mathfrak{R}_{a}\mathscr{B}\mathscr{D}$. By assumption we know that for all
$\mathscr{B}^{\prime}$ there are $\mathscr{C}^{\prime}\supseteq\mathscr{C}$
and $\mathscr{D}^{\prime}\supseteq\mathscr{D}$ with
$\mathfrak{R}_{a}\mathscr{B}^{\prime}\mathscr{C}^{\prime}$ and
$\mathfrak{R}_{a}\mathscr{B}^{\prime}\mathscr{D}^{\prime}$ and so, by
Euclidean, $\mathfrak{R}_{a}\mathscr{C}^{\prime}\mathscr{D}^{\prime}$. With
this we have shown that (c) holds for $\mathfrak{R}_{a}$.

For (d), again, we go through the steps of the construction of
$\mathfrak{R}_{a}$. Again, (2) holds trivially because it only deals with
inconsistent bases.

For $(3b)$, it suffices that for every
$\mathscr{B}^{\prime}\subseteq\mathscr{B}$ we have
$\mathfrak{R}_{a}\mathscr{B}^{\prime}\emptyset$.

For $(3c)$ and $\mathscr{B}^{\prime}\subseteq\mathscr{B}$, there are two cases
to consider: Either there is a $w$ s.t.
$\mathscr{B}^{\prime}\subset\mathscr{B}_{w}$, in which case, by $(3b)$,
$\mathfrak{R}_{a}\mathscr{B}^{\prime}\emptyset$, or there is no such $w$, in
which case for all $\mathscr{C}$, s.t.
$\mathfrak{R}_{a}\mathscr{B}\mathscr{C}$, we also have
$\mathfrak{R}_{a}\mathscr{B}^{\prime}\mathscr{C}$, by $(3c)$.

For $(3a)$ and $\mathscr{B}^{\prime}\subseteq\mathscr{B}$, there are similarly
two cases to consider. If $\mathscr{B}_{w}$ is still the only maximally-
consistent superset of $\mathscr{B}^{\prime}$, then, by $(3a)$,
$\mathfrak{R}_{a}\mathscr{B}^{\prime}\mathscr{C}$ for all $\mathscr{C}$ s.t.
$\mathfrak{R}_{a}\mathscr{B}\mathscr{C}$. Otherwise, by $(3b)$,
$\mathfrak{R}_{a}\mathscr{B}^{\prime}\emptyset$.

For $(1)$ we have to consider three cases now: The case in which
$\mathscr{B}^{\prime}=\mathscr{B}_{w}$ is trivial, the case in which
$\mathscr{B}_{w}$ is the only maximally-consistent superset base of
$\mathscr{B}^{\prime}$ immediately follows from $(3a)$, and, finally, if there
are multiple maximally-consistent supersets of $\mathscr{B}^{\prime}$, then,
by $(3b)$, $\mathfrak{R}_{a}\mathscr{B}^{\prime}\emptyset$.

For (4), (5), and (6), it suffices to take the proofs of (c) for these cases
and flip the subset-relations.

With these results, we have show that every relation
$\mathfrak{R}_{a}\in\mathfrak{R}^{A}$ is an $S5$-modal relation.

We proceed to show step (v): for all $\phi$ and $w\in W$,
$\Vdash_{\mathscr{B}_{w},\mathfrak{R}^{A}}\phi$ iff $M,w\vDash\phi$. We do so
by induction on $\phi$. The case in which $\phi=p$ follows directly from our
construction of $\mathscr{B}_{w}$.

For the case in which $\phi=\bot$ it suffices to point out that $\bot$ cannot
hold at $w$ and that $\mathscr{B}_{w}$ is consistent.

For $\phi=\psi\to\chi$, note that $M,w\Vdash\psi\to\chi$ iff $M,w\Vdash\psi$
or $M,w\nVdash\chi$. By Lemma 4.8, we similarly have
$\Vdash_{\mathscr{B}_{w},\mathfrak{R}^{A}}\psi\to\chi$ iff
$\nVdash_{\mathscr{B}_{w},\mathfrak{R}^{A}}\psi$ or
$\Vdash_{\mathscr{B}_{w},\mathfrak{R}^{A}}\chi$. We conclude by the inductive
hypothesis.

Finally, for $\phi=K_{a}\psi$, $M,w\Vdash K_{a}\psi$ iff for all $v$ s.t.
$R_{a}wv$, $M,v\Vdash\psi$. Again by Lemma 4.8, we have
$\Vdash_{\mathscr{B}_{w},\mathfrak{R}^{A}}K_{a}\psi$ iff for all $\mathscr{C}$
s.t. $\mathfrak{R}_{a}\mathscr{B}_{w}\mathscr{C}$,
$\Vdash_{\mathscr{C},\mathfrak{R}^{A}}\psi$. By our construction of
$\mathfrak{R}_{a}$ we know for every such $\mathscr{C}$ there is a $v\in W$
s.t. $\mathscr{C}=\mathscr{B}_{v}$ and $R_{a}wv$. By the inductive hypothesis
$\Vdash_{\mathscr{C},\mathfrak{R}^{A}}\psi$ iff $M,v\Vdash\psi$ and we are
done.

With this we can reach our result by step (vi). From $M^{\prime},w\nvDash\phi$
and (v), it follows that $\nVdash_{\mathscr{B}_{w},\mathfrak{R}^{A}}\phi$.
Since $\mathfrak{R}^{A}$ is a set of $S5$-modal relations, $\phi$ is not valid
in the base-extension semantics for $S5$.

We conclude that (for arbitrary $\phi$), if $\phi$ is not valid in the Kripke
semantics for $S5$, then it is not valid in the base-extension semantics for
epistemic logic either.