A Cut-free sequent calculus for modal logic S5

TL;DR

This paper introduces G3S5, a new sequent calculus for modal logic S5 that maintains the subformula property and proves key rule admissibilities, enhancing proof-theoretic understanding.

Contribution

It presents G3S5, a Gentzen-style sequent calculus for S5 with the subformula property and establishes the admissibility of weakening, contraction, and cut rules.

Findings

G3S5 has the subformula property.

Weakening, contraction, and cut rules are admissible in G3S5.

The system improves proof-theoretic analysis of S5.

Abstract

We present the system G3S5, a Gentzen-style sequent calculus system for the modal propositional logic S5, which in a sense has the subformula property. We formulate the rules of G3 S5 in the system G3S5; which has the subformula property and prove the admissibility of the weakening, contraction and cut rules for it.