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.

The code for this course, including the live code in lectures is available in the repository (the octocat on the top right corner also links to this).

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

At least 50% of the grade will be based on assignments and projects, which will be in Idris. Please e-mail your assignments to siddhartha.gadgil@gmail.com with "LTS2019" in the subject. The submissions will be added to the repository the day after the due date, and no late submissions will be accepted.

Recursion rules, due by Wed, 03 Apr 2019.
Odds and Evens, due by Thu, 24 Jan 2019.

Projects

Projects are to be submitted as pull requests on the repository. You will be graded based on total contribution to all the class projects, which can be based on my suggestions or your own ideas. My suggestions will be at the issue tracker of the repository and will be labelled as projects. You are welcome to comment on these and seek clarifications. You may also start a new issue with a project idea.

Suggested books

Edwin Brady, Type-Driven Development with Idris, Manning Publications.
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.
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

Instructor: Siddhartha Gadgil
E-mail: siddhartha.gadgil@gmail.com.
Office: N-15, Department of Mathematics.
Timing: Tuesday, Thursday 8:30 - 10:00 am.
Lecture Venue: LH-5, Department of Mathematics, IISc.
First Lecture: Thursday, January 3, 2019.
Course Email Group: lts2019@iisc.ac.in