Nonstandard Analysis as a corollary of Model Theory
Abraham Robinson's originally discovered Non-standard Analysis by realizing there must be a model of the reals with an infinitesimal. In the decades since, however, the model theory has commonly been avoided or at least "watered-down". Instead, the most common approach has been to perform model-theoretically inspired constructions on a "superstructure" within ZFC; the side-effect, however, is a "black box" approach to NSA without real intuition of why it works.
This article is meant to be a summary of Robinson's original model-theoretic approach; for a fuller treatment, see Robinson's original book or this modernized introduction. Even if one ultimately decides to use another approach, studying the model theory may give some intuition to nonstandard analysis which would not have been acquired otherwise.
Model Theory, summarized
We assume prior knowledge of first order logic, that is, of sentences written only in terms of unrestricted "for all", "there exists", and n-ary relations which determine whether n-tuples (x_1,...,x_n) of the universe are true or false.
Model theory essentially studies these sentences when they have been interpreted in a structure, which consists of an underlying set (a "universe") as well as relations on this set. The essential observation made by Robinson was that there are usually many structures satisfying the same sentences.
A structure which satisfies a list of sentences is said to be a model of those sentences. Conversely, the set of all sentences satisfied by a structure is called its theory. The ultimate goal here is to find a "nonstandard model" for the theory of the (standard) reals.
Finding a first-order theory of the reals
The first problem, of course, is that first-order sentences are only quantified universally with "for all reals" as opposed to "for all reals in a certain set" or "for all subsets". To this end, Robinson defined a structure where the members of the universe are allowed to have "types". Individuals are of type 0, relations and functions on the individuals would have some other type, functions on functions would have yet another type, etc. In ZFC, these types are realized in the superstructure; it is sufficient just to assume they exist somewhere.
In such a typed model, one can define type relations that are satisfied iff an input is a certain type (of course, these also have an analogue in the superstructure, but finding it can be quite difficult). Using these type relations, sentences could be given higher-order expressive power.
For example, "for all subsets of the reals, something happens" can be worded "for all individuals x, if x is of type (0), something happens", since an individual is a subset of the reals iff it is of type (0). More precisely, the sentence would be "for all individuals x, if x satisfies type relation (0), then something happens."
The last technicality is that these functions and relations are not "really" functions or relations, since they belong to the model's universe of individuals. They can, however, be evaluated by "evaluation relations" designed precisely to evaluate these individuals in the expected way.
In this way, higher-order expressive power is attained.
Toward a saturated model
Starting with the standard first-order model of the reals, Robinson originally followed up by defining enlargements, models with additional individuals to satisfy certain relations. The more modern treatment, however, skips straight to saturated models (which are "even more" enlarged), as modern model theory has a simple way of constructing them.
One starts with the classical compactness theorem: "A list of sentences has a model iff every finite subset has a model".
One then defines complete types (not related to type), which are lists of formulae denoting a "thing" that might or might not be in the model. By definition, we require that a complete type be finitely realized; i.e. for any finitely many of the formulae, there is an element in the model for which they are true. One can then use compactness to prove that the entire type is realized in a larger model. In fact, by using compactness on the theory as well, this larger model can be taken as an elementary extension satisfying the same sentences.
Thus, starting at the standard model, one "adds" complete types to it by repeatedly passing to the elementary extension. By doing this transfinitely many times in a careful way, one can eventually get a model *M where every complete type is actually realized in *M, a saturated model. Of course, there are other caveats, such as the saturation not being complete, but this is essentially what happens.
Infinitesimals clearly exist in a saturated model of the reals, for consider the complete type with such formulae as:
"e > 0"
"e < 1"
"e < 1/2"
"e < 1/3"
"..."
These are finitely realized in the reals, as for any finitely many 1/n, there is some e less than them. So, in the saturated model, this complete type is realized by an e that is less than all 1/n.
The saturated model of the reals is called the hyperreals *R.
What this approach explains
The mysterious internal sets of NSA have an easy interpretation in model theory: they are the sets (or other entities, functions, sequences, etc) that actually are in the saturated model *M's universe. The existence of external sets (resp. functions, etc), i.e. those that aren't in *M, is easily seen by certain sets not satisfying some of the sentences that are transferred from the standard model.
For instance, in the reals, the sentence "every nonempty set that has an upper bound has a least upper bound" is true. Thus, this sentence must be true in the hyperreals as well. But consider the set F of all finite hyperreals. F has an upper bound, any infinite hyperreal, but no least upper bound; as for any infinite x, there is a smaller infinite x - 1. We conclude that F cannot actually be a set in *R, it is external.
Thus, to remind us that some sets can't be considered, the above sentence could be properly read in *R as "every internal set that has an upper bound has a least upper bound".
Conclusion
One should keep in mind that this is only a basic summary of the model-theoretic approach; we skip many important details. One should consult the references in the introduction for a fuller approach.
Although the kind of Nonstandard Analysis used is ultimately immaterial, intuition is usually served by developing any concept in its natural setting. I hope that this summary might have helped put some concepts into perspective, or at least given a starting point to find out more about them.
References
Non-Standard Analysis, Abraham Robinson
Nonstandard Analysis from a Model-Theoretic Perspective
Math 595 Lecture Notes (a model-theoretic approach that does use superstructures)