Trying to understand Sequent Calculus inference rules for quantifiers $\forall$ and $\exists$.

I'm trying to understand any of the LK sequent calculus (logic) inference rules for quantifiers (if I can understand one well enough, perhaps I can use that to inform my understanding of the other three). Per Wikipedia, the rules are:

The Wikipedia article says this about these rules:

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.

(First question: The inference rules use both $A[t/x]$ and $A[y/x]$. Is there a difference between $A[t/x]$ and $A[y/x]$? I know $t$ conventionally denotes a term. Does $y$ also?)

The same Wikipedia article states the meaning of the notation $A[t/x]$:

$A[t/x]$ denotes the formula that is obtained by substituting the term $t$ for every free occurrence of the variable $x$ in formula $A$ with the restriction that the term $t$ must be free for the variable $x$ in $A$ (i.e., no occurrence of any variable in $t$ becomes bound in $A[t/x]$).

It should also be noted that in sequent calculus

• a term $t$ has no quantifiers (or any binders) hence all of its variables are free
• a formula $A$ may have quantifiers. It may also have free variables. Hence, it may have bound variables and free variables.

Why are the rules of the form:

$$\Gamma, A[t/x] \vdash \Delta \over \Gamma, \forall xA \vdash \Delta$$

instead of of the form:

$$\Gamma, A \vdash \Delta \over \Gamma, \forall xA \vdash \Delta$$

Why are the substitutions necessary? For a particular rule, does the substitution ensure that $x$ is a free variable?

You had a careful observation for the difference between arbitrary term $t$ and arbitrary variable $y$ used in the 4 quantifier rules in $LK$. Indeed there's some purpose for this difference intentionally in most sequent calculi.

Recall $\forall$L implicitly corresponds to $\forall$-elim of natural deduction, so if $A$ holds for every object then we can substitute any term $t$, however complex, into $A$ for $x$ (of course assuming $t$ is free for $x$ in $A$), and then if we can still derive $\Delta$ that's when $\forall$L makes sense. Conversely, $\forall$R corresponds to $\forall$-intro rule in ND, so we need an arbitrary single variable $y$ (assuming $y$ is not mentioned elsewhere) to substitute for $x$ in $A$ to be derived as a result of $\Gamma$ as the most generic case to introduce $\forall x A$.

And interestingly, for the $\exists$ quantifier the situations reverse since in the introduction case ($\exists$R rule) usually a generic variable $y$ won't qualify to derive $A(y)$ from $\Gamma$, you need to work hard to find a specific term $t$ satisfying $\Gamma \vdash A[t/x]$. Similar reasoning for $\exists$L rule.

Finally if you understand $\forall$L rule as $\forall$-elim of natural deduction, then you can easily see from same above reasoning you have to prove $\Delta$ from $\Gamma$ and $A[t/x]$ for an arbitrary term, only then $\forall$L makes sense and holds.

Because we don't just want to slap a "$\forall x$" on the front of the formula $A$. (For simplicity, below I work with $\Gamma=\emptyset$ and $\Delta$ a single formula, namely $\Delta=\exists xU(x)$.)

For example, suppose $A$ is the formula $U(c)$ where $U$ is a unary predicate symbol and $c$ is a constant symbol. From the sequent $$U(c)\vdash\exists xU(x)$$ (whose derivation I leave as an exercise) we would like to infer the sequent $$\forall xU(x)\vdash \exists xU(x).$$ However, your version of the ${\forall}L$ rule would only give us $$\forall xU(c)\vdash\exists xU(x),$$ and this isn't at all the same thing.