Logical Substitution

Substitution is the process of remapping the syntax (i.e. the symbols) of a formula. Depending on the type of logic, i.e. whether we are considering propositional logic or predicate logic, different operations may be allowed. Hence substitution is a meta-logical operation.

Definition §

Substitution (Logic) ^definition

A substitution, $\theta$, is a mapping (function) of symbols to symbols, also known as a syntactic transformation (because symbols define syntax):

$$\theta :\Sigma \to \Sigma$$

A substitution is represented (conventionally) as $\theta =\{x_1\mapsto t_1,x_2\mapsto t_2,\dots \}$, where $x_i$ gets replaced by $t_i$. A substitution, $\theta$, can only have a finite number of mappings. There are many different notations for substitution:

$$F[\theta ]=\theta (F)=F[x_1:=t_1,x_2:=t_2,\dots ]=F(x_1/t_1,x_2/t_2,\dots )=F\text{ substituted under }\theta$$

The resulting expression, $F[\theta ]$, is a substitution instance of $F$.

In Propositional Logic §

See Propositional Substitution

In Predicate Logic §

See Predicate Substitution

Compositions of Substitutions §

Since substitutions are basically functions, function composition also applies to them. If we have $\theta$ and $\Phi$ being two substitutions, then:

$$F[\Phi \circ \theta ]=\Phi (\theta (F))$$

which means $\Phi$ is applied to the substituted instance $\theta (F)$