Limits of first-order definability, syntax and semantics of second-order logic, expressive power of second-order logic, second-order arithmetic, simple type theory, typed lambda calculi, interactive theorem proving in higher-order logic
First meeting: Tuesday, 25 April 2017, 14:00, seminar room "Gödel".
In the first meeting I will give a brief overview of the course and discuss administrative and assessment details. The first lecture will be on Thursday, 27 April 2017, 14:00, seminar room "Gödel".
- Stefan Hetzl: Higher-order logic. Lecture notes.*main reference*
- Stefan Hetzl: Mathematical Logic 2. Lecture notes.*Prerequisite material on first-order logic*
- Johan Van Benthem and Kees Doets. Higher-order logic. Book chapter. Handbook of Philosophical Logic. Vol. 164, pages 275-329.*
- Daniel Leivant: Higher-order Logic, Handbook of Logic in Artificial Intelligence and Logic Programming (2) 1994, pages 229-322.*
- Peter B. Andrews: An Introduction to Mathematical Logic and Type Theory: To Truth through Proof, Academic Press, 1986
- Dale Miller and Gopalan Nadathur: Programming with Higher-Order Logic, Cambridge University Press, 2012
- Chad E. Brown: Automated Reasoning in Higher-Order Logic, College Publications, 2007
- Henk Barendregt, Wil Dekkers and Richard Statman: Lambda Calculus with Types, 2013
- Manzano: Extensions of first-order logic, 1996.
- M.H. Sorensen and P. Urzyczyn: Lectures on the Curry-Howard Isomorphism, 2006
This is an advanced course in logic. Firm knowledge of classical first-order logic (formulas, models, proofs) is a prerequisite. In the first lecture I will overview the key concepts and definitions from first-order logic.