English

A Cut-free sequent calculus for modal logic S5

Logic 2018-05-24 v3

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.

Cite

@article{arxiv.1711.04634,
  title  = {A Cut-free sequent calculus for modal logic S5},
  author = {Mojtaba Aghaei and Hamzeh Mohammadi},
  journal= {arXiv preprint arXiv:1711.04634},
  year   = {2018}
}

Comments

21 pages

R2 v1 2026-06-22T22:44:19.107Z