Journal of Symbolic Logic 60 (4):1208-1241 (1995)

Zlatan Damnjanovic
University of Southern California
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 derived
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2307/2275884
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 63,375
Through your library

References found in this work BETA

Introduction to Metamathematics.Ann Singleterry Ferebee - 1968 - Journal of Symbolic Logic 33 (2):290-291.
Mathematical Logic.Donald Monk - 1975 - Journal of Symbolic Logic 40 (2):234-236.
A Classification of the Ordinal Recursive Functions.S. S. Wainer - 1970 - Archive for Mathematical Logic 13 (3-4):136-153.

Add more references

Citations of this work BETA

Elementary Realizability.Zlatan Damnjanovic - 1997 - Journal of Philosophical Logic 26 (3):311-339.
Polynomially Bounded Recursive Realizability.Saeed Salehi - 2005 - Notre Dame Journal of Formal Logic 46 (4):407-417.

Add more citations

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.
Elementary Realizability.Zlatan Damnjanovic - 1997 - Journal of Philosophical Logic 26 (3):311-339.


Added to PP index

Total views
223 ( #44,952 of 2,448,908 )

Recent downloads (6 months)
1 ( #443,144 of 2,448,908 )

How can I increase my downloads?


My notes