3
$\begingroup$

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?

$\endgroup$
3
$\begingroup$

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)}$$

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.