Interactive Learning-Based Realizability for Heyting Arithmetic with EM1

Abstract. We define a constructive model for Delta-0-2 -maps, that is, maps recursively definable from a map deciding the halting problem. Our model refines existing constructive interpretation for classical reasoning over one-quantifier formulas: it is compositional (Modus Ponens is interpreted as an application) and semantical (rather than translating classical proofs into intuitionistic ones, we define a mathematical structure intuitionistically validating Excluded Middle for one-quantifier formulas).