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.

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 101,060

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

Ramsey's Theorem for Pairs and Provably Recursive Functions.Alexander Kreuzer & Ulrich Kohlenbach - 2009 - Notre Dame Journal of Formal Logic 50 (4):427-444.
Reverse formalism 16.Sam Sanders - 2020 - Synthese 197 (2):497-544.
Nonstandard combinatorics.Joram Hirshfeld - 1988 - Studia Logica 47 (3):221 - 232.
Proof mining in lp spaces.Andrei Sipoş - 2019 - Journal of Symbolic Logic 84 (4):1612-1629.

Analytics

Added to PP
2017-05-08

Downloads
27 (#820,541)

6 months
15 (#200,807)

Historical graph of downloads
How can I increase my downloads?

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.
The self-embedding theorem of WKL0 and a non-standard method.Kazuyuki Tanaka - 1997 - Annals of Pure and Applied Logic 84 (1):41-49.

View all 14 references / Add more references