Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM1

We introduce a new notion of realizability for Heyting Arith- metic plus Excluded middle axiom restricted to §0 1 formulas (HA+EM1). Our work is based on the notion of atomic realizability introduced in [6] by Berardi and de'Liguoro for quanti¯er free primitive recursive Arithmetic plus EM1 and extends and adapts it in a non trivial way to full predicate logic. Our notion extends Kleene's realizability and differs from it only in the atomic case: we interpret atomic realizers as learning agents. We show how to extract realizers from classical proofs, and how they intuitionistically realize Pi-0-2 -formulas.