The Gödel-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.

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

Tesi, Matteo
;
Negri, Sara
2023

Abstract

The Gödel-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.
2023
Settore M-FIL/02 - Logica e Filosofia della Scienza
Proof theory; Infinitary logic; Modal embedding; Intuitionistic logic; Cut elimination
File in questo prodotto:
File Dimensione Formato  
1-s2.0-S0168007223000428-main.pdf

Accesso chiuso

Tipologia: Published version
Licenza: Non pubblico
Dimensione 576.83 kB
Formato Adobe PDF
576.83 kB Adobe PDF   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11384/131402
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 3
  • OpenAlex ND
social impact