Logic and AI Seminar: Yet another sequent calculus for S5
The speaker will be Paul Svanberg, who will give a talk on “Yet another sequent calculus for S5”
Main content
In this seminar, we will discuss work in progress on a new sequent calculus for propositional S5. The sequent calculus is constructed around sequents of the form $\Pi ; \Gamma \vdash \Delta ; \Sigma$, where $\Gamma\vdash\Delta$ is an S4-sequent in the usual sense, $\Pi, \Sigma$ are multisets of implicitly modalized formulae, diamonds for $\Pi$ and boxes for $\Sigma$, and the semi-colon is a non-commutative sequent comma governed by rules satisfying the subformula property. Cut elimination is currently being investigated, hence the “work in progress”-qualifier. We will pay particular attention to how the principle of necessitation is captured by not one, but two pairs of rules in the sequent calculus, one for necessitation in S4 and one for necessitation in S5.