[FOM] Replies to Sanders on Nonstandard Analysis 1

[Harvey Friedman]

SANDERS

The so-called Friedman A-translation establishes that Peano Arithmetic (PA)
and Heyting Arithmetic (HA) prove the same Pi_2^0-formulas.   Since HA has
the existence property, the innermost existential quantifier can be witnessed.
Arguably, Pi_2^0 is only a small class of the arithmetical hierarchy,
and includes
very few mathematical theorems.

RESPONSE

I have heard of the A-translation, good stuff (smile).

I think that "includes very few mathematical theorems" is misleading.
Actually, the whole of mathematics is essentially Pi-0-1, with some
Pi-0-2 and Pi-0-3 sentences begging to become Pi-0-1. Generally, this
happens after the sentence is proved, or after people make a
breakthrough giving a decent upper bound, thrusting it into a Pi-0-1
stated fact.

Of course, there is the very interesting problem of giving Pi-0-1 or
Pi-0-2 or Pi-0-3 interpretations of theorems involving real numbers -
or continuous functions on Polish spaces, or analytic functions of a
complex variable, etcetera. At the heart of the matter, it appears
that the essence is Pi-0-1.

But what do I mean? Well, this requires some thought, to see what I
mean. One formulation is as follows.

CONJECTURE. For many, most, nearly all(?) theorems of analysis,
especially constructive ones, you can identify a Pi-0-1 fact which is
the essence of the theorem, in the following sense. If you assume this
Pi01 fact, then the theorem follows very straightforwardly.

For instance, there may be a lot of real numbers, but by some fairly
uniform kind of argument, you can replace the real numbers by
rationals, and get a formulation that pretty much immediately implies
the statement with the reals. Then you prove the form with the
rationals, which is a Pi01 or at least very low statement.

It would be interesting to see what happens if we systematically try
to tease out the Pi01 (or maybe a bit higher) content out of
statements in analysis.

SANDERS

A similar “translation" result holds for fragments of Nelson’s IST and
PA (and HA), BUT the associated
formula class is VERY large: it includes all theorems of PURE NSA,
i.e. formulated
with nonstandard definitions (of continuity, compactness, …) rather
than “epsilon-delta” definitions.

RESPONSE

In the way I like to think and discuss things, you have made a big
jump by moving so quickly to NSA.

Slowing down, note that you started with the conservative extension result

*Any Pi02 sentence provable in PA is provable in HA.*

Before thinking about NSA, where the A stands for "analysis", we need
to consider the possibility of interesting further conservative
extension results that involve real numbers.

The most well known generalization of the above, which I think I did a
form of, also by A-translation, is this.

*Any Pi-1-1 sentence provable in PA with functions is provable in HA
with functions*

Now, this has some things not well pinned down.

One attractive form of this is that we add a unary function symbol F
from N into N, to PA and to HA. There are no nonlogical axioms. A
Pi-0-2(F) sentence has the obvious meaning, generalizing a Pi-0-2
sentence.

*Any Pi-0-2(F) sentence provable in PA(F) is provable in HA(F)"

If we allow quantification over functions from N into N, then on the
classical side, we have various systems including ones arising in my
Reverse Mathematics. They have intuitionists counterparts, although to
make most of them intuitionistically reasonable, you should use a lot
of double negations. I haven't considered RCA_0, which may have
simpler good intuitionistic counterparts. In any case, one wants, for
such systems, T,

*Any Pi-1-1 sentence provable in classical T is provable in the
intuitionistic form of T"

But this is not quite where we want to go. We want to work on the
reals R or on [0,1].

So one immediate general question is.

QUESTION. What are the interesting classical theories of arithmetic
plus real numbers which, like PA, have an obvious intuitionstic
counterpart (HA in the case of PA), and where all sentences of a
certain interesting involving real numbers, provable in the classical
theory, is provable in the intuitionistic counterpart?

Now of course, it is also interesting to decouple this question from
intuitionsitic systems.

