Minimal realizability of intuitionistic arithmetic and elementary analysis

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

Our Archive

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

References found in this work BETA

Introduction to Metamathematics.Stephen Cole Kleene - 1968 - Journal of Symbolic Logic 33 (2):290-291.
Mathematical Logic.Joseph R. Shoenfield - 1975 - Journal of Symbolic Logic 40 (2):234-236.

Add more references

Citations of this work BETA

Elementary Realizability.Zlatan Damnjanovic - 1997 - Journal of Philosophical Logic 26 (3):311-339.

Add more citations

Similar books and articles

A Realizability Interpretation for Classical Arithmetic.Jeremy Avigad - 2002 - Bulletin of Symbolic Logic 8 (3):439-440.
On the No-Counterexample Interpretation.Ulrich Kohlenbach - 1999 - Journal of Symbolic Logic 64 (4):1491-1511.
Models of Intuitionistic TT and N.Daniel Dzierzgowski - 1995 - Journal of Symbolic Logic 60 (2):640-653.
A New "Feasible" Arithmetic.Stephen Bellantoni & Martin Hofmann - 2002 - Journal of Symbolic Logic 67 (1):104-116.
Church's Thesis, Continuity, and Set Theory.M. Beeson & A. Ščedrov - 1984 - Journal of Symbolic Logic 49 (2):630-643.
Strictly Primitive Recursive Realizability, I.Zlatan Damnjanovic - 1994 - Journal of Symbolic Logic 59 (4):1210-1227.
Elementary Realizability.Zlatan Damnjanovic - 1997 - Journal of Philosophical Logic 26 (3):311-339.


Added to PP index

Total views
208 ( #30,496 of 2,237,224 )

Recent downloads (6 months)
3 ( #601,414 of 2,237,224 )

How can I increase my downloads?


My notes

Sign in to use this feature