I am struggling to understand the terminology behind free variables.
If we have $\forall x \ P(x)$ I would believe $x$ is bound and not free.
If we have $\forall x \ P(x, y)$ I believe $y$ is free, as it is not "bound" / "quantified over" / "attached to a quantifier".
Is this right so far?
Now, if we're using $\forall$ elim and we turn $\forall x \ P(x)$ into $P(a)$ on the next line, what is $a$ here? Does this "become" a free variable? A constant? A term? Something else? What is this?
Your guesses are right. Re: your question, you have options! $\forall$-elimination lets you deduce $P(t)$ from $\forall xP(x)$ for any term $t$ in your language. E.g. suppose my language has a constant symbol $c$ and a unary function symbol $f$. Then these are some of the things I could deduce from $\forall xP(x)$:
$P(y)$ (here $y$ is a variable - and it's free in the formula $P(y)$).
$P(c)$ (here $c$ is my constant symbol - there are no variables at all occurring in $P(c)$).
$P(f(c))$ (still no variables).
$P(f(y))$ (now I have a free variable $y$ in my formula, but the term I've selected is $f(y)$, which is more than just a free variable).