A cut-free sequent system for Grzegorczyk logic, with an application to the Gödel-McKinsey-Tarski embedding

DOI10.1093/LOGCOM/EXT036MaRDI QIDQ2804325zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

intuitionistic logicmodal logicsequent calculusdecision proceduresprovability logicGrzegorczyk logiclabelled deduction

Mathematics Subject Classification ID

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)

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

Cited in

(9)

• Constructive embedding from extensions of logics of strict implication into modal logics
• Cut-elimination for weak Grzegorczyk logic Go
• NON-WELL-FOUNDED PROOFS FOR THE GRZEGORCZYK MODAL LOGIC
• Proofs and countermodels in non-classical logics
• Proof analysis in intermediate logics
• The Gödel-McKinsey-Tarski embedding for infinitary intuitionistic logic and its extensions
• scientific article; zbMATH DE number 4045717 (Why is no real title available?)
• Cut-elimination for the modal Grzegorczyk logic via non-well-founded proofs
• The intensional side of algebraic-topological representation theorems

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)