Valentini's cut-elimination for provability logic resolved

DOI10.1017/S1755020311000323zbMATH Open1254.03113OpenAlexW2102143997MaRDI QIDQ2890695FDOQ2890695

Authors Rajeev Goré, Revantha Ramanayake

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 GLsyntactical cut eliminationLöb axiom

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)

Recommendations

• Valentini's cut-elimination for provability logic resolved
• The modal logic of provability: cut-elimination
• Cut elimination for GLS using the terminability of its regress process
• scientific article; zbMATH DE number 7668109
• On some proof theoretical properties of the modal logic GL

Cites work

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

Cited in

(12)

• Cut-elimination for provability logic by terminating proof-search: formalised and deconstructed using Coq
• Sequent calculi for intuitionistic Gödel-Löb logic
• scientific article; zbMATH DE number 7668109 (Why is no real title available?)
• Formalized meta-theory of sequent calculi for linear logics
• Generic methods for formalising sequent calculi applied to provability logic
• Valentini's cut-elimination for provability logic resolved
• The modal logic of provability: cut-elimination
• Formalized meta-theory of sequent calculi for substructural logics
• Circular proofs for the Gödel-Löb provability logic
• A proof theory for the logic of provability in true arithmetic
• Provability multilattice logic
• scientific article; zbMATH DE number 7243672 (Why is no real title available?)

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)