VALENTINI’S CUT-ELIMINATION FOR PROVABILITY LOGIC RESOLVED

DOI10.1017/S1755020311000323zbMath1254.03113OpenAlexW2102143997MaRDI QIDQ2890695

Revantha Ramanayake, Rajeev Goré

Publication date: 11 June 2012

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

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

zbMATH Keywords

contractionprovability logic GLLöb axiomsyntactical cut elimination

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05) Provability logics and related algebras (e.g., diagonalizable algebras) (03F45)

Related Items (8)

Cut-elimination for provability logic by terminating proof-search: formalised and deconstructed using Coq ⋮ Provability multilattice logic ⋮ A proof theory for the logic of provability in true arithmetic ⋮ Formalized meta-theory of sequent calculi for linear logics ⋮ Sequent calculi for intuitionistic Gödel-Löb logic ⋮ Formalized meta-theory of sequent calculi for substructural logics ⋮ Unnamed Item ⋮ Circular proofs for the Gödel-Löb provability logic

Cites Work

• The modal logic of provability: cut-elimination
• Proof analysis in modal logic
• The modal logic of provability. The sequential approach
• Provability interpretations of modal logic
• \(LE^{t}_{ \to }, LR^{ \circ }_{\widehat{\sim}}, LK\) and cutfree proofs
• A CUT-FREE SIMPLE SEQUENT CALCULUS FOR MODAL LOGIC S5
• On modal systems having arithmetical interpretations
• On the Proof Theory of the Modal Logic Grz
• A Syntactic Proof of Cut‐Elimination For GL_lin
• A cut-free Gentzen-type system for the modal logic S5
• On the proof theory of the modal logic for arithmetic provability
• Relations between propositional normal modal logics: an overview
• On permuting cut with contraction
• Theoremhood-preserving Maps Characterizing Cut Elimination for Modal Provability Logics
• Sequent-systems for modal logic
• A system of interaction and structure
• A PURELY SYNTACTIC AND CUT-FREE SEQUENT CALCULUS FOR THE MODAL LOGIC OF PROVABILITY
• A proof of Gentzen's \textit{Hauptsatz} without multicut

This page was built for publication: VALENTINI’S CUT-ELIMINATION FOR PROVABILITY LOGIC RESOLVED