I am trying to learn sequent calculus for a while and for the life of me, I cannot make sense of the below quantifier rules for sequent calculus:
| $L$ | $R$ | |
|---|---|---|
| $\forall$ | $$\Gamma, A[t/x] \vdash \Delta \over \Gamma, \forall xA \vdash \Delta$$ | $$\Gamma \vdash A[y/x], \Delta\over \Gamma \vdash \forall xA, \Delta$$ |
| $\exists$ | $$\Gamma, A[y/x] \vdash \Delta \over \Gamma, \exists xA \vdash \Delta$$ | $$\Gamma \vdash A[t/x], \Delta \over \Gamma \vdash \exists xA, \Delta$$ |
I've already read many related questions here about quantifier rules and I am trying to come up with intuitive explanations for each rule which also explains their eigenvariable condition. Here is my attempt:
$\forall R$ rule:
From the linked Wikipedia page, their explanation goes like this:
For an intuition about the quantifier rules, consider the rule $\forall R$. Of course concluding that $\forall{x} A$ holds just from the fact that $A[y/x]$ is true is not in general possible. If, however, the variable y is not mentioned elsewhere (i.e. it can still be chosen freely, without influencing the other formulae), then one may assume, that $A[y/x]$ holds for any value of y. The other rules should then be pretty straightforward.
I disagree with that other rules are "pretty straightforward."
$\forall L$ rule:
Suppose $\Delta$ is derivable from the set of assumptions $\Gamma\cup\{A[t/x]\}$. Then, it is true that $\Delta$ is derivable from the stronger set of assumptions $\Gamma\cup\{\forall xA\}$.
$\exists R$ rule:
When $\{A[t/x]\}\cup\Delta$ is derivable from assumptions $\Gamma$, since $t$ is an "object" that exists, $\{\exists xA\}\cup\Delta$ is derivable from $\Gamma$.
$\exists L$ rule:
When $\Delta$ is derivable from $\Gamma\cup\{A[y/x]\}$, since $y$ is arbitrary "object", then $\Delta$ is derivable from $\Gamma\cup\{\exists xA\}$.
Unfortunately, it doesn't explain why eigenvariable condition is needed for this rule. This rule could be written as
$$\dfrac{\Gamma,A[t/x]\vdash \Delta}{\Gamma,\exists x A\vdash\Delta}$$
Is there any resources that goes in detail on how quantifier rules can be understood intuitively?