[FOM] Nonstandard Analysis and the Transfer Principle

[Sam Sanders]

Dear Bob,

Thanks for your helpful questions.  I have used
them to improve my question.  

> What is a "classic" nonstandard system?

A system based on classical logic.   There are a few 
systems (e.g. by Moerdijk and Palmgren) of NSA based
on intuitionistic logic.  

> I have a sense of proof-theoretic
> strength of an axiom system, but I don't think that's what you mean by
> "first-order strength" here. So what does that mean?

I am talking about proof theoretic strength in the usual sense.
(E.g. "RCA_0 has the proof theoretic / first order strength of I\Sigma_1" )

> Are you thinking only
> relative to the standard reals, or do you want to relativize the question to
> systems non-standard relative to some base system, which could itself be
> non-standard?

Let us concentrate on systems of (nonstandard) second-order arithmetic.  

For instance, in his 2006 BSL paper, Jerry Keisler introduced
a nonstandard counterpart *X for every Big Five system X of Reverse Mathematics.  
Similar systems have been introduced by Keita Yokoyama and others.  

If we add the Transfer Principle for \Pi_1 formulas (with set parameters) to a nonstandard version of RCA_0,
the resulting theory is as strong as ACA_0.  

Thus, I repeat my (better phrased) question: 

What classical system of nonstandard second-order arithmetic is strong enough 
to prove (instances of) the Transfer Principle of NSA?

Best,

Sam