Wikipedia's Sequent Calculus article states:
$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]$).
Is the bolded text slightly wrong/confusing? Shouldn't it be:
(i.e., no occurrence of any free variable in $t$ becomes bound in $A[t/x]$)
since $A$ may have bounded variables already.
Best Answer
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).