[FOM] Conservation of Nonstandard Methods

[Harvey Friedman]

There are a number of results that have been obtained to the effect
that any statement of a certain form proved using nonstandard methods
can be proved using standard methods. Of course, one has to be very
careful about how one formulates such results.

An early (earliest?) result of this kind is the result I proved as a
student to the effect that an obvious nonstandard form of PA, where
the universe is the "integers including nonstandard ones" and with a
predicate for "being standard", is conservative over PA. I don't think
I published an article on this, but it has made its way into the
folklore.

But there has been I think quite a lot of followup, extensions,
refinements, etcetera.

When moving to conservation results concerning nonstandard analysis,
not just nonstandard arithmetic, we of course want to prove results
about conservation of statements that go well beyond the arithmetical.

Also, do we have a solid formulation of "intuitionistic nonstandard
analysis" with proofs of conservation over standard intuitionistic
systems?

I think I recall seeing results to the effect that the use of
ultrafilters, even of certain sharp kinds, is conservative over
systems without them. This should be distinguished, it seems, from
using nonstandard objects as primitive.

This might be a good time and place for experts to give the FOM
readership a good general picture of the Conservation of Nonstandard
Methods. I would think that there are plenty of opportunities for new
conservation results.

Harvey Friedman