[FOM] The computational content of Nonstandard Analysis

[katzmik at macs.biu.ac.il]

FOM readers may find it of interest to have the following issues clarified:

(1) in Kohlenbach's theory, getting explicit estimates seems to hinge on the
uniqueness of the solution.  From this viewpoint being able to get explicit
estimates without such uniqueness seems like a total miracle.  Can you comment
on that?

(2) the condition that the statements have to be in pure IST is not very
clear.  What does this translate into in practice?  No alternating
quantifiers?

MK

On Mon, October 26, 2015 18:40, Sam Sanders wrote:
> Dear Harvey, dear FOM,
>
> Here is a new attempt at explaining the computational content of Nonstandard
> Analysis (NSA) in approximately five steps:
>
>
> 0) I take it everyone has (vaguely) heard of constructive math and the
> underlying so-called intuitionistic logic.  I also assume that
> everyone has heard of “Nonstandard Analysis”, where (somehow) a distinction
> between standard and nonstandard objects is made.
>
> 1) First of all, constructive approaches to math and logic are different from
> the mainstream (or ‘classical’) approach in the following way (among other
> ways):
>
>>From a proof of “there exists x such that A(x)”, one can extract some term t
>> such that A(t).  By contrast, classical logic and classical mathematics do
>> not have this “existence property”.
>
> This existence property is often touted as an advantage of constructive math,
> as one can in principle implement the latter's results in a suitable
> programming language (like Agda)
> and extract the computational information carried by the existential
> quantifiers.
>
> 2) Secondly, one *can* of course translate theorems proved using classical
> logic into (modified) theorems with constructive proofs (See Goedel-Gentzen
> and H. Friedman’s work).
> However, the resulting (modified) theorems are generally quite different from
> and more complicated than the original theorems, with the exception of classes
> of
> ’simple' formulas, like
>
> “For all natural numbers x, there is a natural number y such that A(x,y)”,
> (*)
>
> where A is decidable.  As a result of the aforementioned proof translations,
> (*) does have the “existence property”, i.e. there is a computable function f
> such that A(x,f(x)) from a given x, and
> this f can be extracted (after translation) from a classical proof of (*).
>
> 3) Thirdly, as it turns out, proofs of theorems in fragments of Nonstandard
> Analysis (in Nelson’s internal set theory) can *also* be translated into
> (modified) theorems in “standard” mathematics (not involving NSA).  Again, the
> resulting (modified) theorems are generally much more complicated and
> different from the original ones, except for a specific formula class which
> also turns out to have a kind of existence property.  This special formula
> class is as follows:
>
> “For all standard x, there is a standard y such that A(x,y)”, where A does not
> involve the notion “standard”.  (**)
>
> These results may be found in van den Berg et al (APAL, 2012).
>
>
> 4) And now comes the crux:  The formula class given by (*) from 2) is
> “relatively small”, while the formula class given by (**) from 3) encompasses
> all theorems of “pure” Nonstandard Analysis (and much more).  A theorem is
> part of “pure NSA” if it is formulated solely with the nonstandard definitions
> (of continuity, open set, compactness, differentiability, Riemann integration,
> etc).
>
> In particular, any theorem of pure NSA can be brought into the form (**), and
> applying the existence
> property to the latter provides a term t such that the associated "standard"
> system (not involving NSA) proves
>
> “For all x, we have A(x,t(x))”
>
> (with slight simplification regarding the witnesses t(x) to increase
> readability).
>
> 5) In conclusion, similar to the proof translations from classical to
> intuitionistic logic, there are proof translations from fragments of NSA to
> “standard mathematics” (not involving NSA).
> In particular, the former translations bestow the existence property onto
> certain classically proved formulas (so-called Pi_2^0-formulas like (*)),
> while the latter translations do the same
> for a certain class of nonstandard formulas (like (**)).  However, the latter
> class encompasses all of “pure” NSA, i.e. nonstandard theorems formulated
> solely with nonstandard definitions (rather than the epsilon-delta variety).
>
>
> With kind regards,
>
> Sam Sanders
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>