Valentini's cut-elimination for provability logic resolved

DOI10.1017/S1755020311000323MaRDI QIDQ2890695zbMATH OpenOpenAlexFDO

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

(17)

• A proof theory for the logic of provability in true arithmetic
• Circular proofs for the Gödel-Löb provability logic
• Generic methods for formalising sequent calculi applied to provability logic
• scientific article; zbMATH DE number 7243672 (Why is no real title available?)
• Formalized meta-theory of sequent calculi for substructural logics
• scientific article; zbMATH DE number 7668109 (Why is no real title available?)
• The modal logic of provability: cut-elimination
• 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
• Analytic proofs for tense logic
• Cut-free sequent calculi for the provability logic D
• Unifying sequent systems for Gödel-Löb provability logic via syntactic transformations
• Valentini's cut-elimination for provability logic resolved
• Syntactic cut-elimination for provability logic GL via nested sequents
• Facilitating meta-theory reasoning (invited paper)

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)