A Calculus of Realizers for EM_1 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, which we call EM_1-arithmetic. We interpret classical proofs as interactive learning strategies, namely as processes going through several stages of knowledge and learning by interacting with the "environment" and with each other. With respect to known constructive interpretations of classical arithmetic, the present one differs under many respects: for instance, the interpretation is compositional in a strict sense; in particular the interpretation of (the analogous of) the cut rule is the plain composition of functionals. As an additional remark, any two quantifier-free formulas provably equivalent in classical arithmetic have the same realizer.