A cut-free sequent system for Grzegorczyk logic, with an application to the Gödel-McKinsey-Tarski embedding
DOI10.1093/LOGCOM/EXT036zbMATH Open1444.03170OpenAlexW2132979411MaRDI QIDQ2804325FDOQ2804325
Authors: Roy Dyckhoff, Sara Negri 
Publication date: 28 April 2016
Published in: Journal of Logic and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1093/logcom/ext036
Recommendations
- Cut-elimination for the modal Grzegorczyk logic via non-well-founded proofs
- Proof analysis in intermediate logics
- Constructive embedding from extensions of logics of strict implication into modal logics
- DECIDABILITY OF ADMISSIBILITY IN THE MODAL SYSTEM Grz AND IN INTUITIONISTIC LOGIC
- Problems of substitution and admissibility in the modal system Grz and in intuitionistic propositional calculus
intuitionistic logicmodal logicsequent calculusdecision proceduresprovability logicGrzegorczyk logiclabelled deduction
Modal logic (including the logic of norms) (03B45) Proof theory in general (including proof-theoretic semantics) (03F03) Cut-elimination and normal-form theorems (03F05) Provability logics and related algebras (e.g., diagonalizable algebras) (03F45)
Cited In (9)
- Cut-elimination for weak Grzegorczyk logic Go
- NON-WELL-FOUNDED PROOFS FOR THE GRZEGORCZYK MODAL LOGIC
- Proofs and countermodels in non-classical logics
- The Gödel-McKinsey-Tarski embedding for infinitary intuitionistic logic and its extensions
- Proof analysis in intermediate logics
- Title not available (Why is that?)
- Cut-elimination for the modal Grzegorczyk logic via non-well-founded proofs
- The intensional side of algebraic-topological representation theorems
- Constructive embedding from extensions of logics of strict implication into modal logics
This page was built for publication: A cut-free sequent system for Grzegorczyk logic, with an application to the Gödel-McKinsey-Tarski embedding
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2804325)
