The computational content of Nonstandard Analysis

TL;DR

This paper explores the broad potential of proof mining in classical Nonstandard Analysis, demonstrating its ability to extract effective content from a wide range of theorems using nonstandard definitions.

Contribution

It shows that proof mining in classical Nonstandard Analysis has a much larger scope than in standard mathematics, including all theorems using only nonstandard definitions.

Findings

Proof mining applies broadly to pure Nonstandard Analysis theorems.

Nonstandard Analysis allows extraction of effective content where standard methods face limitations.

The scope includes results in analysis, computability theory, and Reverse Mathematics.

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 (and not the epsilon-delta kind) are used. In this note, we survey results in analysis, computability theory, and Reverse Mathematics.