[FOM] Computational Nonstandard Analysis

[Harvey Friedman]

SANDERS
wrote: http://www.cs.nyu.edu/pipermail/fom/2015-August/018948.htmlre: [FOM]
CFR and Programme: SoTFoM III and The Hyperuniverse Programme, Vienna,
21-23 September 2015.

Disclaimer:  Any mention of “Nonstandard Analysis” below refers to Nelson’s
> internal set theory IST (and fragments), i.e. the syntactic approach to
> NSA.
> As Harvey pointed out, nonstandard models have all kinds of undefinability
> properties, the most well-known one is Tennenbaum’s theorem.  As already
> noted by Nelson in his BAMS paper introducing IST, the latter DOES NOT
> suffer from Tennenbaum’s theorem (and related undefinability issues).
> In other words, IST does not have the oft-cited drawbacks of the
> model-theoretic approach to NSA.  (IST does have other drawbacks though,
> see the literature).


​Most people have something very very different in mind when they use the
phrase "nonstandard analysis". Following A. Robinson, they assume one is
talking about at least a proper elementary extension of (R,Z,+,dot), which
even be proved to exist in ZF. As I wrote, there is the impressive
Kanovei/Shelah showing that there is a formula of ZFC which, provably in
ZFC, defines such things and much more. However, as I pointed out, getting
at even some nonstandard integer like this is impossible, and also having
the construction provably lie in L(R) is also impossible. There are other
impossibility statements I am looking at, but not ready to report further.

This usual kind of nonstandard analysis has been mostly used for doing
rather abstract analysis, far far far above what you are concerned with,
which is computational issues. HOWEVER, I am vaguely aware of some
situations where sometimes people like to use nonstandard arguments to get
some computational information out at the end, arguably "easier" or
"differently" than they would if they got their hands really dirty. WHAT
are the best examples of this? WHAT about forging tools to eliminate this,
and retain any computational content?

There are some conservatively results in Reverse Mathematics relevant here,
and probably they need to be fine tuned. One is the conservatively of WKL_0
over RCA_0 for Pi02 sentences. There are others, There are also general
speedup issues as to whether the length of proofs is blowing up
exponentially, or even iterated exponentially, etcetera.

So I can tell that you are living in a different galaxy than classical
nonstandard analysis in the sense of Abraham Robinson with his ultra power
constructions.

So I would like to understand what you are doing SLOWLY. Very few readers
have any idea what IST is and what Nelson was up to. We need to start with
your explanation of Nelson.

It would be much more helpful to state Tennenbaum's Theorem which, I think,
is something about all models of weak fragments of PA are non recursive
(there atomic diagram, not their theory). What is the threshold of having a
recursive nonstandard model or not? Also I gather you are NOT just looking
at nonstandard models of fragments of arithmetic, but rather fragments of
fragments of second order arithmetic? This should be discussed, including
the possibility of introducing interesting primitives. Maybe that is what
you do.

Since your are talking about nonstandard analysis is a very fine grained
delicate setting, we need to proceed with SLOW explanations.

2) In the case of Nelson’s IST, the following is meant by “computational
> foundation”:
> From the proof of a theorem of *pure* Nonstandard Analysis (i.e. only
> involving the nonstandard notions of continuity, compactness,…), one can
> extract
> the proof of the associated “effective” theorem.  The latter is either a
> theorem of constructive/computable analysis, OR an equivalence/implication
> from
> Reverse Math.  The “effective” theorem has its existential quantifiers
> witnessed by terms also extracted from the original proof.
> Conclusion: In other words, one can just “do pure Nonstandard Analysis”
> and extract the effective version at the end.  This effective version gives
> one
> a lot of computational content (as good as the proof can provide).  In
> this way, NSA provides a “computational” foundation.


​We need some slowly presented nice examples of such extractions. Also
"computational" is a very multifaceted word. All the way from just about
any countable piece of mathematics, all the way down to something that can
be implemented by a computer in less than a day, available from a major
computer company in 2015 for a reasonable price. ​

​Harvey Friedman
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150830/24d36e04/attachment.html>