Variables, Quantifiers, and Logic Are statements like:
$∀x∈ℕ,∃y∈ℕ,x+y=5⇒∀x∈ℕ,x>-1$
This is just some mumbo jumbo that I wrote up but I just want to know whether the two $x$'s in the statement refer to different values and whether its legal to write it this way (in which both use the variable $x$).
 A: Yes, this is legal. Yes, they refer to different values. You can rename a bound variable (i.e. quantified over) as long as you consistently rename occurrences. However, in renaming the occurrences, we don't "look inside" other quantified subexpressions whose quantifier binds the same variable. This is called capture-avoiding substitution (or rather this is the special cases where we're substituting one variable for another.)
Your formula is equivalent to: $$\forall x\in \mathbb N.\exists y\in\mathbb N. x+y = 5 \implies \forall z\in\mathbb N. z > -1$$ or to:
$$\forall w\in \mathbb N.\exists y\in\mathbb N. w+y = 5 \implies \forall x\in\mathbb N. x > -1$$
It would, of course, be incorrect in the second example to replace the $x$ in $x > -1$ with $w$. That would produce a quite different formula.
Note, I'm interpreting your formula as $$\forall x\in \mathbb N.\exists y\in\mathbb N. (x+y = 5 \implies \forall x\in\mathbb N. x > -1)$$
If you meant $$(\forall x\in \mathbb N.\exists y\in\mathbb N. x+y = 5) \implies (\forall x\in\mathbb N. x > -1)$$ then everything I said still applies except that the second $\forall$ isn't nested within the first so there is no risk of capture.
A: Yes, to both questions, under most interpretations.
Quantifiers bind the statements that follow them; you can think of it as a quantifier defining what object a variable is going to refer to in the formula. But quantifiers have a very high priority - they rank very early in the order of operations. Usually, a quantifier covers only the smallest piece that would make sense. For example, in your statement, "$x + y = 5$" is the smallest piece that $\exists y \in \mathbb{N}$ could refer to - any smaller and it wouldn't be a sentence. Likewise, the smallest thing that first $\forall x \in \mathbb{N}$ could refer to is $\exists y \in \mathbb{N}, x + y = 5$.
But once the segment that the quantifier covers is over, the quantifier's gone - just like in an expression like $2(x + 7) + x$, you don't double the second $x$ just because you're multiplying the first one by $2$.
Now, the way you wrote it is a little dangerous - some systems would interpret it like $\forall x \in \mathbb{N}, \exists y \in \mathbb{N}(x + y = 5 \implies \forall x \in \mathbb{N}, x > -1)$. That still works fine - the second $\forall x$ is now inside the first, and we think of it as "overriding", so that the $x$ in $x > -1$ refers only to that last quantifier - but it means something very different.
For the sake of clarity, I would recommend this syntax: $\forall x \in \mathbb{N},\exists y \in \mathbb{N}(x + y = 5) \rightarrow \forall x \in \mathbb{N}, (x > -1)$. Some authors even put parentheses around the quantifiers, which helps with readability.
