Prädikatenlogik/Substitution/Ohne Beweis/Einführung/Textabschnitt

Aus Wikiversity

Variablen repräsentieren verschiedene Werte, die man für sie einsetzen kann. Auf formaler Ebene bedeutet dies, dass eine oder mehrere Variablen durch gewisse Terme ersetzt werden. In der Ersetzung macht es einen großen Unterschied, ob gebundene oder freie Variablen vorliegen. Der Ausdruck

bedeutet in einem angeordneten Körper interpretiert, dass die nichtnegative Zahl als Quadrat darstellbar ist (also eine Quadratwurzel besitzt), was für wahr ist, für im Allgemeinen (das hängt von der Interpretation für ab) nicht. Gleichbedeutend (bei einer inhaltlichen Interpretation) mit diesem Ausdruck ist

aber nicht

das nur bei oder wahr ist. Von daher wird die weiter unten zu gebende Definition für die Substitution von Ausdrücken berücksichtigen, ob Variablen frei oder gebunden sind. Ferner wird es wichtig sein, in einem Ausdruck neue Variablen einzuführen. Damit diese Konstruktion eindeutig definiert ist, legen wir eine durchnummerierte (und abzählbare) Variablenmenge zugrunde.


Definition  

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


Definition  

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.

Die folgende Aussage, das Substitutionslemma, geben wir ohne Beweis. Es stiftet eine Beziehung zwischen Substitutionen und Uminterpretationen.


Lemma

Es sei ein Symbolalphabet einer Sprache erster Stufe gegeben und es seien paarweise verschiedene Variablen und fixierte -Terme. Es sei eine -Interpretation gegeben. Dann gelten folgende Aussagen.

  1. Für jeden -Term gilt
  2. Für jeden -Ausdruck gilt