Logic

Introduction to formal logic, with a bias towards proof theory. Highlights of this course:

the use of formal languages to represent reasoning patterns;
reasoning in the meta-language about the object language (especially by induction);
the intimate connection between logic and computation.

Outline & slides

Intuitionistic logic
- Formal languages of propositional & first-order logic
- The Brouwer–Heyting–Kolmogorov interpretation
- Natural deduction
- Heyting arithmetic
- Syntactic consistency and completeness
Classical logic
- Classical semantics of propositional & first-order logic
- Soundness and semantic completeness
- Gödel–Gentzen negative translation (if time permits)
Curry–Howard correspondence
- Simply typed λ-calculus with constants
- Proof normalisation
- Dependent types

Mark van Atten. The development of intuitionistic logic. In Edward N. Zalta, editor, Stanford Encyclopedia of Philosophy.
Dirk van Dalen. Logic and Structure. Springer-Verlag, fourth edition, 2004.
Apostolos Doxiadis and Christos H. Papadimitriou. Logicomix: An Epic Search for Truth. Bloomsbury Publishing, 2009.
Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types. Cambridge University Press, 1989.
Robert Harper. Practical Foundations for Programming Languages. Working draft, 2012.
Stephen Cole Kleene. Introduction to Metamathematics. Elsevier B.V., 1952.
Leslie Lamport. How to Write a 21st Century Proof. To appear in Journal of Fixed Point Theory and Applications.
Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Napoli, 1984.
Per Martin-Löf. Constructive mathematics and computer programming. In Philosophical Transactions of the Royal Society of London, 312(1522):501–518, 1984.
Per Martin-Löf. Truth of a Proposition, evidence of a judgement, validity of a proof. In Synthese, 73(3):407–420, 1987.
Morten Heine Sørensen and Paweł Urzyczyn. Lectures on the Curry-Howard Isomorphism. Elsevier B.V., 2006.
Richard Zach. Hilbert's Program. In Edward N. Zalta, editor, Stanford Encyclopedia of Philosophy.