I know two common variants of set abstraction notation. An examples of the first variant is $$ \{\,(x, y)\in\mathbf{R}^2\,|\,x^2 + y^2 = 1\,\} $$ (it is reminiscent of the axiom schema of specification of ZF), and an example of the second is $$ \{\,(\cos t,\sin t)\,|\,t\in\mathbf{R}\,\} $$ (it is reminiscent of the axiom schema of replacement of ZF). I think that in common mathematical tradition, these two "set-builder" expressions unambiguously denote the same set.
The first form of the notation can always be used instead of the second, for example: $$ \{\,(\cos t,\sin t)\,|\,t\in\mathbf{R}\,\} = \{\,(x, y)\in\mathbf{R}^2\,|\,(\exists t\in\mathbf{R})(x =\cos t\wedge y =\sin t)\,\}. $$ However, the "translated" expression is noticeably more verbose.
Sometimes the two are combined: $$ \{\,(\cos t,\sin t)\,|\,t\in\mathbf{R}\wedge 0 < t <\pi\,\}, $$ or simply $$ \{\,(\cos t,\sin t)\,|\,0 < t <\pi\,\}. $$
The first form can be translated into the combined form without much "overhead": $$ \{\,(x, y)\in\mathbf{R}^2\,|\,x^2 + y^2 = 1\,\} = \{\,(x, y)\,|\,x^2 + y^2 = 1\wedge (x, y)\in\mathbf{R}^2\,\}. $$ The second form is just a particular case of this combined form.
In practice, the combined form of "set-builder" notation is quite convenient, but it appears to be ambiguous, unless some artificial syntactic conventions are made. For example, what set $S$ is defined in the following sentence?
Let $p = 1$ and $S = \{\,(p + q, p - q)\,|\,pq = 1\wedge p\in\mathbf{R}\wedge q\in\mathbf{R}\wedge 1 < 2\,\}$.
I see two equally legitimate values for $S$ so defined:
$S =\{(2, 0)\}$ or
$S =\{\,(x, y)\in\mathbf{R}^2\,|\,x^2 - y^2 = 4\,\}$.
Once you think of it, there is also a possibility for $S$ to be empty, if both $p$ and $q$ are viewed as parameters and if the value of $q$ happens to be different from $1$.
Does there exist an unambiguous form of the combined variant of "set-builder" notation?
In general, I do not see how to specify in an expression like $$ \{\,\{\,f(\bar a,\bar b,\bar c)\,|\,\Phi(\bar a,\bar b,\bar c)\,\}\,|\,\Psi(\bar a,\bar b,\bar c)\,\} $$ that, for example, $\bar c$ are parameters, and $\bar b$ are parameters in the inner "set-builder" but not in the outer one. (Note that though all the variables are listed in parentheses each time, it does not mean that all of them are "used": $f$, $\Phi$ and $\Psi$ may very well not depend on some of these "formal parameters.")
For reference, here is how some programming languages deal with a similar issue in list comprehension. More precisely, in programming languages there is no issue, because iterating over a collection and testing a predicate are two different operations in programming, while they are indistinguishable in mathematics.
In Haskell,
[ (m, n) | m <- [0..5], 0 <= n, n <= 5, m^2 + n^2 == 25 ]
is the list of all pairs $(m, n)$, where $m$ is an integer from $0$ to $5$,
$0\le n\le 5$, and $m^2 + n^2 = 25$. Note that this very sentence in English is ambiguous! The above expression in Haskell is only valid if $n$ is defined. The value of this expression is [(3,4)]
if the value of $n$ is 4
, but it is []
(the empty list) if the value of $n$ is 2
, for example.
A similar definition in Python will be:
[ (m, n) for m in range(0, 6) if 0 <= n and n <= 5 and m**2 + n**2 == 25 ]
However, the analogous "set-builder" notation $$ \{\,(m, n)\,|\,m\in\{0,\dotsc,5\}\wedge 0\le n\le 5 \wedge m^2 + n^2 = 25\,\} $$ is ambiguous (are "$m$" and "$n$" parameters or bound variables of this expression?).
Here is another example of an ambiguous situation: $$ \{\,\{\,x\,|\,x\in\mathbf{Z}\}\,|\,x\in\mathbf{R}\,\}. $$
For my personal needs, I start considering using my own notation $\{\ldots|\ldots|\ldots\}$ with bound variables listed in the middle, with the following formal "translation": $$ S =\{\,f(\bar x, \bar y)\,|\,\bar x\,|\,\Phi(\bar x, \bar y)\,\}\\ \equiv (\forall\xi)(\xi\in S\Leftrightarrow(\exists\bar x)(\xi = f(\bar x, \bar y)\wedge\Phi(\bar x, \bar y))), $$ where the new variable $\xi$ is distinct from all variables in $\bar x$ and $\bar y$. For example: $$ A =\{\,(\cos t,\sin t)\,|\,t\,|\,t\in\mathbf{R}\,\},\\ B =\{\,(x, y)\,|\,x, y\,|\,x^2 + y^2 = 1\wedge (x, y)\in\mathbf{R}^2\,\},\\ C =\{\,(m, n)\,|\,m\,|\,m\in\{0,\dotsc,5\}\wedge 0\le n\le 5 \wedge m^2 + n^2 = 25\,\},\\ D =\{\,\{\,f(\bar a,\bar b,\bar c)\,|\,\bar a\,|\,\Phi(\bar a,\bar b,\bar c)\,\}\,|\,\bar a,\bar b\,|\,\Psi(\bar a,\bar b,\bar c)\,\},\\ E =\{\,\{\,x\,|\,|\,x\in\mathbf{Z}\,\}\,|\,x\,|\,x\in\mathbf{R}\,\}\quad (=\{\,\{x\}\,|\,x\,|\,x\in\mathbf{Z}\,\}\cup\{\{\}\}), $$ or, alternatively, with words instead of symbols: $$ A =\{\,(\cos t,\sin t)\ \text{for}\ t\ \text{such that}\ t\in\mathbf{R}\,\}. $$ Isn't there some kind of a standard alternative?
It seems that the Z notation might be an example of what I am looking for, but at a first glance it looks incompatible with the usual mathematical "set-builder" syntax, and I wonder how standard it is.
Some comments and answers suggest to never use the same variable name for different variables, at least when their scopes are nested, thus avoiding variable shadowing altogether. IMO, such a restriction is unusual (surely uncommon in programming or formal languages), unnecessary, not easy to observe, and it would require explicit introduction of all parameters (consider omitting "Let $p = 1$" in my example above while still using "$p$" as a parameter).
Quoting the HoTT Book (page 23),
Of course, this should all be familiar to any mathematician: it is the same phenomenon as the fact that if $f(x):\equiv\int_1^2\frac{dt}{x - t}$, then $f(t)$ is not $\int_1^2\frac{dt}{t - t}$, but rather $\int_1^2\frac{ds}{t - s}$.