Why is there a limitation on the existential introduction in sequent calculus?

Question

In sequent calculus there is the rule $\exists \vdash$ $~~~~~\dfrac{\Gamma,\phi[y]\vdash \Delta}{\Gamma,\exists x\phi[x/y]\vdash\Delta}$ with the limitation that y is not used in any of the formulas of $\Gamma$ or $\Delta$ or in $\phi$. There's a similar rule for $\vdash \forall$ with the same limitation where I can imagine a contradiction. But doesn't the $\exists$ quantor always "searches" for the right element in our universe and therefore it is impossible to use a constant y which would create a contradiction?

Answer 1

EDIT: Actually, it's way simpler than what I wrote below: clearly we have $\psi(y)\vdash\psi(y)$ but in general we don't have $\exists x(\psi(x))\vdash\psi(y)$. That is, take $\Gamma=\emptyset$ and $\Delta=\{\psi(y)\}$.

---

Well, $\{\varphi(y),\psi(y)\}$ proves $\exists x(\varphi(x)\wedge\psi(x))$, but $\{\varphi(y), \exists x(\psi(x))\}$ doesn't. The problem is that the way in which $\Gamma$ together with $\psi(y)$ proves something might crucially involve the specific variable $y$ interacting with stuff in $\Gamma$.

That is, it's not that the top hypotheses don't imply the bottom hypotheses (they do), but that the top sequent doesn't imply the bottom sequent. Indeed, we should expect that the top sequent isn't enough to imply the bottom sequent precisely because the top hypotheses are stronger than the bottom hypotheses.

Answer 2

The "trick" is the interplay of the semantics fof sequents with that for free variables.

We have that a sequent $\Gamma \vdash \Delta$ is falsifiable if for some (non-empty) domain $D$ and some assignment in $D$ to all its free variables, it has the value $\text {False}$.

A variable assignment is a function $v: \text {Var} \to D$ that maps variables to elements of the domain.

Now for the counterexample. Consider the simple case:

$$\dfrac{\phi[y] \vdash \phi[y]}{\exists x \phi[x/y] \vdash \phi[y]},$$

and interpret it in the domain $\mathbb N$ of natural numbers with $\phi$ meaning "$\text {Even}$".

Thus, our rule amounts to:

$$\dfrac{\text {Even}[y] \vdash \text {Even}[y]}{\exists x \text {Even}[x/y] \vdash \text {Even}[y]},$$

and consider a variable assignment function $v: \text {Var} \to \mathbb N$, such that $v(y)=1$.

With it, we have that the upper sequent is $\text {True}$ while the lower sequent is $\text {False}$.

Conclusion: without proviso the rule is not sound.