The Gödel-McKinsey-Tarski embedding for infinitary intuitionistic logic and its extensions

DOI10.1016/J.APAL.2023.103285MaRDI QIDQ6156417FDOQ6156417

Authors: Matteo Tesi, Sara Negri 

Publication date: 13 June 2023

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

zbMATH Keywords

proof theoryintuitionistic logiccut eliminationinfinitary logicmodal embedding

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) Structure of proofs (03F07)

Cites Work

• Cut Elimination in the Presence of Axioms
• Title not available (Why is that?)
• Constructivism in mathematics. An introduction. Volume I
• An introduction to non-classical logic. From if to is
• Glivenko sequent classes in the light of structural proof theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• Some theorems about the sentential calculi of Lewis and Heyting
• Proof analysis in modal logic
• Geometric Rules in Infinitary Logic
• Proof analysis in intermediate logics
• Title not available (Why is that?)
• Does the deduction theorem fail for modal logic?
• Neighborhood semantics for modal logic
• Infinitary intuitionistic logic from a classical point of view
• A cut-free sequent system for Grzegorczyk logic, with an application to the Gödel-McKinsey-Tarski embedding
• Some remarks on the proof-theory and the semantics of infinitary modal logic
• Non-normal modal logics: bi-neighbourhood semantics and its labelled calculi
• Duality for \(\kappa\)-additive complete atomic modal algebras
• From axioms to synthetic inference rules via focusing
• Neighborhood Semantics for Basic and Intuitionistic Logic
• Infinitary propositional intuitionistic logic
• On Glinvenko sequent classes
• Neighbourhood semantics and labelled calculus for intuitionistic infinitary logic
• Remarks on Barr's theorem: proofs in geometric theories

Cited In (4)

• Infinitary logic with infinite sequents: syntactic investigations
• Iterated elementary embeddings and the model theory of infinitary logic
• Subintuitionistic logics and their modal companions: a nested approach
• Embeddings into Free Heyting Algebras and Translations into Intuitionistic Propositional Logic

This page was built for publication: The Gödel-McKinsey-Tarski embedding for infinitary intuitionistic logic and its extensions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6156417)