Hyperreals

You can construct infinitesimals from a proper, ordered field extension of the reals. Unfortunately a great deal of logic machinery seems necessary to do analysis with these critters. Since field extensions are part of classical mathematics, I don't see why.