Kurs:Einführung in die mathematische Logik (Osnabrück 2014)/Vorlesung 14/latex
\setcounter{section}{14}
\zwischenueberschrift{Die Korrektheit des Ableitungskalküls}
Im Laufe der Einführung des syntaktischen Prädikatenkalküls haben wir gesehen, dass die in ihm ableitbaren Ausdrücke allgemeingültig sind, dass also sämtliche durch den Prädikatenkalkül generierten formalen Tautologien auch semantische Tautologien sind. Wir halten den sogenannten \stichwort {Korrektheitssatz (für Tautologien)} {} fest.
\inputfaktbeweis
{Vollständigkeitssatz/Korrektheitssatz für Tautologien/Fakt}
{Satz}
{}
{
\faktsituation {Es sei $S$ ein
\definitionsverweis {Symbolalphabet}{}{}
und sei
\mavergleichskette
{\vergleichskette
{ \alpha
}
{ \in }{ L^S
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
eine
\definitionsverweis {syntaktische Tautologie}{}{.}}
\faktfolgerung {Dann ist $\alpha$ auch eine
\definitionsverweis {semantische Tautologie}{}{.}}
\faktzusatz {}
\faktzusatz {}
}
{
Dies ergibt sich aus den einzelnen Korrektheitsüberlegungen im Anschluss an die Ableitungsregeln, siehe beispielsweise Lemma 11.4.
Der entworfene Kalkül produziert also nur inhaltlich korrekte Ableitungen. Eine gleichwertige Variante davon bezieht sich auf die Ableitbarkeit und die Folgerung.
\inputfaktbeweis
{Vollständigkeitssatz/Korrektheitssatz/Fakt}
{Satz}
{}
{
\faktsituation {Es sei $S$ ein
\definitionsverweis {Symbolalphabet}{}{,}
$\Gamma$ eine Menge an
$S$-\definitionsverweis {Ausdrücken}{}{}
und $\alpha$ ein weiterer $S$-Ausdruck.}
\faktfolgerung {Dann folgt aus der
\definitionsverweis {Ableitungsbeziehung}{}{}
\mathl{\Gamma \vdash \alpha}{} die
\definitionsverweis {Folgerungsbeziehung}{}{}
\mathl{\Gamma \vDash \alpha}{.}}
\faktzusatz {}
\faktzusatz {}
}
{
Es sei
\mathl{\Gamma \vdash \alpha}{} vorausgesetzt. Dann gibt es endlich viele Ausdrücke
\mavergleichskette
{\vergleichskette
{ \alpha_1 , \ldots , \alpha_n
}
{ \in }{ \Gamma
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
derart, dass
\mavergleichskette
{\vergleichskette
{\varphi
}
{ = }{ \alpha_1 \wedge \ldots \wedge \alpha_n \rightarrow \alpha
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
eine formale Tautologie ist. Nach
Satz 14.1
ist $\varphi$ auch allgemeingültig. Es sei $I$ eine Interpretation mit
\mathl{I \vDash \Gamma}{.} Dann ist insbesondere
\mathl{I \vDash \alpha_1 \wedge \ldots \wedge \alpha_n}{} und wegen der Allgemeingültigkeit von $\varphi$ gilt
\mathl{I \vDash \varphi}{.} Also gilt auch
\mathl{I \vDash \alpha}{.}
Die Umkehrung dieser beiden Aussagen ist deutlich schwieriger: Es geht um die Frage, ob der Kalkül jeden allgemeingültigen Ausdruck formal ableiten kann, ob es also für jeden mathematischen Beweis eines Ausdrucks einer Sprache erster Stufe auch einen formalen Beweis gibt. Es ist die Frage, ob der Kalkül \stichwort {vollständig} {} ist. Dies ist in der Tat der Fall. Dies ist der Inhalt des \stichwort {Vollständigkeitssatzes} {,} der auf Gödel zurückgeht und den wir in dieser und der nächsten Vorlesung beweisen werden. Der Beweis ist recht aufwändig, so dass wir kurz die Strategie erläutern, die in einer einfacheren Form schon im Beweis des Vollständigkeitssatzes für die Aussagenlogik verwendet wurde. Wir verwenden Kontraposition und zeigen, dass aus der Nichtableitbarkeit
\mathl{\Gamma \not \vdash \alpha}{} die Nichtfolgerung
\mathl{\Gamma \not\vDash \alpha}{} folgt. Ersteres bedeutet, dass
\mathl{\Gamma \cup \{ \neg \alpha \}}{} widerspruchsfrei ist, und Letzteres bedeutet, dass
\mathl{\Gamma \cup \{ \neg \alpha \}}{} erfüllbar ist. Wir zeigen daher allgemein, dass eine widerspruchsfreie Ausdrucksmenge erfüllbar ist.
Dazu füllen wir eine widerspruchsfreie Ausdrucksmenge, analog zum aussagenlogischen Fall
\zusatzklammer {siehe
Lemma 5.17} {} {,}
zu einer maximal widerspruchsfreien Ausdrucksmenge auf. Wenn diese zusätzlich \anfuehrung{Beispiele enthält}{}
\zusatzklammer {um das zu erreichen, muss man die Symbolmenge erweitern} {} {}
so kann man auf der Sprache eine Äquivalenzrelation definieren, deren Äquivalenzklassen die Grundlage eines erfüllenden Modells bilden. Wir beginnen mit dem \stichwort {Satz von Henkin} {,} der die Erfüllbarkeit im maximal widerspruchsfreien Fall mit Beispielen erledigt.
\zwischenueberschrift{Der Satz von Henkin}
\inputdefinition
{}
{
Eine Menge $\Gamma$ an
$S$-\definitionsverweis {Ausdrücken}{}{}
\zusatzklammer {über einem
\definitionsverweis {Symbolalphabet}{}{}
$S$} {} {}
heißt
\definitionswort {maximal widerspruchsfrei}{,}
wenn sie
\definitionsverweis {widerspruchsfrei}{}{}
ist und wenn jede Hinzunahme eines jeden Ausdrucks
\mavergleichskette
{\vergleichskette
{ \alpha
}
{ \notin }{\Gamma
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
die Menge widersprüchlich macht.
}
\inputdefinition
{}
{
Man sagt, dass eine Menge $\Gamma$ an
$S$-\definitionsverweis {Ausdrücken}{}{}
\zusatzklammer {über einem
\definitionsverweis {Symbolalphabet}{}{}
$S$} {} {}
\definitionswort {Beispiele enthält}{,}
wenn es für jeden Ausdruck der Form
\mathl{\exists x \alpha}{} einen
$S$-\definitionsverweis {Term}{}{}
$t$ derart gibt, dass
\mathdisp {\exists x \alpha \rightarrow \alpha { \frac{ t }{ x } }} { }
zu $\Gamma$ gehört.
}
Diese beiden Begriffe sind durch folgende Aussage motiviert.
\inputfaktbeweis
{Logik/Modell/Maximal widerspruchsfrei/Beispiele/Fakt}
{Lemma}
{}
{
\faktsituation {Es sei $S$ ein
\definitionsverweis {Symbolalphabet}{}{}
und $I$ eine
$S$-\definitionsverweis {Interpretation}{}{}
auf einer Menge $M$,}
\faktvoraussetzung {wobei die
\definitionsverweis {Terminterpretation}{}{} \definitionsverweis {surjektiv}{}{}
sei.}
\faktfolgerung {Dann ist die Gültigkeitsmenge
\mavergleichskette
{\vergleichskette
{ \Gamma
}
{ = }{I^\vDash
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
\definitionsverweis {maximal widerspruchsfrei}{}{}
und
\definitionsverweis {enthält Beispiele}{}{.}}
\faktzusatz {}
\faktzusatz {}
}
{
\teilbeweis {}{}{}
{Zunächst ist
\mavergleichskette
{\vergleichskette
{\Gamma
}
{ = }{I^\vDash
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
aufgrund des
Korrektheitssatzes
abgeschlossen unter Ableitungen. Für jeden
$S$-\definitionsverweis {Ausdruck}{}{}
$\alpha$ gilt die Alternative: Entweder
\mavergleichskette
{\vergleichskette
{ \alpha
}
{ \in }{\Gamma
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
oder
\mavergleichskette
{\vergleichskette
{ \neg \alpha
}
{ \in }{\Gamma
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{.}
Insbesondere ist $\Gamma$ widerspruchsfrei. Wenn
\mavergleichskette
{\vergleichskette
{ \alpha
}
{ \notin }{\Gamma
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
ist, so ist
\mavergleichskette
{\vergleichskette
{ \neg \alpha
}
{ \in }{\Gamma
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
und daher ist
\mathl{\Gamma \cup \{ \alpha \}}{} widersprüchlich. Also ist $\Gamma$ maximal widerspruchsfrei.}
{}
\teilbeweis {}{}{}
{Wir betrachten nun einen Ausdruck der Form
\mavergleichskette
{\vergleichskette
{\alpha
}
{ = }{\exists x \beta
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{.}
Wenn
\mavergleichskette
{\vergleichskette
{ \alpha
}
{ \notin }{\Gamma
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
gilt, so gilt
\mathl{\exists x \beta \rightarrow \beta { \frac{ t }{ x } }}{} in $I$ für jeden Term $t$, da ja der Vordersatz nicht gilt. Wenn hingegen
\mavergleichskette
{\vergleichskette
{ \alpha
}
{ \in }{\Gamma
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
gilt, so gibt es aufgrund des semantischen Aufbaus der Gültigkeitbeziehung ein
\mavergleichskette
{\vergleichskette
{m
}
{ \in }{M
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
derart, dass
\mathl{I{ \frac{ m }{ x } } \vDash \beta}{} gilt. Wegen der vorausgesetzten Surjektivität der Belegung gibt es einen Term $t$, der durch $m$ interpretiert wird. Daher gilt
nach dem Substitutionslemma
\mathl{\beta { \frac{ t }{ x } }}{} in $I$. Also gilt
\mathl{\exists x \beta \rightarrow \beta { \frac{ t }{ x } }}{} in $I$.}
{}
\inputfaktbeweis
{Prädikatenlogik/Maximal widerspruchsfrei/Folgerungen/Fakt}
{Lemma}
{}
{
\faktsituation {Es sei $\Gamma$ eine Menge an
$S$-\definitionsverweis {Ausdrücken}{}{}
\zusatzklammer {über einem
\definitionsverweis {Symbolalphabet}{}{}
$S$} {} {,}
die
\definitionsverweis {maximal widerspruchsfrei}{}{}
ist.}
\faktuebergang {Dann gelten folgende Eigenschaften.}
\faktfolgerung {\aufzaehlungdrei{Für jeden Ausdruck $\alpha$ ist entweder
\mavergleichskette
{\vergleichskette
{ \alpha
}
{ \in }{ \Gamma
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
oder
\mavergleichskette
{\vergleichskette
{ \neg \alpha
}
{ \in }{ \Gamma
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{.}
}{Aus
\mathl{\Gamma \vdash \alpha}{} folgt
\mavergleichskette
{\vergleichskette
{ \alpha
}
{ \in }{ \Gamma
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{,}
d.h. $\Gamma$ ist abgeschlossen unter Ableitungen.
}{Für Ausdrücke
\mathl{\alpha , \beta}{} ist
\mavergleichskette
{\vergleichskette
{ \alpha \wedge \beta
}
{ \in }{ \Gamma
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
genau dann, wenn
\mathkor {} {\alpha \in \Gamma} {und} {\beta \in \Gamma} {}
ist.
}}
\faktzusatz {}
\faktzusatz {}
}
{
\teilbeweis {}{}{}
{(1). Wegen der Widerspruchsfreiheit kann nicht sowohl $\alpha$ als auch $\neg \alpha$ zu $\Gamma$ gehören. Wenn weder $\alpha$ noch
\mathl{\neg \alpha}{} zu $\Gamma$ gehören, so ist entweder
\mathl{\Gamma \cup \{ \alpha \}}{} oder
\mathl{\Gamma \cup \{ \neg \alpha \}}{} widerspruchsfrei. Wären nämlich beide widersprüchlich, so würde für einen beliebigen Ausdruck $\beta$ sowohl
\mathdisp {\Gamma \cup \{ \alpha \} \vdash \beta} { }
als auch
\mathdisp {\Gamma \cup \{ \neg \alpha \} \vdash \beta} { }
gelten. Dies bedeutet
\mathdisp {\Gamma \vdash \alpha \rightarrow \beta} { }
und
\mathdisp {\Gamma \vdash \neg \alpha \rightarrow \beta} { , }
woraus aufgrund der
Fallunterscheidungsregel
\mathdisp {\Gamma \vdash \beta} { }
folgt. Dies bedeutet aber, dass $\Gamma$ widersprüchlich ist.}
{}
\teilbeweis {}{}{}
{(2). Es sei
\mathl{\Gamma \vdash \alpha}{.} Nach (1) ist
\mavergleichskette
{\vergleichskette
{ \alpha
}
{ \in }{ \Gamma
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
oder
\mavergleichskette
{\vergleichskette
{ \neg \alpha
}
{ \in }{ \Gamma
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{.}
Das zweite kann nicht sein, da sich daraus sofort ein Widerspruch ergeben würde. Also ist
\mavergleichskette
{\vergleichskette
{ \alpha
}
{ \in }{ \Gamma
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{.}}
{}
\teilbeweis {}{}{}
{(3). Die Richtung von links nach rechts folgt aus (2). Es seien also
\mavergleichskette
{\vergleichskette
{ \alpha, \beta
}
{ \in }{ \Gamma
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{.}
Da
\mathl{\alpha \rightarrow { \left( \beta \rightarrow \alpha \wedge \beta \right) }}{}
nach Aufgabe 3.14
eine Tautologie ist, folgt
\mavergleichskette
{\vergleichskette
{ \alpha \wedge \beta
}
{ \in }{\Gamma
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
nach Teil (2).}
{}
Wir werden nun umgekehrt zu
Lemma 14.5
zeigen, dass man zu einer jeden maximal widerspruchsfreien Ausdrucksmenge $\Gamma$, die Beispiele enthält, eine Interpretation konstruieren kann, deren Gültigkeitsmenge mit $\Gamma$ übereinstimmt. Diese Konstruktion, die wir die \stichwort {kanonische Term\-identifizierung} {} nennen, geht folgendermaßen.
\inputkonstruktion{}
{
Es sei $\Gamma$ eine Menge an
$S$-\definitionsverweis {Ausdrücken}{}{}
\zusatzklammer {über einem
\definitionsverweis {Symbolalphabet}{}{}
$S$} {} {,}
die
\definitionsverweis {abgeschlossen unter Ableitungen}{}{}
ist. Dann definiert man auf der Menge aller
$S$-\definitionsverweis {Terme}{}{}
eine
\definitionsverweis {Äquivalenzrelation}{}{}
durch
\mathdisp {t \sim s \text{ genau dann, wenn der Ausdruck } t=s \text{ zu } \Gamma \text{ gehört}} { . }
Es sei $M$ die Menge der Termklassen
\zusatzklammer {also die Menge der Äquivalenzklassen zu dieser Äquivalenzrelation} {} {.}
Auf $M$ definiert man für jedes $n$-stellige
\definitionsverweis {Relationssymbol}{}{}
$R$ eine $n$-stellige
\definitionsverweis {Relation}{}{}
\mathl{R^M}{} durch
\mathdisp {R^M([t_1],[t_2] , \ldots , [t_n] ) \text{ genau dann, wenn der Ausdruck } R t_1 t_2 \cdots t_n \text{ zu } \Gamma \text{ gehört}} { }
und für jedes $n$-stellige
\definitionsverweis {Funktionssymbol}{}{}
$f$ eine $n$-stellige
\definitionsverweis {Funktion}{}{}
\mathl{f^M}{} durch
\mavergleichskettedisp
{\vergleichskette
{ f^M([t_1],[t_2] , \ldots , [t_n] )
}
{ \defeq} {[ f t_1 t_2 \cdots t_n ]
}
{ } {
}
{ } {
}
{ } {
}
}
{}{}{.}
Konstanten werden als
\mavergleichskettedisp
{\vergleichskette
{c^M
}
{ \defeq} {[c]
}
{ } {
}
{ } {
}
{ } {
}
}
{}{}{}
interpretiert.
}
Wir müssen natürlich zunächst zeigen, dass wirklich eine Äquivalenzrelation vorliegt und dass die Relationen und Funktionen wohldefiniert sind.
\inputfaktbeweis
{Logik/Vollständigkeitssatz/Modellkonstruktion/Fakt}
{Lemma}
{}
{
\faktsituation {Es sei $\Gamma$ eine Menge an
$S$-\definitionsverweis {Ausdrücken}{}{}
\zusatzklammer {über einem
\definitionsverweis {Symbolalphabet}{}{}
$S$} {} {,}
die
\definitionsverweis {abgeschlossen unter Ableitungen}{}{}
ist.}
\faktfolgerung {Dann liefert die in
Konstruktion 14.7
beschriebene Konstruktion eine Äquivalenzrelation auf der Menge aller Terme und wohldefinierte Relationen bzw. Funktionen auf der Menge der Termklassen.}
\faktzusatz {}
\faktzusatz {}
}
{
Eine Äquivalenzrelation liegt aufgrund von Axiom 10.5 (1) und Lemma 10.7 (1), (2) vor, da ja $\Gamma$ nach Voraussetzung abgeschlossen unter Ableitungen ist und insbesondere alle syntaktischen Tautologien enthält.
Es sei $M$ die Menge der Äquivalenzklassen, die wir in diesem Zusammenhang Termklassen nennen. Es sei $R$ ein $n$-stelliges Relationssymbol. Es sei
\mathl{([s_1] , \ldots , [s_n])}{} ein $n$-Tupel aus Termklassen, die einerseits durch das Termtupel
\mathl{(s_1 , \ldots , s_n)}{} und andererseits durch das Termtupel
\mathl{(t_1 , \ldots , t_n)}{} repräsentiert werde. Es gilt also
\mathl{s_i \sim t_i}{} bzw.
\mavergleichskette
{\vergleichskette
{ s_i = t_i
}
{ \in }{ \Gamma
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{.}
Wenn nun
\mathl{R s_1 \ldots s_n}{} zu $\Gamma$ gehört, so folgt aus
Lemma 10.7 (4)
auch
\mavergleichskette
{\vergleichskette
{ R t_1 \ldots t_n
}
{ \in }{ \Gamma
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{.}
Unter den gleichen Voraussetzungen folgt mit
Lemma 10.7 (3)
die Zugehörigkeit
\mathl{fs_1 \ldots s_n=ft_1 \ldots t_n \in \Gamma}{} und somit
\mavergleichskettedisp
{\vergleichskette
{[ fs_1 \ldots s_n]
}
{ =} {[ ft_1 \ldots t_n]
}
{ } {
}
{ } {
}
{ } {
}
}
{}{}{,}
also die Wohldefiniertheit der Funktion.
\inputfaktbeweis
{Logik/Vollständigkeitssatz/Modellkonstruktion/Konsistente Terminterpretation/Fakt}
{Lemma}
{}
{
\faktsituation {Es sei $\Gamma$ eine Menge an
$S$-\definitionsverweis {Ausdrücken}{}{}
\zusatzklammer {über einem
\definitionsverweis {Symbolalphabet}{}{}
$S$} {} {,}
die
\definitionsverweis {abgeschlossen unter Ableitungen}{}{}
ist.}
\faktfolgerung {Dann gilt für die Interpretation
\mathl{(M, \beta)}{,} wobei $M$ die in
Konstruktion 14.7
beschriebene Menge aus Termklassen
\zusatzklammer {mit der natürlichen Interpretation $I$ von Konstanten, Funktionssymbolen und Relationssymbolen} {} {}
und $\beta$ die natürliche Belegung
\mavergleichskette
{\vergleichskette
{\beta(x)
}
{ = }{[x]
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
für Variablen ist, die Beziehung
\mavergleichskettedisp
{\vergleichskette
{I(t)
}
{ =} {[t]
}
{ } {
}
{ } {
}
{ } {
}
}
{}{}{}
für alle Terme $t$.}
\faktzusatz {}
\faktzusatz {}
}
{
Wir führen Induktion über den Aufbau der Terme, wobei der Induktionsanfang unmittelbar durch die natürliche Belegung gesichert ist. Die Aussage gelte nun für Terme
\mathl{t_1 , \ldots , t_n}{} und $f$ sei ein $n$-stelliges Funktionssymbol. Dann ist
\mavergleichskettedisp
{\vergleichskette
{I (ft_1 \ldots t_n)
}
{ =} { f^M(I(t_1) , \ldots , I(t_n))
}
{ =} { f^M([t_1] , \ldots , [t_n] )
}
{ =} { [ft_1 \ldots t_n]
}
{ } {
}
}
{}{}{.}
Die folgende Aussage heißt \stichwort {Satz von Henkin} {.} Er wird durch Induktion über den sogenannten Rang eines Ausdrucks bewiesen. Dazu definieren wir.
\inputdefinition
{}
{
Unter einem
\definitionswort {atomaren Ausdruck}{}
versteht man Ausdrücke der Form
\mavergleichskette
{\vergleichskette
{s
}
{ = }{t
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{,}
wobei $s$ und $t$ Terme sind, und der Form
\mathl{Rt_1 \ldots t_n}{,} wobei $R$ ein $n$-stelliges Relationssymbol ist und
\mathl{t_1 , \ldots , t_n}{} Terme sind.
}
\inputdefinition
{}
{
Es sei ein
\definitionsverweis {Alphabet einer Sprache erster Stufe}{}{}
gegeben. Dann definiert man für Ausdrücke
\mavergleichskette
{\vergleichskette
{ \alpha
}
{ \in }{ L^S
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
den
\definitionswort {Rang}{}
$\rho$ von $\alpha$ durch
\aufzaehlungvier{
\mavergleichskette
{\vergleichskette
{ \rho( \alpha )
}
{ = }{ 0
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{,}
falls $\alpha$ atomar ist.
}{
\mavergleichskette
{\vergleichskette
{ \rho( \alpha )
}
{ = }{ \rho( \beta )+1
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{,}
falls
\mavergleichskette
{\vergleichskette
{ \alpha
}
{ = }{ \neg ( \beta )
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
ist.
}{
\mavergleichskette
{\vergleichskette
{\rho( \alpha )
}
{ = }{ \rho( \beta ) + \rho( \gamma ) + 1
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{,}
falls
\mavergleichskette
{\vergleichskette
{\alpha
}
{ = }{ ( \beta ) \circ ( \gamma )
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
mit
\mavergleichskette
{\vergleichskette
{\circ
}
{ = }{ \wedge,\, \vee, \, \rightarrow, \leftrightarrow
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
ist.
}{
\mavergleichskette
{\vergleichskette
{\rho( \alpha )
}
{ = }{ \rho( \beta ) +1
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{,}
falls
\mavergleichskette
{\vergleichskette
{ \alpha
}
{ = }{ \exists x \beta
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
oder
\mavergleichskette
{\vergleichskette
{ \alpha
}
{ = }{ \forall x \beta
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
ist.
}
}
Diese beiden Begriffe sind vor allem dann wichtig, wenn man eine Aussage über alle Ausdrücke induktiv beweisen möchte.
\inputfaktbeweis
{Logik/Vollständigkeitssatz/Henkin/Fakt}
{Satz}
{}
{
\faktsituation {Es sei $\Gamma$ eine Menge an
$S$-\definitionsverweis {Ausdrücken}{}{}
\zusatzklammer {über einem
\definitionsverweis {Symbolalphabet}{}{}
$S$} {} {,}
die
\definitionsverweis {maximal widerspruchsfrei}{}{}
ist und
\definitionsverweis {Beispiele enthält}{}{.}}
\faktfolgerung {Dann ist die in
Konstruktion 14.7
gegebene Interpretation ein Modell für $\Gamma$.}
\faktzusatz {Insbesondere ist $\Gamma$
\definitionsverweis {erfüllbar}{}{.}}
\faktzusatz {}
}
{
Es sei $M$ das konstruierte Modell zu $\Gamma$ und $I$ die zugehörige Interpretation mit der natürlichen Belegung für die Variablen. Wir zeigen die Äquivalenz
\mathdisp {\alpha \in \Gamma \text{ genau dann, wenn } I \vDash \alpha} { }
für alle Ausdrücke $\alpha$, durch Induktion über den
\definitionsverweis {Rang}{}{}
der Ausdrücke. Zum Induktionsanfang sei der Rang von $\alpha$ gleich $0$, also $\alpha$
\definitionsverweis {atomar}{}{.}
D.h. $\alpha$ ist entweder von der Form
\mathkor {} {s=t} {oder} {Rt_1 \ldots t_n} {.}
Im ersten Fall ist
\mavergleichskette
{\vergleichskette
{s = t
}
{ \in }{ \Gamma
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
äquivalent zu
\mavergleichskette
{\vergleichskette
{s
}
{ \sim }{t
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
bzw.
\mavergleichskette
{\vergleichskette
{[s]
}
{ = }{[t]
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
in $M$. Dies ist nach
Lemma 14.9
äquivalent zu
\mavergleichskette
{\vergleichskette
{I(s)
}
{ = }{I(t)
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
und das bedeutet
\mathl{I \vDash s= t}{.}
Im zweiten Fall ist
\mavergleichskette
{\vergleichskette
{ Rt_1 \ldots t_n
}
{ \in }{ \Gamma
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
\zusatzgs {nach Konstruktion von $M$ und $R^M$} {}
äquivalent zu
\mathl{R^M([t_1] , \ldots , [t_n])}{,} und dies ist äquivalent zu
\mathl{I \vDash Rt_1 \ldots t_n}{.}
Es sei nun die Aussage für alle Ausdrücke vom Rang $\leq r$ bewiesen und sei $\alpha$ ein Ausdruck vom Rang
\mathl{r+1}{.} Wir betrachten die mögliche Struktur von $\alpha$ gemäß
Definition 7.2.
Bei
\mavergleichskettedisp
{\vergleichskette
{ \alpha
}
{ =} {\neg \beta
}
{ } {
}
{ } {
}
{ } {
}
}
{}{}{}
ergibt sich die Äquivalenz aus der Induktionsvoraussetzung
\zusatzklammer {$\beta$ hat kleineren Rang als $\alpha$} {} {}
und
Lemma 14.6 (1).
Bei
\mavergleichskettedisp
{\vergleichskette
{ \alpha
}
{ =} { \beta_1 \wedge \beta_2
}
{ } {
}
{ } {
}
{ } {
}
}
{}{}{}
besitzen die beiden Bestandteile kleineren Rang als $\alpha$. Die Zugehörigkeit
\mavergleichskette
{\vergleichskette
{ \alpha
}
{ \in }{\Gamma
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
ist nach
Lemma 14.6 (3)
äquivalent zur gemeinsamen Zugehörigkeit
\mavergleichskette
{\vergleichskette
{ \beta_1, \beta_2
}
{ \in }{ \Gamma
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{.}
Nach Induktionsvoraussetzung bedeutet dies
\mathkor {} {I \vDash \beta_1} {und} {I \vDash \beta_2} {.}
Dies bedeutet wiederum
\mathl{I \vDash \beta_1 \wedge \beta_2}{} aufgrund der
\definitionsverweis {Modellbeziehung}{}{.}
Bei
\mavergleichskettedisp
{\vergleichskette
{\alpha
}
{ =} {\exists x \beta
}
{ } {
}
{ } {
}
{ } {
}
}
{}{}{}
besitzt wieder $\beta$ einen kleineren Rang. Die Zugehörigkeit
\mavergleichskette
{\vergleichskette
{ \alpha
}
{ \in }{ \Gamma
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
ist aufgrund der Eigenschaft, Beispiele zu enthalten und aufgrund von
Axiom 11.1
äquivalent zur Existenz eines Terms $t$ und der Zugehörigkeit
\mavergleichskette
{\vergleichskette
{ \beta \frac{t}{x}
}
{ \in }{ \Gamma
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{.}
Die Substitution von $\beta$ nach
\mathl{\beta \frac{t}{x}}{} verändert nach
Aufgabe 14.3
nicht den Rang. Wir können also auf
\mathl{\beta \frac{t}{x}}{} die Induktionsvoraussetzung anwenden und erhalten die Äquivalenz zu
\mathl{I \vDash \beta \frac{t}{x}}{.} Nach
dem Substitutionslemma
ist dies äquivalent zu
\mathl{I \frac{I(t)}{x} \vDash \beta}{} bzw.
\mathl{I \frac{[t]}{x} \vDash \beta}{} wegen
Lemma 14.9.
Dies ist äquivalent zu
\mathl{I \vDash \exists x \beta}{} aufgrund der
\definitionsverweis {Modellbeziehung}{}{}
und der Surjektivität der Termabbildung.