I'm trying to understand the logical structure of statements of the form $ (\forall x\ \mathsf{P}(x)) \implies \mathsf{Q}$, where $x$ does not occur in $\mathsf{Q}$. To prove such statements it is sufficient to prove that $ \mathsf{P}(c) \implies \mathsf{Q}$, for some $c$ in $x$'s domain. This can be seen in two ways:
Either
$$ \begin{array}{rl} & \forall x\ \mathsf{P}(x) \\ & \mathsf{P}(c) \\ & \mathsf{Q} \\ \hline \therefore & \forall x\ \mathsf{P}(x) \implies \mathsf{Q}\end{array} $$
Or,
$\forall x \ \mathsf{P}(x) \implies \mathsf{Q}$ is logically equivalent to $ \lnot \forall x \ \mathsf{P}(x) \lor \mathsf{Q}$, which is logically equivalent to $ \exists x \ \lnot \mathsf{P}(x) \lor \mathsf{Q}$, which is logically equivalent to $ \exists x \ (\lnot \mathsf{P}(x) \lor \mathsf{Q})$, which is equivalent to $ \exists x \ ( \mathsf{P}(x) \implies \mathsf{Q})$ amounts to showing the same thing.
All this is fine and dandy, and I'm able to see how it all fits together "formally". However, I'm trying to get an intuitive sense of why proving such propositions involve just exhibiting a special case, $ \mathsf{P}(c)$, that implies $\mathsf{Q}$. Is there an easy way to see this, preferably with some concrete examples? Such statements don't seem to be quite common in my undergraduate courses.
I assume that you are asking for an "intuitive explanation" of why :
are equivalent if $x$ is not free in $Q$.
Form left to right : assume that $(∀x \ P(x)) → Q$ holds.
We have two cases :
(i) $Q$ is true; in this case, by the truth table for conditional : $A \to Q$ is true for $A$ whatever. Thus, also $P(c) \to Q$ is true for $c$ whatever.
And thus we have that $∃x \ (P(x) → Q)$ holds.
(ii) $∀x \ P(x)$ is false; in this case, we have that for some $c$ : $P(c)$ is false and so $P(c) \to Q$ is true (for that $c$).
And thus again we have that $∃x \ (P(x) → Q)$ holds.
In the same way we can prove the case form right to left.
The above argument follows exactly Gowers' manipulations.
By easy transformations, the original formula is equivalent to :
Thus, whe have only to apply the truth-conditions for $\lor$ (its truth-table).
Either $Q$ is true or there is some $c$ such that $\lnot P(c)$ holds.
But to say that $\lnot P(c)$ holds for some $c$ is the same as : $\forall x \ P(x)$ does not hold.