[FOM] Regarding my 1966 NSA Axioms

[Harvey Friedman]

In I wrote

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

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.

I certainly had the idea of extending this to higher systems in 1966,
but didn't pursue it.

Harvey Friedman