Show The Graduate Center Menu

Modal Logic

Instructor: Distinguished Professor Sergei Artemov


Modal logic is a prominent and useful branch of logic which should be taught systematically.

Course Description

Modal logic originated in the domain of Philosophy, but during the past decades became a vibrant area with fundamental applications in computer science, AI, mathematics, epistemology, etc. This course offers a systematic exposition of fundamentals of modal logic together with an adjacent area of constructive reasoning.

Learning Goals/Outcomes

Students are expected to

  • understand the concepts of logical language, models, deduction and decidability.
  • apply these concepts to a variety of modal logics and related systems,
  • learn a wide variety of applications of modal logics in computer science, AI, mathematics and epistemology,
  • become prepared to conduct research in modal logics and their applications.

Mastering the following theoretical concepts:

  • Constructive reasoning and its proof semantics.
  • Intuitinistic logic, proof systems and Kripke semantics.
  • Semantics of realizability and computational content of constructive reasoning.
  • Classical modal logic, its alethic, epistemic, deontic and temporal motivations.
  • Possible world semantics, frame conditions.
  • Temporal logics and verification.
  • Proof systems for modal logics, canonical models.
  • Epistemic logic, common knowledge.
  • Goedel embeddings of intuitionistic logic into classical modal logic.
  • Modal logics of provability and explicit proofs, justification logics,
  • Knowability paradox and its resolution in bi-modal classical logic.
  • Constructive epistemic logic.


There will be manageable homework assignments expected to be prepared on weekly basis. The subjects will be clustered in three groups according to the learning goals 1-3, each accounts for 30% of the final grade. The attendance and participation will account for 10% of the final grade. Those who don't score the top grades for the homework clusters, will be offered a comprehensive test at the end of the course.