Substitution (Prädikatenlogik)

Eine Substitution ist eine Abbildung $\mathcal{S}:V\to {\mathcal{T}}_{\sigma }$ von einer endlichen Menge von Variablen auf Terme.
Die Anwendung auf eine Formel $\phi$, geschrieben $\phi \mathcal{S}$ oder $\phi [x_1/t_1,\dots ]$, ersetzt freie Vorkommen der Variablen.
Wichtig: Um Variablenfang zu vermeiden, müssen gebundene Variablen in $\phi$ ggf. umbenannt werden, falls sie in den eingesetzten Termen vorkommen.