I have a (possibly really stupid) question about sequent calculus.
My problem is that I am not able to figure out an intuitive explanation of the particular form in which I always find presented the rules for introducing the quantifiers. For example, let's take in consideration the left and right rule introducing $\forall$:
(L$\forall$ )$ \cfrac{\Gamma, A[t/x] \vdash \Delta}{\Gamma, \forall x A \vdash \Delta}$
(R$\forall$)$\cfrac{\Gamma \vdash A[y/x], \Delta}{\Gamma \vdash \forall x A, \Delta}$
What I don't understand is the asymmetry between these two rules. In particular, what is the reason behind using the $t$ in (L$\forall$ ), which I think stands for "any term", instead of just a variable $y$ like in the other rule? Why not vice-versa? why not both with $t$ or both with $y$? Does this have anything to do with the fact that the Right rule is invertible (i.e. can be also read from bottom to top), while the Left one is not? Or is it just nonsense notation?
Intuitively, ($\forall$L) corresponds to the elimination rule $\forall$-elim of Natural Deduction:
where $t$ is a term, i.e. a "name": variable, constant or "complex" name.
The intuition is quite clear: if $A$ holds for every object, like e.g. "__ is greater-or-equal to zero" in the domain of the natural numbers, then we can assert it of everythng : $0, x, x+0, 0+0, \ldots$
The ($\forall$R) rule instead is the equivalent of the introduction rule for $\forall$:
where $y$ is a "fresh" variable, i.e. $y$ must not occur free in any assumption that $A(y/x)$ depends on nor in $\forall xA$.
This syntactical conditions capture the fact that we can correctly "generalize" something if it is asserted for a "generic" object, i.e. an object about which we are assuming any "specificity".
Consider e.g. as $A$ the formula $x=0$; if we use $0$ itself as $y$, we can derive from the "obvious $0=0$ the wrong $\forall x (x=0)$.
See e.g. :