Base-extension semantics for S5 modal logic

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). This note directly supplements [4] and does not repeat the discussion in it.