QUESTION. What sentence forms involving arithmetic plus the real
numbers have the property that if they are true, then they
automatically have some associated computational meaning?

We have to be careful how we spell out this computational meaning. One
obvious example is

*every real number is less than some integer*

and the computational meaning of this kind of thing needs to be
fleshed out properly for use in other examples. I know that this jay
be reinventing the wheel, but often a previously invented wheel can
benefit from being reinvented.

Coming to something more sophisticated, we would like to look at
sentences like, say,

*for all reals x there exist reals y such that something of a certain form*
*for all continuous functions from R into R there exists a continuous
function from R to R such that something of a certain form*

and maybe

i. Say that if the above statements are true then they have thus and
thus computational content.
ii. Say that if the above statements are provable in certain systems
then they have (possibly provably) thus and thus computational
content.
iii. Say that if the above statements are provable in certain
classical systems then they are provable in certain intuitionsitci
systems.

Before I personally look at "term extraction" in the nonstandard
settings, I would like to get clear about what is going on with the
above and "term extraction" issues in standard settings.

And before I personally look at term "extraction" in nonstandard
analysis, I would like to understand what this means in nonstandard
arithmetic.

SANDERS

> I would like to propose the following thought experiment, extending your
> argument. Every proof using the real numbers can be paraphrased using the
> rational numbers only. I have it on Harvey's authority that this is a feasible
> project.

Well, the late Pat Suppes proposed such a program (“Dispensing with
the continuum”) about 25 years ago.

He and his co-authors (Sommer, Chuaqui, Alper) developed basic math
(intended for physics) using only
the hyperrational numbers *Q, (the fraction field resulting from the
hyperintegers),
i.e. an infinitesimal calculus in which there is no notion of “real number”.

Then, one proves (either by hand of via meta-theorems) that one can
replace in a given theorem
infinitesimals by “very small rationals”, while keeping the theorem true.

The theorems proved in this style are not too complicated, but complications
build up along the way.   At some point, the math is no longer manageable.

RESPONSE

I believe Pat was right on in the following sense. I think that the
usual epsilon/delta and the nonstandard approach are BOTH transitional
developments in the history of mathematics, where in the future, there
will be highly manageable and powerful finite combinatorial reworkings
and extensions of current mathematics. "At some point, the math is no
longer manageable". There has to be the right kind of breakthroughs
that make the mathematics not only manageable, but as beautiful and
attractive as all of the current infantry approaches. I believe that
this can be done - which of course doesn't mean that I have done
this..

SANDERS

> I agree with you
> (Hendrik) though that the mathematical possibility of paraphrazing arguments
> in terms of narrower number systems is interesting in its own right, and is
> close to the spirit of Reverse Mathematics.

One does run into the problem of “faithfulness”, i.e. how faithful
is the representation?  Even the coding of mathematical objects
in second-order arithmetic as done in RM is not without problems, as discussed
here recently.

RESPONSE

Strict Reverse Mathematics, in an embryonic state, is designed to
pulverize the coding issues in a systematic, powerful, way.

FRIEDMAN

> I think that the "are found" is misleading. Where are they? If this is
> "constructive" in the usual sense, then the existential statement
> "there exists an infinitesimal" should have an explicitly defined
> witness. The so called existential property is a hallmark of
> constructive systems.

SANDERS

I agree that the existence property (if something exists, we can construct it)
is a hallmark of constructive systems.  Now, constructive systems of
Nonstandard Analysis (like the system H discussed in van den Berg et
al, APAL2012)
DO have the existence property for *internal* sentences (i.e. not involving the
new “standardness” predicate).  In fact, a stronger property, called
the “Transfer rule” holds; See Prop. 5.12 in the aforementioned paper.

RESPONSE

I was thinking of a statement on the FOM to the effect that a benefit
of Nelson's approach is that "infinitesimals can be found among the
standard objects". I was objecting to this notion of "found" here.

SANDERS

