Syntax for complex restrictions on domains of quantifiers

Question

In restricting the domains of the universal and existential quantifiers, all of the examples that I've seen take the form: $\forall x \in X[P(x)]$. But what is the correct syntax for more complicated domain restrictions such as $x \in \mathbb{R}$ and $x < 0$?

Consider an assertion like: "The equation $x^2 + a = 0$ has a real root for any negative real number, a."

I know that this can be expressed as: $\forall a \in \mathbb{R} \exists x[a < 0 \implies x^2 + a = 0]$.

Can it also be expressed as: $\forall a \in \mathbb{R} \land a < 0 \exists x[x^2 + a = 0]$?

What about $\forall a \in \mathbb{R}, a < 0 \exists x[x^2 + a = 0]$?

Thanks for the help.

Answer 1

"The equation $x^2+a=0$ has a real root for any negative real number $a$"

reads :

"for every $a$, if $a$ is real and negative, then the equation $x^2+a=0$ has a real root",

i.e. :

"for every $a$, if $a$ is real and negative, then there is a $b$ such that $b$ is real and $b^2+a=0$."

Now we can easily symbolize it :

$\forall a \ [(a \in \mathbb R \land a < 0) \to \exists b \ (b \in \mathbb R \land b^2+a=0)]$,

or equivalently :

$\forall a \ \exists b \ [(a \in \mathbb R \land a < 0) \to (b \in \mathbb R \land b^2+a=0)].$

Note. If we want to use the restricted quantifier notation, we can rewrite is as follows :

$\forall a_{(a \in \mathbb R \land a < 0)} \exists b_{(b \in \mathbb R)} \ (b^2+a=0),$

or, in an "intermediate" version as :

$\forall a_{(a \in \mathbb R)} \exists b_{(b \in \mathbb R)} \ (a < 0 \to b^2+a=0).$

IMO, we have not gained so much regarding readibility.