Intuition behind the Idealization Axiom of Internal Set Theory Wikipedia describes the idealisation axiom as follows: "The statement of this axiom comprises two implications. The right-to-left implication can be reformulated by the simple statement that elements of standard finite sets are standard. The more important left-to-right implication expresses that the collection of all standard sets is contained in a finite (non-standard) set, and moreover, this finite set can be taken to satisfy any given internal property shared by all standard finite sets."
Given that standard sets are supposed to represent the finite sets that we could plausibly construct, it makes sense that there would only be a finite number of them and that their union would therefore be finite. However, I can't understand why we can choose this set such that it satisfies any internal property shared by all standard finite sets. Why is this the case?
 A: I think it's a bit worse than that.  The idealization axiom is equivalent to the existence of a finite set containing all standard  sets AND plenty of standard sets are infinite, for example, N, Q, R, etc.  All the classically constructed sets that are infinite are still infinite in IST.  This axiom is something I have also been thinking about.  It seems to receive brief discussion in the literature that I have read.  It's the sort of thing that if you started a presentation with that sentence, folks would certainly want more information.
The finite set (call it A) containing all standard sets cannot itself be internal because it uses the predicate standard.  So it must be an external set.  I know that IST isn't able to access external sets (though I can't make that precise) very well.  Given that we measure whether a set is finite or infinite with functions I wonder if the issue is whether the function exists.  That would require looking at subsets of AxA but that product isn't necessarily guaranteed to exist because transfer only gives us products of standard sets.  So can we even construct an injection from A to A in order to determine that it is necessarily surjective?
EDIT: I'm working on these ideas too and so have been thinking about this some more. Within IST the 'usual' natural numbers or 'usual reals' aren't sets and so we might relax our surprise that there is a finite set containing them.  Cardinality, I read somewhere, is necessarily an external concept because it depends on the sets available in the model.  Additionally, I wonder if there is some equivocation of the use of "finite" which in our everyday language doesn't necessarily match up with the mathematical definition which can be "not infinite" which allows for considerable quantities to be finite (the number of books in the Library of Babel by Jorge Borges) or Graham's number, even those these numbers are...I'm not sure how to say, larger than anything we can reasonably conceptualize.
