Kurs:Einführung in die mathematische Logik (Osnabrück 2011-2012)/Vorlesung 7/latex
\setcounter{section}{7}
\zwischenueberschrift{Quantorenaxiome und -regeln}
Wir besprechen nun die Tautologien und Ableitungsregeln, die mit den Quantoren zusammenhängen. Wir arbeiten allein mit dem Existenzquantor und wir arbeiten nur mit nichtleeren Grundmengen. Letzteres ist Voraussetzung dafür, dass es überhaupt eine Variablenbelegung geben kann. Bei den jetzt einzuführenden Axiomen handelt es sich um eine Tautologie \zusatzklammer {genauer gesagt um ein Schema von Tautologien} {} {,} nämlich die \stichwort {Existenzeinführung im Sukzedens} {} und um eine Schlussregel, nämlich die \stichwort {Existenzeinführung im Antezedens} {.} Für letztere ist die exakte Formulierung und der Korrektheitsnachweis nicht trivial.
\inputaxiom
{}
{
Es sei $S$ ein
\definitionsverweis {Symbolalphabet erster Stufe}{}{,}
$\alpha$ ein
$S$-\definitionsverweis {Ausdruck}{}{,}
$x$ eine Variable und $t$ ein
$S$-\definitionsverweis {Term}{}{.}
Dann ist
\mathdisp {\vdash \alpha \frac{t}{x} \rightarrow \exists x \alpha} { . }
}
Diese Tautologie bedeutet inhaltlich gesprochen, dass ein Ausdruck, für den man einen erfüllenden Term gefunden hat, auf die entsprechende Existenzaussage schließen kann. Diese Tautologie ist allgemeingültig: Wenn in einer Interpretation $I$ die Beziehung
\mathdisp {I \vDash p \frac{t}{x}} { }
gilt, so ist dies nach dem
Substitutionslemma
äquivalent zu
\mathdisp {I \frac{I(t)}{x} \vDash p} { , }
und das bedeutet wiederum
\mathdisp {I \vDash \exists x p} { . }
Einen wichtigen Spezialfall dieser Tautologie erhält man für
\mathl{t=x}{,} nämlich
\mathdisp {\vdash p \rightarrow \exists x p} { . }
Für den Allquantor (den wir als Abkürzung verstehen) ergibt sich die entsprechende Tautologie
\mathdisp {\vdash \forall x p \rightarrow p \frac{t}{x}} { . }
\inputaxiom
{}
{
Es sei $S$ ein
\definitionsverweis {Symbolalphabet erster Stufe}{}{,}
\mathkor {} {\alpha} {und} {\beta} {}
seien
$S$-\definitionsverweis {Ausdrücke}{}{,}
\mathkor {} {x} {und} {y} {}
seien Variablen. Dann gilt die folgende Regel:
Wenn
\mathdisp {\vdash \alpha \frac{y}{x} \rightarrow \beta} { }
gilt und wenn $y$ weder in
\mathl{\exists x \alpha}{} noch in $\beta$ frei vorkommt, so gilt auch
\mathdisp {\vdash \exists x \alpha \rightarrow \beta} { . }
}
Ein Spezialfall dieser Ableitungsregel ist, dass man aus
\mathl{\vdash p \rightarrow q}{} unter der Bedingung, dass $x$ nicht frei in $q$ vorkommt, auf
\mathl{\vdash \exists x p \rightarrow q}{} schließen kann.
Die Allvariante dieser Schlussregel ist die \stichwort {All\-einführung im Sukzedens} {.} Sie besagt, dass man aus
\mathdisp {\vdash q \rightarrow p \frac{y}{x}} { }
unter der Bedingung, dass $y$ weder in $\forall x p$ noch in $q$ frei vorkommt, auf
\mathdisp {\vdash q \rightarrow \forall x p} { }
schließen kann.
Die Existenzeinführung im Antezedens ist die einzige syntaktische Gesetzmäßigkeit, deren Korrektheit nicht unmittelbar klar ist.
\inputfaktbeweis
{Prädikatenlogik/Existenzeinführung im Antezedens/Korrektheit/Fakt}
{Lemma}
{}
{
\faktsituation {}
\faktfolgerung {Die
Existenzeinführung im Antezedens
ist eine korrekte Regel.}
\faktzusatz {}
\faktzusatz {}
}
{
Es sei
\mathl{\alpha \frac{y}{x} \rightarrow \beta}{}
\definitionsverweis {allgemeingültig}{}{,}
d.h.
\mathdisp {I \vDash \alpha \frac{y}{x} \rightarrow \beta} { }
für jede
$S$-\definitionsverweis {Interpretation}{}{}
$I$. Wir müssen zeigen, dass dann auch
\mathl{\exists x \alpha \rightarrow \beta}{} allgemeingültig ist
\zusatzklammer {unter den gegebenen Voraussetzungen} {} {.}
Es sei dazu $I$ eine Interpretation mit
\mathdisp {I \vDash \exists x \alpha} { . }
Aufgrund der
\definitionsverweis {Modellbeziehung}{}{}
bedeutet dies, dass es ein
\mavergleichskette
{\vergleichskette
{m
}
{ \in }{M
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
\zusatzklammer {aus der Grundmenge der Interpretation} {} {}
mit
\mathdisp {I \frac{m}{x} \vDash \alpha} { }
gibt. Die Variable $y$ kommt nach Voraussetzung in $\exists x \alpha$ nicht frei vor, d.h. bei
\mavergleichskette
{\vergleichskette
{y
}
{ \neq }{x
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{,}
dass $y$ in $\alpha$ nicht frei vorkommt. Wir können daher
das Koinzidenzlemma
anwenden und erhalten
\mathdisp {{ \left( I \frac{m}{x} \right) } \frac{m}{y} \vDash \alpha} { . }
Diese Aussage gilt trivialerweise auch bei
\mavergleichskette
{\vergleichskette
{x
}
{ = }{y
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{.}
Damit gilt auch
\mathdisp {{ \left( I \frac{m}{y} \right) } \frac{m}{x} \vDash \alpha} { . }
Wir schreiben dies
\zusatzklammer {etwas künstlich} {} {}
als
\mathdisp {{ \left( I \frac{m}{y} \right) } \frac{ { \left( I\frac{m}{y} \right) }(y) }{x} \vDash \alpha} { . }
Darauf können wir
das Substitutionslemma
\zusatzklammer {für die Interpretation
\mavergleichskettek
{\vergleichskettek
{ J
}
{ = }{I \frac{m}{y}
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
und den Term $y$} {} {}
anwenden und erhalten
\mathdisp {I \frac{m}{y} \vDash \alpha \frac{y}{x}} { . }
Wegen der vorausgesetzten Allgemeingültigkeit von
\mathl{\alpha \frac{y}{x} \rightarrow \beta}{} folgt
\mathdisp {I \frac{m}{y} \vDash \beta} { . }
Da $y$ in $\beta$ nicht frei vorkommt, liefert
das Koinzidenzlemma
\mathdisp {I \vDash \beta} { . }
\inputbemerkung
{}
{
Die Variablenbedingung in der Existenzeinführung im Antezedenz ist wesentlich. Das zeigt am besten die Betrachtung
\mavergleichskette
{\vergleichskette
{ \beta
}
{ = }{ \alpha
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{,}
wobei darin die Variable
\mavergleichskette
{\vergleichskette
{x
}
{ = }{y
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
frei vorkommen möge
\zusatzklammer {also z.B.
\mavergleichskettek
{\vergleichskettek
{ \alpha
}
{ = }{ Rx
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{,}
wobei $R$ ein einstelliges Relationssymbol sei} {} {.}
Dann ist natürlich
\mathdisp {\vdash \alpha \rightarrow \alpha} { }
richtig, und die Variablenbedingung an $x$, bezogen auf diesen Ausdruck, ist nicht erfüllt. Die Aussage
\mathdisp {\exists x \alpha \rightarrow \alpha} { , }
die man unter Missachtung dieser Variablenbedingung ableiten könnte, ist keine Tautologie. Aus der Existenz eines Elementes
\mavergleichskette
{\vergleichskette
{m
}
{ \in }{M
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{,}
das die Relation
\mathl{R^M}{} erfüllt, folgt ja keineswegs, dass die Relation für alle Elemente gilt. Diese Ableitungsregel lässt sich also insbesondere nicht durch eine interne Tautologie ersetzen.
}
\zwischenueberschrift{Abgeleitete Regeln}
\inputfaktbeweis
{Prädikatenlogik/Ableitbar/Allquantor/Fakt}
{Lemma}
{}
{
\faktsituation {Es sei $S$ ein
\definitionsverweis {Symbolalphabet erster Stufe}{}{,}
$\alpha$ ein
$S$-\definitionsverweis {Ausdruck}{}{} und $x$ eine Variable.}
\faktfolgerung {Dann ist
\mathl{\vdash \alpha}{} genau dann, wenn
\mathl{\vdash \forall x \alpha}{} ist.}
\faktzusatz {}
\faktzusatz {}
}
{
\teilbeweis {}{}{}
{Nach der Allquantorversion von
Axiom 7.1
ist
\mathdisp {\vdash \forall x \alpha \rightarrow \alpha \frac{x}{x}} { , }
also
\mathdisp {\vdash \forall x \alpha \rightarrow \alpha} { . }
Daher folgt aus
\mathdisp {\vdash \forall x \alpha} { }
mittels
\definitionsverweis {Modus ponens}{}{}
direkt
\mathdisp {\vdash \alpha} { . }
}
{}
\teilbeweis {}{}{}
{Es sei umgekehrt
\mathl{\vdash \alpha}{} gegeben. Es sei $\beta$ ein beliebiger Ausdruck, in dem $x$ nicht vorkomme. Nach
Axiom 6.4 (1)
und Modus ponens ergibt sich
\mathdisp {\vdash \beta \rightarrow \alpha} { }
und
\mathdisp {\vdash \neg \beta \rightarrow \alpha} { . }
Auf diese beiden abgeleiteten Ausdrücke wird nun die Allquantorversion der
Existenzeinführung im Antezedens
\zusatzklammer {also die Alleinführung im Sukzedens} {} {}
angewendet. Dies ist möglich, da $x$ in $\beta$ überhaupt nicht und in
\mathl{\forall x \alpha}{} nicht frei vorkommt. Man erhält
\mathdisp {\vdash \beta \rightarrow \forall x \alpha} { }
und
\mathdisp {\vdash \neg \beta \rightarrow \forall x \alpha} { . }
Daraus ergibt sich mit der Fallunterscheidungsregel
\mathdisp {\vdash \forall x \alpha} { . }
}
{}
Diese Aussage bedeutet aber keineswegs, dass man den Allquantor überall weglassen oder hinzufügen könnte. Sie bedeutet lediglich, dass bei einem Ausdruck, der als Ganzes als eine Tautologie erwiesen ist, auch der entsprechende Allausdruck eine Tautologie ist und umgekehrt. Semantisch betrachtet beruht diese Äquivalenz darauf, dass die Allgemeingültigkeit von $p$ bedeutet, dass bei einer beliebigen \zusatzklammer {Struktur- und} {} {} Variablenbelegung die entstehende Aussage ohne freie Variable wahr wird. Da ist also eine Allaussage schon miteingebunden.
Für den Existenzquantor gilt die entsprechende Äquivalenz nicht. Zwar ergibt sich aus
\mathl{\vdash p}{} direkt
\mathl{\vdash \exists x p}{}
\zusatzklammer {und zwar unabhängig davon, ob $x$ in $p$ vorkommt oder nicht; die Allgemeingültigkeit beruht darauf, dass nur nichtleere Grundmengen betrachtet werden} {} {,}
aber nicht umgekehrt. Beispielsweise ist
\mathdisp {\vdash \exists x (x=y)} { , }
aber
\mathl{x=y}{} ist keine Tautologie.
\inputfaktbeweis
{Prädikatenlogik/Quantoren/Tautologien/Ableitungen/Fakt}
{Lemma}
{}
{
\faktsituation {}
\faktuebergang {Die folgenden Ausdrücke sind im Prädikatenkalkül
\definitionsverweis {ableitbar}{}{.}}
\faktfolgerung {\aufzaehlungfuenf{
\mathdisp {\vdash \exists x \exists y \alpha \rightarrow \exists y \exists x \alpha} { . }
}{
\mathdisp {\vdash \forall x \alpha \wedge \forall x (\alpha \rightarrow \beta) \rightarrow \forall x \beta} { . }
}{
\mathdisp {\vdash \forall x \alpha \wedge \forall x \beta \leftrightarrow \forall x { \left( \alpha \wedge \beta \right) }} { . }
}{
\mathdisp {\vdash \exists x \alpha \wedge \forall x (\alpha \rightarrow \beta) \rightarrow \exists x \beta} { . }
}{
\mathdisp {\vdash \exists x (\alpha \wedge \beta) \rightarrow \exists x \alpha \wedge \exists x \beta} { . }
}}
\faktzusatz {}
\faktzusatz {}
}
{
\teilbeweis {}{}{}
{(1). Durch
\definitionsverweis {Existenzeinführung im Sukzedenz}{}{}
haben wir
\mathdisp {\vdash \alpha \rightarrow \exists x \alpha} { }
und
\mathdisp {\vdash \exists x \alpha \rightarrow \exists y \exists x \alpha} { }
und daraus
\mathdisp {\vdash \alpha \rightarrow \exists y \exists x \alpha} { . }
Dabei ist $y$ hinten gebunden und somit kann man mit der
\definitionsverweis {Existenzeinführung im Antezedens}{}{}
auf
\mathdisp {\vdash \exists y \alpha \rightarrow \exists y \exists x \alpha} { }
schließen. Da auch $x$ hinten gebunden ist, ergibt sich
\mathdisp {\vdash \exists x \exists y \alpha \rightarrow \exists y \exists x \alpha} { . }
}
{}
\teilbeweis {}{}{}
{(2). Aufgrund der Alleinführung im Antezedens ist
\mathdisp {\vdash \forall x \alpha \rightarrow \alpha} { }
und
\mathdisp {\vdash \forall x (\alpha \rightarrow \beta) \rightarrow (\alpha \rightarrow \beta)} { . }
Dies konjugiert
\zusatzklammer {unter Verwendung von
Lemma 6.7 (2)} {} {}
ergibt
\mathdisp {\vdash \forall x \alpha \wedge \forall x (\alpha \rightarrow \beta) \rightarrow \alpha \wedge (\alpha \rightarrow \beta)} { . }
Ferner haben wir die aussagenlogische Tautologie
\mathdisp {\vdash \alpha \wedge (\alpha \rightarrow \beta) \rightarrow \beta} { . }
Damit ergibt sich aufgrund der Transitivität der Implikation die Ableitung
\mathdisp {\vdash \forall x \alpha \wedge \forall x (\alpha \rightarrow \beta) \rightarrow \beta} { . }
Da $x$ vorne und in
\mathl{\forall x \beta}{}
\definitionsverweis {gebunden}{}{}
vorkommt, gilt nach der Allein\-führung im Sukzedens auch
\mathdisp {\vdash \forall x \alpha \wedge \forall x (\alpha \rightarrow \beta) \rightarrow \forall x \beta} { . }
}
{}
\teilbeweis {}{}{}
{Zu (3) siehe
Aufgabe *****
und
Aufgabe *****.}
{}
\teilbeweis {}{}{}
{(4). Aufgrund der
\definitionsverweis {Alleinführung im Antezedens}{}{}
ist
\mathdisp {\vdash \forall x (\alpha \rightarrow \beta) \rightarrow (\alpha \rightarrow \beta)} { , }
was wir als
\mathdisp {\vdash \alpha\wedge \forall x (\alpha\rightarrow \beta) \rightarrow \beta} { }
schreiben. Wegen
\mathl{\vdash \beta \rightarrow \exists x \beta}{} ist auch
\mathdisp {\vdash \alpha \wedge \forall x (\alpha \rightarrow \beta) \rightarrow \exists x \beta} { , }
was wir als
\mathdisp {\vdash \alpha \rightarrow ( \forall x (\alpha \rightarrow \beta) \rightarrow \exists x \beta)} { }
schreiben. Im Sukzedens ist $x$ gebunden, daher folgt aus der
\definitionsverweis {Existenzeinführung im Antezedens}{}{}
\mathdisp {\vdash \exists x \alpha \rightarrow ( \forall x (\alpha \rightarrow \beta) \rightarrow \exists x \beta)} { , }
was aussagenlogisch äquivalent zur Behauptung ist.}
{}
\teilbeweis {}{}{}
{Zu (5) siehe
Aufgabe 7.3.}
{}
\zwischenueberschrift{Die Ableitungsbeziehung}
Analog zur Folgerungsbeziehung definieren wir die Ableitungsbeziehung aus einer Ausdrucksmenge.
\inputdefinition
{}
{
Es sei $S$ ein
\definitionsverweis {Symbolalphabet}{}{,}
$\Gamma$ eine Menge an
$S$-\definitionsverweis {Ausdrücken}{}{}
und $\alpha$ ein weiterer $S$-Ausdruck. Man sagt, dass $\alpha$ aus $\Gamma$ \definitionswort {ableitbar}{} ist, geschrieben
\mathdisp {\Gamma \vdash \alpha} { , }
wenn es endlich viele Ausdrücke
\mavergleichskette
{\vergleichskette
{ \alpha_1 , \ldots , \alpha_n
}
{ \in }{ \Gamma
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
derart gibt, dass
\mathdisp {\vdash \alpha_1 \wedge \ldots \wedge \alpha_n \rightarrow \alpha} { }
gilt.
}
Man kann sich also wieder fragen, welche Ausdrücke aus einer vorgegebenen Ausdrucksmenge $\Gamma$, beispielsweise einem Axiomensystem einer Sprache erster Stufe, ableitbar sind. Unser \anfuehrung{unbedingter}{} Prädikatenkalkül, der die syntaktischen Tautologien generiert, führt zu einem entsprechenden Regelsatz für die Ableitbarkeit aus $\Gamma$. Dies ist näher an der mathematischen Praxis, da man sich dort in einem bestimmten mathematischen Kontext bewegt \zusatzklammer {z.B. der Gruppentheorie} {} {} und daher unter der Voraussetzung arbeitet, dass eine gewisse Ausdrucksmenge \zusatzklammer {z.B. die Gruppenaxiome} {} {} vorliegt, aus der heraus man etwas beweisen möchte.
\zwischenueberschrift{Der Vollständigkeitssatz}
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. Daraus ergibt sich insbesondere, dass sich aus der Ableitbarkeitsbeziehung
\mathdisp {\Gamma \vdash p} { }
die Folgerungsbeziehung
\mathdisp {\Gamma \vDash p} { }
ergibt. Diese Aussage nennt man auch den \stichwort {Korrektheitssatz} {.} Der entworfene Kalkül produziert also nur korrekte mathematische Aussagen.
Die Umkehrung 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. Für diesen \stichwort {Vollständigkeitssatz} {,} der auf Gödel zurückgeht, geben wir nur eine kurze Beweisidee.
{Prädikatenlogik/Vollständigkeitssatz/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 gilt
\mathl{\Gamma \vDash \alpha}{} genau dann, wenn
\mathl{\Gamma \vdash \alpha}{} gilt.}
\faktzusatz {}
\faktzusatz {}
}
{ Die Implikation von rechts nach links, dass also ein aus $\Gamma$ ableitbarer Ausdruck auch aus $\Gamma$ folgt, beruht auf der Korrektheit des Prädikatenkalküls. Die umgekehrte Richtung wird durch Kontraposition bewiesen. Es sei also $p$ ein Ausdruck, der nicht aus
\mathl{\Gamma}{} ableitbar ist. Man muss dann zeigen, dass er auch nicht aus $\Gamma$ folgt. D.h. man muss zeigen, dass es eine Interpretation $I$
\zusatzklammer {also insbesondere eine $S$-\definitionsverweis {Struktur}{}{}} {} {}
gibt, unter der $\Gamma$ gilt, aber nicht $p$. Wegen der Unableitbarkeit kann man aus der Ausdrucksmenge
\mathl{\Gamma \cup \{ \neg p\}}{} keinen Widerspruch ableiten. Daher muss man zu einer (syntaktisch) widerspruchsfreien Ausdrucksmenge ein erfüllendes Modell konstruieren. Die Grundidee dazu ist, auf der Menge der $S$-Terme eine \definitionsverweis {Äquivalenzrelation}{}{}
unter Berücksichtigung der Ausdrucksmenge einzuführen und die resultierende \definitionsverweis {Quotientenmenge}{}{}
Das folgende Korollar, der sogenannte \stichwort {Endlichkeitssatz} {,} demonstriert, dass der Vollständigkeitssatz keineswegs selbstverständlich ist. Es sei eine Folgerungsbeziehung
\mathl{\Gamma \vDash p}{} bewiesen, also gezeigt, dass jede Interpretation, die $\Gamma$ erfüllt, auch $p$ erfüllen muss. Dabei sei $\Gamma$ unendlich, man denke etwa an ein unendliches Axiomenschema, wie es im Induktionsschema der erststufigen Peano-Arithmetik vorliegt. Ist es vorstellbar, dass in einem Beweis irgendwie auf all diese unendlich vielen Voraussetzungen Bezug genommen wird?
\inputfaktbeweis
{Prädikatenlogik/Endlichkeitssatz/Fakt}
{Korollar}
{}
{
\faktsituation {Es sei $S$ ein
\definitionsverweis {Symbolalphabet}{}{,}
$\Gamma$ eine Menge an
$S$-\definitionsverweis {Ausdrücken}{}{} und $\alpha$ ein weiterer $S$-Ausdruck.}
\faktfolgerung {Dann gilt
\mathl{\Gamma \vDash \alpha}{} genau dann, wenn es eine endliche Teilmenge
\mavergleichskette
{\vergleichskette
{ \Gamma_e
}
{ \subseteq }{ \Gamma
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
gibt mit
\mathl{\Gamma_e \vDash \alpha}{.}}
\faktzusatz {}
\faktzusatz {}
}
{
Dies folgt direkt aus Satz 7.8, da die Endlichkeitsbeziehung für das \definitionsverweis {Ableiten}{}{} nach Definition gilt.
| << | Kurs:Einführung in die mathematische Logik (Osnabrück 2011-2012) | >> |
|---|