Prädikatenlogik/Variablensubstitution/Ausdrücke/Definition

Aus Wikiversity
Zur Navigation springen Zur Suche springen
Variablensubstitution für Ausdrücke

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 -Ausdrücke die Substitution für jeden -Ausdruck .

  1. Für Terme setzt man
  2. Für ein -stelliges Relationssymbol und Terme setzt man
  3. Für einen Ausdruck setzt man
  4. Für Ausdrücke und setzt man

    und ebenso für die anderen zweistelligen Junktoren.

  5. Für einen Ausdruck seien diejenigen Variablen (unter den ), die in frei vorkommen. Es sei , falls nicht in vorkommt. Andernfalls sei die erste Variable (in einer fixierten Variablenaufzählung, falls es abzählbar viele Variablen gibt, bzw. in einer fixierten Wohlordnung der Variablenmenge), die weder in noch in vorkommt. Dann setzt man

    und ebenso für den Existenzquantor.