Realizability (or recursive realizability) was introduced by Kleene in 1945 as a method for giving computational interpretations of mathematical proofs, more specifically formal proofs carried out from Peano's axioms of arithmetic using intuitionistic logic. The method has since then been extended in various directions. For instance, set theory based on intuitionstic logic (IZF and CZF) can be given such interpretation. The method can also be extended to allow of extraction of other kinds information from proofs, such as estimates in mathematical analysis. This idea is exploited in so called proof mining where explicit bounds are obtained by performing formal interpretations of pure existence proofs.
Realizability techniques are also very important for establishing independence results for intuitionistic theories.
The course is suitable for students in mathematical logic, mathematics, computer science and philosophy with background knowledge in basic computability theory and some advanced courses in logic.
Topics will include
Lectures and course start: Mondays 15.00-16.45 in room 306, building 6, Kräftriket. First lecture January 16, 2017.
Lecturer: Prof. Erik Palmgren, Department of Mathematics, Stockholm University
January 14, 2017, Erik Palmgren. Email: palmgren (at) math (dot) su (dot) se