Table of Contents

Instructor: Max Schaefer

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

None

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

*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.

- M. Sørensen and P. Urzyczyn: Lectures on the Curry-Howard Isomorphism
- G. Restall: Proof Theory and Philosophy
- H. Barendregt: Lambda Calculi with Types
- B. Nordström, K. Petersson, J. M. Smith: Programming in Martin-Löf's Type Theory
- J.-Y. Girard, Y. Lafont, P. Taylor: Proofs and Types