Abstract
We present a uniform proof-theoretic proof of the Gödel–McKinsey–Tarski embedding for a class of first-order intuitionistic theories. This is achieved by adapting to the case of modal logic the methods of proof analysis in order to convert axioms into rules of inference of a suitable sequent calculus. The soundness and the faithfulness of the embedding are proved by induction on the height of the derivations in the augmented calculi. Finally, we define an extension of the modal system for which the result holds with respect to geometric intuitionistic.
Matteo Tesi
PostDoc Researcher
Matteo’s research focuses on non-classical (modal, intermediate, and substructural) logics, structural proof theory and their philosophical applications. He has worked with sequent calculi and their generalizations (hypersequents, nested sequents, and labelled sequents) to offer analytic presentations of families of non-classical logics.