By way of example of this difference, the system H mentioned above
proves LLPO^st and MP^st
(i.e. an omniscience and Markov’s principle relative to ‘st’).  But H proves
the same internal formulas as E-HA^\omega, i.e. H cannot prove LLPO or LPO.

Another example, H includes the axiom NCR (again see above paper),
which is classically false, yet
H does not prove anything internal which is classically false (as
E-HA^\omega does not).

In other words, H and E-HA^\omega have the same “usual” (that is
internal) constructive
content, but the external properties may (must) be very different.

RESPONSE

There are far far too much jargon in what you wrote for this to be
really useful to other than experts.

SANDERS
...

I disagree:  As Nelson has pointed out many times, IST does not
introduce new objects, in contrast to Robinson’s approach.  In IST
(and fragments), one just introduces a new predicate “x is standard”,
which some objects satisfy, and some do not.

RESPONSE

There is a huge cost for Nelson to be viewing IST as not introducing
new objects. The huge cost is an INCOMPATIBILITY between the standard
world and the real world. E.g., it is a theorem that the set of all
standard integers does not exist. But full comprehension on the
integers, VIA ANY DEFINITE MATHEMATICAL DESCRIPTION, is a time worn
axiom of mathematics (ok, you can reformable it in terms of real
numbers and Dedekind cuts). THEREFORE, Nelson is completely committed
to the idea that the notion of STANDARD is extra-mathematical.
Something outside the usual mathematical framework that mathematicians
work in for some centuries. Whereas, under the A. Robinson approach,
there is no incompatibility, and one is in no way going outside the
usual mathematical framework. Just use an ultra power, and stop trying
to say that you are adding an extra mathematical notion.

Of course, A. Robinson's approach would be the most ordinary way of
giving models of Nelson's setups.

NOW, I did NOT say that I am uninterested in seeing what happens IF
YOU pay this HUGE COST, and inject this foreign concept into
mathematics (standard integer, standard blah blah blah). On the
contrary, I am interested in

i. Its coherence.
ii. Its incoherence.

There are plenty of both for us to chew on.

SANDERS

By the way, in the constructive system H, there is no axiom st(x) OR
NOT st(x), so certain objects have an unknown status wrt standardness
constructively.

RESPONSE

Of course, this underlines that Sanders is primarily(?) concerned with
CONSTRUCTIVE NONSTANDARD ANALYSIS. That can be confusing to people
outside logic, who at most use A. Robinson's construction.

SANDERS

Reverse Mathematics (RM) is arguably a successful research program in FOM.

RESPONSE

Please omit "arguably". Also FOM should be f.o.m.

SANDERS

I) (ideology-freeness of NSA) Yes, infinitesimals have a lot of
history, and can have properties which apparently even instill fear
in, and cause nightmares for, some of the more ardent platonists.

In light of these properties, one could easily claim, like Errett
Bishop and Alain Connes did, that NSA must therefore lack any
numerical meaning.

This ideological claim lives quite strongly in the minds of
mathematicians, CS people, philosophers (especially), etc.

This ideological claim is also COMPLETELY FALSE, as shown below.

RESPONSE

I don't think it is "COMPLETELY FALSE" in capitals. I would think that
is true in some senses, and false in others.

I think we need to distinguish here between different kinds of NSA.

1. The usual classical nonstandard analysis. It is obviously PRIMA
FACIE without any DIRECT numerical meaning. It depends on an
ultrafilter. So it has a prima facie extremely high level of removal
from the computational.

2. BUT I think you are saying that if a certain kind of sentence is
provable in a certain brand of NSA, then one can extract some
computational meaning. That is a more nuanced position, that is not in
any direct conflict with Connes and Bishop.

3. It would be nice to provide here on the FOM a couple of really
simple clear examples of what you are saying here.

FRIEDMAN

> I left out a major component of my 1966 axioms. Here is what I did:
>
> 1. The usual axioms for successor, +,dot.
> 2. Induction for all formulas in the extended language.
> 3. There exists a nonstandard integer.
> 4. Transfer. (forall standard x1,...,xk)(phi(x1,...,xk) iff
> phi*(x1,...,xk)), where phi does not mention st, and all free
> variables are shown.
>
> I showed that that is conservative over PA.

