I’m learning some basic ZF set theory (from Tao’s Analysis book) and am wondering about the axiom of specification.
It states that given a set $X$ and a proposition $P(x)$ that is true or false for all $x \in X$, then $\{x \in X : P(x) \text{true}\}$ is a set.
Suppose $\mathbb{N}$ is axiomatically a set. Then the book says I can construct the set $\{0,1,2,3\}$ via $\{x \in \mathbb{N} : x < 4\}$. But what about a subset like $\{1,3,7,8,9,999\}$? I can’t see how to use specification for this without assuming circularly that it’s already a set.
As mentioned in the comments, Specification (or Separation) will work via the formula $$x=a_1\vee ...\vee x=a_n.$$ But in order to apply this we also need a given set $A$ which we already know contains each of the $a_i$s. In this context we have such a set - namely, $\mathbb{N}$ - but leaves open the question of whether arbitrary finite collections of sets are sets.
To show that the answer is yes, we'll actually use a different approach: Pairing and Union. For example, suppose I have sets $a_1,a_2,a_3,a_4, a_5$. Then:
For each $i$, Pairing gives us $\{a_i,a_i\}=\{a_i\}.$
We now repeatedly apply Pairing and Union:
By Pairing applied to $\{a_1\}$ and $\{a_2\}$, we get $\{\{a_1\},\{a_2\}\}$; applying Union to that gives $\{a_1,a_2\}$.
By Pairing applied to $\{a_1,a_2\}$ and $\{a_3\}$, we get $\{\{a_1,a_2\},\{a_3\}\}$; applying Union to that gives $\{a_1,a_2,a_3\}$.
Continuing in this way we ultimately get $\{a_1,...,a_n\}$.
There's actually a bit of subtlety here with either approach: when we sit down to make this rigorous what we wind up doing is using proof by induction in the metatheory to show that ZF proves each of a family of sentences - in the original case the family of sentences of the form $$\forall x_1,...,x_n\in\mathbb{N}\exists y\forall z(z\in y\iff (z=x_1\vee...\vee z=x_n))$$ for $n$ finite, and in the more general case the family of sentences of the form $$\forall x_1,...,x_n\exists y\forall z(z\in y\iff (z=x_1\vee...\vee z=x_n))$$ for $n$ finite (this is a more precise way of saying "For all $x_1,...,x_n$ the set $\{x_1,...,x_n\}$ exists"). We're not constructing a single proof in ZF here.
So is there a "purely internal" version of this? Well, when we try to precisely formulate the statement "Every finite subcollection of a set is a set" in ZF, what we get (since "finite" means "in bijection with some natural number") is "For every $n\in\mathbb{N}$, every set $X$, and every function $f$ with domain $n$ each of whose outputs is in $X$, the range of $f$ is a set." This is an immediate consequence of Separation ("is in the range of $f$"), and an even more immediate consequence of Replacement (since then $X$ doesn't even enter into the situation). But this isn't actually a very useful thing to prove, since constructing the required function $f$ won't be any easier than outright building the desired set itself.