A CUT-FREE SIMPLE SEQUENT CALCULUS FOR MODAL LOGIC S5

DOI10.1017/S1755020308080040zbMath1204.03024OpenAlexW2164133707MaRDI QIDQ3580655

Francesca Poggiolesi

Publication date: 13 August 2010

Published in: The Review of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s1755020308080040

zbMATH Keywords

sequent calculusS5contraction-freecut-freemodal propositional logic

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Decidability of theories and sets of sentences (03B25)

Related Items (28)

VALENTINI’S CUT-ELIMINATION FOR PROVABILITY LOGIC RESOLVED ⋮ Linear Nested Sequents, 2-Sequents and Hypersequents ⋮ Conservativeness and Eliminability for Anti-Realistic Definitions ⋮ An Analytic Propositional Proof System on Graphs ⋮ From single agent to multi-agent via hypersequents ⋮ Hypersequent rules with restricted contexts for propositional modal logics ⋮ Labeled sequent calculi for modal logics and implicit contractions ⋮ LINEAR TIME IN HYPERSEQUENT FRAMEWORK ⋮ Rooted hypersequent calculus for modal logic \textsf{S5} ⋮ Varieties of Relevant S5 ⋮ THE LOGIC OF HYPERLOGIC. PART A: FOUNDATIONS ⋮ Falsification-aware calculi and semantics for normal modal logics including S4 and S5 ⋮ Natural deduction calculi for classical and intuitionistic S5 ⋮ Cut Elimination Theorem for Non-Commutative Hypersequent Calculus ⋮ Hypersequent Calculi for S5: The Methods of Cut Elimination ⋮ Eliminability of cut in hypersequent calculi for some modal logics of linear frames ⋮ A Critical Overview of the Most Recent Logics of Grounding ⋮ Through an Inference Rule, Darkly ⋮ Non-classical elegance for sequent calculus enthusiasts ⋮ A contraction-free and cut-free sequent calculus for propositional dynamic logic ⋮ A CUT-FREE SIMPLE SEQUENT CALCULUS FOR MODAL LOGIC S5 ⋮ Hypersequent and display calculi -- a unified perspective ⋮ Display calculi and other modal calculi: a comparison ⋮ The Method of Tree-Hypersequents for Modal Propositional Logic ⋮ On a multilattice analogue of a hypersequent S5 calculus ⋮ Truth values and proof theory ⋮ Cut elimination for \(\mathrm{S4}_n\) and \(\mathrm{K4}_n\) with the central agent axiom ⋮ CUT-FREE COMPLETENESS FOR MODULAR HYPERSEQUENT CALCULI FOR MODAL LOGICS K, T, AND D

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proof analysis in modal logic
• A perspective on modal sequent logic
• Cut-free modal sequents for normal modal logics
• Indexed systems of sequents and cut-elimination
• A CUT-FREE SIMPLE SEQUENT CALCULUS FOR MODAL LOGIC S5
• A cut-free Gentzen-type system for the modal logic S5
• Sequent Calculi for Normal Modal Propositional Logics
• A cut-free Gentzen formulation of the modal logic S5
• Sequent-systems for modal logic

This page was built for publication: A CUT-FREE SIMPLE SEQUENT CALCULUS FOR MODAL LOGIC S5