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

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

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)

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 (12)

• 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
• Title not available (Why is that?)
• Formalized meta-theory of sequent calculi for substructural logics
• Title not available (Why is that?)
• 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
• Valentini's cut-elimination for provability logic resolved

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)