Extracting Algorithms from Intuitionistic Proofs

&
Mathematical Logic Quarterly 44 (2):143-160 (1998)
  Copy   BIBTEX

Abstract

This paper presents a new method - which does not rely on the cut-elimination theorem - for characterizing the provably total functions of certain intuitionistic subsystems of arithmetic. The new method hinges on a realizability argument within an infinitary language. We illustrate the method for the intuitionistic counterpart of Buss's theory Smath image, and we briefly sketch it for the other levels of bounded arithmetic and for the theory IΣ1.

Categories

Keywords

Reprint years

DOI

10.1002/malq.19980440202

Links

PhilArchive



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

External links

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

Through your library

My notes

Similar books and articles

Polynomially Bounded Recursive Realizability.Saeed Salehi - 2005 - Notre Dame Journal of Formal Logic 46 (4):407-417.
Provably total functions of intuitionistic bounded arithmetic.Victor Harnik - 1992 - Journal of Symbolic Logic 57 (2):466-477.
Two General Results on Intuitionistic Bounded Theories.Fernando Ferreira - 1999 - Mathematical Logic Quarterly 45 (3):399-407.
Provably recursive functions of constructive and relatively constructive theories.Morteza Moniri - 2010 - Archive for Mathematical Logic 49 (3):291-300.
Minimal realizability of intuitionistic arithmetic and elementary analysis.Zlatan Damnjanovic - 1995 - Journal of Symbolic Logic 60 (4):1208-1241.
A feasible theory for analysis.Fernando Ferreira - 1994 - Journal of Symbolic Logic 59 (3):1001-1011.
Generalized quantifier and a bounded arithmetic theory for LOGCFL.Satoru Kuroda - 2007 - Archive for Mathematical Logic 46 (5-6):489-516.
Preservation theorems for bounded formulas.Morteza Moniri - 2007 - Archive for Mathematical Logic 46 (1):9-14.
The function \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document} $\lfloor a/m\rfloor$\end{document} in sharply bounded arithmetic. [REVIEW]Mitsuru Tada & Makoto Tatsuta - 1997 - Archive for Mathematical Logic 37 (1):51-57.
Provably total functions of Basic Arithemtic.Saeed Salehi - 2003 - Mathematical Logic Quarterly 49 (3):316.
Classical arithmetic as part of intuitionistic arithmetic.Michael Potter - 1998 - Grazer Philosophische Studien 55 (1):127-41.
Elementary realizability.Zlatan Damnjanovic - 1997 - Journal of Philosophical Logic 26 (3):311-339.
The provably total NP search problems of weak second order bounded arithmetic.Leszek Aleksander Kołodziejczyk, Phuong Nguyen & Neil Thapen - 2011 - Annals of Pure and Applied Logic 162 (6):419-446.
How to characterize provably total functions by local predicativity.Andreas Weiermann - 1996 - Journal of Symbolic Logic 61 (1):52-69.

Analytics

Added to PP
2013-12-01

Downloads
38 (#430,166)

6 months
5 (#700,287)

Historical graph of downloads
How can I increase my downloads?

Author Profiles

Citations of this work

Two General Results on Intuitionistic Bounded Theories.Fernando Ferreira - 1999 - Mathematical Logic Quarterly 45 (3):399-407.

Add more citations

References found in this work

Subrecursion: functions and hierarchies.H. E. Rose - 1984 - New York: Oxford University Press.
Bounded arithmetic, propositional logic, and complexity theory.Jan Krajíček - 1995 - New York, NY, USA: Cambridge University Press.

View all 9 references / Add more references