Constructive Analysis (aka BISH) was introduced by Errett Bishop as a “computational“ redevelopment of Mathematics in the spirit of the intuitionistic tradition. As such, BISH is based on the BHK (Brouwer-Heyting-Kolmogorov) interpretation of logic, where the notions of “proof” and “algorithm” are central. Constructive Reverse Mathematics (CRM) is a spin-off from Harvey Friedman's “Reverse Mathematics” program where the base theory is based on BISH.
In this talk, we introduce an interpretation of BISH in classical Nonstandard Analysis. The role of “proof” in this interpretation is played by the Transfer Principle of Nonstandard Analysis. The role of “algorithm” is played by ‘\(\Omega\)-invariance’. Intuitively, an object is \(\Omega\)-invariant if it does not depend on the choice of infinitesimal used in its definition. Using this new interpretation, we obtain many of the well-known results form CRM. In particular, all non-constructive principles (like LPO, LLPO, MP, etc) are interpreted as Transfer Principles, which are not available in our (nonstandard) base theory.