The computational content of Nonstandard Analysis

Abstract

Kohlenbach's proof mining program deals with the extraction of effective information from typically ineffective proofs. Proof mining has its roots in Kreisel's pioneering work on the so-called unwinding of proofs. The proof mining of classical mathematics is rather restricted in scope due to the existence of sentences without computational content which are provable from the law of excluded middle and which involve only two quantifier alternations. By contrast, we show that the proof mining of classical Nonstandard Analysis has a very large scope. In particular, we will observe that this scope includes any theorem of pure Nonstandard Analysis, where 'pure' means that only nonstandard definitions are used. In this note, we survey results in analysis, computability theory, and Reverse Mathematics.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,616

External links

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

Through your library

  • Only published works are available at libraries.

Similar books and articles

Reverse formalism 16.Sam Sanders - 2020 - Synthese 197 (2):497-544.
A Nonstandard Delta Function in a Predicative Theory.Peter Zahn - 1995 - Mathematical Logic Quarterly 41 (2):257-260.
A nonstandard proof of a lemma from constructive measure theory.David A. Ross - 2006 - Mathematical Logic Quarterly 52 (5):494-497.
Nonstandard combinatorics.Joram Hirshfeld - 1988 - Studia Logica 47 (3):221 - 232.
Erna and Friedman's reverse mathematics.Sam Sanders - 2011 - Journal of Symbolic Logic 76 (2):637 - 664.
Nonstandard set theory.Peter Fletcher - 1989 - Journal of Symbolic Logic 54 (3):1000-1008.
More infinity for a better finitism.Sam Sanders - 2010 - Annals of Pure and Applied Logic 161 (12):1525-1540.
Nonstandard analysis and constructivism?Frank Wattenberg - 1988 - Studia Logica 47 (3):303 - 309.
An Effective Conservation Result for Nonstandard Arithmetic.Erik Palmgren - 2000 - Mathematical Logic Quarterly 46 (1):17-24.

Analytics

Added to PP
2017-05-08

Downloads
6 (#1,269,929)

6 months
1 (#1,042,085)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Sam Sanders
Ruhr-Universität Bochum

Citations of this work

No citations found.

Add more citations

References found in this work

Non-standard Analysis.Gert Heinz Müller - 2016 - Princeton University Press.
A functional interpretation for nonstandard arithmetic.Benno van den Berg, Eyvind Briseid & Pavol Safarik - 2012 - Annals of Pure and Applied Logic 163 (12):1962-1994.
Mathematical significance of consistency proofs.G. Kreisel - 1958 - Journal of Symbolic Logic 23 (2):155-182.

View all 16 references / Add more references