In a follow up to this answer to a previous question, I want to see if I have a correct understanding now of the semantic interpretation of the axiom of restricted separation. As a side note I'm also interested in how to avoid ambiguity when writing about models of set theory (like sets definable in the structure versus sets as the actual objects of the theory, as well as the use of $\in$ both formally and informally in the metalanguage.) Ok. This is what I think
Let $\mathcal{M}$ be a structure in the language of set theory. Then the axiom of restricted separation implies that for any formula $\phi(x)$ and $\mathbf{a}$ in $|\mathcal{M}|$ that if $S\subset |\mathcal{M}|$ is such that for all $x$: $$x \in S \; \iff \; \mathcal{M} \models \phi(x) \wedge x\in \mathbf{a}$$ Then there exists a $\mathbf{b}$ in $|\mathcal{M}|$ such that for all $x$: $$x\in S \; \iff \; \mathcal{M} \models \; x \in \mathbf{b}$$ Is that correct? Thanks.
That's basically correct (although I'd strongly encourage you to include parameters in your formulas; while technically unnecessary, that's nontrivial). However, there's no reason to introduce $S$: just say "there is some ${\bf b}\in\vert\mathcal{M}\vert$ such that $$\{x\in\vert\mathcal{M}\vert: \mathcal{M}\models x \in{\bf b}\}=\{x\in\vert\mathcal{M}\vert: \mathcal{M}\models x\in{\bf a}\wedge \varphi(x)\}."$$ Incidentally, note that the set on the left hand side is often conflated with ${\bf b}$ itself; obviously this is technically improper, but it is common. (When multiple models with possibly-overlapping domains are considered, I find notation like "${\bf b}^\mathcal{M}$" to be a happy medium between confusion and tedium.)