Kurs:Einführung in die mathematische Logik (Osnabrück 2011-2012)/Vorlesung 6/latex
\setcounter{section}{6}
\zwischenueberschrift{Peano-Axiome}
\bild{ \begin{center}
\includegraphics[width=5.5cm]{\bildeinlesung {Giuseppe_Peano.jpg} }
\end{center}
\bildtext {Giuseppe Peano (1858 -1932)} }
\bildlizenz { Giuseppe Peano.jpg } {} {Kalki} {Commons} {PD?} {}
Wir besprechen nun, inwiefern man die natürlichen Zahlen $\N$ axiomatisieren kann, und was davon erststufig durchführbar ist. Dazu diskutieren wir die Peano-Axiome, wobei wir mit der zweitstufigen Version beginnen.
\inputaxiom
{}
{
Eine Menge $N$ mit einem ausgezeichneten Element
\mavergleichskette
{\vergleichskette
{0
}
{ \in }{N
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
\zusatzklammer {die \stichwort {Null} {}} {} {}
und einer
\zusatzklammer {Nachfolger} {} {-}Abbildung
\maabbeledisp {'} { N} {N
} {n} {n'
} {,}
heißt \definitionswort {natürliche Zahlen}{} \zusatzklammer {oder \stichwort {Dedekind-Peano-Modell} {} für die natürlichen Zahlen} {} {,}
wenn die folgenden
\definitionswortenp{Dedekind-Peano-Axiome}{} erfüllt sind.
\aufzaehlungdrei{Das Element $0$ ist kein Nachfolger
\zusatzklammer {die Null liegt also nicht im Bild der Nachfolgerabbildung} {} {.}
}{Jedes
\mavergleichskette
{\vergleichskette
{n
}
{ \in }{N
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
ist Nachfolger höchstens eines Elementes
\zusatzklammer {d.h. die Nachfolgerabbildung ist injektiv} {} {.}
}{Für jede Teilmenge
\mavergleichskette
{\vergleichskette
{T
}
{ \subseteq }{N
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
gilt: Wenn die beiden Eigenschaften
\auflistungzwei{
\mavergleichskette
{\vergleichskette
{0
}
{ \in }{T
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{,}
}{mit jedem Element
\mavergleichskette
{\vergleichskette
{n
}
{ \in }{T
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
ist auch
\mavergleichskette
{\vergleichskette
{n'
}
{ \in }{T
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{,}
}
gelten, so ist
\mavergleichskette
{\vergleichskette
{T
}
{ = }{N
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{.}
}
} Mit zweitstufig ist gemeint, dass nicht nur über die Elemente der Menge $\N$, die man axiomatisch charakterisieren will, quantifiziert wird, sondern auch über beliebige Teilmengen dieser Menge. Mit dieser Axiomatik lassen sich ausgehend von der Nachfolgerfunktion die Addition und die Multiplikation rekursiv einführen, und es lässt sich zeigen, dass je zwei Modelle für diese zweistufigen Peano-Axiome \anfuehrung{isomorph}{} sind, dass es also zwischen ihnen eine strukturerhaltende Bijektion gibt. Das im Wesentlichen eindeutig bestimmte Modell für diese Arithmetik bezeichnen wir mit $\N$.
Wir betrachten zwei erststufige Varianten. Dabei wird die Nachfolgerfunktion beibehalten und das Induktionsaxiom, das oben für beliebige Teilmengen formuliert war, wird durch ein Induktionsaxiom für die in der Sprache formulierbaren Ausdrücke ersetzt. Das Induktionsaxiom gilt somit lediglich für Teilmengen, die in der gegebenen Sprache charakterisierbar sind.
\inputaxiom
{}
{
Die \stichwort {Peano-Axiome für die Nachfolgerfunktion in der ersten Stufe} {} werden
\zusatzklammer {in der Sprache $L$ zur Symbolmenge mit einer Konstanten $0$ und einem einstelligen Funktionssymbol $N$} {} {}
folgendermaßen definiert.
\aufzaehlungdrei{
\mathl{\forall x ( \neg ( Nx = 0))}{.}
}{
\mathl{\forall x \forall y ( ( Nx = Ny) \rightarrow (x=y) )}{.}
}{Für jeden Ausdruck $\alpha$ von $L$ mit einer freien Variablen $x$ gilt
\mathdisp {\alpha \frac{0}{x} \wedge \forall x { \left( \alpha \rightarrow \alpha \frac{N x}{x} \right) } \rightarrow \forall x \alpha} { . }
}
}
Aus der obigen zweitstufigen Formulierung der Axiomatik, die nur die Nachfolgerabbildung verwendet, kann man in jedem Modell in eindeutiger Weise eine Addition und eine Multiplikation definieren. Dafür ist das obige erststufige Axiomensystem zu schwach. Stattdessen werden wir unter der Peano-Arithmetik das folgende Axiomensystem verstehen, das mit zwei Konstanten
\mathkor {} {0} {und} {1} {}
und zwei zweistelligen Operationen
\mathkor {} {+} {und} {\cdot} {}
auskommt. Die Nachfolgerfunktion ist dann durch
\mathl{Nx=x+1}{} definiert und es braucht dafür kein eigenes Funktionssymbol.
\inputaxiom
{}
{
Die \stichwort {Peano-Axiome für Addition und Multiplikation in der ersten Stufe} {} werden
\zusatzklammer {in der Sprache $L^{\rm Ar}$ zur Symbolmenge mit den beiden Konstanten $0$ und $1$ und zwei zweistelligen Funktionssymbolen
\mathkor {} {+} {und} {\cdot} {}} {} {}
folgendermaßen definiert.
\aufzaehlungsieben{
\mathl{\forall x ( \neg ( x+ 1 = 0))}{.}
}{
\mathl{\forall x \forall y ( ( x+1 = y+1) \rightarrow (x=y) )}{.}
}{
\mathl{\forall x ( x+ 0 = x)}{.}
}{
\mathl{\forall x \forall y ( x+ (y+1) = ( x +y)+1))}{.}
}{
\mathl{\forall x ( x \cdot 0 = 0)}{.}
}{
\mathl{\forall x \forall y ( x \cdot (y+1) = (x \cdot y) +x)}{.}
}{Für jeden Ausdruck $\alpha$ von $L^{Ar}$ mit einer freien Variablen $x$ gilt
\mathdisp {\alpha \frac{0}{x} \wedge \forall x { \left( \alpha \rightarrow \alpha \frac{x+1}{x} \right) } \rightarrow \forall x \alpha} { . }
}
}
Die Axiome \mathkor {} {(1), (2)} {und} {(7)} {} entsprechen dabei direkt den Nachfolgeraxiomen von oben. Die Axiome \mathkor {} {(3)} {und} {(4)} {} spiegeln die Grundregeln in der zweistufigen Peano-Arithmetik für die rekursive Definition der Addition wider, und die Axiome \mathkor {} {(5)} {und} {(6)} {} entsprechen den Grundregeln für die rekursive Definition der Multiplikation. Bekanntlich gelten diese Axiome für die natürlichen Zahlen. Anders als bei der obigen zweitstufigen Axiomatik gibt es aber von $\N$ verschiedene Modelle (nicht Standard-Arithmetiken), die die erststufige Peano-Arithmetik erfüllen. Dies ist aber kein \anfuehrung{zufälliges}{} Defizit der gewählten Axiomatik, sondern dahinter verbirgt sich eine grundsätzliche Schwäche der Sprache erster Stufe, die durch die Gödelschen Unvollständigkeitssätze präzisiert werden wird.
\zwischenueberschrift{Kalkül der Prädikatenlogik}
Gegeben sei ein Symbolalphabet einer Sprache erster Stufe und damit die zugehörige Termmenge und die zugehörige Ausdrucksmenge. Wir möchten die logisch wahren Aussagen einer solchen Sprache syntaktisch charakterisieren. Mathematische Aussagen sind im Allgemeinen \anfuehrung{wenn-dann}{-}Aussagen, d.h. sie behaupten, dass, wenn gewisse Voraussetzungen erfüllt sind, dann auch eine gewisse Folgerung erfüllt ist.
Wenn man einen Beweis eines Satzes der Gruppentheorie oder der elementaren Arithmetik entwirft, so sind dabei die Axiome der Gruppentheorie bzw. die Peano-Axiome stets präsent. Wenn
\mathl{p_1, p_2, p_3}{} die Gruppenaxiome bezeichnen und $p$ die Aussage, dass das neutrale Element eindeutig bestimmt ist, bezeichnet, so folgt $p$ aus
\mathl{p_1, p_2, p_3}{.} Mit der Folgerungsbeziehung kann man dies als
\mathdisp {\{p_1, p_2, p_3 \} \vDash p} { }
formulieren. Dies kann man auch so ausdrücken, dass
\mathdisp {p_1 \wedge p_2\wedge p_3 \rightarrow p} { }
\definitionsverweis {allgemeingültig}{}{}
ist, also dass
\mathdisp {\vDash p_1 \wedge p_2\wedge p_3 \rightarrow p} { }
gilt. So kann man jede Folgerung
\mathl{\Gamma \vDash p}{} aus einer endlichen Ausdrucksmenge $\Gamma$ \anfuehrung{internalisieren}{,} also durch einen allgemeingültigen Ausdruck der Form
\mathdisp {\vDash p_1 \wedge \ldots \wedge p_n \rightarrow p} { }
wiedergegeben, wobei vorne die Ausdrücke aus $\Gamma$ konjugiert werden. Die Folgerungsbeziehung (zumindest aus endlichen Ausdrucksmengen) kann also vollständig durch allgemeingültige Ausdrücke verstanden werden.
Wir besprechen nun die syntaktische Variante der allgemeingültigen Ausdrücke, nämlich die syntaktischen prädikatenlogischen Tautologien. Über den soeben besprochenen Zusammenhang ergibt sich daraus auch ein Ableitungskalkül, der das syntaktische Analogon zur Folgerungsbeziehung ist. Da wir Ausdrücke der Form
\mathl{p_1 \wedge \ldots \wedge p_n \rightarrow p}{} als Grundtyp für eine mathematische Aussage ansehen, arbeiten wir allein mit den Junktoren $\neg, \wedge, \rightarrow$ und lesen
\mathkor {} {\vee} {und} {\leftrightarrow} {}
als Abkürzungen. Man könnte auch noch
\mathkor {} {\wedge} {bzw.} {\rightarrow} {}
eliminieren und durch die verbleibenden beiden Junktoren ausdrücken, doch würde dies zu recht unleserlichen Formulierungen führen.
Der prädikatenlogische Kalkül, den wir vorstellen wollen, soll es erlauben, \anfuehrung{alle}{} prädikatenlogischen allgemeingültigen Ausdrücke formal abzuleiten. Der Aufbau dieses Kalküls geschieht wiederum rekursiv (und für beliebige Symbolalphabete gleichzeitig). D.h. man hat eine Reihe von Anfangstautologien (oder Grundtautologien) und gewisse Schlussregeln, um aus schon nachgewiesenen Tautologien neue zu produzieren. Sowohl die Anfangstautologien als auch die Schlussregeln sind aus der mathematischen Beweispraxis vertraut.
Zur Formulierung dieses Kalküls verwenden wir die Schreibweise
\mathdisp {\vdash p} { . }
Sie bedeutet, dass der Ausdruck $p$ in der Prädikatenlogik
\zusatzklammer {erster Stufe zu einem gegebenen Alphabet} {} {}
ableitbar ist, also eine Tautologie
\zusatzklammer {im syntaktischen Sinne} {} {}
ist.
\zwischenueberschrift{Aussagenlogische Tautologien}
In den folgenden aussagenlogischen Tautologien sind \mathkor {} {p} {und} {q} {} beliebige Ausdrücke. Um Klammern zu sparen verwenden wir die Konvention, dass die Negation sich auf das folgende Zeichen bezieht und dass die Konjunktion stärker bindet als die Implikation.
\inputaxiom
{}
{
Für eine Aussagenvariablenmenge $V$ und beliebige Ausdrücke
\mathl{\alpha, \beta, \gamma}{} legt man folgende
\zusatzklammer {syntaktische} {} {}
\definitionswortenp{Tautologien}{} axiomatisch fest.
\aufzaehlungsechs{
\mathdisp {\vdash \alpha \rightarrow (\beta \rightarrow \alpha)} { . }
}{
\mathdisp {\vdash (\alpha \rightarrow \beta) \wedge (\beta \rightarrow \gamma) \rightarrow (\alpha \rightarrow \gamma)} { . }
}{
\mathdisp {\vdash (\alpha \rightarrow \beta) \wedge ( \alpha \rightarrow \gamma) \rightarrow (\alpha \rightarrow \beta \wedge \gamma)} { . }
}{
\mathdisp {\vdash (\alpha \wedge \beta \rightarrow \gamma) \rightarrow (\alpha \rightarrow ( \beta \rightarrow \gamma))} { }
und
\mathdisp {\vdash (\alpha \rightarrow ( \beta \rightarrow \gamma)) \rightarrow (\alpha \wedge \beta \rightarrow \gamma)} { . }
}{
\mathdisp {\vdash \neg \alpha \wedge \alpha \rightarrow \beta} { . }
}{
\mathdisp {\vdash (\alpha \rightarrow \beta) \wedge (\neg \alpha \rightarrow \beta) \rightarrow \beta} { . }
}
}
Diese Tautologien sind also die Startglieder. Dabei stehen
\mathl{p,q,r}{} für beliebige Ausdrücke der Prädikatenlogik erster Stufe (in der Aussagenlogik werden diese Tautologien einfach mit Aussagenvariablen formuliert). Das Axiom (3) besagt die Transitivität der Implikation, Axiom (5) heißt Widerspruchsaxiom und Axiom (6) heißt Fallunterscheidungsaxiom.
Um überhaupt aus diesen Axiomen weitere Tautologien generieren zu können, braucht man Ableitungsregeln. Davon gibt es lediglich eine.
\stichwort {Modus ponens} {}
Aus
\mathkor {} {\vdash p} {und} {\vdash p \rightarrow q} {}
folgt
\mathl{\vdash q}{.}
Wir wollen uns nicht lange an aussagenlogischen Tautologien aufhalten. Eine Durchsicht der angeführten Tautologien zeigt, dass es sich auch um semantische Tautologien, also allgemeingültige Ausdrücke, handelt.
\inputbemerkung
{}
{
Die aussagenlogischen Axiome der Form
\mathl{\vdash \alpha \rightarrow \beta}{} führen zu entsprechenden Schlussregeln, d.h. Vorschriften, wie man aus
\zusatzklammer {schon etablierten} {} {}
syntaktischen Tautologien neue Tautologien erhält. Wir gehen unter diesem Gesichtspunkt die Axiome durch.
Aus
\mathl{\vdash \alpha}{} folgt
\mathl{\vdash \beta \rightarrow \alpha}{.}
Dies ergibt sich aus der Voraussetzung
\mathl{\vdash \alpha}{} aus
\mathl{\vdash \alpha \rightarrow ( \beta \rightarrow \alpha )}{} und dem Modus ponens.
Aus
\mathl{\vdash \alpha \wedge \beta}{} folgt
\mathl{\vdash \alpha}{}
\zusatzklammer {und ebenso \mathlk{\vdash \beta}{}} {} {.}
Dies ergibt sich aus
\mathl{\vdash \alpha \wedge \beta \rightarrow \alpha}{}
nach Fakt *****
und der Voraussetzung
\mathl{\vdash \alpha \wedge \beta}{} mittels Modus ponens. Umgekehrt gilt die sogenannte \stichwort {Konjunktionsregel} {,} d.h. aus
\mathkor {} {\vdash \alpha} {und} {\vdash \beta} {}
folgt auch
\mathl{\vdash \alpha \wedge \beta}{.} Dies ergibt sich aus
\mathdisp {\vdash \alpha \rightarrow ( \beta \rightarrow \alpha \wedge \beta )} { }
\zusatzklammer {was aus den Axiomen folgt, siehe
Aufgabe 6.5} {} {}
aus den Voraussetzungen durch eine zweifache Anwendung des Modus ponens.
Aus
\mathkor {} {\vdash \alpha \rightarrow \beta} {und} {\vdash \beta \rightarrow \gamma} {}
ergibt sich
\mathl{\vdash \alpha \rightarrow \gamma}{.} Diese Regel heißt \stichwort {Kettenschlussregel} {.} Nach der obigen abgeleiteten Konjunktionsregel folgt aus den Voraussetzungen direkt
\mathl{\vdash ( \alpha \rightarrow \beta ) \wedge (\beta \rightarrow \gamma )}{} und daraus und dem Kettenschlussaxiom mit dem Modus ponens
\mathl{\vdash \alpha \rightarrow \gamma}{.}
}
\inputfaktbeweis
{Aussagenlogik/Syntaktische Tautologien/Implikation, Negation, Konjunktion/Axiomatik/Kommutativität der Konjunktion/Fakt}
{Lemma}
{}
{
\faktsituation {}
\faktfolgerung {Es ist
\mathdisp {\vdash \alpha \wedge \beta \rightarrow \beta \wedge \alpha} { . }
}
\faktzusatz {}
\faktzusatz {}
}
{
Nach
Axiom 6.4 (3)
ist
\mathdisp {\vdash (( \alpha \wedge \beta ) \rightarrow \beta) \wedge ((\alpha\wedge \beta ) \rightarrow \alpha) \rightarrow ( \alpha \wedge \beta\rightarrow \beta \wedge \alpha )} { . }
Die beiden Bestandteile des Vordersatzes gelten nach
Fakt *****,
sodass auch ihre Konjunktion ableitbar ist. Daher ist auch der Nachsatz ableitbar.
\inputfaktbeweis
{Aussagenlogik/Syntaktische Tautologien/Implikation, Negation, Konjunktion/Axiomatik/Konjugierte Implikation/Fakt}
{Lemma}
{}
{
\faktsituation {}
\faktfolgerung {\aufzaehlungzwei {
\mathdisp {\vdash ( \alpha \rightarrow \beta) \rightarrow (\alpha \wedge \gamma\rightarrow \beta)} { . }
} {
\mathdisp {\vdash (\alpha \rightarrow \beta) \wedge (\gamma \rightarrow \delta) \rightarrow (\alpha \wedge \gamma\rightarrow \beta \wedge \delta)} { . }
}}
\faktzusatz {}
\faktzusatz {}
}
{
\aufzaehlungzwei {\teilbeweis {}{}{}
{Nach
Axiom 6.4 (2)
ist
\mathdisp {\vdash { \left( \alpha \wedge \gamma \rightarrow \alpha \right) } \wedge { \left( \alpha \rightarrow \beta \right) } \rightarrow { \left( \alpha \wedge \gamma \rightarrow \beta \right) }} { }
und daher mit
Axiom 6.4 (4)
auch
\mathdisp {\vdash ( \alpha \wedge \gamma \rightarrow \alpha ) \rightarrow ((\alpha \rightarrow \beta) \rightarrow ( \alpha \wedge \gamma \rightarrow \beta))} { . }
Der Vordersatz ist nach
Fakt *****
ableitbar, also auch der Nachsatz.}
{}
} {\teilbeweis {}{}{}
{Nach Teil (1) ist
\mathdisp {\vdash (\alpha \rightarrow \beta) \rightarrow (\alpha \wedge \gamma \rightarrow \beta)} { }
und
\zusatzklammer {unter Verwendung von
Fakt *****
und
Aufgabe *****} {} {}
\mathdisp {\vdash (\gamma \rightarrow \delta) \rightarrow (\alpha \wedge \gamma \rightarrow \delta)} { . }
Daher gilt auch
\zusatzklammer {nach der Regelversion zu Teil (1)} {} {}
\mathdisp {\vdash (\alpha \rightarrow \beta) \wedge (\gamma \rightarrow \delta) \rightarrow (\alpha \wedge \gamma \rightarrow \beta)} { }
und
\mathdisp {\vdash (\alpha \rightarrow \beta) \wedge (\gamma \rightarrow \delta) \rightarrow (\alpha \wedge \gamma \rightarrow \delta)} { }
bzw. unter Verwendung von
Axiom 6.4 (4)
und der
Assoziativität der Konjunktion
\mathdisp {\vdash (\alpha \rightarrow \beta) \wedge (\gamma \rightarrow \delta) \wedge \alpha \wedge \gamma \rightarrow \beta} { }
und
\mathdisp {\vdash (\alpha \rightarrow \beta) \wedge (\gamma \rightarrow \delta) \wedge \alpha \wedge \gamma \rightarrow \delta} { . }
Nach
Axiom 6.4 (3)
ist mit der Abkürzung
\mathl{\varphi =(\alpha \rightarrow \beta) \wedge (\gamma \rightarrow \delta) \wedge \alpha \wedge \gamma}{}
\mathdisp {\vdash (\varphi \rightarrow \beta ) \wedge (\varphi \rightarrow \delta) \rightarrow (\varphi \rightarrow \beta \wedge \delta)} { . }
Da die beiden Teilaussagen im Vordersatz ableitbar sind, ist auch der Nachsatz ableitbar, was unter Verwendung von
Axiom 6.4 (4)
zur Behauptung umformulierbar ist.}
{}
}
Die folgende Aussage gibt eine \anfuehrung{interne Version}{} des Modus Ponens, der ja nach Definition eine Schlussregel ist.
\inputfaktbeweis
{Aussagenlogik/Syntaktische Tautologien/Implikation, Negation, Konjunktion/Axiomatik/Modus ponens intern/Fakt}
{Lemma}
{}
{
\faktsituation {}
\faktfolgerung {Es ist
\mathdisp {\vdash \alpha \wedge (\alpha \rightarrow \beta) \rightarrow \beta} { . }
}
\faktzusatz {}
\faktzusatz {}
}
{
Nach
Axiom 6.4 (6)
ist
\mathdisp {\vdash (\alpha \rightarrow \beta) \wedge (\neg \alpha \rightarrow \beta) \rightarrow \beta} { , }
und
Axiom 6.4 (5)
kann man wegen
Axiom 6.4 (4)
zu
\mathdisp {\vdash \alpha \rightarrow ( \neg \alpha \rightarrow \beta)} { }
umformulieren. Daraus und aus
\zusatzklammer {Fakt *****} {} {}
\mathdisp {\vdash { \left( \alpha \rightarrow \beta \right) } \rightarrow { \left( \alpha \rightarrow \beta \right) }} { }
ergibt sich mit der Regelversion zu
Lemma 6.7 (2)
\mathdisp {\vdash \alpha \wedge { \left( \alpha \rightarrow \beta \right) } \rightarrow { \left( \neg \alpha \rightarrow \beta \right) } \wedge { \left( \alpha \rightarrow \beta \right) }} { }
und daraus durch den Kettenschluss die Behauptung.
\inputfaktbeweis
{Aussagenlogik/Syntaktische Tautologien/Implikation, Negation, Konjunktion/Axiomatik/Weitere Schlussregeln/Fakt}
{Lemma}
{}
{
\faktsituation {}
\faktvoraussetzung {\aufzaehlungzwei {Aus
\mathl{\vdash \alpha \rightarrow ( \beta \rightarrow \gamma)}{} und
\mathl{\vdash \gamma \rightarrow \delta}{} folgt
\mathl{\vdash \alpha \rightarrow (\beta \rightarrow \delta)}{.}
} {Aus
\mathl{\vdash \alpha}{} und
\mathl{\vdash \alpha \wedge \beta \rightarrow \gamma}{} ergibt sich
\mathl{\vdash \beta \rightarrow \gamma}{.}
}}
\faktfolgerung {}
\faktzusatz {}
\faktzusatz {}
}
{
\aufzaehlungzwei {\teilbeweis {}{}{}
{Sei
\mathdisp {\vdash \alpha \rightarrow (\beta \rightarrow \gamma)} { }
und
\mathdisp {\vdash \gamma \rightarrow \delta} { . }
Nach
Bemerkung *****
gilt auch
\mathdisp {\vdash \alpha \rightarrow ( \gamma \rightarrow \delta )} { }
und daraus ergibt sich mit
Axiom 6.4 (3),
der Konjunktionsregel und dem Modus ponens
\mathdisp {\vdash \alpha \rightarrow (\beta \rightarrow \gamma ) \wedge (\gamma \rightarrow \delta)} { . }
Mittels des Kettenschlusses ergibt sich daraus und aus Axiom 6.4 (2)
die Behauptung.}
{}
} {\teilbeweis {}{}{}
{Siehe
Aufgabe 6.8.}
{}
}
Die folgenden Tautologien machen wichtige Aussagen über das Negationszeichen. Die Tautologie (2) ist eine wichtige Variante der \stichwort {Widerspruchstautologie} {} und die Tautologie (5) heißt \stichwort {Kontraposition} {.}
\inputfaktbeweis
{Aussagenlogik/Syntaktische Tautologien/Implikation, Negation, Konjunktion/Axiomatik/Weitere Tautologien/Mit Negation/Fakt}
{Lemma}
{}
{
\faktsituation {}
\faktfolgerung {\aufzaehlungsechs{
\mathdisp {\vdash ( \neg \alpha \rightarrow \alpha) \rightarrow \alpha} { . }
}{
\mathdisp {\vdash ( \neg \beta \rightarrow \neg \alpha) \wedge (\neg \beta \rightarrow \alpha) \rightarrow \beta} { }
}{
\mathdisp {\vdash \alpha \rightarrow \neg \neg \alpha} { . }
}{
\mathdisp {\vdash \neg \neg \alpha \rightarrow \alpha} { . }
}{
\mathdisp {\vdash ( \alpha \rightarrow \beta ) \rightarrow ( \neg \beta \rightarrow \neg \alpha)} { . }
}{
\mathdisp {\vdash ( \neg \beta \rightarrow \neg \alpha) \rightarrow ( \alpha \rightarrow \beta )} { . }
}}
\faktzusatz {}
\faktzusatz {}
}
{
\aufzaehlungsechs{\teilbeweis {}{}{}
{Die Fallunterscheidungstautologie liefert
\mathdisp {\vdash ( \alpha \rightarrow \alpha) \wedge ( \neg \alpha \rightarrow \alpha) \rightarrow \alpha} { . }
Aus
\zusatzklammer {Fakt *****} {} {}
\mathdisp {\vdash \alpha \rightarrow \alpha} { }
ergibt sich daraus die Behauptung.}
{}
}{\teilbeweis {}{}{}
{Nach
Axiom 6.4 (3)
gilt
\mathdisp {\vdash ( \neg \beta \rightarrow \neg \alpha) \wedge (\neg \beta \rightarrow \alpha) \rightarrow (\neg \beta \rightarrow \neg \alpha \wedge \alpha)} { }
und nach
Axiom 6.4 (5)
gilt
\mathdisp {\vdash \neg \alpha\wedge \alpha \rightarrow \beta} { . }
Nach
Lemma 6.8 (1)
folgt
\mathdisp {\vdash ( \neg \beta \rightarrow \neg \alpha) \wedge (\neg \beta \rightarrow \alpha) \rightarrow (\neg \beta \rightarrow \beta )} { , }
woraus nach Teil (1) die Behauptung mit der Kettenschlussregel folgt.}
{}
}{\teilbeweis {}{}{}
{Nach
Axiom 6.4 (1)
ist
\mathdisp {\vdash \neg \neg \alpha \rightarrow ( \alpha \rightarrow \neg \neg \alpha)} { . }
Nach
Axiom 6.4 (5)
ist
\mathdisp {\vdash \neg \alpha \wedge \alpha \rightarrow \neg \neg \alpha} { , }
was wir mit
Axiom 6.4 (4)
zu
\mathdisp {\vdash \neg \alpha \rightarrow ( \alpha \rightarrow \neg \neg \alpha)} { , }
umformulieren können. Daraus ergibt sich
\mathdisp {\vdash \alpha \rightarrow \neg \neg \alpha} { }
mit der Fallunterscheidungsregel.}
{}
}{\teilbeweis {}{}{}
{Nach
Axiom 6.4 (1)
ist
\mathdisp {\vdash \alpha \rightarrow ( \neg \neg \alpha \rightarrow \alpha)} { . }
Nach
Axiom 6.4 (5)
ist
\mathdisp {\vdash \neg \alpha \wedge \neg \neg \alpha \rightarrow \alpha} { , }
was wir zu
\mathdisp {\vdash \neg \alpha \rightarrow (\neg \neg \alpha \rightarrow \alpha)} { , }
umformulieren können. Daraus ergibt sich
\mathdisp {\vdash \neg \neg \alpha \rightarrow \alpha} { }
mit der Fallunterscheidungsregel.}
{}
}{\teilbeweis {}{}{}
{Es ist nach
Axiom 6.4 (1)
\mathdisp {\vdash \neg \alpha \rightarrow (\neg \beta \rightarrow \neg \alpha)} { }
und damit auch
\mathdisp {\vdash \neg \alpha \rightarrow ((\alpha \rightarrow \beta ) \rightarrow (\neg \beta \rightarrow \neg \alpha))} { . }
Ferner ist nach einer Variante von
Axiom 6.4 (5)
\mathdisp {\vdash \beta \rightarrow (\neg \beta \rightarrow \neg \alpha)} { . }
Nach
Lemma 6.7
ist
\mathdisp {\vdash \alpha \rightarrow ((\alpha \rightarrow \beta ) \rightarrow \beta )} { , }
woraus sich
\mathdisp {\vdash \alpha \rightarrow ((\alpha \rightarrow \beta ) \rightarrow (\neg \beta \rightarrow \neg \alpha))} { }
ergibt. Mit der Fallunterscheidungsregel folgt die Behauptung.}
{}
}{\teilbeweis {}{}{}
{Dies folgt aus (3), (4) und (5).}
{}
}
\zwischenueberschrift{Gleichheitstautologien}
Es gelten die beiden folgenden Tautologien für die Gleichheit.
\inputaxiom
{}
{
Es sei $S$ ein
\definitionsverweis {Symbolalphabet}{}{,}
\mathl{s,t}{} seien
$S$-\definitionsverweis {Terme}{}{}
und $\alpha$ sei ein
$S$-\definitionsverweis {Ausdruck}{}{.}
Dann sind die beiden folgenden Ausdrücke syntaktische Tautologien.
\aufzaehlungzwei {
\mathdisp {\vdash t=t} { . }
} {
\mathdisp {\vdash s=t \wedge \alpha\frac{s}{x} \rightarrow \alpha\frac{t}{x}} { . }
}
}
Diese beiden Axiome heißen \stichwort {Gleichheitsaxiom} {} und \stichwort {Substitutionsaxiom} {.}
In der folgenden Aussage wird ein wichtiger Begriff für eine syntaktische Tautologie, eine Ableitungsregel oder einen ganzen formalen Kalkül verwendet, den der \stichwort {Korrektheit} {.} Er besagt, dass die Tautologie auch (im semantischen Sinn) allgemeingültig ist bzw. dass der Kalkül nur wahre Aussagen liefert. Die weiter oben axiomatisch formulierten aussagenlogischen Tautologien sind korrekt, d.h. sie \zusatzklammer {und auch jede weitere daraus mittels Modus Ponens ableitbare Tautologie} {} {} sind allgemeingültig, wie eine direkte Durchsicht zeigt. Die folgende Aussage zeigt, dass auch die eben postulierten Gleichheitsaxiome allgemeingültig sind und dass der Kalkül daher korrekt ist.
\inputfaktbeweis
{Prädikatenlogik/Gleichheitstautologien/Axiom/Korrektheit/Fakt}
{Lemma}
{}
{
\faktsituation {Die
\definitionsverweis {Gleichheitsaxiome}{}{}}
\faktfolgerung {sind
\definitionsverweis {korrekt}{}{.}}
\faktzusatz {}
\faktzusatz {}
}
{
Es sei $I$ eine beliebige
$S$-\definitionsverweis {Interpretation}{}{.}
\teilbeweis {}{}{}
{(1). Aufgrund der Bedeutung des Gleichheitszeichens unter jeder Interpretation gilt
\mavergleichskette
{\vergleichskette
{ I(t)
}
{ = }{ I(t)
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{,}
also
\mathdisp {I \vDash t = t} { . }
}
{}
\teilbeweis {}{}{}
{(2). Es gelte
\mathdisp {I \vDash s=t \wedge\alpha \frac{s}{x}} { , }
also
\mathkor {} {I \vDash s=t} {und} {I \vDash \alpha \frac{s}{x}} {.}
Das bedeutet einerseits
\mavergleichskette
{\vergleichskette
{ I(s)
}
{ = }{I(t)
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{.}
Andererseits gilt nach
dem Substitutionslemma
\mathdisp {I \frac{I(s)}{x} \vDash \alpha} { . }
Wegen der Termgleichheit gilt somit auch
\mathdisp {I \frac{I(t)}{x} \vDash \alpha} { }
und daher, wiederum aufgrund
des Substitutionslemmas,
auch
\mathdisp {I \vDash \alpha \frac{t}{x}} { . }
}
{}
\inputfaktbeweis
{Prädikatenlogik/Gleichheitstautologien/Folgerungen/Fakt}
{Korollar}
{}
{
\faktsituation {Aus den
\definitionsverweis {Gleichheitsaxiomen}{}{}}
\faktuebergang {lassen sich folgende Gleichheitstautologien ableiten
\zusatzklammer {dabei sind
\mathl{r,s,t,s_1 , \ldots , s_n, t_1 , \ldots , t_n}{}
\definitionsverweis {Terme}{}{,} $f$ ein $n$-stelliges Funktionssymbol und $R$ ein $n$-stelliges Relationssymbol} {} {.}}
\faktfolgerung {\aufzaehlungvier{
\mathdisp {\vdash s=t \rightarrow t=s} { . }
}{
\mathdisp {\vdash r=s \wedge s=t \rightarrow r=t} { . }
}{
\mathdisp {\vdash s_1=t_1 \wedge \ldots \wedge s_n=t_n \rightarrow fs_1 \ldots s_n =ft_1 \ldots t_n} { . }
}{
\mathdisp {\vdash s_1=t_1 \wedge \ldots \wedge s_n=t_n \wedge Rs_1 \ldots s_n \rightarrow Rt_1 \ldots t_n} { . }
}}
\faktzusatz {}
\faktzusatz {}
}
{
\teilbeweis {}{}{}
{(1). Aufgrund der
\definitionsverweis {Gleichheitsaxiome}{}{}
haben wir
\mathdisp {\vdash s=s} { }
und
\mathdisp {\vdash s=t \wedge (x=s) \frac{s}{x} \rightarrow (x=s) \frac{t}{x}} { , }
wobei $x$ eine Variable sei, die weder in
\mathkor {} {s} {noch in} {t} {}
vorkomme. Daher sind die beiden substituierten Ausdrücke gleich
\mathkor {} {s=s} {bzw.} {t=s} {.}
Eine aussagenlogische Umstellung der zweiten Zeile ist
\mathdisp {\vdash s=s \rightarrow (s=t \rightarrow t=s)} { , }
sodass sich aus der ersten Zeile mittels Modus ponens
\mathdisp {\vdash s=t \rightarrow t=s} { }
ergibt.}
{}
\teilbeweis {}{}{}
{(2). Es sei wieder $x$ eine Variable, die weder in $r$ noch in $s$ noch in $t$ vorkomme. Eine Anwendung des
\definitionsverweis {Substitutionsaxioms}{}{}
liefert
\mathdisp {\vdash s=t \wedge (r=x) \frac{s}{x} \rightarrow (r=x) \frac{t}{x}} { . }
Nach Einsetzen und einer aussagenlogischen Umstellung ist dies die Behauptung.}
{}
\teilbeweis {}{}{}
{Für (3) siehe
Aufgabe *****.}
{}
\teilbeweis {}{}{}
{(4). Es sei $u$ eine Variable, die weder in einem der $s_i$ noch in einem der $t_i$ vorkommt. Für jedes
\mavergleichskette
{\vergleichskette
{i
}
{ = }{1 , \ldots , n
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
gilt nach
Axiom ***** (2)
\zusatzklammer {mit
\mavergleichskettek
{\vergleichskettek
{ \alpha
}
{ = }{ \alpha_i
}
{ = }{ Rt_1 \ldots t_{i-1}us_{i+1} \ldots s_n
}
{ }{
}
{ }{
}
}
{}{}{}} {} {}
dann
\mathdisp {\vdash s_i =t_i \rightarrow { \left( Rt_1 \ldots t_{i-1} u s_{i+1} \ldots s_n { \frac{ s_i }{ u } } \rightarrow Rt_1 \ldots t_{i-1} u s_{i+1} \ldots s_n { \frac{ t_i }{ u } } \right) }} { , }
also
\mathdisp {\vdash s_i =t_i \rightarrow { \left( Rt_1 \ldots t_{i-1} s_i s_{i+1} \ldots s_n \rightarrow Rt_1 \ldots t_{i-1} t_i s_{i+1} \ldots s_n \right) }} { . }
Diese Ableitbarkeiten gelten auch, wenn man die Vordersätze durch ihre Konjunktion
\mathdisp {(s_1=t_1) \wedge \ldots \wedge (s_n=t_n)} { }
ersetzt. Durch die Transitivität der Implikation ergibt sich daher
\mathdisp {\vdash (s_1=t_1) \wedge \ldots \wedge (s_n=t_n) \rightarrow { \left( Rs_1 \ldots s_n \rightarrow Rt_1 \ldots t_n \right) }} { . }
}
{}
| << | Kurs:Einführung in die mathematische Logik (Osnabrück 2011-2012) | >> |
|---|