Minimal realizability of intuitionistic arithmetic and elementary analysis

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


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



    Upload a copy of this work     Papers currently archived: 79,826

External links

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

Through your library

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

227 (#60,541)

6 months
3 (#242,620)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Zlatan Damnjanovic
University of Southern California

Citations of this work

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

References found in this work

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