Substitution for predicate letters is a syntactically intricate inference procedure that is derivable in standard systems of non-modal quantificational logic. It allows a new theorem to be deduced from a given theorem ϕ by replacing an atomic formula Pτ1 ··· τn within ϕ by another formula ψ, of arbitrary complexity, involving the terms τ1, …, τn. The intricacy comes in stating the restrictions that must be placed on free variables of ϕ and ψ for the substitution to be allowed.

Church [1956, p. 289] gives some historical notes on this rule, pointing out that it was inadequately stated in early works of Hilbert and Ackerman, Carnap, and Quine; and first correctly stated, but not in full generality, in Hilbert and Bernays's Grundlagen der Mathematik in 1934. Church himself calls the predicate letter P a functional variable, viewing it as a variable whose values are propositional functions of individuals. In non-modal logic, this means that P is interpreted as an n-ary function Un → {truth, falsehood} from individuals to truth-values.

Intuitively, a logic that is closed under substitution for predicate letters is one whose theorems represent “universal laws”, expressing properties that hold of all predicates, i.e. hold no matter what interpretation is given to the predicate letters, hence hold no matter what formulas are (correctly) substituted for them.