- Freie Variablen
In einem Ausdruck
über einem Symbolalphabet nennt man die Variablen, die
(und zwar für jedes Vorkommen)
innerhalb der Reichweite eines Quantors stehen, gebunden, die anderen frei. Dies wird streng über den Aufbau der Ausdrücke definiert.
-
-
für ein -stelliges Relationssymbol und Terme .
-
für einen Ausdruck .
-
für Ausdrücke und . Ebenso für .
-
für einen Ausdruck und eine Variable .
-
für einen Ausdruck und eine Variable .
Einen Ausdruck ohne freie Variablen nennt man einen Satz, auch wenn diese Bezeichnung nicht ganz glücklich ist, da „Satz“ die Gültigkeit einer Aussage suggeriert. Die Menge der Sätze wird mit bezeichnet, die Menge der Ausdrücke mit genau einer freien Variablen
(die aber in dem Ausdruck beliebig oft vorkommen darf)
mit .
Beispielsweise ist in
-
die Variable gebunden, während die Variablen frei sind, wobei die Freiheit von auf dem freien Vorkommen im hinteren Ausdruck beruht.
- Das Koinzidenzlemma
Die folgende Aussage, das Koinzidenzlemma, zeigt, dass der Wert eines Terms und die Gültigkeit eines Ausdrucks unter einer Interpretation
(bei einer fixierten -Struktur)
nur von den in dem Term vorkommenden Variablen bzw. in dem Ausdruck vorkommenden freien Variablen abhängt. Ihr Beweis ist ein typisches Beispiel für einen Beweis durch Induktion über den Aufbau der Terme bzw. Ausdrücke.
(1). Wir führen Induktion über den Aufbau der -Terme. Für den Induktionsanfang müssen wir Variablen und Konstanten aus betrachten. Für eine Variable
(oder eine Konstante)
aus ist nach Voraussetzung
.
Im Induktionsschritt können wir annehmen, dass ein -stelliges Funktionssymbol aus gegeben ist sowie -Terme , für die die Interpretationsgleichheit schon gezeigt wurde. Nach Voraussetzung wird in beiden Interpretationen durch die gleiche Funktion interpretiert. Daher ist
(2). Wir führen Induktion über den Aufbau der -Ausdrücke, wobei die zu beweisende Aussage über je zwei Interpretationen zu verstehen ist. Für die Gleichheit und ein Relationssymbol aus folgt die Aussage unmittelbar aus (1), da ja in beiden Interpretationen als die gleiche Relation zu interpretieren ist. Der Induktionsschritt ist für Ausdrücke der Form aufgrund der Modellbeziehung unmittelbar klar. Es sei nun ein -Ausdruck der Form gegeben, und es gelte . Dies bedeutet aufgrund der Modellbeziehung, dass es ein
derart gibt, dass gilt. Die beiden umbelegten Interpretationen
und
stimmen auf den Symbolen aus und den in frei vorkommenden Variablen überein: Die Variable wird so oder so als interpretiert und die anderen freien Variablen aus sind auch in frei. Nach Induktionsvoraussetzung gilt und daher wiederum .
- Substitution
Wir besprechen nun die Variablensubstitution, wobei wir weitgehend der Darstellung von Ebbinghaus, Flum, Thomas folgen.
Variablen repräsentieren verschiedene Werte
(in einer Grundmenge ),
die man für sie einsetzen kann. Auf formaler Ebene bedeutet dies, dass eine oder mehrere Variablen durch gewisse Terme ersetzt werden. Im semantischen Kontext wird dies durch die Uminterpretation von Variablen bei einer Interpretation präzise gemacht. Im syntaktischen Kontext spricht man von Substitution, die wir nun definieren 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 entweder eine durchnummerierte
(und abzählbare)
Variablenmenge zugrunde, oder aber eine beliebig große Variablenmenge, die mit einer Wohlordnung versehen sei.
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 .
- Für eine Variable ist
-
- Für eine Konstante ist
-
- Für ein -stelliges Funktionssymbol und Terme ist
-
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 .
- Für Terme setzt man[1]
-
- Für ein -stelliges Relationssymbol und Terme setzt man
-
- Für einen Ausdruck setzt man
-
- Für Ausdrücke und setzt man
-
und ebenso für die anderen zweistelligen Junktoren.
- 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, stiftet eine Beziehung zwischen Substitutionen und Uminterpretationen.
In Verallgemeinerung der Schreibweise für eine Uminterpretation schreiben wir für die sukzessive Uminterpretation der untereinander verschiedenen Variablen
(dabei seien Elemente der Grundmenge der Interpretation).
Es werden also die als interpretiert und alle anderen Variablen werden gemäß interpretiert.
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.
- Für jeden
-
Term
gilt
-
- Für jeden
-
Ausdruck
gilt
-
Dies wird über den induktiven Aufbau der Terme bzw. der Ausdrücke bewiesen. (1). Für eine Konstante ist die Aussage richtig, da ihre Interpretation unverändert ist. Für eine Variable macht man eine Fallunterscheidung. Wenn
-
mit einer der an der Substitution beteiligten Variablen ist, so ist
-
Bei einer an der Substitution nicht beteiligten Variablen ist
-
Wenn ein -stelliges Funktionssymbol ist und Terme sind, für die die Gleichheit schon bekannt ist, so ist
(2). Für einen Ausdruck der Form
bedeutet
-
einfach
-
Dies ist äquivalent zu
-
was nach dem ersten Teil einfach
-
bedeutet. Dies wiederum ist äquivalent zu
-
Es sei nun ein -stelliges Relationssymbol und seien Terme. Die Gültigkeit
-
bedeutet
-
und dies bedeutet, dass
-
zur Relation gehört. Nach dem ersten Teil ist dieses Tupel gleich
-
Wegen
ist dies äquivalent zu
-
Für die weiteren Aussagen beweist man die Äquivalenz durch Induktion über den Aufbau der Ausdrücke, und zwar über alle Interpretationen simultan; dies ist für die aussagenlogischen Junktoren unmittelbar klar. Betrachten wir also einen Ausdruck der Form . Die Gültigkeit
-
bedeutet gemäß der Festlegung in
Definition 9.4,
dass
-
gilt, wobei in nicht vorkommt. Dies bedeutet, dass für jedes
der Grundmenge der Interpretation die Beziehung
-
gilt. Nach Induktionsvoraussetzung
(angewendet auf die Interpretation )
bedeutet dies
-
für alle
.
Aufgrund
des Koinzidenzlemmas
ist dies äquivalent zu
-
Dies ist äquivalent
(für alle
)
zu
-
was bei
klar ist und bei
aus dem Koinzidenzlemma
folgt, da dann nicht in vorkommt. Dies bedeutet wiederum
-
und damit, wiederum nach dem Koinzidenzlemma, da die von verschiedenen Variablen in nicht frei vorkommen,
-
- Fußnoten
- ↑ Die Klammern unterstreichen hier lediglich den Gesamtausdruck, für den die Substitution durchgeführt wird