Substitution rule

One of the derivation rules (cf. Derivation rule) in logico-mathematical calculi. By a "substitution rule" one may mean various forms of the rule. For example, in the propositional calculus a substitution rule is a formula together with all occurrences of the propositional variable. In predicate calculus it is: a) a formula together with the predicate variable (here one has to obey a series of constraints on the occurrence of the individual variables in order to avoid variable collisions, i.e. a situation were a variable that is free in the formula becomes bounded as a result of the substitution); b) a substitution rule for a term together with free occurrences of an individual variable of the corresponding type (here also it is necessary to avoid variable collisions).

References

[1]	P.S. Novikov, "Elements of mathematical logic" , Oliver & Boyd and Acad. Press (1964) (Translated from Russian)
[2]	J.R. Shoenfield, "Mathematical logic" , Addison-Wesley (1967)
[3]	D. Hilbert, P. Bernays, "Grundlagen der Mathematik" , 1–2 , Springer (1968–1970)