Clarification regarding substitution in sequent calculus

Solution 1:

The original bold text is correct. Indeed, $t$ is a term, not a formula, and so no quantifiers or any other kind of binders can occur in it, hence every variable occurring in $t$ is free (in $t$) by necessity. Actually, your version of the bold text (which adds "free") is not wrong, but only superfluous: adding "free" does not change anything in the restriction.

The point is that when you substitute $t$ for every free occurrence of $x$ in $A$, some variables in $t$ (which are free in $t$ by necessity, as said above) can become bound in $A[t/x]$ (because of some quantifiers in $A$), and this is what must be avoided.


More generally, the notion of "being free" is not absolute, but is always relative to a context where variables appear. The free variables of a formula $A$ are the variables that occur free in $A$, i.e. that are not bound by any binders in $A$. The free variables of a term $t$ are the variables that are free in $t$, i.e. that are not bound by any binders in $t$ (which is always the case because there are no binders in a term in first-order logic).