MA 210: Logic, Types and Spaces

Course Syllabus

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.
  • Church-Turing unsolvability 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 and the use of dependent type theory to integrate computations and proofs will be explored.

Aims, Background etc

The main aim of this course is to give a self-contained exposition of the (topological) foundations of mathematics and computation known as Homotopy Type Theory. These are foundations that are close to real-life mathematics, allow an integration of programs and proofs, and have deep connection with .

The only background assumed is some basic mathematics, in particular being comfortable with proofs and with the concept of continuity (at least over real numbers). Some familiarity with programming will be helpful, but mainly a willingness to learn and write code. In particular no familiarity with Idris or functional programming, or with formal logic, is assumed.

Note that the topic of this course is not a mature subject. In particular there is no book at this level. This will require some maturity and open-mindedness from the students.

To get a head-start on the course, I recommend installing Idris. Using Idris is pleasant, but installation can be painful. On Windows, I suggest using the binary on that page. If you are using linux, you may find this answer helpful (i.e., use stack). You may also wish to get familiar with the version control system git.

Assignments and Projects

At least 50% of the grade will be based on assignments and projects, which will be in Idris. More details will be posted as the course gets underway.

Suggested books

  1. Edwin Brady, Type-Driven Development with Idris, Manning Publications.
  2. Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Studies, Princeton 2013; available at http://homotopytypetheory.org/book/.
  3. Manin, Yu. I., A Course in Mathematical Logic for Mathematicians, Second Edition ,Graduate Texts in Mathematics, Springer-Verlag, 2010.
  4. Srivastava, S. M., A Course on Mathematical Logic, Universitext, Springer-Verlag, 2008.
  5. Abelson, Sussman and Sussman, Structure and Interpretation of Computer Programs, MIT Press, available at https://mitpress.mit.edu/sites/default/files/sicp/index.html.

Course Details

Upcoming Assignments

Announcements