Internal set theory is a theory introduced by Edward Nelson, notably an ultrafinitist. it introduces a new function std: * -> Bool. You have to just know if something is standard or not. This may sound bad, but is actually a brilliant way of venting complexity. Figuring out if something is standard is obvious.

1 is standard.

pi is standard.

1 + epsilon is nonstandard if epsilon is infinitesimal.

a hyperfinite number is nonstandard.

Because this is a syntactic theory, it can’t really distinguish infinitesimal and unlimited elements from regular ones. But we can provide the semantics and just know if something is standard or not.

as long as we stick to internal formulas, this extension transfers to the original axioms.

a function is internal if it treats standard and nonstandard elements the same.

example:

1 + x is internal. no distinction is made on what x is.

(1 if standard else 0) is external aka not internal.

no recursive calls can lead to anything with the term ‘standard‘ in it. in practice, this is also fine.

this trick of interpreting syntax in a larger domain of elements (sometimes called abstract interpretation) is also how dual numbers in autodiff work too. the hyperreals are the dual numbers’ bigger sister.

amazingly, griewank’s autodiff book only mentions nonstd analysis once, for like 2 sentences.

James Bradbury if you’re reading this learn some stuff about the hyperreals and make an autodiff system that can differentiate functions that aren’t even continuous.

New to LessWrong?

New Comment
1 comment, sorted by Click to highlight new comments since: Today at 6:04 AM

You could plug in  and take the standard part as the answer and each power of  to be that order of derivate.

If one is already dealing in infinidesimals the fact of separate archimedian fields means the standard part does not mix with the infinidesimals as long as the functions of interest are tame "standard only" mechanics (ie real polynomials and such)

It could also be interesting to use the big side to maybe cancel some unwanted infinities. That is  is no fun as a end answer and  is no fun as answer but  where y and z are smaller than standard so it has a usable standard part answer of 2.