# Proving $\forall x \neg P(x) \implies \neg \exists y P(y)$ in sequent calculus

Having the inference rules

$$\frac{\Gamma, A[x:t] \implies \Delta}{\Gamma, \forall x A \implies \Delta} \forall L$$

$$\frac{\Gamma, A[x:y] \implies \Delta}{\Gamma, \exists x A \implies \Delta} \exists L$$

$$\frac{\Gamma \implies \Delta, A[x:y]}{\Gamma\implies\Delta,\forall x A}$$

$$\frac{\Gamma \implies \Delta, A[x:t]}{\Gamma\implies\Delta,\exists x A}$$

I want to prove $$\forall x \neg P(x) \implies \neg \exists y P(y)$$. I already tried

$$\dfrac{\dfrac{\dfrac{\dfrac{P(t)\implies P(t)}{\neg P(t), P(t)\implies}}{\neg P(t), \exists y P(y) \implies}}{\forall x \neg P(x), \exists y P(y) \implies}}{\forall x \neg P(x) \implies \neg \exists y P(y)}$$

but in the second step, I cannot use $$t$$, can I? How can I prove this?

Your second step (from $$\lnot P(t), P (t) \implies$$ to $$\lnot P(t), \exists y P (y) \implies$$) is wrong for two reasons, according to the restrictions to the inference rule $$\exists L$$ (see here and here):
1. $$t$$ should be a variable, not a generic term;
2. if you consider $$t$$ as a variable, it must not occur free anywhere in the sequent $$\lnot P(t), \exists y P (y) \implies$$, but it does occur free in $$\lnot P(t)$$.
It is easy to fix this problem: you have to swap the rule $$\exists L$$ and $$\forall L$$ in your derivation. Indeed, in your second step you have to apply the inference rule $$\forall L$$ (which does not have any restriction), in this way you get the sequent $$\forall x \lnot P(x), P(y) \implies$$, where no variable occurs free except the one you want to quantify with $$\exists$$ and then you can apply the inference rule $$\exists L$$, so as to get $$\forall x \lnot P(x), \exists y P(y) \implies$$ where no variable occurs free. So, a correct derivation in the sequent calculus is the following:
$$\dfrac{\dfrac{\dfrac{\dfrac{P(y)\implies P(y)}{\neg P(y), P(y)\implies}}{ \forall x \lnot P(x), P(y) \implies}\forall L}{\forall x \neg P(x), \exists y P(y) \implies}\exists L}{\forall x \neg P(x) \implies \neg \exists y P(y)}$$