Substitution instance

In formal logic, a substitution instance describes a manipulation of symbols in a formal system from one line of a derivation to the next.

Where Ψ and Φ are metalinguistic variables, Ψ is a substitution instance of Φ if and only if Ψ may be obtained from Φ by substituting sentences for symbols in Φ, always replacing an occurrence of the same symbol by an occurrence of the same sentence. For example:

(R $\to$ S) $\wedge$ (T $\to$ S)

is a substitution instance of:

P $\wedge$ Q

as is

(A $\leftrightarrow$ A) $\leftrightarrow$ (A $\leftrightarrow$ A)

a substitution instance of

(A $\leftrightarrow$ A)