Difference between free variables and universal quantifiers in predicate logic?

Question

I'm learning about Gentzen's System LK, and the issue with the RHS $\forall$ introduction rule. This rule would allow us to derive the following:

$$\frac{\longrightarrow Pa}{\longrightarrow \forall x Px}$$

However the notes released by my prof. claim that this is not a legal deduction. I don't see the problem with this (I have no free variables in the bottom sequent).

So, why is the above an illegal deduction, and what is the difference between $Pa$ and $\forall x Px$?

Answer 1

$Pa$ is the claim that "term $a$ satisfied predicate $P$".

$\forall x~Px$ is the claim that "any term satisfied predicate $P$".

In order for the former to entail the latter, you must have an assertion that term $a$ is arbitrary.