For the purposes of giving the procedure for evaluation and explaining the semantics of judgements, we would only need to consider substitution of closed terms for free variables and hence would not need to consider simultaneous substitution or capture. However, for the purpose of specifying inference rules later we shall want to have simultaneous substitution of terms with free variables for free variables. The result of such a substitution is indicated thus:

where , are variables (not necessarily
distinct) and are terms.
It is handy to permit multiple occurrences of the same variable among
the targets for replacements, all but the last of which are ignored.
is the result of replacing
each free occurrence of in **t** by for ,
where is with **j** the greatest **k** such that is .

Thu Sep 14 08:45:18 EDT 1995