80-818 Seminar on Topics in Logic: Intuitionistic Logic

This is the course webpage for 80-818 Seminar on Topics in Logic: Intuitionistic Logic. This is still preliminary and subject to change. Contact me at andrewsw@andrew.cmu.edu for more information.

Syllabus

Below is a preliminary list of topics that I hope to cover in the course.

Lecture notes

  1. Introduction(revised 10/1/21)
  2. Heyting arithmetic(revised 9/8/21)
  3. Omniscience principles(revised 10/4/21)
  4. Heyting algebras and topology(revised 9/21/21)
  5. Heyting valued models(revised 10/4/21)
  6. Kripke models and formal topological models(revised 10/26/21)
  7. Heyting valued models of second order arithmetic(revised 10/5/21)
  8. Heyting valued models of arithmetic with finite types(revised 10/26/21)
  9. Independence of choice and omniscience principles over \(\mathbf{HA}_\omega\)(revised 10/26/21)
  10. Completeness and existence properties(revised 10/26/21)
  11. Partial combinatory algebras(revised 10/28/21)
  12. Realizability(revised 11/2/21)
  13. Kleene Realizability(revised 11/16/21)
  14. The second Kleene algebra and function realizability(updated 11/24/21)
  15. Realizability with truth

Exercise sheets

  1. Exercise sheet 1(updated 9/7/21) solutions
  2. Exercise sheet 2(updated 9/13/21) solutions
  3. Exercise sheet 3 solutions
  4. Exercise sheet 4(updated 9/28/21)
  5. Exercise sheet 5
  6. Exercise sheet 6
  7. Exercise sheet 7(updated 10/25/21)
  8. Exercise sheet 8
  9. Exercise sheet 9(updated 11/10/21)
  10. Exercise sheet 10

Individual projects

The list of final projects are below. Each project should consist of a written report and a 20 minute presentation explaining the ideas to the other students. The report should be enough to demonstrate that you have a solid understanding of the basic theory and the way that it can be used to prove some results about intuitionistic logic. I expect this to typically take less than 10 pages. The final project is used for 50% of the assessment. Projects are to be done individually and are assigned "first come, first served." If you have a specific topic or paper already in mind that is related to the course and want to study that instead of the suggestions below, you may be able use that for the final project. Contact me to check if it's suitable.

Realizability models of set theory

Just as with topological models, there are also realizability models for set theory. This project also focuses on intuitionistic Zermelo-Fraenkel, and constructive Zermelo-Fraenkel set theories. In each case we are careful to only use the axioms of each set theory in the metatheory where we are working. You will need to already have some familiarity with set theory from other courses for this project.

Recommended reading

Realizability with infinite time Turing machines

The definition of Turing machine can be modified to allow "infinite time" computations. These behave quite differently to ordinary Turing machines, and when used to define a pca give a very interesting realizability model. A key feature of the realizability model is the existence of an injective function from \(\mathbb{N}^\mathbb{N}\) to \(\mathbb{N}\). Although the paper below refers to some definitions in category theory, the main ideas are sufficiently close to definitions we have seen in class that very little prior knowledge of category theory will be needed. You should however, be confident in your understanding of Turing machines and basic computability theory.

Recommended reading

Lifschitz realizability

Lifschitz realizability is a modification of Kleene realizability that is similar in that it satisfies the version of Church's thesis we have seen in class, \(\mathbf{CT}_0 !\) which states that every function is computable. However, unlike Kleene realizability it does not satisfy the axiom of countable choice, and as a consequence does not satisfy another common formulation of Church's thesis called \(\mathbf{CT}_0\). Somewhat surprisingly the model satisfies the lessor limited principle of omniscience.

Goodman's Theorem

Goodman's theorem is a "conservativity" result. It states that we can the axiom of choice to \(\mathbf{HA}_\omega\) without adding any new theorems in the language of HA. It can be proved using a construction that combines forcing with realizability. I recommend focusing on a version of this proof due to Beeson that views this construction as a realizability model carried out internally in a forcing model.

Recommended reading

Realizability with the graph model

The Scott-Plotkin graph model is a pca that gives rise to some interesting realizability models that satisfy strong versions of the axiom of choice. This was used by Lietz and Streicher to give an example of a realizability model that falsifies a famous constructive axiom called \(\mathbf{BD}\text{-}\mathbb{N}\). Although the paper below refers to some definitions in category theory, the main ideas are sufficiently close to definitions we have seen in class that very little prior knowledge of category theory will be needed.

Recommended reading

No longer available projects

The following projects have already been assigned to students, and so are no longer available.

Topological models of set theory

In the course we have seen how to construct topological models of \(\mathbf{HAS}\) and \(\mathbf{HA}_\omega\). The aim of this project is to apply the same ideas to models of set theory. In particular you will look at two variants of Zermelo-Fraenkel set theory, intuitionistic Zermelo-Fraenkel, and constructive Zermelo-Fraenkel set theories. In each case we are careful to only use the axioms of each set theory in the metatheory where we are working. You will need to already have some familiarity with set theory from other courses for this project.

Recommended reading

Sheaf toposes and H-sets

For each complete Heyting algebra, H, the H-sets that we have seen in class are equivalent (as a category) to the category of sheaves on H. These are very famous examples of toposes and include many interesting examples. The aim of this project is to define sheaf toposes, show that they are toposes and are equivalent to the category of H-sets. You will need to already have some familiarity with category theory from other courses for this project.

Recommended reading

Realizability toposes

Realizability can be studied from a categorical point of view via realizability toposes. The first, and most famous example of this is Hyland's effective topos. However, just as for higher order arithmetic, one can construct a realizability topos for any pca. Many of the constructions we have seen in class can be seen as instances of more general constructions in topos theory. You will need to already have some familiarity with category theory from other courses for this project.

Recommended reading

Piazza

A page has been set up on Piazza for discussing the course. Find it at https://piazza.com/cmu/fall2021/80818/home

Further reading

Beeson, Foundations of Constructive Mathematics
Troelstra, Van Dalen, Constructivism in Mathematics, Volume II