$$A = \{ a \in \mathbb{Q} : a^2 < 2 \text{ or } a < 0 \}$$

$$B = \{ b \in \mathbb{Q} : b^2 \geq 2 \text{ and } b > 0 \}$$

To give the cut for $\sqrt{2}$ as shown above, we are relying on the formula $x^2$. To me, this means that we are relying on the axiom schema of specification to partition $\mathbb{Q}$ into the subsets $A$ and $B$ using the formula $x^2$.

**Question(s):**

What happens for noncomputable reals where there is no formula with which to apply the axiom schema of specification when partitioning $\mathbb{Q}$? More directly, if there is no formula in the language of set theory to invoke the axiom schema of specification and create the partition, how is it we assert that there is a Dedekind cut consisting of $A$ and $B$?

My (likely flawed) idea is that the axiom of powerset is required to assert the existence of $\mathcal{P}(\mathbb{N})$ within a model of ZF set theory because the axiom schema of specification cannot be applied to the natural numbers to assert the existence of noncomputable subsets of $\mathbb{N}$. If it could so as to ensure that every noncomputable subset of $\mathbb{N}$ existed within the model, then I think the axioms of union and pairing would also allow for the existence of $\mathcal{P}(\mathbb{N})$ within the model even if the power set axiom where omitted from ZF.

* Should anyone be unfamiliar, a Dedekind cut of the rational numbers is given by partitioning $\mathbb{Q}$ into the sets $A$ and $B$ where $A$ is nonempty, $A \neq \mathbb{Q}$, $A$ is closed downwards, and $A$ does not contain a greatest element. Where each real number results in a unique partition of $\mathbb{Q}$ into $A$ and $B$, we generally assert that Dedekind cuts are a method of constructing the real numbers from the rationals.