I have been through constructions of the reals, and the proofs for the hyperreals. It has been years, but I am confident that without much difficulty I could probably give you every proof that is necessary from scratch.
The proofs for the hyperreals involve a lot more machinery than the proofs for the standard reals. That is my educated opinion based on knowing both sets of proofs and constructions. (Of course this need not make infinitesmals a pedagogical disaster - very few students actually care much about learning the proofs.)
As for the model theory approach, I am intimately familiar with the ultrafilter construction. It uses choice. I know there is a second construction which I am not familiar with, but from what I've read it also requires choice. Both involve model theory. That's a mighty big sledgehammer for a pretty small fly.
Incidentally Dedekind cuts can be understood as follows. The set of reals can be equated with the set of points where you can cut the rationals into two. More precisely if X is a nonempty subset of the rationals with an upper bound, we get a cut of the rationals into the set of upper bounds of X, and things that are not an upper bound of X. Any two subsets can be considered equivalent if their set of upper bounds is identical. An equivalence class of subsets is a real number.
For any cut you can generate a unique set A of rationals that are not upper bounds, and a set B of rationals that are upper bounds. When you do this, all rationals in A are less than all rationals in B, and A does not contain an upper bound.
Conversely if we have a partition of the rationals into 2 non-empty sets A and B such that all members of A are less than all members of B, and A does not contain an upper bound. Then we have a cut of the rationals.
So there is a 1-1 correspondence of reals to places we can cut the rationals to partitions of rationals with that property.
Those partitions of the rationals are called Dedekind cuts.
(This is one of two constructions of the real numbers. The other, Cauchy sequences, turns out to generalize more usefully in the field of topology.)
Hey, you are right. the method I was thinking of does require model theory to justify its axioms (IST). It had been waved away as you put it, so that the core could be focused on. But you don't really need to understand why the axioms are justified any more than most people understand the axioms of ZFC (excepting those like you of course). And if the outcome is a better first intuition of calculus, I don't think it is accurate to label it a fly.
I did find out that there is a constructive approach though, so the axiom of choice is not actually necessary. www.math.ucla.edu/~asl/bsl/0403/0403-001.ps
The proofs for the hyperreals involve a lot more machinery than the proofs for the standard reals. That is my educated opinion based on knowing both sets of proofs and constructions. (Of course this need not make infinitesmals a pedagogical disaster - very few students actually care much about learning the proofs.)
As for the model theory approach, I am intimately familiar with the ultrafilter construction. It uses choice. I know there is a second construction which I am not familiar with, but from what I've read it also requires choice. Both involve model theory. That's a mighty big sledgehammer for a pretty small fly.
Incidentally Dedekind cuts can be understood as follows. The set of reals can be equated with the set of points where you can cut the rationals into two. More precisely if X is a nonempty subset of the rationals with an upper bound, we get a cut of the rationals into the set of upper bounds of X, and things that are not an upper bound of X. Any two subsets can be considered equivalent if their set of upper bounds is identical. An equivalence class of subsets is a real number.
For any cut you can generate a unique set A of rationals that are not upper bounds, and a set B of rationals that are upper bounds. When you do this, all rationals in A are less than all rationals in B, and A does not contain an upper bound.
Conversely if we have a partition of the rationals into 2 non-empty sets A and B such that all members of A are less than all members of B, and A does not contain an upper bound. Then we have a cut of the rationals.
So there is a 1-1 correspondence of reals to places we can cut the rationals to partitions of rationals with that property.
Those partitions of the rationals are called Dedekind cuts.
(This is one of two constructions of the real numbers. The other, Cauchy sequences, turns out to generalize more usefully in the field of topology.)