$\forall xA\Rightarrow A[t/x]$ and rule of left universal quantification in sequent calculus

Question

Consider the rule of left universal quantification in the sequent calculus: $$\dfrac{\Gamma,A[t/x]\vdash \Delta}{\Gamma,\forall xA\vdash\Delta}.$$ This can be used to give the following proof: $$\dfrac{A[t/x]\vdash A[t/x]}{\dfrac{\forall x A\vdash A[t/x]}{\vdash (\forall x)A\Rightarrow A[t/x]}}$$ What is the relation between $\vdash(\forall x)A\Rightarrow A[t/x]$ and left universal quantification rule? Obviously one is a sequent and the other a deductive rule. They aren't saying the same thing, right?

Answer 1

Obviously one is a sequent and the other a deductive rule.

Yes, indeed, and that is the distinction.

The sequent, $~\vdash (\forall x~A)\to A[t\backslash x]~$, is the claim that the implication is provable to be a tautology.

The Left Universal Rule is one among the rules of inference used to do so.

$$\dfrac{\dfrac{\dfrac{}{A[t/x]\vdash A[t/x]\qquad\;}{\small\textsf{Id}}}{\forall x A\vdash A[t/x]\qquad}{\small{\forall}\textsf{L}}}{\qquad\quad\,\vdash(\forall x)A\to A[t/x]}{\small{\to}\textsf{R}}$$