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

• Handouts.
• Glossary.
• Greek Alphabet.
• Homework for Lecture 1, solutions.
• Homework for Lecture 2, solutions.

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

• Homework for Lecture 3, solutions.

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

• Oxford University Computing Laboratory
  • MSc in Computer Science
  • MSc in Mathematics and the Foundations of Computer Science
• International Center for Computational Logic
  • Information for Prospective Students
  • How to apply