SANDERS

So parameter-free Transfer (axiom no 4) has some advantages
and disadvantages:

RESPONSE

I think of 4 as with 'standard parameters" not "parameter-free". We
should get on the same page with some of our terminology.

SANDERS

1) On the PLUS side, “nonstandard RM” and “vanilla RM” start
overlapping given parameter-free Transfer.

For instance, given parameter-free Transfer in a suitable base theory,
one can prove:

The Transfer principle limited to Pi_1^0-formulasa <=> The Turing jump
functional exists.

The Transfer principle limited to Pi_1^1-formulasa <=> The Suslin
functional exists

Note that the right-hand side of these equivalences does not involve “st”.
Note that standard parameters are allowed in the Transfer principles
on the left-hand side.
A similar result for WKL and ATR seems impossible/unlikely.

I should mention the following paper on this topic:
http://arxiv.org/abs/1409.6881

RESPONSE

Too much jargon for general FOM readers, I think.

SANDErS

2) On the MINUS side, parameter-free Transfer destroys the “term
extraction” property
which the systems in van den Berg et al (APAL 2012) have.   In two
words, this is
because e.g. the Turing jump functional is standard if it exists at
all (given parameter-free Transfer)
and will thus be an oracle in the extracted term.

In CONCLUSION, parameter-free Transfer brings classical and
nonstandard RM a little closer together,
but no computational information can be extracted anymore.  This loss
is too great for the gain,
and my so-called Herbrandisations show that nonstandard RM and
classical RM are “the same”
at the meta-level anyway.

RESPONSE

I think you should slowly describe just what nonstandard RM is. RCA_0,
WKL_0, ACA_0, ATR_0, Pi11-CA_0 have associated nonstandard like
systems? And intuitionistic ones? I haven't even seen intuitionistic
versions of the five presented.

SANDERS

ROBINSON’S NSA

Robinson’s “semantic” approach to NSA is based on the construction of
a nonstandard model (nowadays usually via the well-known ultrafilter
construction).  Nonstandard models were known to Skolem already,
but they are not so useful from a mathematical point of view.
Robinson’s contribution was to prove various theorems which *connect*
the nonstandard model and
the original structure.  With these theorems in place, one can jump
“back and forth” between the original structure (“the standard world”
consisting of standard sets) and the nonstandard model ("the
nonstandard world” in which also nonstandard sets live).   In
particular, these *connections* between the standard and nonstandard
world allow one to do “infinitesimal calculus a la Leibniz” and NSA in
general.

The following are three important theorems (going back to Robinson)
connecting the standard and nonstandard world:

TRANSFER:  A formula from the original language (say of ZFC) holds in
the standard world IFF it holds in the nonstandard world (parameters
from the standard world are allowed)

STANDARD PART:  For every set (from the nonstandard world), there is a
set from the standard world which has the same standard elements.

IDEALISATION:  An intuitive description is best: One can bring all
quantifiers pertaining to standard objects up front, i.e. “pull them
through” normal quantifiers (pertaining to the entire universe).

(We are ignoring “saturation” for the moment).

Transfer expresses that the standard and nonstandard world have the
same properties (in the original language), going back to Leibniz’
similar idea.

Standard Part allows one to “go back” to the standard world after a
construction in the nonstandard world.  It is a kind of inverse of the
well-known “star morphism”.

NELSON’S IST

Nelson’s “syntactic” approach to NSA is essentially an axiomatic
version of Robinson’s NSA:  Nelson adds a new predicate “st( x ) “ to
the language of ZFC, to be read “x is standard”
and extends ZFC with three new axioms governing “st( x )", namely
Transfer, Standard Part, and Idealisation, which are versions of the
above theorems.  The new system is called IST,
and is a conservative extension of ZFC.   IST has a lot more nice
properties beyond the scope of this email.

By the previous, IST certainly LOOKS like Robinson’s NSA, but there
are some important (IMHO fundamental) differences too

