## Realizability: computational interpretations of logic 7.5 cp

- a PhD level course in mathematics, Spring 2017

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

- Kleene realizability
- Partial combinatory algebras and general realizability
- Modified realizability - realizing with typed lambda calculus
- The Dialectica interpretation
- The effective topos
- Extraction of algorithms from classical proofs
- Proof mining

Course plan: See http://staff.math.su.se/palmgren/Realizability_plan.pdf.
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