internal in nonstandard analysis

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.