Syntactic cut-elimination for provability logic GL via nested sequents

DOI10.4204/EPTCS.415.11MaRDI QIDQ6934038zbMATH OpenFDO

Authors Akinori Maniwa, Ryo Kashima

Publication date 3 September 2025

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4204/EPTCS.415.11

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Provability logics and related algebras (e.g., diagonalizable algebras) (03F45)

Cites work

• A proof theory for the logic of provability in true arithmetic
• A purely syntactic and cut-free sequent calculus for the modal logic of provability
• Cut-free sequent calculi for some tense logics
• Deep sequent systems for modal logic
• Focused and Synthetic Nested Sequents
• scientific article; zbMATH DE number 2242586 (Why is no real title available?)
• On modal systems having arithmetical interpretations
• On some proof theoretical properties of the modal logic GL
• On the proof theory of the modal logic for arithmetic provability
• Proof analysis in modal logic
• Provability interpretations of modal logic
• The Method of Tree-Hypersequents for Modal Propositional Logic
• The modal logic of provability. The sequential approach
• The modal logic of provability: cut-elimination
• Valentini's cut-elimination for provability logic resolved

This page was built for publication: Syntactic cut-elimination for provability logic GL via nested sequents

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6934038)