On page 121, A Mathematical Introduction to Logic, Herbert B. Enderton（2ed),
3c. The remaining case is where $ϕ$ is $¬∀x ψ$. (In order to show $\Gamma \vdash ¬∀x ψ$)It would suffice to show that $ \Gamma \vdash¬ψ^x_t$ , where $t$ is some term substitutable for $x$ in $ψ$. (Why?) Unfortunately this is not always possible. There are cases in which $$\Gamma \vdash ¬∀x ψ$$, and yet for every term $t$,$$\Gamma \nvdash ¬ψ^x_t$$ (One such example is $\Gamma= ∅$,$ψ = ¬(Px→∀y Py)$.) Contraposition is handy here; $$\Gamma;α \vdash ¬∀x ψ$$ iff $$\Gamma; ∀ x ψ \vdash ¬α$$
Notations: $\Gamma$ represents a set of axioms; $P$ is a unitary relation: $\Gamma \vdash \phi$ means $\phi$ is deducible from $\Gamma$, or $\phi$ is a theorem of $\Gamma$.
The part from "Contraposition is handy here" to the end eludes me, especially I don't know what $\alpha$ represents.
Here's my attempt to understand it: The example is equivalent to: $$\vdash \exists x (Px→∀y Py)$$ for any term $t$, $$\nvdash Pt→∀y Py$$
The former can be shown to be true by discussing situation $\forall x Px$ and its negation(By contrast, in a previous question, Hurkyl argues that whether the formula is well-formed, is, at best, ambiguous). But I got stuck on how to show the latter "for any term $t$, $\nvdash Pt→∀y Py$"