[FOM] The unreasonable effectiveness of Nonstandard Analysis

[Hendrik Boom]

On Fri, Sep 04, 2015 at 05:38:12PM +0200, Sam Sanders wrote:

> 
> These two observations lead to the following application, leading to the extraction, from NSA, of LOTS of computational content (the technical term I have heard on the other side of the pond is “up the wazoo”):
> 
> There is a carefully crafted “term extraction" algorithm based on logical meta-theorems, among others from the above paper by van den Berg et al (APAL 2012).
> 
> On input (proofs of) theorems of pure NSA, this term extraction algo will:
> 
> a) always yield theorems of usual mathematics, i.e. not involving NSA.
> 
> b) yield either theorems of constructive/comp. math, or equivalences from RM if the original theorem is non-constructive.  The extracted terms (prim. rec., i.e. Goedel’s T) witness the existential quantifiers.  

This leaves me with a few questions.

(I) Is the situation with NSA similar to the situation of choice 
sequences in intuitionism? 

(II) Are choice sequences perhaps expressible as a form of NSA?

-- hendrik