I was studying foundations of arithmetic, and reasoning about the set of natural numbers. In Peano arithmetic, we can talk about $\mathbb{N}$ without defining it explicitly or trying to prove its existence (or simply not talk about $\mathbb{N}$ at all), since that is not the purpose of the system.
But I was thinking about a way to define $\mathbb{N}$. Some sources try to do that by postulating some axiom asserting the existence of an inductive set, and extracting the naturals from it in a weird way (perhaps weird because the notation seemed strange to me).
My reasoning, however, is as follows:
We first define a set $I$ as the set of all sets $S$ that satisfy the conditions $0\in S$ and $\forall n[(n\in S)\rightarrow(n^{+}\in S)]$:
$$[S\in I]\Leftrightarrow[(0\in S)\land\forall n[(n\in S)\rightarrow (n^{+}\in S)]]$$
Finally, we define $\mathbb{N}$ as the intersection of all the sets in $I$:
$$\mathbb{N}:=\bigcap_{S\in I}(S)$$
My question is whether this definition is correct or not, and whether it is circular somehow, specially in the condition with quantification over $n$:
Are we already assuming the universe of discourse as $\mathbb{N}$ in the quantified condition?
Some insights I had so far:
It appears that the condition could be replaced with $\forall n\in S(n^+\in S)$, but I'm not sure if this is different though.
Correct me if I'm wrong: in standard set-theory, we assume the universe of discourse to be all sets, so I think that the universe is not necessarily a set, otherwise we could reach a paradox. So maybe the universe of discourse of the quantified condition is not necessarily $\mathbb N$. I wonder if we can talk about the natural numbers collectively without referring to the set that we are trying to define, or if we need a larger superset containing them, but not only them, for the definition to hold.
Yes, $\forall n \in S(n^+ \in S)$ and $\forall n ((n \in S) \rightarrow (n^+ \in S))$ are equivalent (and usually the first is just short way to write the second).
Property you use ($0 \in S \wedge \forall n \in S(n^+ \in S)$) is called "inductive" (we say "$S$ is inductive set"). But your $I$ is ill-defined: there is no set of all inductive sets (there are too many inductive sets).
However, in set theory there is axiom of infinity, that says there is at least one inductive set. Let $A$ be some inductive set, and let $I_A$ be family of all inductive subsets of $A$ (including $A$ itself). Then we can define $\mathbb N$ as $\bigcap\limits_{S \in I_A} S$. We need to prove that this intersection doesn't depend on choice of $A$, but it's easy.
"Universe" in such context is usually considered to be all sets, and we need to find $\mathbb N$ among all sets. Peano arithmetic doesn't speak about $\mathbb N$ directly, but when we speak about models of arithmetic, we need $\mathbb N$ as a set we can define functions and subsets on.