A constructive analysis of learning in Peano Arithmetic

作者：Aschieri Federico^*

来源：Annals of Pure and Applied Logic, 2012, 163(11): 1448-1470.

DOI：10.1016/j.apal.2011.12.004

• Learning based realizability
• Classical arithmetic
• Update procedures
• Epsilon substitution method
• Constructive termination proof

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%26apos;s update procedures and epsilon substitution method. in particular, we show how to compute in Godes system T upper bounds on the length of learning processes, which are themselves represented in T through learning based realizability. The result is achieved by the introduction of a new non standard model of Coders T, 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 Sigma(0)(1) formulas (for which it was designed) and of all Peano Arithmetic when combined with Godel%26apos;s double negation translation. As a byproduct of our approach, we also obtain a new proof of Avigad%26apos;s theorem for update procedures and thus of the termination of the epsilon substitution method for PA.

• 出版日期2012-11