An introduction to first-order modal logic. The course considers several modalities aside from the so-called alethic ones (necessity, possibility). Epistemic, temporal or deontic modalities are studied, as well as computationally motivated modals (like 'after the computation terminates'). Several conceptual problems in formal ontology that motivated the field are reviewed, as well as more recent applications in computer science and linguistics. Kripke models are used throughout the course, but we also study recent Kripkean-style systematizations of the modals without using possible worlds. Special attention is devoted to Scott-Montague models of the so-called 'classical' modalities.
