# Making sense of eigenvariable restriction in $\exists L$ rule in sequent calculus

I still cannot understand why the $$\exists L$$ rule from sequent calculus is sound:

$$\Gamma, A[y/x] \vdash \Delta \over \Gamma, \exists xA \vdash \Delta$$

Intuitively I can explain this rule as "When $$\Delta$$ can be derived from assumptions $$\Gamma\cup\{A[y/x]\}$$, due to the existence of some object $$y$$ that makes $$A$$ hold, it follows that $$\Delta$$ can be derived from assumptions $$\Gamma\cup\{\exists xA\}$$."

What prevents me from fully understanding this rule is the eigenvariable restriction on $$y$$. Why this restriction is necessary for soundness?

I know there is one counterexample when the eigenvariable restriction is lightened: I could derive $$\exists x A\vdash A[y/x]$$ from $$A[y/x]\vdash A[y/x]$$ which is not always true. However, this counterexample does not explain to me why it is possible to derive $$\exists xA \vdash \Delta$$ from $$A[y/x] \vdash \Delta$$ when $$y$$ is not present in $$\Delta$$.

P.S. I already read this related question but I don't understand this part

Now, since $$y$$ does not occur free in $$\Gamma$$ and $$\Delta$$, this means that you didn't make any hypothesis about $$y$$, so the fact that $$\Delta$$ derives from $$\Gamma$$ and $$\phi[y]$$ actually means that you can derive $$\Delta$$ from $$\Gamma$$ and $$\phi[y]$$, for any value of the variable $$y$$.

What happens when $$y$$ does occur free in $$\Gamma$$ and $$\Delta$$?

I am looking for more dumbed-down explanation of $$\exists L$$ rule.

The "intuition" is: under what condition we can derive $$A(t)$$ from $$\exists x A$$?

If we use a term (a "name") $$t$$ that is already used in the proof, we may get into trouble, because if $$t$$ is used already the formula that uses it "impose" a meaning on the term that can be not consistent with that expressed by $$\exists x A$$.

Thus, the meaning of the $$(\exists \text L)$$ rule is:

from a proof of $$Δ$$ with premises $$Γ,A[y/x]$$ we can derive a proof of $$Δ$$ with premises $$Γ,∃xA$$,

provided that the term $$y$$ is "the right one".

How we can formalize the proviso above? imposing that the "name" $$y$$ is nowhere used in the upper sequent except for the formula $$A(y)$$.

Consider a very simple counterexample: $$(1=0) \to (1=0)$$ is a correct initial sequent (or axiom).

Thus, applying the rule without the proviso we get: $$\exists x(x=0) \to (1=0)$$, which is clearly wrong.

Another approach is using the intuitive semantical reading of sequent calculus: If the upper sequent is true, then the lower sequent is; and contraposing it: if the lower sequent is false, also the upper sequent is.

But for the lower one to be false we must have (forgetting about $$\Gamma$$ for simplicity) that $$\exists x A$$ is true and $$\Delta$$ false. And thus, also $$A[y/x]$$ must be true. But without proviso we can run in the counter-example above, if $$A[y/x]$$ is in $$\Delta$$.

• Thanks again. In the last paragraph, why $A[y/x]$ must follow from $\exists x A$? Perhaps it is because y is a constant that can assume any value…? Feb 12 at 18:38