Abstract

The aim of my talk is to highlight a hitherto unknown computational aspect of Nonstandard Analysis. In particular, we provide an algorithm which takes as input the proof of a mathematical theorem from pure Nonstandard Analysis, i.e. formulated solely with the nonstandard definitions (of continuity, integration, dif- ferentiability, convergence, compactness, et cetera), and outputs a proof of the as- sociated effective version of the theorem. Intuitively speaking, the effective version of a mathematical theorem is obtained by replacing all its existential quantifiers by functionals computing (in a specific technical sense) the objects claimed to exist. Our algorithm often produces theorems of Bishops Constructive Analysis ([2]). The framework for our algorithm is Nelsons syntactic approach to Nonstandard Analysis, called internal set theory ([4]), and its fragments based on Goedels T as introduced in [1]. Finally, we establish that a theorem of Nonstandard Analysis has the same computational content as its highly constructive Herbrandisation. Thus, we establish an algorithmic two-way street between so-called hard and soft analysis, i.e. between the worlds of numerical and qualitative results.

References: [1] Benno van den Berg, Eyvind Briseid, and Pavol Safarik, A functional interpretation for non- standard arithmetic, Ann. Pure Appl. Logic 163 (2012), no. 12, 19621994.

[2] Errett Bishop and Douglas S. Bridges, Constructive analysis, Grundlehren der Mathematis- chen Wissenschaften, vol. 279, Springer-Verlag, Berlin, 1985.

[3] Fernando Ferreira and Jaime Gaspar, Nonstandardness and the bounded functional interpre- tation, Ann. Pure Appl. Logic 166 (2015), no. 6, 701712.

[4] Edward Nelson, Internal set theory: a new approach to nonstandard analysis, Bull. Amer. Math. Soc. 83 (1977), no. 6, 11651198.

[5] Stephen G. Simpson, Subsystems of second order arithmetic, 2nd ed., Perspectives in Logic, CUP , 2009.