Infinitesimals

I'm currently reading this article on the history of the infinitesimals. My interest in the subject comes from a subject I've mentioned earlier: automatic differentiation. Implementing infinitesimals as an extension to the real numbers is straightforward in modern programming languages but for some reason it's not well known. They give a nice efficient way to compute derivatives of functions and remove removable singularities from functions.

One of the earliest ways to construct the real numbers from the rationals was as an equivalence class of sequences of rational numbers. Two sequences are equivalent if the difference tends to zero. In Non-Standard Analysis, developed by Robinson, this definition is tweaked slightly so that the sequences are equivalent if they are equal on a 'large' subset of the sequence. The trick is to define 'large' appropriately leading to the concept of an ultrafilter. This results in a set *R which is an extension of the usual set of reals R but also contains infinitely small and large numbers. There's also a nice 'metatheorem' that goes with this construction showing that 'reasonable' theorems about *R are also theorems about R. This basically gives us license to use infinitesimals in our proofs and still be sure that our results make sense as propositions about real numbers. So many of Leibniz's old 'proofs' using infinitesimals, say, can now be reinterpreted as perfectly valid proofs.

Anyway, you don't need all this machinery to do automatic differentiation, just an algebraic structure with elements whose square is zero.

Incidentally, Gödel used ultrafilters to 'prove' the existence of God.