To my way of thinking, there are at least three distinct
perspectives one can naturally take on when undertaking work in
nonstandard analysis. In addition, each of these perspectives can
be varied on two other dimensions, independently. Those dimensions are, first,
the order of nonstandardness (whether one
wants nonstandardness only for objects, or also for functions and
predicates, or also for sets of functions and sets of those and so
on), and second, how many levels of
standardness and nonstandardness one desires. Let me describe the three
views I have in mind, and give them names, and then discuss how
they relate to one another.
Classical model-construction perspective. In this approach,
one thinks of the nonstandard universe as the result of an
explicit construction, such as an ultrapower construction. In the
most basic instance, one has the standard real field structure
$\newcommand\R{\mathbb{R}}\newcommand\Z{\mathbb{Z}}\langle\R,+,\cdot,0,1,\Z\rangle$,
and you perform the ultrapower construction with respect to an
fixed ultrafilter on the natural numbers (or on some other set, if
this was desirable). In time, one is led to want more structure in
the pre-ultrapower model, so as to be able to express more ideas,
which will each have nonstandard counterparts. And so very soon
one will have constants for every real, a predicate for the
integers $\Z$, or indeed for every subset of $\mathbb{R}$ and a
function symbol for every function on the reals, and so on. Before
long, one wants nonstandard analogues of the power set $P(\R)$ and
higher iterates. In the end, what one realizes is that one might
as well take the ultrapower of the entire set-theoretic universe
$V\to V^{\omega}/U$, which amounts to doing nonstandard analysis
with second-order logic, third-order, $\alpha$-order for every
ordinal $\alpha$. One then has the copy of the standard universe
$V$ inside the nonstandard realm $V^*$, which one analyzes and
understands by means of the ultrapower construction itself.
Some applications of nonstandard analysis have required one to
take not just a single ultrapower, but an iterated ultrapower
construction along a linear order. Such an ultrapower construction
gives rise to many levels of nonstandardness, and this is
sometimes useful. Ultimately, as one adds additional construction methods, this amounts as Terry Tao mentioned to just adopting all of model theory as one toolkit. One will want to employ advanced saturation properties or embeddings or the standard system and so on. There is a very well-developed theory of models of arithmetic that uses quite advanced methods.
To give a sample consequence of saturation: every infinite graph, no matter how large, arises as an induced subgraph of a nonstandard-finite graph in any sufficiently saturated model of nonstandard analysis. This often allows you to undertake finitary constructions with infinite graphs, modulo the move to a nonstandard context.
Standard Axiomatic approach. Most applications of nonstandard
analysis, however, do not rely on the details of the ultrapower or
iterated ultrapower constructions, and so it is often thought
worthwhile to isolate the general principles that make the
nonstandard arguments succeed. Thus, one writes down the axioms of
the situation. In the basic case, one has the standard structure
$\R$ and so on, perhaps with constants for every real (and for all
subsets and functions in the higher-order cases), with a map to
the nonstandard structure $\R^*$, so that every real number $a$ has
its nonstandard version $a^*$ and every function $f$ on the reals
has its nonstandard version $f^*$. Typically, the main axioms
would include the transfer principle, which asserts that any
property expressible in the language of the original structure
holds in the standard universe just in case it holds of the
nonstandard analogues of those objects in the nonstandard realm.
The transfer principle amounts precisely to the elementarity of
the map $a\mapsto a^*$ from standard objects to their nonstandard
analogues. One often also wants a saturation principle,
expressing that any sufficiently realizable type is actually
realized in the nonstandard model, and this just axiomatizes the
saturation properties of the ultrapower. Sometimes one wants more saturation than one would get from an ultrapower on the natural numbers, but one can still achieve this by larger ultrapowers or other model-theoretic methods.
Essentially the same axiomatic approach works with the high-order
approach, where one has nonstandard version of every set-theoretic
object, and a map $V\to V^*$, with nonstandard structures of any
order.
And similarly, one can axiomatize the features one wants to use in
the iterated ultrapower case, with various levels of standardness.
As with most mathematical situations where one has a construction
approach and an axiomatic approach, it is usually thought to be
better to argue from the axioms, when possible, than to use
details of the construction. And most applications of nonstandard
analysis that I have seen can be undertaken using only the usual
nonstandard axioms.
Nonstandard Axiomatic approach. This is a more radical
perspective, which makes a foundational change in how one thinks
about one's mathematical ontology. Namely, rather than thinking of
the standard structures as having analogues inside a nonstandard
world, one essentially thinks of the nonstandard world as the real
world, with "standardness" structures picking out parts of it. So
one has the real numbers including both infinite and infinitesimal
reals, and one can say when two finite real numbers have the same
standard part and so on. With this perspective, we think of the
real real numbers as what on the other perspective would be the
nonstandard reals, and then we have a predicate on that, which
amounts to the range of the star map in the other approach. So
some real numbers are standard, and some functions are standard
and so on.
One sometimes sees this kind of perspective used in arguments of
finite combinatorics, where one casually considers the case of an
infinite integer or an infinitesimal rational. (I have a colleague
who sometimes talks this way.) That kind of talk may seem alien
for someone not used to the perspective, but for those that adopt
the perspective it is very useful. In a sense, one goes whole-hog
into the nonstandard realm.
More extreme versions of this idea adopt many levels of
standardness and nonstandardness, extended to all orders. Karel Hrbáček has a very well-developed theory like this for nonstandard
set theory, with an infinitely deep hierarchy of levels of
standardness. He spoke on this last year at the CUNY
set theory seminar, and I refer you to his articles on this topic.
In Karel's system, one doesn't start with a standard universe and
go up to the nonstandard universe, but rather, one starts with the
full universe (which is fundamentally nonstandard) and goes down
to deeper and deeper levels of standardness. Every model of ZFC,
he proved, is the standard universe inside another model of the
nonstandard set theories he considers.
Ultimately, my view is that the choice between the perspectives I
mentioned is a matter of taste, and that in principle any
achievement of nonstandard analysis that can be undertaken with
one of the perspectives has natural analogues that can be
expressed with the other perspectives.
