A constructive analysis of learning in Peano Arithmetic

Annals of Pure and Applied Logic 163 (11):1448-1470 (2012)
  Copy   BIBTEX

Abstract

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 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 Gödel’s T, whose new basic objects are pairs of non standard 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 Σ10 formulas 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 PA

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 101,505

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Analytics

Added to PP
2013-10-27

Downloads
38 (#595,594)

6 months
12 (#302,973)

Historical graph of downloads
How can I increase my downloads?

References found in this work

Interpretation of analysis by means of constructive functionals of finite types.Georg Kreisel - 1959 - In A. Heyting (ed.), Constructivity in mathematics. Amsterdam,: North-Holland Pub. Co.. pp. 101--128.
Update Procedures and the 1-Consistency of Arithmetic.Jeremy Avigad - 2002 - Mathematical Logic Quarterly 48 (1):3-13.
On bar recursion of types 0 and 1.Helmut Schwichtenberg - 1979 - Journal of Symbolic Logic 44 (3):325-329.

Add more references