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

DOI10.1093/logcom/ext036zbMath1444.03170OpenAlexW2132979411MaRDI QIDQ2804325

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

modal logicsequent calculusintuitionistic logicprovability logicdecision proceduresGrzegorczyk logiclabelled deduction

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05) Proof theory in general (including proof-theoretic semantics) (03F03) Provability logics and related algebras (e.g., diagonalizable algebras) (03F45)

Related Items

The Gödel-McKinsey-Tarski embedding for infinitary intuitionistic logic and its extensions, The intensional side of algebraic-topological representation theorems, Proof analysis in intermediate logics, Proofs and countermodels in non-classical logics, NON-WELL-FOUNDED PROOFS FOR THE GRZEGORCZYK MODAL LOGIC