Kurs:Einführung in die mathematische Logik (Osnabrück 2014)/Vorlesung 10/latex
\setcounter{section}{10}
\zwischenueberschrift{Ableitungskalkül der Prädikatenlogik}
Gegeben sei ein Symbolalphabet $S$ einer Sprache erster Stufe und damit die zugehörige Termmenge und die zugehörige Ausdrucksmenge $L^ S$. 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{\alpha_1, \alpha_2, \alpha_3}{} die Gruppenaxiome bezeichnen und $\alpha$ die Aussage, dass das inverse Element eindeutig bestimmt ist, bezeichnet, so folgt $\alpha$ aus
\mathl{\alpha_1, \alpha_2, \alpha_3}{.} Mit der Folgerungsbeziehung kann man dies als
\mathdisp {\{\alpha_1, \alpha_2, \alpha_3 \} \vDash \alpha} { }
formulieren. Dies kann man auch so ausdrücken, dass
\mathdisp {\alpha_1 \wedge \alpha_2\wedge \alpha_3 \rightarrow \alpha} { }
\definitionsverweis {allgemeingültig}{}{}
ist, also dass
\mathdisp {\vDash \alpha_1 \wedge \alpha_2\wedge \alpha_3 \rightarrow \alpha} { }
gilt. So kann man jede Folgerung
\mathl{\Gamma \vDash \alpha}{} aus einer endlichen Ausdrucksmenge $\Gamma$ \anfuehrung{internalisieren}{,} also durch einen allgemeingültigen Ausdruck der Form
\mathdisp {\vDash \alpha_1 \wedge \ldots \wedge \alpha_n \rightarrow \alpha} { }
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{\alpha_1 \wedge \ldots \wedge \alpha_n \rightarrow \alpha}{} 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 \alpha} { . }
Sie bedeutet, dass der Ausdruck $\alpha$ in der Prädikatenlogik
\zusatzklammer {erster Stufe zu einem gegebenen Alphabet} {} {}
ableitbar ist, also eine Tautologie
\zusatzklammer {im syntaktischen Sinne} {} {}
ist. Wir beschreiben nun rekursiv die syntaktischen Tautologien in der Prädikatenlogik, die sich in aussagenlogische Tautologien, Gleichheitstautologien und Quantorentautologien und zwei Ableitungsregeln untergliedern. Wir beginnen mit den schon bekannten, allerdings in einer anderen Sprache formulierten aussagelogischen Tautologien.
\inputaxiom
{}
{
Zu einem beliebigen
\definitionsverweis {Symbolalphabet}{}{}
$S$ und beliebige Ausdrücke
\mavergleichskette
{\vergleichskette
{ \alpha, \beta, \gamma
}
{ \in }{ L^S
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
legt man folgende
\zusatzklammer {syntaktische} {} {}
\stichwort {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 \alpha \wedge \neg \alpha \rightarrow \beta} { . }
}{
\mathdisp {\vdash (\alpha \rightarrow \beta) \wedge (\neg \alpha \rightarrow \beta) \rightarrow \beta} { . }
}
}
Als Schlussregel erlaubt man wieder den Modus Ponens, so dass die Prädikatenlogik in einem gewissen Sinne die Aussagenlogik umfasst. Die Einschränkung in dieser Formulierung beruht darauf, dass es in der Sprache der Prädikatenlogik keine Aussagenvariablen gibt. Man kann sich vorstellen, dass die oben angeführten Tautologien aus den entsprechenden aussagelogischen \zusatzklammer {in Aussagenvariablen formulierten} {} {} Tautologien entstehen, indem man für die Aussagenvariablen beliebige prädikatenlogische Ausdrücke einsetzt. Dies führt zu folgendem Prinzip.
\inputfaktbeweis
{Prädikatenlogik/Aussagenlogische Tautologie/Einsetzen/Fakt}
{Lemma}
{}
{
\faktsituation {Es sei $\varphi$ eine in den
\definitionsverweis {Aussagenvariablen}{}{}
\mathl{p_1 , \ldots , p_n}{} formulierte aussagenlogische Tautologie und es seien
\mavergleichskette
{\vergleichskette
{ \beta_1 , \ldots , \beta_n
}
{ \in }{ L^S
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
prädikatenlogische Ausdrücke über einem
\definitionsverweis {Symbolalphabet}{}{}
$S$.}
\faktfolgerung {Dann ist auch der prädikatenlogische Ausdruck $\varphi'$, der entsteht, wenn man in $\varphi$ jedes Auftreten der Aussagenvariablen $p_i$ durch $\beta_i$ ersetzt, eine prädikatenlogische Tautologie.}
\faktzusatz {}
\faktzusatz {}
}
{
Wir führen Induktion über den Aufbau der aussagenlogischen Tautologien. Es sei $\varphi$ eines der
aussagenlogischen Axiome
in den Ausdrücken
\mathl{\alpha, \beta, \gamma}{} und es seien
\mathl{p_1 , \ldots , p_n}{} die darin auftretenden Aussagenvariablen. Wir schreiben die zugrunde liegende aussagenlogische Tautologie in den Aussagenvariablen
\mathl{p,q,r}{} und nennen diese $\psi$. Dann ist\zusatzfussnote {Wir verwenden hier das gleiche Substitutionssymbol für die Ersetzung von Aussagenvariablen durch aussagenlogische bzw. prädikatenlogische Ausdrücke wie in der Termsubstitution} {.} {}
\mavergleichskettedisp
{\vergleichskette
{\varphi
}
{ =} { \psi { \frac{ \alpha, \beta, \gamma }{ p, \, \, \, q, \, \, \, r } }
}
{ } {
}
{ } {
}
{ } {
}
}
{}{}{.}
Somit ist insgesamt
\mavergleichskettedisp
{\vergleichskette
{\varphi'
}
{ =} { \varphi { \frac{ \beta_1 , \ldots , \beta_n }{ p_1 , \ldots , p_n } }
}
{ =} { \psi { \frac{ \alpha { \frac{ \beta_1 , \ldots , \beta_n }{ p_1 , \ldots , p_n } } , \beta { \frac{ \beta_1 , \ldots , \beta_n }{ p_1 , \ldots , p_n } } , \gamma { \frac{ \beta_1 , \ldots , \beta_n }{ p_1 , \ldots , p_n } } }{ p,\, \, \,\, \, \,\, \, \,\, \, \, \, \,\, \, \,\, \, \, q,\, \, \,\, \, \,\, \, \,\, \, \, \, \, \,\, \, \,\, \, r } }
}
{ } {
}
{ } {
}
}
{}{}{.}
D.h. $\varphi'$ entsteht durch Einsetzung von prädikatenlogischen Ausdrücken in eine Basistautologie und gehört somit zu den in
Axiom 10.1
gelisteten Tautologien. Es sei nun $\varphi$ eine aussagenlogische Tautologie, die durch Modens ponens erhalten wird. Dann gibt es also eine aussagenlogische Tautologie $\psi$ und $\psi \rightarrow \varphi$ ist ebenfalls eine aussagenlogische Tautologie. Nach Induktionsvoraussetzung sind dann
\mathkor {} {\psi { \frac{ \beta_1 , \ldots , \beta_n }{ p_1 , \ldots , p_n } }} {und} {{ \left( \psi \rightarrow \varphi \right) } { \frac{ \beta_1 , \ldots , \beta_n }{ p_1 , \ldots , p_n } } = \psi { \frac{ \beta_1 , \ldots , \beta_n }{ p_1 , \ldots , p_n } } \rightarrow \varphi { \frac{ \beta_1 , \ldots , \beta_n }{ p_1 , \ldots , p_n } }} {}
prädikatenlogische Tautologien. Da der Modus ponens eine erlaubte Schlussregel in der Prädikatenlogik ist, folgt, dass
\mathl{\varphi { \frac{ \beta_1 , \ldots , \beta_n }{ p_1 , \ldots , p_n } }}{} eine prädikatenlogische Tautologie ist.
\inputbeispiel{}
{
Wir betrachten die aussagenlogische Tautologie der Form
\mathdisp {\alpha \rightarrow { \left( \beta \rightarrow \alpha \right) }} { }
mit
\mathdisp {\alpha = p_1 \wedge p_2 \text{ und } \beta = p_3 \rightarrow p_4} { , }
also, angelehnt an
Lemma 10.2,
\mavergleichskettedisp
{\vergleichskette
{\varphi
}
{ =} { { \left( q \rightarrow { \left( r \rightarrow q \right) } \right) } { \frac{ p_1 \wedge p_2 ,\, p_3 \rightarrow p_4 }{ q ,\, r } }
}
{ =} { { \left( p_1 \wedge p_2 \right) } \rightarrow { \left( { \left( p_3 \rightarrow p_4 \right) } \rightarrow { \left( p_1 \wedge p_2 \right) } \right) }
}
{ } {
}
{ } {
}
}
{}{}{.}
In diese aussagenlogische Tautologie soll
\mathdisp {p_1 \text{ durch } \beta_1 \defeq Rxy,\, p_2 \text{ durch } \beta_2 \defeq \forall u u=c ,\, p_3 \text{ durch } \beta_3 \defeq \exists y \forall x fxz= y,\, p_4 \text{ durch } \beta_4 \defeq \neg Pu,\,} { }
ersetzt werden. Das ergibt die prädikatenlogische Tautologie
\mathdisp {{ \left( Rxy \wedge \forall u u = c \right) } \rightarrow { \left( { \left( { \left( \exists y \forall x fxz = y \right) } \rightarrow \neg Pu \right) } \rightarrow { \left( Rxy \wedge \forall u u = c \right) } \right) }} { . }
}
Im Laufe der Einführung der prädikatenlogischen Tautologien und der zugehörigen Schlussregeln werden wir sogleich die Korrektheit feststellen, d.h., dass es sich auch um allgemeingültige Ausdrücke \zusatzklammer {semantische Tautologien} {} {} handelt. Für die aussagenlogischen Tautologien wurde die Korrektheit für aussagenlogische Modelle schon gezeigt, eine einfache Variante davon liefert die Korrektheit innerhalb von prädikatenlogischen Modellen.
\inputfaktbeweis
{Prädikatenlogik/Aussagenlogische Tautologie/Korrektheit/Fakt}
{Lemma}
{}
{
\faktsituation {}
\faktvoraussetzung {Jede aussagenlogische Tautologie im Sinne von
Axiom 10.1
ist}
\faktfolgerung {\definitionsverweis {allgemeingültig in der Prädikatenlogik}{}{.}}
\faktzusatz {}
\faktzusatz {}
}
{
Es sei $I$ eine
\definitionsverweis {Interpretation}{}{}
von $L^S$ und $\varphi$ eine aussagenlogische Grundtautologie in den prädikatenlogischen Ausdrücken
\mathl{\alpha, \, \beta , \, \gamma}{.} Dann ist der Wahrheitswert von $\varphi$ in $I$ nur abhängig von den Wahrheitswerten von
\mathl{\alpha, \, \beta , \, \gamma}{} in $I$ und den Junktoren in $\varphi$. Da es sich um eine aussagenlogische Tautologie handelt und die Wahrheitsvorschrift für die Junktoren in einem prädikatenlogischen Modell mit der in einem aussagenlogischen Modell übereinstimmt, besitzt $\varphi$ den Wahrheitswert $w$. Also ist $\varphi$ allgemeingültig.
Da allgemeingültige Aussagen unter Modus Ponens abgeschlossen sind, folgt daraus, dass generell alle prädikatenlogisch formulierten aussagenlogischen Tautologien allgemeingültig sind.
\zwischenueberschrift{Gleichheitstautologien}
In der Prädikatenlogik 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
\zusatzklammer {oder genauer Axiomenschemata} {} {}
heißen \stichwort {Gleichheitsaxiom} {} und \stichwort {Substitutionsaxiom} {.} Mit einer aussagenlogischen Umformulierung sieht man, dass das Substitutionsaxiom äquivalent zu
\mathdisp {\vdash s=t \rightarrow { \left( \alpha { \frac{ s }{ x } } \rightarrow \alpha { \frac{ t }{ x } } \right) }} { }
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}} { . }
}
{}
Bei leerer Variablenmenge ist das Substitutionsaxiom aussagelos. In Hinblick auf
Lemma 10.7
fordern wir, dass die Variablenmenge stets unendlich ist.
\inputfaktbeweis
{Prädikatenlogik/Gleichheitstautologien/Folgerungen/Fakt}
{Lemma}
{}
{
\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 10.3.}
{}
\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 10.5 (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) }} { . }
}
{}