MA 210: Logic, Types and Spaces
Credits: 3:0
Pre-requisites :
- No prior knowledge of logic is assumed.
- Some background in algebra and topology will be assumed.
- It will be useful to have some familiarity with programming.
This course is an introduction to logic and foundations from both a modern point of view (based on type theory and its relations to topology) as well as in the traditional formulation based on first-order logic.
Topics:
- Basic type theory: terms and types, function types, dependent types, inductive types.
- First order logic: First order languages, deduction and truth, Models, Godel’s completeness and compactness theorems.
- Godel’s incompleteness theorem
- Homotopy Type Theory: propositions as types, the identity type family, topological view of the identity type, foundations of homotopy type theory.
- Most of the material will be developed using the dependently typed language Idris. Connections with programming in functional languages will be explored.
Suggested books and references:
- Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Studies, Princeton 2013; available at http://homotopytypetheory.org/book/.
- Manin, Yu. I., A Course in Mathematical Logic for Mathematicians, Second Edition, Graduate Texts in Mathematics, Springer-Verlag, 2010.
- Srivastava, S. M., A Course on Mathematical Logic, Universitext, Springer-Verlag, 2008