Table of Contents
Logic
Lecturer: 柯向上 HsiangShang Ko
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 metalanguage about the object language (especially by induction);
 the intimate connection between logic and computation.
Outline & slides

 Formal languages of propositional & firstorder logic
 The Brouwer–Heyting–Kolmogorov interpretation
 Natural deduction
 Heyting arithmetic
 Syntactic consistency and completeness

 Classical semantics of propositional & firstorder logic
 Soundness and semantic completeness
 Gödel–Gentzen negative translation (if time permits)

 Simply typed λcalculus with constants
 Proof normalisation
 Dependent types
Homework
 Homework 1 (due on Wednesday, 29 Aug 2012) sample solutions
 Homework 2 (due on Monday, 3 Sep 2012) sample solutions
References
 Mark van Atten. The development of intuitionistic logic. In Edward N. Zalta, editor, Stanford Encyclopedia of Philosophy.
 Dirk van Dalen. Logic and Structure. SpringerVerlag, fourth edition, 2004.
 Apostolos Doxiadis and Christos H. Papadimitriou. Logicomix: An Epic Search for Truth. Bloomsbury Publishing, 2009.
 JeanYves 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 MartinLöf. Intuitionistic Type Theory. Bibliopolis, Napoli, 1984.
 Per MartinLöf. Constructive mathematics and computer programming. In Philosophical Transactions of the Royal Society of London, 312(1522):501–518, 1984.
 Per MartinLö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 CurryHoward Isomorphism. Elsevier B.V., 2006.
 Richard Zach. Hilbert's Program. In Edward N. Zalta, editor, Stanford Encyclopedia of Philosophy.