The following line well-defines a family of subsets $\{S_i\}_{i\in\mathbb N}$ of $\mathbb N$:

$n\in S_i$ iff $n=i$ or $\exists j<i$ such that $n\in S_j$.

The following line does not:

$n\in S_i$ iff $n=i$ or $\exists j$ such that $n\in S_j$.

Now what about the following line? I suspect that it does well-define a family of subsets, but I'm not sure how one would prove it; some clever application of the Recursion Theorem or Godel's fixed point theorem perhaps?

$n\in S_i$ iff $n=i$ or $\mbox{Prov}_{PA}(\exists j\mbox{ such that }n\in S_j)$

And similarly

$n\in S_i$ iff $n=i$ or $\exists j$ such that $\mbox{Prov}_{PA}(n\in S_j)$

In both cases $\mbox{Prov}_{PA}$ is a predicate symbol for provability from $PA$, and $\mbox{Prov}_{PA}(\phi)$ is shorthand for $\mbox{Prov}_{PA}(\ulcorner\phi\urcorner)$ where $\ulcorner\phi\urcorner$ is a Godel number of $\phi$. I suspect the latter two lines, suitably formalized (how?), do well-define sets $S_i$: because the ill-founded part (references to arbitrary $S_j$) are inside of $\mathrm{Prov}_{PA}$, they are not actually statements about $S_j$ at all, but only about what $PA$ proves about $S_j$ (which suggests using the Recursion Theorem).

In the literature, would it be acceptable to write either of the latter two lines while brushing aside the details?

The following line well-defines a family of subsets $\{S_i\}_{i\in\mathbb N}$ of $\mathbb N$:

$n\in S_i$ iff $n=2i$ or $\exists j<i$ such that $n\in S_j$.

The following line does not:

$n\in S_i$ iff $n=2i$ or $\exists j$ such that $n\in S_j$.

Now what about the following line? I suspect that it does well-define a family of subsets, but I'm not sure how one would prove it; some clever application of the Recursion Theorem or Godel's fixed point theorem perhaps?

$n\in S_i$ iff $n=2i$ or $\mbox{Prov}_{PA}(\exists j\mbox{ such that }n\in S_j)$

And similarly

$n\in S_i$ iff $n=2i$ or $\exists j$ such that $\mbox{Prov}_{PA}(n\in S_j)$

In both cases $\mbox{Prov}_{PA}$ is a predicate symbol for provability from $PA$, and $\mbox{Prov}_{PA}(\phi)$ is shorthand for $\mbox{Prov}_{PA}(\ulcorner\phi\urcorner)$ where $\ulcorner\phi\urcorner$ is a Godel number of $\phi$. I suspect the latter two lines, suitably formalized (how?), do well-define sets $S_i$: because the ill-founded part (references to arbitrary $S_j$) are inside of $\mathrm{Prov}_{PA}$, they are not actually statements about $S_j$ at all, but only about what $PA$ proves about $S_j$ (which suggests using the Recursion Theorem).

In the literature, would it be acceptable to write either of the latter two lines while brushing aside the details?