A cut-free Gentzen-type system for the modal logic S5

DOI10.2307/2273355zbMath0444.03010OpenAlexW2112784644MaRDI QIDQ3887437

Masahiko Sato

Publication date: 1980

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

Full work available at URL: https://doi.org/10.2307/2273355

zbMATH Keywords

modal logiccut-eliminationS5cut-free Gentzen-type system

Mathematics Subject Classification ID

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

Related Items (6)

VALENTINI’S CUT-ELIMINATION FOR PROVABILITY LOGIC RESOLVED ⋮ Rooted hypersequent calculus for modal logic \textsf{S5} ⋮ A simple tableau system for the logic of elsewhere ⋮ Full classical S5 in natural deduction with weak normalization ⋮ A CUT-FREE SIMPLE SEQUENT CALCULUS FOR MODAL LOGIC S5 ⋮ A cut-free sequential system for the propositional modal logic of finite chains

Cites Work

• A study of Kripke-type models for some modal logics by Gentzen's sequential method
• Untersuchungen über das logische Schliessen. II

This page was built for publication: A cut-free Gentzen-type system for the modal logic S5