Minimal realizability of intuitionistic arithmetic and elementary analysis
Journal of Symbolic Logic 60 (4):1208-1241 (1995)
Abstract
A new method of "minimal" realizability is proposed and applied to show that the definable functions of Heyting arithmetic (HA)--functions f such that HA $\vdash \forall x\exists!yA(x, y)\Rightarrow$ for all m, A(m, f(m)) is true, where A(x, y) may be an arbitrary formula of L(HA) with only x, y free--are precisely the provably recursive functions of the classical Peano arithmetic (PA), i.e., the $ -recursive functions. It is proved that, for prenex sentences provable in HA, Skolem functions may always be chosen to be $ -recursive. The method is extended to intuitionistic finite-type arithmetic, HA ω 0 , and elementary analysis. Generalized forms of Kreisel's characterization of the provably recursive functions of PA and of the no-counterexample-interpretation for PA are consequently derivedAuthor's Profile
DOI
10.2307/2275884
My notes
Similar books and articles
A Realizability Interpretation for Classical Arithmetic.Jeremy Avigad - 2002 - Bulletin of Symbolic Logic 8 (3):439-440.
Strictly primitive recursive realizability, I.Zlatan Damnjanovic - 1994 - Journal of Symbolic Logic 59 (4):1210-1227.
Church's thesis, continuity, and set theory.M. Beeson & A. Ščedrov - 1984 - Journal of Symbolic Logic 49 (2):630-643.
A new "feasible" arithmetic.Stephen Bellantoni & Martin Hofmann - 2002 - Journal of Symbolic Logic 67 (1):104-116.
Models of intuitionistic TT and N.Daniel Dzierzgowski - 1995 - Journal of Symbolic Logic 60 (2):640-653.
On the no-counterexample interpretation.Ulrich Kohlenbach - 1999 - Journal of Symbolic Logic 64 (4):1491-1511.
Analytics
Added to PP
2009-01-28
Downloads
225 (#55,967)
6 months
2 (#298,443)
2009-01-28
Downloads
225 (#55,967)
6 months
2 (#298,443)
Historical graph of downloads
Author's Profile
Citations of this work
Polynomially Bounded Recursive Realizability.Saeed Salehi - 2005 - Notre Dame Journal of Formal Logic 46 (4):407-417.
References found in this work
Introduction to Metamathematics.Ann Singleterry Ferebee - 1968 - Journal of Symbolic Logic 33 (2):290-291.
A classification of the ordinal recursive functions.S. S. Wainer - 1970 - Archive for Mathematical Logic 13 (3-4):136-153.