Abstract

Classical first-order logic can be extended in two different ways to serve as a foundation for mathematics: introduce higher orders, type theory, or introduce sets. As it happens, both approaches have natural analogs for quantified modal logics, both approaches date from the 1960’s, one is not very well-known, and the other is well-known as something else. I will present the basic semantic ideas of both higher order intensional logic, and intensional set theory. Before doing so, I’ll quickly sketch some necessary background material from quantified modal logic. Except for standard material concerning propositional modal logics, the paper is essentially self-contained.