This is not a complete answer: it's just too long to be a comment.
Hackstaff begins his discussion of quantification over predicate variables by saying (my paraphrase,) "Wouldn't it be nice if $(\Phi x \rightarrow \Phi y) \rightarrow (x=y)$ were a theorem, so that we could define equality by $x = y$ if and only if $\Phi x \rightarrow \Phi y$?" (He's already introduced $(x=y) \rightarrow (\Phi x \rightarrow \Phi y)$ as Axiom LFA7: Axiom 7 of the lower-functional calculus, where "lower-functional" is to be read "first-order.")
Hackstaff then observes that $(\Phi x \rightarrow \Phi y) \rightarrow (x=y)$ cannot be a theorem for the obvious reason: a quantifier on $\Phi$ is missing. However, up to that point, $(\forall \Phi ~.~ \Phi x \rightarrow \Phi y) \rightarrow (x=y)$ is not even a wff.
He then goes on to extend the syntax to allow quantification over predicate variables, and adds two axioms that, in modern notation, look like this:
\begin{align*}
\text{2FA8}\quad\quad & (x=y) \rightarrow (\forall \Phi ~.~ \Phi x \rightarrow \Phi y) \\
\text{2FA9}\quad\quad & (\forall \Phi ~.~ \Phi x) \rightarrow \Phi y \enspace.
\end{align*}
Hackstaff then proves that $(\forall \Phi ~.~ \Phi x \rightarrow \Phi y) \rightarrow (x=y)$ is a theorem of the resulting second-order calculus. He instantiates 2FA9 in the process as $(\forall \Phi ~.~ \Phi x) \rightarrow \Phi x$, labeling the instantiation as a new theorem, which would be strange if 2FA9 were any different from what it is.
Finally, he concludes that $x = y$ if and only if $\forall \Phi ~.~ \Phi x \rightarrow \Phi y$ is a theorem of the second order calculus.
There seems to be an assumption in Axiom 2FA9 that the predicate that is false of all individuals is not a valid value for $\Phi$; else the implication holds vacuously. I have been unable, though, to quickly locate a discussion of this.
