An axiom that is not like axiom

Question

Hackstaff designed a second-order logic system with identity to deal with those logical formulas with equal signs. One of the axioms in the system is:

 $ \forall \Phi (\Phi x) \to \Phi y$

An interpretations of the axiom can be "If A has all the physiological characteristics of birds, then B has wings." It should be noted that A and B may be the same individual, or may be not.

I believe that you will immediately find out the problem : Since A does not have to be B, how can we derived "B has wings" from "If A has all the physiological characteristics of birds"? Is Hackstaff wrong? This is hard to imagine. Or does he have other supposition without explanation in the book?

There are very few textbooks for second-order logic, and I don't know the answer right now.

References : L.H.Hackstaff (1966), Systems of Formal Logic, p.289

Answer 1

In a second order logic system you define the equality $t=u$ as: $$(\forall R^1)R^1t\iff R^1u$$ Where $R^1$ is a function variable of 1 argument. Maybe he wanted to define the equality and it was a typo the right arrow instead of the left/right arrow.

Answer 2

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.