sequent calculus for first order logic

Question

I've just started learning sequent calculus. Now I'm trying to prove the formula below: $$ \exists x (P → Q) ⊨ P → \forall x Q $$ My approach to the problem:
$$ \underline{_⊢\exists x (P → Q) , _⊣ P → \forall x Q} $$ $$ \underline{_⊢\exists x (P → Q) , _⊢P, _⊣\forall x Q} $$ $$ \underline{_⊢P(y) → Q(y), _⊢P, _⊣\forall x Q } $$ $$ \underline{_⊣P(y), _⊢P, _⊣\forall x Q \ \ \ (1) \ {\Bigg|} { \ \ _⊢Q(y), _⊢P, _⊣\forall x Q \ \ \ (2) }} $$ In the second case we have $ _⊣\forall x Q $, thus $ _⊣ Q(y) $ - contradiction (because of $_⊢Q(y)$) .
In the first one we only have $ _⊣P(y) $ and $ _⊢P $, so there is a counterexample for the formula: $$ P(x)=T, \text{if x = y and } F \text{ otherwise} $$ $$ Q(x)=F \ \forall x $$
Am I right? (An unquantified $P$ is a bit embarrasing for me)

Answer 1

Long comment

Quite a strange way of writing sequents...

Having said that, and assuming that $x$ is free in $P$, the answer is :

$\exists x (Px \to Qx) \nvDash Px \to \forall x Qx$.

Assume a domain with one Black ball and one White ball and interpret $P$ with "... is Black" and $Q$ with "... is White".

We have that $Px$ is FALSE for the White ball, and thus the conditional $Px \to Qx$ is TRUE of it.

Thus, in this interpretation, the formula $\exists x (Px \to Qx)$ is TRUE.

But $P$ is TRUE of the Black ball and $\forall x Qx$ is FALSE (not every ball is White).

Thus, in this interpretation, the formula $Px \to \forall x Qx$ is FALSE.