I'm wondering how (or if) sets can be proven to be unique within certain subsystems of second order arithmetic (such as $\mathbf{ACA}_0$).
I was thinking that we would have a kind of extensionality as a logical axiom such as: $\forall X\forall Y\forall n[[n\in X\iff n\in Y]\implies X=Y]$, but then I realized we cannot even say ''$X=Y$'' in the language of second order arithmetic.
The reason I am asking is because Simpson says "Within $\mathbf{ACA}_0$, we define $\mathbb{N}$ to be the unique $X$ such that $\forall n(n\in X)$". I understand how we can say such an $X$ is unique in a model of $\mathbf{ACA}_0$ (since we have extensionality in the metatheory), but I'm not sure how uniqueness of $X$ follows from within $\mathbf{ACA}_0$.
Any help is appreciated, thanks.
(By the way, I quote Simpson from page 9 of $\textit{Subsystems of Second Order Arithmetic}$. Here's the link: http://www.personal.psu.edu/t20/sosoa/chapter1.pdf)
By convention, the equality relation for sets is added to the language as a definitional extension, using the definition you gave: $$ X = Y \quad \equiv \quad (\forall n)[n \in X \Leftrightarrow n \in Y] $$
Don't get too concerned about the claim "unique" in that quote. Every set defined by an instance of the comprehension scheme is "unique" in the sense that all sets that satisfy the same defining formula have to be equal to each other in the sense of the definitional extension for set equality.
In other words (although it is somewhat trivial), $\mathsf{ACA}_0$ proves $$ ((\forall n) [ n \in Y \Leftrightarrow n = n] \land (\forall n)[ n \in X \Leftrightarrow n = n]) \Rightarrow X = Y $$ which is an abbreviation of $$ ((\forall n) [ n \in Y \Leftrightarrow n = n] \land (\forall n)[ n \in X \Leftrightarrow n = n]) \Rightarrow (\forall n)[n \in X \Leftrightarrow n \in Y] $$ That is how "unique" is expressed in second order arithmetic in this case.
I suspect that the reason Simpson mentioned uniqueness at all is that he is making a definitional extension of the set constant $\mathbb{N}$, and to do a definitional extension by a constant one must verify that the definition of the constant defines a unique object. But in this case the uniqueness is very trivial.