Minimal realizability of intuitionistic arithmetic and elementary analysis

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

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 derived

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,991

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

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.
Strictly primitive recursive realizability, I.Zlatan Damnjanovic - 1994 - Journal of Symbolic Logic 59 (4):1210-1227.
Provably total functions of Basic Arithemtic.Saeed Salehi - 2003 - Mathematical Logic Quarterly 49 (3):316.
Tennenbaum's Theorem and Unary Functions.Sakae Yaegasi - 2008 - Notre Dame Journal of Formal Logic 49 (2):177-183.
On the contrapositive of countable choice.Hajime Ishihara & Peter Schuster - 2011 - Archive for Mathematical Logic 50 (1-2):137-143.
Elementary descent recursion and proof theory.Harvey Friedman & Michael Sheard - 1995 - Annals of Pure and Applied Logic 71 (1):1-45.
Extracting Algorithms from Intuitionistic Proofs.Fernando Ferreira & António Marques - 1998 - Mathematical Logic Quarterly 44 (2):143-160.

Analytics

Added to PP
2009-01-28

Downloads
272 (#77,501)

6 months
33 (#105,010)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Zlatan Damnjanovic
University of Southern California

Citations of this work

Provably total functions of Basic Arithemtic.Saeed Salehi - 2003 - Mathematical Logic Quarterly 49 (3):316.
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