If a wff is simply atomic (e.g. $Pxy$) are $x$ and $y$ considered free in it? (Using First-Order Logic Hilbert System)
I found the following "solution" to $\forall x \forall y Pxy \vdash \forall y \forall x Pyx$:

  
*
  
*$\forall x \forall y Pxy \vdash \forall y Pzy$ (A2, MP)
  
*$\forall y Pzy \vdash Pzx$ (A2, MP)
  
*$\forall x \forall y Pxy \vdash Pzx$ (1,2)
  
*$Pzx \vdash \forall x Pzx$ (GT)
  
*$\forall x Pzx \vdash \forall z \forall x Pzx$ (GT)
  
*$\forall x \forall y Pxy \vdash \forall z \forall x Pzx$ (3,4,5)
  
*$\forall z \forall x Pzx \vdash \forall x Pyx$ (A2, MP)
  
*$\forall x Pyx \vdash \forall y \forall x Pyx$ (GT)
  
*$\forall x \forall y Pxy \vdash \forall y \forall x Pyx$ (6,7,8)

Where GT = Generalization Theorem, A2 = Substitution axiom, MP = Modus Ponens.
My problem is with line 4. How can you just throw a $\forall x$ in front of there? Doesn't the generalization theorem assume that $x$ is NOT free in the wff. Is $x$ not free in $Pzx$?
Here are all the axioms I can use:

  
*
  
*Tautologies
  
*$\forall x \alpha \rightarrow \alpha_t^x$, where $t$ is substitutable for $x$ in $\alpha$.
  
*$\forall x (\alpha \rightarrow \beta)\rightarrow(\forall x \alpha \rightarrow \forall x \beta)$
  
*$\alpha \rightarrow \forall x \alpha$, where $x$ does not occur free in $\alpha$
And if the language includes equality, 
  
  
*
  
*$x=x$
  
*$x=y \rightarrow (\alpha \rightarrow \alpha')$, where $\alpha$ is atomic and $\alpha'$ is obtained from $\alpha$ by replacing $x$ in
  zero or more places by $y$.
  

 A: Of course, in an atomic formula $Pxy$, $x$ and $y$ are free.
As you says (correctly) you cannot do : $Pzx ⊢ ∀xPzx$; you have to apply it to Line 3 :

from $∀x∀yPxy ⊢ Pzx$, derive $∀x∀yPxy ⊢ \forall xPzx$.

The Generalization Theorem [see Enderton, page 117] says :

If $\Gamma \vdash \varphi$ and $x$ does not occur free in any formula in $\Gamma$, then $\Gamma \vdash \forall x \varphi$.

You can apply it to Line 3 because in it we have $\Gamma = \{ ∀x∀yPxy \}$ and $x$ is not free in it.
Thus, it works...

Note
In using : $\vdash$ in a derivation with annotations, it is a good practice to be consistent with the conventions : 


*

*$\vdash \psi$ means that $\psi$ is theorem of the system, i.e. provable from the axioms 

*$\varphi \vdash \psi$ means that $\psi$ is derivable from the assumption $\varphi$.
In your proof you are using it in an inconsistent way : in Line 4 you wrote to the left of $\vdash$ the formula from which you are deriving your conclusion (and written in this way, the step is illegal), while in other cases you correctly wrote to the left of $\vdash$ the assumptions from which the conclusion depends (see Line 3).
Your misunderstanding, I think, arise because you are "switching" from one way to the other.
