Kurt Gödel Research Center

2012 seminar talk: Reuniting the antipodes: bringing together Nonstandard Analysis and Constructive Analysis

Talk held by Sam Sanders (Ghent University, Belgium and MCMP München, Germany) at the KGRC seminar on 2012-12-13.

Abstract

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.