Federico Aschieri (ENS, Lyon)

Interactive Realizability for classical Peano Arithmetic with Skolem axioms.

Abstract: In what sense classical mathematical proofs are constructive? What kind of constructions is it possible to extract from them? Most importantly, can we describe the behaviour of the extracted programs in a mathematically meaningful way?

In this talk, we present recent advancements on this topic. We shall introduce Interactive realizability, a computational semantics for classical Peano Arithmetic with Skolem choice axioms. A realizer represents a construction depending on a state of evolving knowledge. This state represents a portion of a model which the realizer is trying to construct in order to satisfy the instances of the excluded middle and Skolem axioms used in the proof. A realizer of a formula uses the information in the state in order to compute constructive information for the formula, i.e to provide a construction in the usual intuitionistic sense. The construction however may be falsified by interaction of the realizer with the environment. But the realizer is always able to turn such a negative outcome into a positive information, which consists in a new piece of knowledge that can be added to the state in order to improve it as potential model of Skolem axioms.

We then discuss the problem of efficiency of extracted programs, and to solve it we introduce a constructive version of Kripke-Cohen classical forcing semantics. We shall see that induces a new kind of state-continuation-passing-style translation, which is able to manipulate states; it corresponds to constructive forcing as the usual CPS translation corresponds to negative translations.