Nonstandard analysis introduces a brave new world of mathematical entities.
It also has a number of distinctive structural features and principles
of reasoning that can be used to explore this world Already in the context
of subsets of *IR we have examined several of these principles: permanence,
internal induction, overflow, underflow, saturation. Now we will see that in
the context of a universe embedding U U' they occur in a much more
powerful form, since they apply to properties that may refer to any internal
entities in U'. We assume from now on that we are dealing with such an
embedding for which *N-N =/= 0.
15.1 Permanence Principles
Several times we have discussed situations in which a property of a certain
kind that holds on a particular type of set must continue to hold on some
larger set (cf. Sections 7.10 and 11.9). Here is a statement of how such
situations occur in U':
Theorem 15.1.1 Let cp(x) be an internal.C Jy-formula with only the variable
x free. Then
(1) (Overflow) If there exists k E N such that cp( n) is true for all n E N
with k ::; n, then there exists K E *No-N such that cp(n) is true for
all n E *N with k::; n::; K.
192 15. Permanence, Comprehensiveness, Saturation
(2) (Underflow) If there exists K E *No-N such that cp(n) is true for all
n E *N-N with n ::::; K, then there exists k E N such that cp(n) is
true for all n E N with k ::::; n.
(3) If cp(a) is true for all hyperreals a that are infinitely close to some
b E *JR., then cp(a) is true for all hyperreals a that are within some
positive real distance of b.
(4) lfcp(a) is true for arbitrarily large (resp. small} a E JR., then it is' true
for some positive (resp. negative) unlimited hyperreal a.
(5) If there exists r E lR such that cp(a) is true for all a E JR. with r ::::; a,
then there exists a positive unlimited b E *JR. such that cp( a) is true for
all a E *JR. with r ::::; a ::::; b.
Proof.
(1) We adapt the proof of Theorem 11.4.1. Formula (k < x) 1\ •