Variablen, Substitutionen

• Term(Σ, V): Menge der Terme mit Symbolen aus Σ und Variablen aus V.
• Vereinbarung: Variablen am Ende des Alphabets ( x, y,…), Funktionssymbole am Anfang ( f, g, a, b,…)
• Menge der in einem Term t vorkommende Variablen: Var(t)
• Substitution σ ist Abbildung V→Term(Σ, W)
• eine Substitution σ angewendet auf einen Term t erzeugt Term tσ

  Beispiel t = f (x), Var(t) = {x}, σ : x $\mapsto$ p(0, 0), tσ = f (p(0, 0)).