Nonstandard analysis is one of those things that sounds nice in the abstract, but even though I first learned about it more than ten years ago, I have yet to see a worked didactic-level example of how you would, for example, obtain the derivative of sine using nonstandard analysis, or derive the natural logarithm.

I literally saw the sin one yesterday, so I'll rewrite it!!

Let e be an infinitesimal.

We write st(x) for the function dropping the infinitesimal part of a number.

Then f'(x) = st(1/e (f(x+e)-f(x)))

Now use the angle sum identity and cos(e) = 1 - e^2, sin(e) = e. I don't know how to justify these values other than the power series identities for sin and cos...

So st(1/e (sin(x+e)-sin(x))) = st(1/e (sin(x)cos(e)+cos(x)sin(e)-sin(x)) = st(1/e (sin(x)(1-e^2)+cos(x)e - sin(x))) = st(1/e (sin(x) - sin(x) - e^2 sin(x) + cos(x)e)) = st(e sin(x) + cos(x)) = cos(x)

"cos(e) = 1 - e^2, sin(e) = e. I don't know how to justify these values other than the power series identities for sin and cos..."

Isn't that from the definition of cos and sin, even geometrically?

The version of rigorous infinitesimals I've seen didn't let you have these identities, because e^2 != 0 (because it still maintains the field axiom xy = 0 => x=0 V y=0); but the argument still goes through by carrying the whole power series in place of these simplifications – you can write the higher order terms as e*f(x, e) and drop them when you evaluate st(...).

You can get the relationship:

1 - x^2 < cos(x)^2 < 1 / (1 + x^2)

from ordinary trigonometry, although you can't just do this with nilsquare infinitesimals; you need a more sophisticated setup.

Infinitesimals are commonly used in scientific computing (see forward mode automatic differentiation).

Note though, that nonstandard analysis isn't compatible with more "intuitionistic" https://en.wikipedia.org/wiki/Axiom_of_determinacy (in place of axiom on choice), which free you from Banach–Tarski paradox and have some other appealing properties.

On the contrary, in an intuitionistic setting you can use https://en.wikipedia.org/wiki/Synthetic_differential_geometr... and https://en.wikipedia.org/wiki/Smooth_infinitesimal_analysis which aren't nearly as easy to phrase classically. (Sure you can phrase things in terms of toposes, but that's just a roundabout way of saying that you're operating in a constructive setting.)

Can do it in pure ZF:

https://www.youtube.com/watch?v=YE68yptMMeQ

https://u.cs.biu.ac.il/~katzmik/spot.html