Notes on Gödel’s and Scott’s variants of the ontological argument - Monatshefte für Mathematik

Notes on Kurt Gödel’s modal ontological argument and Dana Scott’s variant of it are presented. These remarks, supported by experimental studies with a proof assistant system for classical higher-order logic, implicitly answer some questions the authors have received over the last decade(s). In addition, some new insights resulting from the conducted experiments are reported.

Contextual modal type theory | ACM Transactions on Computational Logic

The intuitionistic modal logic of necessity is based on the judgmental notion of categorical truth. In this article we investigate the consequences of relativizing these concepts to explicitly specified contexts. We obtain contextual modal logic and its ...

AiML: Volume 11

The Many Worlds of Modal λ-calculi: I. Curry-Howard for Necessity, Possibility and Time

This is a survey of λ-calculi that, through the Curry-Howard isomorphism, correspond to constructive modal logics. We cover the prehistory of the subject and then concentrate on the developments that took place in the 1990s and early 2000s. We discuss logical aspects, modal λ-calculi, and their categorical semantics. The logics underlying the calculi surveyed are constructive versions of K, K4, S4, and LTL.

AiML: Volume 4