Non-standard Nonstandard Analysis and the computational content of standard mathematics

TL;DR

This paper reveals a new computational aspect of Nonstandard Analysis, showing how nonstandard systems can extract approximations from classical proofs, even those not involving Nonstandard Analysis.

Contribution

It demonstrates that nonstandard systems can be used to extract computational content from classical proofs, extending proof mining techniques beyond nonstandard frameworks.

Findings

Nonstandard systems validate uniform boundedness principles.

Classical proofs using weak K"onig's lemma yield approximations.

Computational extraction is possible without nonstandard assumptions.

Abstract

The aim of this paper is to highlight a hitherto unknown computational aspect of Nonstandard Analysis. Recently, a number of nonstandard versions of Goedel's system T have been introduced ([2,9,12]), and it was shown in [26] that the systems from [2] play a pivotal role in extracting computational information from proofs in Nonstandard Analysis. It is a natural question if similar techniques may be used to extract computational information from proofs not involving Nonstandard Analysis. In this paper, we provide a positive answer to this question using the nonstandard system from [9]. This system validates so-called non-standard uniform boundedness principles which are central to Kohlenbach's approach to proof mining ([14]). In particular, we show that from classical and ineffective existence proofs (not involving Nonstandard Analysis but using weak Koenig's lemma), one can `automatically' extract approximations to the objects claimed to exist.