Substitution in sequent calculus vs substitution in lambda calculus

Solution 1:

Yes, your definition of substitution in the $\lambda$-calculus works fine. It is crucial to mention "free" in the definition of substitution in the $\lambda$-calculus, when it says "no occurrence of any free variable in $t$ becomes bound in $A[t/x]$", because a $\lambda$-term $t$ may contain binders and the restriction takes care only of the free variables of $t$.

On the contrary, as I said here, in the definition of substitution in sequent calculus (and more generally, in languages for first-order logic) there is no need to mention "free" when it says "no occurrence of any free variable in $t$ becomes bound in $A[t/x]$", because terms do not have binders and so any variable in $t$ is necessarily free.

There are at least two crucial differences between sequent calculus (and more generally, languages for first-order logic) and the $\lambda$-calculus.

1. In the language for first-order logic, there are two kinds of expressions, formulas and terms, which are well distinct from a syntactic and semantic point of view. In the $\lambda$-calculus, there is only one kind of expressions, $\lambda$-terms.

2. In the language for first-order logic, formulas may have binders for variables, but terms do not have any binders, so variables in a term are always free (if we consider the term alone). In the $\lambda$-calculus, instead, $\lambda$-terms may have binders, called $\lambda$-abstractions, and so a $\lambda$-term may have free and bound variables.