Operationen mit Variablen in Termen

• Term(Σ, V) = Menge der Terme über Signatur Σ mit Variablen aus V

  Beispiel: Σ = {Z/0, S/1, f /2}, V = {y}, f (Z(), y)∈Term(Σ, V).

• Substitution σ: partielle Abbildung V→Term(Σ)

  Beispiel: σ₁ = {(y, S(Z()))}

• eine Substitution auf einen Term anwenden: tσ:

  Intuition: wie t, aber statt v immer σ(v)

  Beispiel: f (Z(), y)σ₁ = f (Z(), S(Z()))

  Definition durch Induktion über t