A Calculus of Realizers for EM1-Arithmetic

We propose a realizability interpretation of a system for quantifier free arithmetic which is equivalent to the fragment of classical arithmetic without nested quantifiers, we call EM1-arithmetic. With respect to known constructive interpretations of classical arithmetic, the present one differs under two respects: first it interprets classical proofs as interactive learning strategies, namely as processes going through several stages of knowledge and learning by interacting with the "environment". Second, the interpretation is compositional in a strict sense; in particular the interpretation of (the analogous of) the cut rule is plain composition of functionals. As an additional remark, any two quantifier free formulas provably equivalent in classical arithmetic have the same realizers.