Valentini's cut-elimination for provability logic resolved

DOI10.1017/S1755020311000323zbMATH Open1254.03113OpenAlexW2102143997MaRDI QIDQ2890695FDOQ2890695

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 GL[https://portal.mardi4nfdi.de/w/index.php?title=+Special%3ASearch&search=L%EF%BF%BD%EF%BF%BDb+axiom&go=Go L��b axiom]syntactical 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)

Cites Work

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

Cited In (9)

• A proof theory for the logic of provability in true arithmetic
• Circular proofs for the Gödel-Löb provability logic
• Title not available (Why is that?)
• Formalized meta-theory of sequent calculi for substructural logics
• Title not available (Why is that?)
• Cut-elimination for provability logic by terminating proof-search: formalised and deconstructed using Coq
• Formalized meta-theory of sequent calculi for linear logics
• Provability multilattice logic
• Sequent calculi for intuitionistic Gödel-Löb logic

This page was built for publication: Valentini's cut-elimination for provability logic resolved

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