I'm referring to the inference rules listed at this page of Wikipedia (https://en.m.wikipedia.org/wiki/Sequent_calculus), under the section of $LK$ system. There are four rules for the quantifiers; however we have restrictions only for $\forall R$ and $\exists L$. The motivations for $\forall R$ are clear, because in order to conclude that $\forall x A(x) \Rightarrow B$, one must prove that $A(t) \Rightarrow B$ for a generic $t$ (i.e. not a variable used before). However why one can't say the same for the rule $\forall L$?
Plus, in the case of $\exists L$ I'm not sure to understand why we have the restrictions, and anyway I don't understand why we have it only in one case. Eventually, can anyone tell me what book (or material in general) I could use to clarify these things?
Best Answer
To make this question self-contained, these are the rules in question:
$$\forall L: \frac{\Gamma, A[t/x] \vdash \Delta}{\Gamma, \forall x A \vdash \Delta}$$
$$\forall R: \frac{\Gamma \vdash A[y/x], \Delta}{\Gamma \vdash \forall x A, \Delta}$$
In the case of $\forall R$, you are trying to conclude $\forall x A$. Therefore your assumption must be $A[y/x]$ where $y$ is a new variable, so that $y$ is a generic element, not a variable you have used before which may have some additional assumptions on it. Therefore there are restrictions necessary for $\forall R$.
However, in the case of $\forall L$, you start with $A[t/x] \Rightarrow \Delta$ and are trying to conclude $\forall x A \Rightarrow \Delta$. The $\forall x A$ appears as an assumption. Therefore no restriction is necessary, because you already know that $A$ holds for all $x$. Therefore you can substitute any $t$ for $x$, and apply the original $A[t/x] \Rightarrow \Delta$ to conclude $\Delta$.
The situation for $\exists$ is similar.