[FOM] Regarding Friedman's 1966 NSA Axioms

[Sam Sanders]

Dear Harvey,

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

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

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


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.  

Best,

Sam