Prädikatenlogik/Variablensubstitution/Terme/Definition

Variablensubstitution für Terme

Es sei ein Symbolalphabet einer Sprache erster Stufe gegeben. Es seien paarweise verschiedene Variablen und fixierte -Terme. Dann definiert man rekursiv über den Aufbau der Terme die Substitution für jeden -Term .

  1. Für eine Variable ist
  2. Für eine Konstante ist
  3. Für ein -stelliges Funktionssymbol und Terme ist