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)) .