Where can I find a proof that nonstandard analysis is a conservative extension of standard analysis? Willie Wong's answer in this post claims that nonstandard analysis (NSA) is a "conservative extension" of standard analysis (SA), meaning that every provable statement in NSA that can be interpreted as a statement purely in SA is also provable within SA alone. 
I find this idea really cool. Where can I find a proof of this fact? Also, what is the subject that even allows this type of thing to be provable?
 A: Welcome to mathematical logic - specifically, model theory!
It's not really possible to understand this result fully without knowing the basics of the subject; however, let me give a general picture of what is involved.

Step one: choice of context. Clearly nonstandard analysis isn't a conservative extension of standard analysis - "there is an infinitesimal" is false classically but true nonstandardly!
When we do logic, we restrict attention to only certain properties. The relevant logic here is first-order logic. This is sufficient for developing most of classical analysis, but also has some serious limitations. These limitations however can also be viewed as positive features, since they allow us to perform various constructions which do not a priori seem possible. The relevant feature here is the compactness theorem. I'm actually not going to say anything about what it actually is; instead, I just want to focus on what it does here, since I think this will make this answer ultimately more readable.

Step two: from structures to theories. Fixing a set of "expressible sentences," we next move to semantics: when is a given sentence true? Specifically, every structure (a term with a precise definition) $\mathcal{A}$ has a corresponding theory $Th(\mathcal{A})$, consisting of all the sentences under consideration true in $\mathcal{A}$. This gives rise to a notion of "similarity" between structures, which is much more flexible than the usual notion of "isomorphism" (which basically says that the two structures in question are identical, but "named differently"): we say $\mathcal{A}\equiv \mathcal{B}$ if $Th(\mathcal{A})=Th(\mathcal{B})$, that is, if our logic can't distinguish them.

Step three: building NSA. The situation we're in now is the following: we have a structure we care about - the actual real line $\mathbb{R}$ - and we want to analyze it. To tell whether some sentence $\varphi$ is true in $\mathbb{R}$, it would be enough to know whether $\varphi$ is true in some $\mathfrak{R}$ as long as $\mathfrak{R}\equiv\mathbb{R}$. This raises two questions:


*

*What might make such a $\mathfrak{R}$ easier to analyze?

*How can we get such a $\mathfrak{R}$?
The first bulletpoint is made clear by reading arguments in NSA: the presence of infinitesimals drastically simplifies arguments. The second point is where the compactness theorem comes in: the compactness theorem is exactly the thing that says that we can produce such a $\mathfrak{R}$!


*

*OK, fine, you don't need compactness specifically; you could also work with ultrapowers and Los' theorem. In many ways this is cleaner, since it allows a one-sentence statement of what's going on: letting $\mathfrak{R}$ be the structure with domain $\mathbb{R}$ and every function and relation on reals, any nontrivial ultrapower of $\mathfrak{R}$ is a hyperreal field. But this isn't really that different, since Los' theorem is one of the ways to prove compactness, so it's essentially the same content packaged differently. Moreover, we can prove compactness without going through Los' theorem, so the compactness approach is also more flexible in some sense.



What to do now. I hope that the above has made a couple things clear: what subject provides the foundations for NSA, what the shape of the proof  of the relevant fact is, and the specific major theorem that proof relies on; I also hope the first paragraph in step one indicates that this whole shebang has serious limitations, and we have to be careful when reasoning with it. The next step is to learn the basics of model theory. This actually is all basic model theory - it's quite feasible to get to the formal development of nonstandard analysis in a relatively short time!
