In 1986 C. Ward Henson and H. J. Keisler published “On the Strength of Nonstandard Analysis” (The Journal of Symbolic Logic, Vol. 51, No. 2 (Jun., 1986), pp. 377-386), which is a seminal contribution to the meta-mathematics of nonstandard analysis. Since their result bears directly on the issue in this thread which has been reopened after laying dormant for some time now, and since no reference to their work is referred to in the original thread, I am taking the liberty of quoting the introduction to Henson and Keisler’s important paper (which I believe is as current today as when it was published).
"It is often asserted in the literature that any theorem which can be proved using nonstandard analysis can also be proved without it. The purpose of this paper is to show that this assertion is wrong, and in fact there are theorems which can be proved with nonstandard analysis but cannot be proved without it. There is currently a great deal of confusion among mathematicians because the above assertion can be interpreted in two different ways. First, there is the following correct statement: any theorem which can be proved using nonstandard analysis can be proved in Zermelo-Fraenkel set theory with choice, ZFC, and thus is acceptable by contemporary standards as a theorem in mathematics. Second, there is the erroneous conclusion drawn by skeptics: any theorem which can be proved using nonstandard analysis can be proved without it, and thus there is no need for nonstandard analysis. The reason for this confusion is that the set of principles which are accepted by current mathematics, namely ZFC, is much stronger than the set of principles which are actually used in mathematical practice. It has been observed (see [F] and [S]) that almost all results in classical mathematics use methods available in second order arithmetic with appropriate comprehension and choice axiom schemes. This suggests that mathematical practice usually takes place in a conservative extension of some system of second order arithmetic, and that it is difficult to use the higher levels of sets. In this paper we shall consider systems of nonstandard analysis consisting of second order nonstandard arithmetic with saturation principles (which are frequently used in practice in nonstandard arguments). We shall prove that nonstandard analysis (i.e. second order nonstandard arithmetic) with the $\omega_{1}$-saturation axiom scheme has the same strength as third order arithmetic. This shows that in principle there are theorems which can be proved with nonstandard analysis but cannot be proved by the usual standard methods. The problem of finding a specific and mathematically natural example of such a theorem remains open. However, there are several results, particularly in probability theory, whose only known proofs are nonstandard arguments which depend on saturation principles; see, for example, the monograph [Ke]. Experience suggests that it is easier to work with nonstandard objects at a lower level than with sets at a higher level. This underlies the success of nonstandard methods in discovering new results. To sum up, nonstandard analysis still takes place within ZFC, but in practice it uses a larger portion of full ZFC than is used in standard mathematical proofs."
[F] S. FEFERMAN. Theories of finite type related to mathematical practice, Handbook of mathematical logic (J. Barwise, editor), North-Holland, Amsterdam, .1977, pp. 913-971.
[Ke] H. J. KEISLER, An infinitesimal approach to stochastic analysis, Memoirs of the American Mathematical Society, No. 297 (1984).
[S] S. SIMPSON, Which set existence axioms are needed to prove the Cauchy/Peano theorem for ordinary differential equations? JSL, vol. 49 (1984), pp. 783-802.
It is perhaps worth adding that Keisler (making use of work of Avigad) subsequently published a sequel to his paper with Henson in which he introduces what might be regarded as a system of Reverse Mathematics for nonstandard analysis with the hope of being able to establish the strength of particular theorems proved using nonstandard analysis. (See “The Strength of Nonstandard Analysis” by H.J. Keisler in The Strength of Nonstandard Analysis ed. By imme van den berg and vitor nerves, Springer, 2007).