We report on work in progress concerning the investigation of a semantics of proofs for intuitionistic modal logic. Starting from a few observations about Martini and Masini's work on a two-dimensional generalization of natural deduction we argue that models of the basic modal logic K can be regarded as simple fibrations, i.e. as an instance of a very general categorical semantics for intuitionistic propositional logic. Having such an account of modal proofs provides a good starting point for the investigation of the relationship between the various proof-theoretical approaches to modal logic
Strada le Grazie 15
37134 Verona
Partita IVA01541040232
Codice Fiscale93009870234
© 2025 | Università degli studi di Verona
******** CSS e script comuni siti DOL - frase 9957 ********