I want to prove this statement: "there exists a real number $x<0$ whose square is 2". This could mean $$ \exists x\in \mathbb{R}, x < 0 \text{ and } x^2=2$$ or $$ \exists x\in \mathbb{R}^-, x^2=2$$ I'm having trouble dissecting where the "domain of discourse" ends and where the "predicate" begins. Is the domain of discourse $\mathbb{R}$, or $\mathbb{R}^-$? Or can it even be taken to be "everything", so the statement becomes $\exists x, P(x)$, where $P(x)$ says "$x$ is a negative real whose square is 2"? (Doesn't this have something to do with Russel's paradox?)
Now, suppose I want to attempt a proof by contradiction and assume the negation, should I use $$\forall x \in \mathbb{R}, x \geq 0 \text{ or } x^2\neq 2 $$ or $$\forall x \in \mathbb{R}^-, x^2\neq 2 $$
Any help on the proof is also appreciated (I'm aware of the direct proof of letting $c = \inf \{z \in \mathbb{R}| z^2 =2\}$ and showing $c^2=2$, but I want to see if it's possible to do it without constructing $\sqrt 2$).
In first order logic, the phrase $\exists x\in \mathbb R$ is not actually an official phrase of the language. All actual statements involve just bare quantifiers $\exists x,$ and the domain of discourse is a property of the interpretation. For instance in a first order language with relation symbol $<$ and constant symbol $0$ we could write $\exists x(x<0)$ and then we could interpret it as a statement about real numbers, or about natural numbers, or whatever else where we interpret $<$ and $0$ as the usual relation and number in whichever domain.
This does not precluded us from informally writing $\exists x \in \mathbb R(x<0)$ to emphasize that we are interpreting the statement in the reals. More importantly, 'bounded quantifiers' like this are often used in an official capacity as abbreviations. For instance, say we're working in the reals and by some means we can define a predicate identifying the naturals within the reals. Then we can write such a predicate $x\in \mathbb N$. Then $$\exists x\in \mathbb N(x<0)$$ can be regarded as an abbreviation for the actual formal sentence $$\exists x(x\in \mathbb N \land x <0)$$ where again, we're interpreting in the reals here.
So in other words, you're right. It's a fuzzy line. For your purposes here, I wouldn't worry too much about the difference between $\exists x\in \mathbb R(x<0\land x^2=2)$ and $\exists x\in \mathbb R^-(x^2=2)$ or what the ultimate domain of discourse is. (As I mentioned in a comment, it could be set theory, so that $\mathbb R$ is a defined set and thus $x\in \mathbb R$ is a defined property and we're using bounded quantifiers as an abbreviation). It's much more important that you understand what the negation says logically than niceties about notation. It's clear that, whatever the formality, $\forall x\in \mathbb R( x\ge 0 \lor x^2\ne 2)$ and $\forall x \in \mathbb R^- (x^2\ne 2)$ mean the same thing and are logically the negation of the first statement. So this is what you need to prove.
(By the way, for a bounded universal quantifier, $\forall x \in A (P(x))$ abbreviates $\forall x (x\in A \to P(x))$ or equivalently $\forall x (x\notin A \lor P(x)),$ so you can see accords with what you wrote down.)