A cut-free Gentzen formulation of the modal logic S5

DOI10.1093/jigpal/8.5.629zbMath0965.03023OpenAlexW2023863745MaRDI QIDQ4511541

Torben Braüner

Publication date: 28 February 2001

Published in: Logic Journal of IGPL (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/jigpal/8.5.629

zbMATH Keywords

modal logiccut-eliminationGentzen systemS5

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05)

Related Items

A deep inference system for the modal logic S5 ⋮ Rooted hypersequent calculus for modal logic \textsf{S5} ⋮ Varieties of Relevant S5 ⋮ Hypersequent Calculi for S5: The Methods of Cut Elimination ⋮ Full classical S5 in natural deduction with weak normalization ⋮ A CUT-FREE SIMPLE SEQUENT CALCULUS FOR MODAL LOGIC S5 ⋮ The multiplicative-additive Lambek calculus with subexponential and bracket modalities ⋮ On a multilattice analogue of a hypersequent S5 calculus ⋮ Why does the proof-theory of hybrid logic work so well? ⋮ Proof analysis in modal logic ⋮ CUT-FREE COMPLETENESS FOR MODULAR HYPERSEQUENT CALCULI FOR MODAL LOGICS K, T, AND D ⋮ Proof-theoretic functional completeness for the hybrid logics of everywhere and elsewhere