Kurs:Einführung in die mathematische Logik (Osnabrück 2021)/Vorlesung 11/latex
\setcounter{section}{11}
\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 man bei einem 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 \alpha \frac{t}{x}} { }
gilt, so ist dies nach dem
Substitutionslemma
äquivalent zu
\mathdisp {I \frac{I(t)}{x} \vDash \alpha} { , }
und das bedeutet wiederum
\mathdisp {I \vDash \exists x \alpha} { . }
Einen wichtigen Spezialfall dieser Tautologie erhält man für
\mavergleichskette
{\vergleichskette
{t
}
{ = }{x
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{,}
nämlich
\zusatzklammer {unabhängig davon, ob $x$ in $\alpha$ vorkommt oder nicht} {} {}
\mathdisp {\vdash \alpha \rightarrow \exists x \alpha} { . }
Für den Allquantor
\zusatzklammer {den wir als Abkürzung verstehen} {} {}
ergibt sich die entsprechende Tautologie
\mathdisp {\vdash \forall x \alpha \rightarrow \alpha \frac{t}{x}} { . }
Streng genommen ergibt sich diese Variante in dieser Form aber erst unter Verwendung der Existenzeinführung im Antezedens, siehe weiter unten und
Aufgabe 11.8
und
Aufgabe 11.1.
\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
\zusatzklammer {bei $x=y$} {} {}
ist, dass man aus
\mathl{\vdash \alpha \rightarrow \beta}{} unter der Bedingung, dass $x$ nicht frei in $\beta$ vorkommt, auf
\mathl{\vdash \exists x \alpha \rightarrow \beta}{} schließen kann.
Die Allvariante dieser Schlussregel ist die \stichwort {All\-einführung im Sukzedens} {.} Sie besagt, dass man aus
\mathdisp {\vdash \beta \rightarrow \alpha \frac{y}{x}} { }
unter der Bedingung, dass $y$ weder in $\forall x \alpha$ noch in $\beta$ frei vorkommt, auf
\mathdisp {\vdash \beta \rightarrow \forall x \alpha} { }
schließen kann. Wir geben ein Beispiel für diese Version
\zusatzklammer {mit
\mavergleichskettek
{\vergleichskettek
{ x
}
{ = }{y
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}} {} {,}
wie sie in der mathematischen Praxis vorkommt.
\inputbeispiel{}
{
Nehmen wir an, wir möchten die Aussage beweisen, dass in einem jeden
\definitionsverweis {Monoid}{}{}
das neutrale Element eindeutig bestimmt ist. Wir formalisieren diese Aussage als
\mathdisp {\beta \rightarrow \forall x \alpha} { , }
wobei $\beta$ die Konjunktion der zwei Monoidaxiome
\zusatzklammer {also Assoziativität und Existenz des neutralen Elementes} {} {}
und
\mavergleichskette
{\vergleichskette
{ \alpha
}
{ \defeq }{\forall z (xz = z) \rightarrow x = e
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
ist. In $\alpha$ ist $x$ nicht gebunden, in
\mathl{\forall x \alpha}{} schon. In einem mathematischen Beweis wird man sich dann ein \anfuehrung{festes, aber beliebiges}{} Monoid $M$ \anfuehrung{denken}{,} und darin ein \anfuehrung{festes, aber beliebiges}{}
\mavergleichskette
{\vergleichskette
{x
}
{ \in }{M
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{.}
Für dieses $x$ beweist man dann die Aussage, dass wenn
\mavergleichskette
{\vergleichskette
{xz
}
{ = }{z
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
für alle
\mavergleichskette
{\vergleichskette
{z
}
{ \in }{M
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
gilt, dass dann
\mavergleichskette
{\vergleichskette
{x
}
{ = }{e
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
sein muss. Im Beweis selbst wird nicht über $x$ quantifiziert, dies steckt gewissermaßen in der gewählten Beliebigkeit drin. Man beweist also eher\zusatzfussnote {Diese Unschärfe in der Begrifflichkeit ist kaum zu vermeiden, da eine formale Interpretation oder Rekonstruktion dessen, was in der mathematischen Praxis passiert, nie ganz eindeutig ist} {.} {}
die Aussage
\mathdisp {\beta \rightarrow \alpha} { , }
und betrachtet dies als einen Beweis für die oben notierte Version. Da $x$ in $\beta$ gar nicht oder allenfalls gebunden vorkommt, ist die Ableitbarkeit beider Versionen auch prädikatenlogisch gleichwertig. Insofern spiegelt sich in der Alleinführung im Sukzedens eine wichtiger Aspekt der mathematischen Praxis.
}
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.
}
\inputdefinition
{}
{
Ein Ausdruck
\mavergleichskette
{\vergleichskette
{ \alpha
}
{ \in }{ L^S
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
heißt
\definitionswort {ableitbar}{}
im Prädikatenkalkül
\zusatzklammer {oder eine
\definitionswort {syntaktische Tautologie}{}} {} {,}
wenn er sich aus den Grundtautologien, also
\auflistungdrei{den aussagenlogischen \definitionsverweis {syntaktischen Tautologien}{}{,}
}{den \definitionsverweis {Gleichheitsaxiomen}{}{,}
}{der \definitionsverweis {Existenzeinführung im Sukzedens}{}{,}
}
durch sukzessive Anwendung der Ableitungsregeln
\definitionsverweis {Modus ponens}{}{}
und der \definitionsverweis {Existenzeinführung im Antezedens}{}{}
erhalten lässt. Die Ableitbarkeit wird durch
\mathdisp {\vdash \alpha} { }
ausgedrückt.
}
\zwischenueberschrift{Abgeleitete Regeln und weitere Tautologien}
Bisher haben wir lediglich den Modus ponens und die Existenzeinführung im Antezedens als Ableitungsregeln für den syntaktischen Kalkül zur Verfügung. Daraus ergeben sich allerdings sofort neue Ableitungsregeln, mit denen man neue Tautologien herleiten kann. Die Hinrichtung in der folgenden Aussage kommt häufig implizit in einer mathematischen Argumentation vor. Man beweist eine Aussage für beliebige, aber feste Elemente, und fasst dies als einen Beweis für die entsprechende Allaussage auf.
\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 11.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 3.8 (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 $\alpha$ bedeutet, dass bei einer beliebigen
\zusatzklammer {Struktur- und} {} {}
Variablenbelegung die entstehende Aussage ohne freie Variable wahr wird. Da ist also eine Allaussage schon miteingebunden. Insbesondere gilt
\betonung{nicht}{}
\mathl{\vdash \alpha \leftrightarrow \forall x \alpha}{.}
Für den Existenzquantor gilt die entsprechende Äquivalenz nicht. Zwar ergibt sich aus
\mathl{\vdash \alpha}{} direkt
\mathl{\vdash \exists x \alpha}{}
\zusatzklammer {und zwar unabhängig davon, ob $x$ in $\alpha$ 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)} { }
nach
Aufgabe 11.2,
aber
\mavergleichskette
{\vergleichskette
{x
}
{ = }{y
}
{ }{
}
{ }{
}
{ }{
}
}
{}{}{}
ist keine Tautologie.
\inputfaktbeweis
{Prädikatenlogik/Quantoren/Tautologie/Vertauschung/Fakt}
{Lemma}
{}
{
\faktsituation {}
\faktuebergang {Die folgenden Ausdrücke sind im Prädikatenkalkül
\definitionsverweis {ableitbar}{}{.}}
\faktfolgerung {\aufzaehlungzwei {
\mathdisp {\vdash \exists x \exists y \alpha \rightarrow \exists y \exists x \alpha} { . }
} {
\mathdisp {\vdash \forall x \forall y \alpha \rightarrow \forall y \forall x \alpha} { . }
}}
\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) wird ähnlich wie (1) bewiesen oder darauf zurückgeführt.}
{}
Für die
\zusatzklammer {Nicht} {} {-}Vertauschbarkeit des Allquantors mit dem Existenzquantor siehe
Aufgabe 11.24.
\inputfaktbeweis
{Prädikatenlogik/Quantoren/Tautologien/Ein Quantor/Ableitungen/Fakt}
{Lemma}
{}
{
\faktsituation {}
\faktuebergang {Die folgenden Ausdrücke sind im Prädikatenkalkül
\definitionsverweis {ableitbar}{}{.}}
\faktfolgerung {\aufzaehlungvier{
\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). 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 3.16 (2)} {} {}
ergibt
\mathdisp {\vdash \forall x \alpha \wedge \forall x (\alpha \rightarrow \beta) \rightarrow \alpha \wedge (\alpha \rightarrow \beta)} { . }
Ferner haben wir nach
Lemma 3.17
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 (2) siehe
Aufgabe 11.9
und
Aufgabe 11.10.}
{}
\teilbeweis {}{}{}
{(3). 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 (4) siehe
Aufgabe 11.11.}
{}
Die folgende Aussage zeigt, dass man quantifizierte Aussagen im Wesentlichen mit beliebigen Variablen formulieren kann.
\inputfaktbeweis
{Prädikatenlogik/Existenz/Variablenumformulierung/Fakt}
{Lemma}
{}
{
\faktsituation {Es sei $\alpha$ ein Ausdruck über einem
\definitionsverweis {erststufigen Symbolalphabet}{}{}
$S$ und seien $x,y$ Variablen.}
\faktvoraussetzung {Die Variable $y$ komme in $\alpha$ nicht und die Variable $x$ komme in $\alpha$ allenfalls frei vor.}
\faktfolgerung {Dann ist
\mathdisp {\vdash \exists x \alpha \rightarrow \exists y { \left( \alpha { \frac{ y }{ x } } \right) }} { . }
}
\faktzusatz {}
\faktzusatz {}
}
{
Nach
Axiom 11.1,
angewendet auf
\mathl{\alpha { \frac{ y }{ x } }}{,} ist
\mathdisp {\vdash \alpha { \frac{ y }{ x } } \rightarrow \exists y { \left( \alpha { \frac{ y }{ x } } \right) }} { . }
Da $y$ in
\mathl{\exists y { \left( \alpha { \frac{ y }{ x } } \right) }}{} gebunden vorkommt und in $\exists x \alpha$ gar nicht, kann man
Axiom 11.2
anwenden und erhält
\mathdisp {\vdash \exists x \alpha \rightarrow \exists y { \left( \alpha { \frac{ y }{ x } } \right) }} { . }
\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.