The effective content of Reverse Nonstandard Mathematics and the nonstandard content of effective Reverse Mathematics

TL;DR

This paper uncovers a computational aspect of Nonstandard Analysis in Reverse Mathematics, showing how nonstandard equivalences can be transformed into effective higher-order equivalences and vice versa.

Contribution

It establishes a method to extract effective higher-order equivalences from nonstandard RM equivalences using primitive recursive terms, bridging nonstandard and standard Reverse Mathematics.

Findings

RM-equivalences in Nonstandard Analysis can be converted into effective higher-order RM-equivalences.

Primitive recursive terms serve as witnesses for these effective equivalences.

Effective equivalences can reconstruct original nonstandard theorems.

Abstract

The aim of this paper is to highlight a hitherto unknown computational aspect of Nonstandard Analysis pertaining to Reverse Mathematics (RM). In particular, we shall establish RM-equivalences between theorems from Nonstandard Analysis in a fragment of Nelson's internal set theory. We then extract primitive recursive terms from Goedel's system T (not involving Nonstandard Analysis) from the proofs of the aforementioned nonstandard equivalences. The resulting terms turn out to be witnesses for effective1 equivalences in Kohlenbach's higher-order RM. In other words, from an RM-equivalence in Nonstandard Analysis, we can extract the associated effective higher-order RM-equivalence which does not involve Nonstandard Analysis anymore. Finally, we show that certain effective equivalences in turn give rise to the original nonstandard theorems from which they were derived.