Computability and Logic

Course Description

Summary

In 1936, Alan Turing wrote a paper that invented computer science. Not a piece of computer science, not a contribution to it. The whole thing. “On Computable Numbers, with an Application to the Entscheidungsproblem” asked a question that nobody had thought to formalize: what does it mean to compute something? And in answering it, Turing proved something that most people find shocking.

We often think of mathematical progress as finding procedures. When you were young, you learned a procedure to subtract one number from another. Later, maybe you learned one to solve a quadratic equation. What Turing showed is that there is a large class of mathematical problems for which no procedure exists. Not that we haven’t found one yet. That none will ever be found. And he proved it.

His proof is the centerpiece of this course. Understanding it will require you to think carefully and abstractly, and to sit with ideas that feel strange at first. You’ll need comfort with basic mathematical concepts like powers and roots, but the real prerequisite is perseverance. Turing’s proof lies at the intersection of formal logic and theoretical computer science, and it settled one of the fundamental questions in the foundations of mathematics.

This is not a typical course in computer science or in formal logic, but you will learn a lot about both.