Elementary Logic

Focusing on propositional logic, leaving quantification to MLTT. It would be easier to have some intuition from FP (e.g., pattern matching and induction); also it is strongly desirable to let the students see some concrete examples of proofs (beforehand, probably also in FP).


  • Intuitionistic logic (1 unit)
  • Classical logic (1 unit)
    • Two-value semantics
    • Consistency
    • Soundness and (in-)completeness
    • Double-negation translation (Glivenko’s Theorem)

Course Materials