Define
$$0:= \emptyset$$ $$1:= \{\emptyset\} =\{0\}$$ $$2:= \{\emptyset, \{\emptyset\}\}=\{0,1\}$$ $$\vdots$$ $$n:= \{0,1, \dots, n-1\}$$
And put $\mathbb{N}:= \{0,1, \dots\}$.
Questions:
(1) Doesn't this kind of 'recursive' definition give us what we want? It seems like we need $\mathbb{N}$ to define a recursion, so this seems circular?
(2) How can I formally show that $\mathbb{N}$, partially ordered by the inclusion, is in fact well-ordered?
Attempt:
Let $\emptyset \neq Y \subseteq \mathbb{N}$. Fix $y \in Y$. If $y= y_0$ is a minimum, we are done. If not, there is an element $y_1< y_0$ with $y_1 \in Y$. If $y_1$ is a minimum, we are done. Otherwise, there is $y_2 < y_1$ with $y_2 \in Y$. If this process does not stop, we obtain infinitely many elements in $\mathbb{N}$ smaller than $y$, which should be impossible, but I think I'm making circulaar reasonings here as well.
Yes, the way you define it make it seem like you're using the natural numbers to define the natural numbers. But it's not really the case.
We are not defining the natural numbers one by one. Instead we give a recursive definition: $0=\varnothing$; if $n$ was defined, $n+1=n\cup\{n\}$; $\Bbb N$ is the smallest collection containing $0$ and closed under this definition.
So we are not appealing to the existence of the natural numbers per se, but rather we are using the axioms that prove the recursive definitions "work out". In the case of ZF-like set theories, this is mainly Replacement (and for this construction also pairing, union, and as always extensionality).
As for your second question, show that if $Y$ is a non-empty set of natural numbers, then $\bigcap Y=\min Y$.