The Godel-McKinsey-Tarski embedding for infinitary intuitionistic logic and its extensions

The Godel-McKinsey-Tarski embedding allows to view intuitionistic logic through the lenses of modal logic. In this work, an extension of the modal embedding to infinitary intuitionistic logic is introduced. First, a neighborhood semantics for a family of axiomatically presented infinitary modal logics is given and soundness and completeness are proved via the method of canonical models. The semantics is then exploited to obtain a labelled sequent calculus with good structural properties. Next, soundness and faithfulness of the embedding are established by transfinite induction on the height of derivations: the proof is obtained directly without resorting to non-constructive principles. Finally, the modal embedding is employed in order to relate classical, intuitionistic and modal derivability in infinitary logic extended with axioms.& COPY; 2023 Elsevier B.V. All rights reserved.

Automated summary

The Godel-McKinsey-Tarski embedding allows for a modal logic interpretation of intuitionistic logic. In this paper, an extension of the modal embedding to infinitary intuitionistic logic is introduced. The paper presents a neighborhood semantics for a family of axiomatically presented infinitary modal logics and proves soundness and completeness using canonical models. The paper also establishes the soundness and faithfulness of the embedding and employs it to relate classical, intuitionistic, and modal derivability in infinitary logic extended with axioms. ©2023 Elsevier B.V. All rights reserved.