1) EXTENSION: Robinson’s NSA provides an *extension* of the original
structure.  Lots of new elements are added:  The sets *N and *R (the
hypernaturals and hyperreals) have rather high cardinality compared to
N and R (the naturals and the reals in the original structure).
Nelson’s IST does not involve an extension:  It just labels some
elements "standard", but does not introduce any new ones.

2) COMPREHENSION: In IST, one CANNOT form the set:  { x : st(x) AND
A(x) } where A is a formula in L_ZFC.  Such a set is an example of
what Nelson calls “illegal set formation”.

By contract, in Robinson’s NSA, one of course has N and *N (the
naturals and the hypernaturals), and the former is the set of all
standard numbers in the latter.
In general, one can always form the “external" set {x : x is standard
AND A(x)} in Robinson’s NSA.

3) LOEB MEASURE:  Due to the absence of external sets, the Loeb
measure is not available in IST.

SOME PROPERTIES OF IST

Because of 1) and 2), IST does not have the oft-cited problems
Robinson’s NSA has.  An obvious example:

Tennenbaum’s thm states that plus and times +_M and x_M from a
nonstandard model M of PA are not recursive in the plus and times from
the standard model of PA.  This theorem does not apply to (NSA in the
spirit of) IST:  IST simply does not allow one to form the set “+
limited to the standard numbers”.

Because of 3), one has to pay a price when using IST:  One cannot have
the (full) Loeb measure.
By contrast, Simpson and Yokoyama have studied weak versions of the
Loeb measure in sosoa (in the same way one studies the Lebesgue
measure).

In general, proofs/techniques/constructions not exploiting external
sets in an essential way, can be translated from Robinson’s NSA to
Nelson’s IST.

I am neutral on the topic which approach (Robinson or Nelson) is
ultimately “best”.  That said, Nelson’s IST, being syntactic in
nature, is more amenable
to proof-theoretic analysis, as shown in my paper:

https://dl.dropboxusercontent.com/u/4558565/Sanders_Unreasonable%20effectiveness%20of%20NSA.pdf

> 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.

The simplest example is perhaps the following:

(i) Let P_0 be the conservative extension (as defined in the above
paper) of Kohlenbach’s system RCA_0^\omega (which in turn is a
conservative extension of RCA_0).

(ii) The system P_0 proves the following equivalence:

“The Transfer principle limited to Pi_1^0-formulas” <=> "Every
standard monotone sequence of reals in the unit interval, nonstandard
converges”  (D)

(A sequence x_n nonstandard converges if for all nonstandard N, M, x_N
≈ x_M., i.e. the terms of the sequence of infinite index are
infinitesimally close).

(iii) From a proof of the equivalence (D) in P_0, one can extract
terms s, t  from Goedel’s T such that Kohlenbach’s RCA_0^\omega proves

"If mu is Feferman’s non-constructive search operator, then t(mu) is
the rate of convergence for any monotone sequence in the unit
interval."  (E)

and

“if xi of type 1->1 provides the rate of convergence for any monotone
sequence in the unit interval, then s(xi) is Feferman’s
non-constructive search operator. " (F)

CONCLUSION:  Equivalences like (D) involving NSA can be “mined” to
obtain “explicit” equivalences like "(E) AND (F)".

>
> 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.

Agreed, but in the aforementioned paper, relatively “strong”
principles are treated too.  An example deals with equivalences from
the RM of Pi_1^1-CA

Consider the following nonstandard equivalence:

“The Transfer principle limited to Pi_1^1-formulas” <=> “Every
standard countable Abelian group, is a the sum of a (standard and
divisible group) and a (standard and reduced group)”  (A)

>From a proof of (A) in P_0, one extracts two terms s, t from Goedel’s
T such that, provable in RCA_0^\omega,

If mu_1 is Feferman’s version of the Suslin functional, then t(mu_1)
provides a divisible and a reduced group for every countable Abelian
group.  (B)

and

