Elementary realizability

Journal of Philosophical Logic 26 (3):311-339 (1997)
  Copy   BIBTEX

Abstract

A realizability notion that employs only Kalmar elementary functions is defined, and, relative to it, the soundness of EA-(Π₁⁰-IR), a fragment of Heyting Arithmetic (HA) with names and axioms for all elementary functions and induction rule restricted to Π₁⁰ formulae, is proved. As a corollary, it is proved that the provably recursive functions of EA-(Π₁⁰-IR) are precisely the elementary functions. Elementary realizability is proposed as a model of strict arithmetic constructivism, which allows only those constructive procedures for which the amount of computational resources required can be bounded in advance

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 93,069

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

Strictly primitive recursive realizability, I.Zlatan Damnjanovic - 1994 - Journal of Symbolic Logic 59 (4):1210-1227.
Polynomially Bounded Recursive Realizability.Saeed Salehi - 2005 - Notre Dame Journal of Formal Logic 46 (4):407-417.
Provably total functions of Basic Arithemtic.Saeed Salehi - 2003 - Mathematical Logic Quarterly 49 (3):316.
Lifschitz' realizability.Jaap van Oosten - 1990 - Journal of Symbolic Logic 55 (2):805-821.
Elementary descent recursion and proof theory.Harvey Friedman & Michael Sheard - 1995 - Annals of Pure and Applied Logic 71 (1):1-45.
Elementary Functions and LOOP Programs.Zlatan Damnjanovic - 1994 - Notre Dame Journal of Formal Logic 35 (4):496-522.
A Simple Proof of Parsons' Theorem.Fernando Ferreira - 2005 - Notre Dame Journal of Formal Logic 46 (1):83-91.

Analytics

Added to PP
2009-01-28

Downloads
96 (#184,359)

6 months
13 (#219,656)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Zlatan Damnjanovic
University of Southern California

Citations of this work

Polynomially Bounded Recursive Realizability.Saeed Salehi - 2005 - Notre Dame Journal of Formal Logic 46 (4):407-417.
Elementary Functions and LOOP Programs.Zlatan Damnjanovic - 1994 - Notre Dame Journal of Formal Logic 35 (4):496-522.

Add more citations

References found in this work

Introduction to metamathematics.Stephen Cole Kleene - 1952 - Groningen: P. Noordhoff N.V..
Constructivism in Mathematics: An Introduction.A. S. Troelstra & Dirk Van Dalen - 1988 - Amsterdam: North Holland. Edited by D. van Dalen.
Finitism.W. W. Tait - 1981 - Journal of Philosophy 78 (9):524-546.
Subrecursion: functions and hierarchies.H. E. Rose - 1984 - New York: Oxford University Press.

View all 13 references / Add more references