A constructive analysis of learning in Peano Arithmetic

We give a constructive analysis of learning as it arises in various computational interpretations of classical Peano Arithmetic, such as Aschieri and Berardi learning based realizability, Avigad’s update procedures and epsilon substitution method. In particular, we show how to compute in Gödel’s system upper bounds on the length of learning processes, which are themselves represented in through learning based realizability. The result is achieved by the introduction of a new non standard model of Gödel’s , whose new basic objects are pairs of non standard natural numbers (convergent sequences of natural numbers) and moduli of convergence, where the latter are objects giving constructive information about the former. As a foundational corollary, we obtain that that learning based realizability is a constructive interpretation of Heyting Arithmetic plus excluded middle over formulas (for which it was designed) and of all Peano Arithmetic when combined with Gödel’s double negation translation. As a byproduct of our approach, we also obtain a new proof of Avigad’s theorem for update procedures and thus of the termination of the epsilon substitution method for .