Instructor: Max Schaefer

This lecture aims to provide students with the logical background knowledge needed to understand and appreciate the other lectures.




  • Classical logic (propositional, first order) and its semantics
  • Intuitionistic logic (propositional, first order), natural deduction, basic proof theory
  • The Curry-Howard isomorphism

Course Materials

Hint: If you're having trouble with Exercise 3.2, try showing (φ → φ ∨ ψ) → (ψ → φ ∨ ψ) → φ ∨ ψ ⊢ φ ∨ ψ first. For this, it may in turn be helpful to consider ⊢ φ → φ ∨ ψ and ⊢ ψ → φ ∨ ψ.


You can use NJEdit to construct derivations in natural deduction. Currently, NJEdit is only tested with Firefox, Opera, and Safari; it does not work with Internet Explorer, as demonstrated during the tutorial.



logic.txt · Last modified: 2008/07/13 17:57 by xiemaisi
Recent changes RSS feed Creative Commons License Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki