Computability and Constructive Mathematics (advanced level 7.5 hp)
Course code and home page
Stockholm University course code: MM8026
Home page (Spring 2014)
Overall motivation and description
This course first addresses the fundamental question: what is computable - in principle - by a computer or a human being? It does so by studying different mathematical models of computers, which are idealized in the sense that there is no limit on time or memory that can be used for a given task. It turns out that many mathematical questions can not be decided even by such ideal computers, or Turing machines. In the course we study the Halting Problem which is one such question, but also undecidable problems from other parts of mathematics (group theory, number theory ...). Computability theory deals with general questions on the relation between computable and non-computable functions, and lays the foundations for further study in complexity theory and other areas of theoretical computer science.
Secondly, the course deals with a general method to ensure computable results in mathematics. The area of constructive mathematics (initiated by L.E.J. Brouwer and Errett Bishop and others during the last century) addresses this issue, by carefully choosing the basic axioms and avoiding the use of non-constructive logical reasoning. The result of this logical discipline (intuitionistic logic) is that existence gets a stronger meaning than in classical mathematics: to claim that a mathematical object exists, we must show that it may (in principle) be constructed by a finite routine. We then connect these intuitionistic systems to computability via so-called recursive realizability, which enables us to extract programs from constructive proofs that compute mathematical objects that are claimed to exists, for instance a converging sequence representing a real number as solution to an equation.
Aim of the course
After completing the course the student is expected to be able to explain and prove theorems in computability theory, and establish (un)decidability of problems in mathematics. Moreover the student should be able to explain the fundamentals of, and use the theory of constructive proofs and make such proofs in any area of mathematics.
Erik Palmgren, January 10, 2014