If xi  provides a divisible and a reduced group for every countable
Abelian group, then s(xi) is Feferman’s version of the Suslin
functional.   (C)


> 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?

Well, I provide examples of such in the paper:   From a proof of a
nonstandard theorem, one can extract the associated “highly
constructive” Herbrandisation (not involving NSA).
In turn, a proof of the Hebrandisation allows one to re-obtain the
nonstandard theorem.

An example of such an Herbrandisation is given above:

" (B) AND (C) “ is the Herbrandisation of (A).

and

“ (F) AND (E) “ is the Herbrandisation of (D).

In other words, one can extract from the proof of (A) in P_0, two
terms s, t of Goedel’s T such that "(B) AND (C)" is provable in
Kohlenbach’s RCA_0^\omega.
Vice versa, a proof of "(B) AND (C)” in the latter (for fixed terms s,
t) yields a proof of (A) in P_0.

Of course, these “Herbrandisations” can be obtained as theorems “an
sich” without NSA, but that would be a lot harder, I think.
The reason is that the Herbrandisations contain a lot of computational
information.

Furthermore, the above paper treats two examples of these
Herbrandisations in detail:

“nonstandard uniform continuity => nonstandard Riemann integration”
(Section 3.1 at the end)

“The Transfer principle limited to Pi_1^0-formulas <=> Every standard
monotone sequence of reals on the unit interval, nonstandard
converges”  (Section 4.1)

> 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.

So my notion of “computational” is closer to the latter:  These
extracted terms are in Goedel’s T and are obtained via a specific
proof interpretation; I am looking for someone to implement the
associated algorithm.
This should be possible as the proof interpretation seems to only
require that one can code finite sequences properly.

Best,

Sam

Dear Harvey,

> In 1966 when I was an undergrad at MIT, I formulated the following
> system PA*, and proved that it is a conservative extension of PA. The
> language is 0,S,+,dot, and a predicate for "being standard".
>
> 1 The usual axioms for successor, +,dot.
> 2. Induction for all formulas in the extended language.
> 3. There exists a nonstandard integer.
>
> I remember sitting in Gerald Sacks' office at MIT and telling him
> about this system and the conservative extension proof. He was
> interested, and spoke to A. Robinson about it, Sacks told me that A.
> Robinson was disappointed that it was a conservative extension. All
> three of us of course were well aware that this did not preclude that
> nonstandard arguments could be useful even though they can be
> systematically a priori eliminated.
>
> Does this fit into the history?

The system you describe here is a very special case of a fragment of
Nelson’s IST (based on Peano Arithmetic).

More general conservative extensions (with fragments of IST) of PA and
HA in all finite types and extensionality are studied in the following
paper:


Benno van den Berg et al, A functional interpretation for nonstandard
arithmetic, APAL, 2012.


The systems by van den Berg et al are special/new/great in that they
come with a “term extraction theorem” as follows:


TERM EXTRACTION THM

Let A  be a formula which does not involve the standardness predicate.

If the nonstandard extension of E-PA^\omega proves “for all standard
x, there is standard y such that A(x,y)” ,

then from this proof, a term t from Goedel’s T can be extracted such
that E-PA^omega proves “for all x, there is y \in t(x) such that
A(x,y)”


TWO NOTES:

The term t provides a finite sequence of witnesses, i.e. t(x) is not a
witness to “exists y”, but a finite sequence of possible witnesses.

A similar “term extraction theorem" holds for E-HA^omega, and the
recent system by Ferreira and Gaspar (APAL2015).


MATHEMATICAL RELEVANCE OF TERM EXTRACTION

The term extraction theorem allows us to extract computational info
(terms from Goedel’s T) from proofs in NSA of a specific formula
class,
namely formulas of the form  “for all standard x, there is standard y
such that A(x,y)” , where A does not involve the standardness
predicate.

An essential question is:  WHICH MATHEMATICAL THEOREMS FALL INTO THIS
CLASS OF FORMULAS?

