Csdrhrt

I have some questions about ZF set theory. I was reading some courses about the construction of $mathbb{N}$, $mathbb{Z}$, $mathbb{Q}$ and $mathbb{R}$ and something disturbes me a bit.

I saw things like :
$$mathbb{N} = {n mid n in I text{ for every inductive set } I},$$
or
$$mathbb{Q} = left{frac{p}{q} mathrel{}middle|mathrel{} p in mathbb{Z}, q in mathbb{N}^{ast}right},$$
and I was wondering if it is really correct to write these sets in such a way.

If I'm not wrong, in ZF, if we consider a set $A$, we can always construct a set $B$ such that :
$$B = {x in A mid phi(x)} , $$
where $phi$ is a formula in ZF language (I'm not really a specialist in logic, but I get the idea of "formula") and it is called the "axiom schema of specification". But we cannot construct set of the form :
$${x mid phi(x)}$$
with this axiom schema right (otherwise, we can find things like Russell's paradox) ?

Now, if we take for example the way I wrote $mathbb{N}$ above, there are two possibilities for me :

1. This way of writing is not correct. In that case, how should we write in particular the set $mathbb{N}$ ? I read some things about von Neumann's construction of $mathbb{N}$ and about Peano's axioms, but I didn't see exactly a way to "write succinctly" $mathbb{N}$...




2. This way of writing is correct. In that case, which axiom of ZF theory is used to write for example $mathbb{N}$ or $mathbb{Q}$ in that way ?

Thank you for your help.

The axioms of ZF only talk about abstraction of the form ${xin X:|:varphi}$, true; but that doesn't mean we can't write the same set another way. In particular, ${x:|:varphi}$ is still a perfectly acceptable way to write something when you know it's a set. It's worth noting, since writers and instructors don't always make this clear, that ${x:|:xin Xwedgevarphi}$ is exactly the same thing as ${xin X:|:varphi}$, so nothing specifically rides on whether the membership claim is in that first space. The important thing is that ${x:|:varphi}$ is a set exactly when there's an $X$ such that $xin Xwedgevarphiiffvarphi$, which is exactly what's happening in the two examples you give.

In the case of $mathbb{N}$ we are given by the ZF axioms that there is an inductive set $I$; the elements that are in every inductive set will also all be in $I$, so there's no difference in the between the extension of "$x$ is a member of every inductive set" and "$xin I$ and $x$ is a member of every inductive set."

In the case of $mathbb{Q}$, as it's written above it's a little bit question-begging. We might write it that way if we're working in $mathbb{R}$ and defining the rational numbers in $mathbb{R}$ by the naturals and integers in $mathbb{R}$; in which case because we've taken two sets of reals and applied an operation defined only on the reals, under which the reals are closed, "$x$ is a quotient of an integer by a non-zero natural" and "$xin mathbb{R}$ and $x$ is a quotient of an integer by a non-zero natural" once again refer to exactly the same collection.

You are right to observe that in a fully formal proof, you would probably prove existence via first using that ${x:|:xin Xwedgevarphi}$ is an instance of separation, and then proving that $xin Xwedgevarphiiffvarphi$ to justify later use of ${x:|:varphi}$; but in practice it's usually obvious (or presumed obvious) how to supply the appropriate $X$ if we really need to, so we skip it and just write the more natural form.