papalex on Nostr: In internal set theory (IST) the idealization principle (I) implements the intuition ...

In internal set theory (IST) the idealization principle (I) implements the intuition that we can only test a finite number of objects at a time. A consequence of (I) is that any infinite set must contain a non-standard element and in particular there exists a non-standard number in ℕ (see [1] end of pg. 5). So to get rid of the infinite numbers in ℕ we would have to add further aximos (invoking the external standard predicate), making the standard model of PA ℕˢᵗ a non-standard model of PA within IST.

I think the intuition is somewhat natural at first and then makes an interesting twist: We do not tell maths what it may do, but only make axioms about what we can check, this gives us the idealization principle: For any property we can always only check the property on finite elements, which is sort of a pragmatic filter of what we mean by that property. However, the real work of (I) is then that it asserts: If (see LHS of (I)) for any finite standard set 𝑥' there exists a 𝑦(𝑥') such that the property holds (made the 𝑥' dependence explicit), then (I) asserts that there also exists a fixed 𝑦 such that the property holds wrt all standard 𝑥.
So the real work of this axiom is in making 𝑦 independent of 𝑥'. I think this is a really nice way of making ∞ and related infinitesimals operational.

So the short form intuition could be:
IST enforces that the sequence 𝑆ₙ={0,1,...,n} with 𝑆ₙ<𝑆ₙ₊₁ must have a supremum with 𝑆ₙ<S_ω for all 𝑛∈ℕˢᵗ and the identification 𝑛≃𝑆ₙ survives this limit. the full set ℕ is the "completion" that the sequence necessitates, because no standard bound suffices.

[1]: https://web.math.princeton.edu/~nelson/books/1.pdf