Set-Builder Notation: "$A$ is a set a of natural numbers that contains $n_0$ and contains $k+1$ whenever it contains $k$" As the title suggests, I wondered if there was a way to encode a set with the following properties using set-builder notation:

$A$ is a set a of natural numbers that contains $n_0$ and contains $k+1$ whenever it contains $k$

At first I thought that I could invoke the Axiom of Separation/Specification:
$A=\{x \in \mathbb N | x = n_0 \lor x-1 \in A\}$
but I have become wary of this attempt because of the self-referencing that takes place in second portion of the disjunction... $x-1 \in A$. My understanding is that this is not allowed.
For the sake of argument, assume that $n_0 \gt 1$. It therefore seems as though this proper subset of $\mathbb N$ cannot be created using the Axiom of Separation/Specification (at least as written above).

Interestingly, one can prove that a set adhering to the properties "contains $n_0$ and contains $k+1$ whenever it contains $k$" necessarily contains all elements of $\mathbb N \geq n_0$. At this point, one could certainly write $A$ in set-builder notation (in a way that allows the Axiom of Separation/Specification to be invoked) as follows:
$A=\{x \in \mathbb N | x \geq n_0\}$.
At quick glance, the following seems to be true:
$\forall x \in A (x = n_0 \lor  x-1 \in A) \leftrightarrow \forall x \in A (x \geq n_0)$ (Edit: This statement actually depends on $A$...i.e. it can be true, but it can also be false)
So I guess my question is:
Why can one FOL representation of the properties of $A$ be "accepted" by the Axiom of Separation/Specification but another semantically equivalent FOL representation of the properties of $A$ be "rejected"
 A: The reason why $A=\{x\in \mathbb{N}:x\ge n_0\}$ is an acceptable definition while $$A=\{x\in \mathbb{N}:x=n_0\vee (x>0\wedge x-1\in A)\}$$
is not is just that with self-reference in general, it's not clear there will be exactly one (if any) set satisfying the definition.  For example, consider $A=\{x\in \mathbb{N}:x\notin A\}$. If $A$ exists, is $0\in A$? is $0\notin A$?
So why can we sometimes get around this?  Well, any definition needs to do two things:

*

*it needs to have something that satisfies it, and

*it needs to have only one thing satisfy it.

So any definition of a set $A$ shouldn't include $A$ because it often won't uniquely describe anything. Sometimes it can, but it's not obvious. $\{x\in \mathbb{N}:\varphi(x)\}$, on the other hand, always uniquely describes something because it's merely talking about properties of elements of $\mathbb{N}$, not the resulting set we (in some sense) haven't formed yet.  So this is why the axiom is phrased the way it is.
The property you describe isn't a definition because (2) isn't true, the $A$ you want isn't unique: $\mathbb{N}$ also has $n_0\in\mathbb{N}$ with $k\in\mathbb{N}\rightarrow k+1\in\mathbb{N}$.  But the fact that something satisfies this property is a big deal, because that means (1) works for many things, and to get (2) we just need to pick out one of them.
For you, the key point that makes this work is that the property you've stated is a closure property: you want $n_0\in A$, and $A$ to be closed under the operation $k\mapsto k+1$.  In this way, you want to define $A$ to be the least (i.e. $\subseteq$-least) set with with that property.  Because we know some such sets exist, we can pick out the least one just by considering
$$A=\bigcap\{X\subseteq\mathbb{N}:X\text{ has the property}\}\text{.}$$
In general, we can do this with closure properties so long as we have a starting point: we should be able to generate $A$ just by taking our starting point and continually applying the operations to all of its elements infinitely many times until we don't need to anymore.