ANSWER:  ALL theorems of *pure* Nonstandard Analysis, i.e. theorems
formulated solely with the nonstandard definitions of
continuity, differentiability, compactness, Riemann integration, ….

Again, see the paper http://arxiv.org/abs/1508.07434 for more details.
An example is provided below.

> And I think the FOM subscribers would be interested in Sanders
> continuing with a SLOW explanation of at least a couple fundamental
> results of his or more or less his. I think Sanders thinks a lot about
> Reverse NSA? But I don't think Sanders wants to sit on top of ZFC.

Indeed, Reverse NSA is the topic of study, using (fragments of) the
systems by van den Berg et al.
>From equivalences in Reverse NSA, one can extract “explicit”
equivalences in normal RM.

AN EXAMPLE of such an extraction:

a) NONSTANDARD EQUIVALENCE:

Here is a nice equivalence from *pure* NSA, provable in a weak system
of NSA based on PRA:

“The Transfer principle limited to Pi_1^0-formulas” <=> "Every
standard monotone sequence of reals in the unit interval, nonstandard
converges”  (D)


(A sequence x_n nonstandard converges if for all nonstandard N, M, x_N
≈ x_M., i.e. the terms of the sequence of infinite index are
infinitesimally close).


b) TERM EXTRACTION:

>From a proof of the equivalence (D), one can extract terms s, t  from
Goedel’s T such that Kohlenbach’s base theory  RCA_0^\omega proves

"If mu is Feferman’s non-constructive search operator, then t(mu) is
the rate of convergence for any monotone sequence in the unit
interval."  (E)

and

“if xi of type 1->1 provides the rate of convergence for any monotone
sequence in the unit interval, then s(xi) is Feferman’s
non-constructive search operator. " (F)


Note that the non-constructive search operator is essentially the
functional version of ACA_0


c) CONCLUSION:  Equivalences like (D) involving NSA can be “mined” to
obtain “explicit” equivalences like "(E) AND (F)”.


I hope this hints at what I am trying to do.


Best,

Sam

> I would like to propose the following thought experiment, extending your
> argument. Every proof using the real numbers can be paraphrased using the
> rational numbers only. I have it on Harvey's authority that this is a feasible
> project.

Well, the late Pat Suppes proposed such a program (“Dispensing with
the continuum”) about 25 years ago.

He and his co-authors (Sommer, Chuaqui, Alper) developed basic math
(intended for physics) using only
the hyperrational numbers *Q, (the fraction field resulting from the
hyperintegers),
i.e. an infinitesimal calculus in which there is no notion of “real number”.

Then, one proves (either by hand of via meta-theorems) that one can
replace in a given theorem
infinitesimals by “very small rationals”, while keeping the theorem true.

The theorems proved in this style are not too complicated, but complications
build up along the way.   At some point, the math is no longer manageable.

> I agree with you
> (Hendrik) though that the mathematical possibility of paraphrazing arguments
> in terms of narrower number systems is interesting in its own right, and is
> close to the spirit of Reverse Mathematics.

One does run into the problem of “faithfulness”, i.e. how faithful
is the representation?  Even the coding of mathematical objects
in second-order arithmetic as done in RM is not without problems, as discussed
here recently.

Best,

Sam

The results in my arXiv paper “The unreasonable effectiveness of NSA”
apply to what you say below.
It is perhaps a nice elementary application, which I therefore spell
out in detail.

> I think that the "are found" is misleading. Where are they? If this is
> "constructive" in the usual sense, then the existential statement
> "there exists an infinitesimal" should have an explicitly defined
> witness. The so called existential property is a hallmark of
> constructive systems.

As you point out in the below THEOREM, one cannot find a formula which
defines a nonstandard integer.  Similarly, one can never
find an internal formula defining the formula “x is infinitesimal”
(This is called the overflow- and underflow principle btw).

HOWEVER, it is possible to replace the formula “x is infinitesimal” in
MATHEMATICAL theorems by a numerical predicate " |x| < r “  (where r
may depend on parameters of the theorem).

VERY BASIC EXAMPLE:

