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/proof assistant Agda. Connections with programming in functional languages will be explored.
Suggested books :
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
.