uva.nl
ILLC

Master of Logic / ILLC

Submit Coordinated Project

2nd Semester 2017/18: Realizability Semantics for Intuitionistic Theories

Instructors

Andrew Swan

If you are interested in this project, please contact the instructor by email.

ECTS
6
Description

Realizability is the idea of using some notion of computation to provide semantics for intuitionistic logic. Taking the Brouwer-Heyting-Kolmogorov interpretation of logic as inspiration, to prove an existential formula, we really need to compute a witness, and to prove an implication A -> B, we need to provide a way to compute proofs of B from proofs of A. There are realizability models for many formal theories used as foundations for constructive mathematics, from first order arithmetic (HA) up to intuitionistic set theory (IZF). Moreover, there is a wide range of different kinds of realizability that give us many interesting metamathematical results about constructive mathematics.

In this project, students will first attend a short course and then carry out an individual project on a more advanced aspect of realizability. This will include both a written report and a presentation.

Topics for the individual project are suggested below:

  • Kleene's realizability for first order arithmetic
  • Function realizability
  • Realizability over Scott's graph model
  • q-realizability
  • Realizability over E-recursive functions
  • Lifschitz realizability
  • The effective topos
Organisation

The course will be in two parts. The first part will be a short lecture course (including example sheets). The second part will be an individual project. This will include both a written report and a presentation to other students.

Prerequisites

Some familiarity with mathematical logic (preferably intuitionistic) is required. Suitable ILLC courses are Mathematical Structures in Logic and Proof Theory.

Most individual projects will have extra prerequisites. Familiarity with computability theory/recursion theory is necessary for Kleene realizability and Lifschitz realizability. Familiarity with axiomatic set theory (preferably but not necessarily intuitionistic) is necessary for E-recursive functions. Contact the instructor for details ().

Assessment

Pass/fail, based on the report and presentation.

References

 

  • Beeson, Foundations of Constructive Mathematics

  • Troelstra and Van Dalen,  Constructivism in Mathematics (Vol 1 & 2)


Back