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.