Since the set N (or ω) of natural numbers is the minimal inductive set, a natural definition of N would be that it is the intersection of all inductive sets:
N = { x : (∀I)(I is inductive → x ∈ I) }
However, this does not fit the comprehension scheme which only allows the formation of sets of the form {x ∈ A: φ(x)} for some set A and formula φ(x). The trick is to pick an arbitrary inductive set I0 and then define
N = { x ∈ I0 : (∀I)(I is inductive → x ∈ I) }.
Note that this is equivalent to the above definition since every set x that belongs to every inductive set necessarily belongs to the particular inductive set I0, no matter what I0 we picked.
This situation is not unique to the set of natural numbers. The same problem occurs when trying to define the empty set via comprehension. A natural definition is
∅ = { x : x ≠ x },
but this is not admissible since x is not restricted to a set. Again, we can pick an arbitrary set A and define
∅ = { x ∈ A : x ≠ x }.
This is of course independent of our choice of A since ∅ is contained in every set.
Why are such arbitrary choices necessary? This is because the language of set theory is a purely relational language: there are no constants and functions, only variable symbols together the relations = and ∈. Therefore there is no closed expression for any set whatsoever!!!
The sets ∅ and ω are merely informal notations for specific sets. Even the set-builder notation is informal. Remember that the notation
{ x ∈ A : φ(x) }
is not part of the language of set theory, it is merely a convenient notation for the unique set B such that
(∀x)(x ∈ B ↔ x ∈ A ∧ φ(x)).
As explained in this answer by Joel Hamkins, it is perfectly reasonable to use set-builder notation, or the constants ∅ and ω within set theory. It can be shown that adding formal function or constant symbols for these is a conservative extension of the axioms ZF/ZFC for set theory. Indeed, every model of ZF has a unique interpretation for these symbols. In practice, set theorists freely use such symbols and notations without worry, since they could always expand the language to include these if they were so inclined.
In the end, the decision by Hrbacek & Jech to define N using the informal notation
N = { x ∈ I0 : (∀I)(I is inductive → x ∈ I) }
is that this is correct and it also implicitly justifies the existence of the set N, whereas the even more informal
N = { x : (∀I)(I is inductive → x ∈ I) }
is also correct but it does not justify the existence of N since it does not fit the comprehension scheme.