a) Suppose the system H (See again van den Berg et al, APAL2012)
proves (forall x, y in [0,1])( x ≈ y => f(x) ≈ f(y) ) (f is
nonstandard uniform continuous).

b) From the proof in a), one can extract a term t from Goedel’s T such
that E-HA^\omega proves (forall k)(\forall x, y in [0,1])( |x-y| < 1/
t(k) => |f(x)-f(y)| <1/k ).  (note that the latter involves no NSA and
is the usual constructive definition of (uniform) continuity).

c) From the proof in b), one ALSO can also conclude that H proves
(forall x, y in [0,1])( x ≈ y => f(x) ≈ f(y) ) (since H believes the
term t from b) is standard)

Thus, in the case of continuity, all instances of  “z≈0” can be
equivalently replaced by the “numerical” predicate “|z| < r”,  where r
may involve extra parameters.

The theme of my paper “The unreasonable…" is that this can be done for
all theorems from *pure* NSA, i.e. solely formulated with the
nonstandard definitions (of continuity, compactness, diff., …)

CONCLUSION:  While the standardness predicate cannot be capture by an
internal formula, and indeed no single infinitesimal can be captured
in a much wider sense,
one can replace every occurrence of “x is infinitesimal” IN
MATHEMATICAL THEOREMS by a numerical formula “ |x| <r” (with
parameters .

This was the “Reverse Mathematics theme” I was hinting at:  Something
nice happens when one restricts oneself to mathematical theorems
(rather than some formula class).

Best,

Sam

As you have pointed out in the past, a non-trivial aspect of Reverse
Math is the representation (aka “coding”) of mathematical objects in
second-order arithmetic.
In your below posting, you also suggest that low levels of the type
hierarchy suffice for formalising mathematics.

In general, I agree with that statement, but there are however
non-trivial exceptions (which seem to tank associated grand claims).
In particular, while most of the coding in RM is innocent, it is not
always completely faithful/harmless,
as shown by the following examples:

1) The definition of continuity (say on Baire space) in RM reduces
type two objects to type one objects.
However, the RM-definition of continuity also gives rise to a type
three “fan functional” as follows:  The RM-theorem

“every RM-cont. function on Cantor space is uniform RM-cont on Cantor space”

is equivalent to

“there is a functional which takes as input an RM-cont function on
Cantor space, and outputs a modulus of uniform (RM) cont.

in Kohlenbach’s higher-order RM.  (See Theorem 4.1 in
http://arxiv.org/abs/1502.03613 )

Similar statements can be obtained for other theorems related to
continuity, of course.
Thus, the practice of coding in RM, designed to obviate higher-type
objects, actually introduces a host of new ones


2) Some RM of topology has been done in sosoa, where topologies are
represented/coded by countable bases.

For instance, a theorem concerning topologies on the reals has the form:

(\forall Y^3)(Y is a topology on the reals => A(Y))  (2)

and (2)  is interpreted in RM as:

(\forall X^1)(X is a countable basis for a topology on the reals =>
A(X)),     (1)

assuming A is nice enough.

However, (1) has the problem that in Kohlenbach’s higher-order RM, the
antecedent “there is a countable basis …” implies full second-order
arithmetic.
Hence, when interpreting (1) in the higher-order framework again, it
becomes a vacuous truth.   (See the PhD thesis of James Hunter at
Madison-Wisc.  http://www.math.wisc.edu/~lempp/theses/hunter.pdf )
Thus, the RM of topology in second-order arithmetic has considerable
problems when re-interpreted in the higher-order framework.

Ironically, Hunter proposes (also in his PhD) to adopt a new type
“alpha” for "points in a topology".  The subsequent RM of topology
looks
a lot nicer as a result (See the final chapters in the aforementioned PhD).


Finally, as I stated at the beginning, the above are exceptions and
Kohlenbach has even shown that coding of continuous functions does
not affect the RM of WKL (See his paper in the Feferman Festschrift).


Best,

Sam

_______________________________________________