Deduktion: Zusammenfassung und Herausforderungen

Zusammenfassung

Diese Lektion schließt die Einheit über die Deduktion ab. Sie rekonstruiert die deduktive Kette, die von der Definition des Łukasiewicz-Kalküls (drei Axiomenschemata und der Modus ponens) zum Deduktionstheorem und zur Grenze dieses Kalküls in der Sprache des Peirce-Pfeils führt; von dort zu den vier grundlegenden Techniken und zur Regel der Ersetzung der doppelten Negation, die den Kalkül des Kurses vervollständigt; vom Fundamentallemma des Peirce-Pfeils zur Ersetzung äquivalenter Formeln und zu den Symmetrien, und von dort zu den Regeln der klassischen Logik und zu den De-Morgan-Gesetzen und den Distributivgesetzen, und gibt bei jedem Glied an, welche Ergebnisse es verwendet und in welcher Lektion es bewiesen wird. Sie unterscheidet, was die Einheit bewiesen, von dem, was sie angenommen hat, ordnet das Erreichte in den Plan des Kurses ein und erklärt, warum die Frage, die die Einheit offenlässt, nämlich ob das Ableitbare mit dem Wahren zusammenfällt, zur Einheit über die Semantik führt. Ihr Abschlusstest wiederholt die Fertigkeiten des Eingangstests, und am Ende stehen sechs Herausforderungen, schwieriger als die Aufgaben der Lektionen, die verlangen, die Werkzeuge mehrerer von ihnen zu verbinden.

Lernziele

Die logische Ordnung der Ergebnisse der Einheit rekonstruieren und dabei die früheren Ergebnisse, auf die sich jedes stützt, und die Lektion, in der es bewiesen wird, angeben.
Erklären, wie das Deduktionstheorem, die doppelte Negation, die Regel der Ersetzung der doppelten Negation, die Kontraposition, das Fundamentallemma und die Ersetzung äquivalenter Formeln ineinandergreifen und warum die klassischen Regeln, die De-Morgan-Gesetze und die Distributivgesetze von ihnen abhängen.
Unterscheiden, was die Einheit bewiesen und was sie angenommen hat (die Axiomenschemata, die beiden primitiven Regeln, die starke und die strukturelle Induktion und die eindeutige Lesbarkeit), und was sie den folgenden Einheiten überlassen hat, insbesondere die Beziehung zwischen Ableitung und Wahrheit.
Aufgaben lösen, die die Markierungen, die Regel der Ersetzung der doppelten Negation, das Deduktionstheorem, die Fallunterscheidung, die Reductio ad absurdum, die Ersetzung äquivalenter Formeln, die De-Morgan-Gesetze und die Distributivgesetze verbinden.

Was die Einheit erreicht hat

Die Einheit hatte sich vorgenommen, die Sprache der vorigen Einheit mit einem Deduktionssystem auszustatten, das heißt mit einer rein syntaktischen Weise, Formeln aus anderen zu gewinnen, und mit diesem System Zeile für Zeile die Techniken zu beweisen, mit denen die Mathematik argumentiert. Das Vorhaben ist mit wenigen Vorbehalten erfüllt, deren jeder an seiner Stelle offengelegt wurde: die drei Axiomenschemata und die beiden primitiven Regeln, die nicht bewiesen, sondern gewählt werden und deren richtige Wahl eine Frage ist, die die Einheit stellt, ohne sie ganz zu beantworten; die starke und die strukturelle Induktion, die eindeutige Lesbarkeit und die Definition durch Rekursion, die in der vorigen Einheit bewiesen wurden und hier verwendet werden; und das Unentbehrliche der Mengenlehre (Teilmengen, Vereinigungen und endliche Mengen), das dort in Erinnerung gerufen wurde, wo es nötig war. Mit diesen Vorbehalten lässt sich der zurückgelegte Weg als eine einzige deduktive Kette in vier Abschnitten lesen.

Der Łukasiewicz-Kalkül und seine Grenze

Die Lektion über formale Deduktionssysteme hat ein System als eine Sprache, einige Axiome und einige Regeln definiert, die sich alle allein durch Betrachtung der Zeichenketten prüfen lassen, und die erste Stufe des Kalküls des Kurses festgelegt, den Łukasiewicz-Kalkül: die Schemata A1, A2 und A3 und den Modus ponens als einzige Regel, die durch die eindeutige Lesbarkeit ohne Mehrdeutigkeit anwendbar wird. Sie hat die Ableitung aus einer Menge $\Gamma$ von Prämissen und die Relation $\Gamma \vdash \varphi$ definiert, $\vdash (\varphi \rightarrow \varphi)$ in fünf Zeilen abgeleitet und die strukturellen Eigenschaften bewiesen: Reflexivität, Monotonie, Modus ponens zwischen Ableitungen, Schnitt und Endlichkeit. Mit ihnen und mit der starken Induktion über die Anzahl der Zeilen hat sie das Deduktionstheorem bewiesen, dessen zweiter Fall verlangt, dass zuvor $(\varphi \rightarrow \varphi)$ abgeleitet wurde, und seine Umkehrung; aus beiden hat sie die beweisbare Äquivalenz gewonnen, die reflexiv, symmetrisch und transitiv ist. Schließlich hat sie die Grenze dieses Kalküls gezeigt: Eine Markierung mit den Werten $0$ und $1$ , definiert durch Rekursion über die primitive Form $(\alpha \downarrow \beta)$ , behandelt die Negation und die Implikation wie gewohnt, wird von A1, A2, A3 und dem Modus ponens erhalten und lässt den Wert von Formeln wie $(v_{1} \downarrow v_{2})$ frei. Daraus folgt, dass $((v_{1} \downarrow v_{2}) \rightarrow \neg v_{1})$ kein Theorem des Łukasiewicz-Kalküls ist und dass aus $(v_{1} \downarrow v_{2})$ nicht $(\neg\neg v_{1} \downarrow v_{2})$ ableitbar ist, noch umgekehrt. Da jede Markierung $\theta$ und $\neg\neg\theta$ denselben Wert gibt, hat die Lektion außerdem darauf hingewiesen, dass nicht einmal die doppelte Negation, einmal bewiesen, diese Grenze beheben würde.

Die vier Techniken und die neue Regel

Die Lektion über die vier Ableitungstechniken hat zuerst das Lemma „vom Ergebnis zur Regel“ bewiesen: Wenn $\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta$ , so erhält man dieselbe Konklusion aus jedem $\Gamma$ , das jedes $\alpha_{i}$ ableitet, und außerdem gilt $\vdash (\alpha_{1} \rightarrow (\alpha_{2} \rightarrow \cdots (\alpha_{n} \rightarrow \beta) \cdots))$ . Dieses Lemma erlaubt es, jede Technik in drei Gestalten zu verwenden (aus Prämissen, als Theorem und als Regel), und die Lektionen über die Symmetrien und über De Morgan, die Ketten von Äquivalenzen mit dem Schnitt verbinden, stützen sich dafür auf die Eigenschaften der beweisbaren Äquivalenz aus der ersten Lektion, die dieselbe Idee für eine einzige Prämisse sind; in der Kette erscheint jedes Ergebnis nur einmal, dort, wo es bewiesen wird. Mit ihm hat die Lektion den hypothetischen Syllogismus aus A1 und A2 in sieben Zeilen abgeleitet, die Vertauschung der Prämissen mit dem Deduktionstheorem, die doppelte Negation (deren erste Richtung A3 zweimal auf eine mit A1 hergestellte Implikation anwendet und deren zweite die erste auf $\neg\varphi$ und A3 anwendet) und die Kontraposition in ihren drei Formen, die die Negationen einer Implikation auf drei Weisen verteilen; alle vier gelten schon im Łukasiewicz-Kalkül.

Nachdem die doppelte Negation bewiesen war, hat die Lektion den Kalkül des Kurses um eine zweite primitive Regel ergänzt, die Ersetzung der doppelten Negation (EDN): Aus $\chi$ folgt $\chi'$ , wenn $\chi'$ aus $\chi$ dadurch entsteht, dass man ein Vorkommen einer Teilformel $\theta$ durch $\neg\neg\theta$ ersetzt oder eines von $\neg\neg\theta$ durch $\theta$ . Die Regel muss postuliert werden, weil die Markierung $m_{1}$ den Theoremen der doppelten Negation den Wert $1$ gibt und dennoch $(v_{1} \downarrow v_{2})$ von $(\neg\neg v_{1} \downarrow v_{2})$ trennt; EDN erhält $m_{1}$ nicht und erweitert deshalb das Ableitbare, erhält aber die ehrliche Markierung und erweitert es deshalb nicht zu sehr. Die Regel wirkt auf die Zeichenkette der Grundsprache, in der eine Negation ihr Argument verdoppelt: $(\varphi \rightarrow \psi)$ enthält die Teilformel $\neg\varphi$ zweimal, und eine doppelte Negation vor ihr Antezedens zu setzen, erfordert zwei Anwendungen. Dieselbe Beobachtung trägt die Erweiterung des Deduktionstheorems: Ergibt sich eine Zeile durch die Regel, so liefert die Induktionsvoraussetzung die Implikation, deren Konsequens die vorige Zeile ist, und zwei Anwendungen der Regel, eine in jeder Kopie dieses Konsequens, liefern die gesuchte Implikation; die übrigen strukturellen Eigenschaften gelten mit demselben Beweis. Die ersten Folgerungen sind, dass eine Formel zu jeder Formel äquivalent ist, die aus ihr durch die Regel entsteht, insbesondere $(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi)$ und $(\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi)$ , und dass die entsprechenden Implikationen, die andere Kalküle als Axiome nehmen, hier Theoreme sind.

Junktoren und Ersetzung

Die Lektion über die Symmetrien der Junktoren hat sich der Schwierigkeit gestellt, die der Sprache der Kreise und Scheiben eigen ist: Die Axiome von Łukasiewicz sprechen nur von Negationen und Implikationen, und fast kein Peirce-Pfeil ist das eine oder das andere. Das Fundamentallemma, $(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi)$ , schlägt die Brücke: Da $\neg(\neg\varphi \rightarrow \psi)$ nichts anderes als $\neg\neg(\neg\neg\varphi \downarrow \psi)$ ist, setzt die Regel EDN die innere doppelte Negation und die doppelte Negation die äußere; in umgekehrter Richtung entfernen die doppelte Negation und die Regel sie. Mit ihm wurde die Ersetzung äquivalenter Formeln, zuerst unter der Negation und auf beiden Seiten der Implikation mit der Kontraposition und dem hypothetischen Syllogismus bewiesen, auf beide Argumente des Peirce-Pfeils ausgedehnt und von dort auf die Disjunktion und die Konjunktion. Die Regel und die Ersetzung machen einander nicht überflüssig: Die Regel vertauscht nur $\theta$ und $\neg\neg\theta$ , während die Ersetzung beliebige äquivalente Formeln zulässt; und die Ersetzung, mit dem Fundamentallemma bewiesen, beruht ihrerseits auf der Regel. Danach hat die Lektion bewiesen, dass die Formen, die andere Texte als Definitionen nehmen, Äquivalenzen sind: $(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi)$ , das zwei Anwendungen der Regel verlangt, eine in jeder Kopie, die die äußere Negation erzeugt, und $(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \downarrow \neg\psi)$ , das die doppelte Negation verlangt; dagegen sind $(\varphi \wedge \psi)$ und $\neg(\varphi \rightarrow \neg\psi)$ dieselbe Zeichenkette. Schließlich hat sie die fünf Symmetrien in der Reihenfolge bewiesen, die die Definitionen vorgeben: die des Peirce-Pfeils mit dem Fundamentallemma und der Kontraposition, und jede der übrigen mit der vorigen, die bei Bedarf mit der Ersetzung unter der Negation übertragen wird.

Die klassischen Regeln und die Gesetze

Die Lektion über die Techniken der klassischen Logik hat, alle mit einer Menge $\Gamma$ von Prämissen, die von Zeile zu Zeile mitgeführt wird, die Einführung und die Elimination der Disjunktion und der Konjunktion bewiesen, das Tertium non datur und den Satz vom Widerspruch, das Ex falso quodlibet, die Reductio ad absurdum in ihren beiden Formen und die Fallunterscheidung, mit einer Formel und ihrer Negation und mit einer beliebigen Disjunktion. Die Reihenfolge der Abhängigkeiten ist streng: Das Ex falso quodlibet beruht auf den Regeln der Disjunktion; die klassische Reductio ad absurdum auf dem Ex falso quodlibet und auf A3; die Fallunterscheidung auf der Kontraposition und auf der Reductio ad absurdum. Keiner dieser Beweise ruft die Regel EDN unmittelbar auf: Die Regel wirkt über die äquivalenten Formen und die Ersetzung äquivalenter Formeln. Die Lektion über die De-Morgan-Gesetze und die Distributivgesetze hat diese Regeln zusammenarbeiten lassen: Das erste De-Morgan-Gesetz ergibt sich aus der Definition der Konjunktion und aus der doppelten Negation; das zweite verlangt, in den Peirce-Pfeil hineinzugehen, wo die Regel EDN zweimal eingreift, einmal in jedem Argument und ohne dass die Symmetrie nötig wäre, und aus ihm folgt, dass $(\varphi \downarrow \psi)$ zu $(\neg\varphi \wedge \neg\psi)$ äquivalent ist, die Lesart „weder $\varphi$ noch $\psi$ “, die die vorige Einheit festgesetzt hatte; zu den Varianten gehört $\neg(\varphi \rightarrow \psi) \dashv\vdash (\varphi \wedge \neg\psi)$ . Die beiden Distributivgesetze wurden in ihren beiden Richtungen durch Fallunterscheidung bewiesen, wobei in jeder die passende Form der Fallunterscheidung gewählt wurde.

Die folgende Abbildung fasst die vier Abschnitte zu einer einzigen Kette zusammen. Jeder Knoten der Säule ist eine Definition oder ein Ergebnis, nummeriert nach der logischen Ordnung und durch einen Bogen mit den früheren Gliedern verbunden, die sein Beweis verwendet; ringsum schweben die Stützen, also die Prinzipien und die Werkzeuge, auf die die Kette immer wieder zurückgreift, jede durch einen durchgezogenen Strich mit den Gliedern verbunden, die sich auf sie stützen, und durch einen gepunkteten mit dem Glied, in dem sie begründet wird, außer denen, die diese Kette nicht beweist (die Axiomenschemata, die angenommen werden, und die Werkzeuge der vorigen Einheit) und die als Ringe gezeichnet sind. Die Regel der Ersetzung der doppelten Negation, obwohl auch sie ohne Beweis angenommen wird, erscheint mit dem Glied verbunden, das sie einführt, weil dort erklärt wird, warum sie postuliert werden muss. Ein Klick auf eine Stütze hebt alle Glieder hervor, die sie verwenden, und jedes Glied verweist auf die Lektion, in der es bewiesen wird. Man beachte, dass das Deduktionstheorem und die doppelte Negation nach den Axiomen die am häufigsten besuchten Stützen der Einheit sind und dass die neue Regel alles trägt, was die Einheit über den Peirce-Pfeil sagt: das erweiterte Deduktionstheorem, das Fundamentallemma, die äquivalenten Formen und das zweite De-Morgan-Gesetz.

Stützen der Kette

AEindeutige Lesbarkeit und Rekursion. Wenn $\sigI\varphi\psi = \sigI\varphi'\psi'$ , wobei alle vier Zeichenketten Formeln sind, dann $\varphi = \varphi'$ und $\psi = \psi'$ ; daher definiert eine Regel, die den Wert von $\sigI\varphi\psi$ aus $\varphi$ , aus $\psi$ und aus deren Werten berechnet, eine einzige Funktion auf den Formeln. Bewiesen in der vorigen Einheit. In dieser Einheit ohne Beweis angenommen.
BStarke Induktion. Gilt eine Eigenschaft für eine natürliche Zahl immer dann, wenn sie für alle kleineren gilt, so gilt sie für alle natürlichen Zahlen. Sie wurde in der vorigen Einheit aus der einfachen Induktion abgeleitet und wird hier auf die Anzahl der Zeilen einer Ableitung angewandt. In dieser Einheit ohne Beweis angenommen.
CAxiome von Łukasiewicz. Die Schemata A1, $(\varphi \rightarrow (\psi \rightarrow \varphi))$ ; A2, $((\varphi \rightarrow (\psi \rightarrow \chi)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \chi)))$ ; und A3, $((\neg\psi \rightarrow \neg\varphi) \rightarrow (\varphi \rightarrow \psi))$ . Sie werden angenommen. In dieser Einheit ohne Beweis angenommen.
DErsetzung der doppelten Negation. Zweite primitive Regel des Kalküls des Kurses: Aus $\chi$ folgt $\chi'$ , wenn $\chi'$ aus $\chi$ dadurch entsteht, dass man ein Vorkommen einer Teilformel $\theta$ durch $\neg\neg\theta$ ersetzt oder eines von $\neg\neg\theta$ durch $\theta$ . Sie wird postuliert, nachdem die doppelte Negation bewiesen ist. Begründet in: 8. Ersetzung der doppelten Negation.
EDeduktionstheorem. $\Gamma \cup \{\varphi\} \vdash \psi$ genau dann, wenn $\Gamma \vdash (\varphi \rightarrow \psi)$ ; es wird im Łukasiewicz-Kalkül bewiesen und gilt, mit einem Fall mehr, im Kalkül des Kurses. Begründet in: 3. Deduktionstheorem und beweisbare Äquivalenz.
FVom Ergebnis zur Regel. Wenn $\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta$ und $\Gamma \vdash \alpha_{i}$ für jedes $i$ , dann $\Gamma \vdash \beta$ : Jede aus Prämissen bewiesene Technik lässt sich unter jeder Prämissenmenge anwenden. Begründet in: 5. Vom Ergebnis zur Regel.
GDoppelte Negation. $\varphi \dashv\vdash \neg\neg\varphi$ , mit den Theoremen $\vdash (\neg\neg\varphi \rightarrow \varphi)$ und $\vdash (\varphi \rightarrow \neg\neg\varphi)$ . Begründet in: 7. Doppelte Negation.
HErsetzung äquivalenter Formeln. Wenn $\varphi \dashv\vdash \varphi'$ , so kann man $\varphi'$ an die Stelle von $\varphi$ setzen, unter einer Negation, auf beiden Seiten einer Implikation, eines Peirce-Pfeils, einer Disjunktion und einer Konjunktion, ohne die Äquivalenz zu verändern. Begründet in: 12. Ersetzung äquivalenter Formeln.

Abschnitt 1 Der Łukasiewicz-Kalkül und seine Grenze
- Die Instanzen der Schemata erkennen und entscheiden, ob eine Folge von Formeln eine Ableitung aus einer Prämissenmenge ist.
- Die strukturellen Eigenschaften der Ableitbarkeit und das Deduktionstheorem durch starke Induktion über die Anzahl der Zeilen beweisen.
- Ableitungen über Ableitungen mit Reflexivität, Monotonie, Schnitt, dem Deduktionstheorem und seiner Umkehrung aufbauen.
- Mit einer Markierung, die die Axiome und der Modus ponens erhalten, beweisen, dass eine Formel nicht ableitbar ist, und mit ihr die Grenze des Łukasiewicz-Kalküls erklären.
1. System, Ableitung und Identität. Die Axiome des Łukasiewicz-Kalküls sind die gleichförmigen Instanzen von A1 bis A3, und seine einzige Regel ist der Modus ponens. $\Gamma \vdash \varphi$ , wenn es eine endliche Folge von Formeln gibt, die mit $\varphi$ endet und deren Glieder jeweils ein Axiom, ein Element von $\Gamma$ oder durch Modus ponens aus zwei früheren gewonnen sind. Das erste Theorem, $\vdash (\varphi \rightarrow \varphi)$ , wird in fünf Zeilen mit A1 und A2 abgeleitet.
  Stützt sich auf: A (Eindeutige Lesbarkeit und Rekursion), C (Axiome von Łukasiewicz). Bewiesen in: Formale Deduktionssysteme.
2. Strukturelle Eigenschaften. Wenn $\varphi \in \Gamma$ , dann $\Gamma \vdash \varphi$ ; wenn $\Gamma \subseteq \Delta$ und $\Gamma \vdash \varphi$ , dann $\Delta \vdash \varphi$ ; aus $\Gamma \vdash \varphi$ und $\Gamma \vdash (\varphi \rightarrow \psi)$ folgt $\Gamma \vdash \psi$ ; wenn $\Gamma \vdash \varphi_{i}$ für jedes $i$ und $\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{r}\} \vdash \psi$ , dann $\Gamma \vdash \psi$ ; und wenn $\Gamma \vdash \varphi$ , so genügt eine endliche Teilmenge von $\Gamma$ .
  Verwendet: 1. System, Ableitung und Identität. Bewiesen in: Formale Deduktionssysteme.
3. Deduktionstheorem und beweisbare Äquivalenz. $\Gamma \cup \{\varphi\} \vdash \psi$ genau dann, wenn $\Gamma \vdash (\varphi \rightarrow \psi)$ , durch starke Induktion über die Anzahl der Zeilen, mit A1, A2 und der Identität. Daraus folgt, dass die beweisbare Äquivalenz, $\varphi \dashv\vdash \psi$ , reflexiv, symmetrisch und transitiv ist und dass zwei äquivalente Formeln aus denselben Mengen ableitbar sind.
  Verwendet: 1. System, Ableitung und Identität, 2. Strukturelle Eigenschaften. Stützt sich auf: B (Starke Induktion), C (Axiome von Łukasiewicz). Bewiesen in: Formale Deduktionssysteme.
4. Grenze des Łukasiewicz-Kalküls. Eine durch Rekursion definierte Markierung mit den Werten $0$ und $1$ erfüllt $m(\neg\varphi) = 1 - m(\varphi)$ und $m((\varphi \rightarrow \psi)) = 1 - m(\varphi) \left( 1 - m(\psi) \right)$ , und A1, A2, A3 und der Modus ponens erhalten die Markierung $1$ ; daher ist $((v_{1} \downarrow v_{2}) \rightarrow \neg v_{1})$ kein Theorem des Łukasiewicz-Kalküls, und es gilt $\{(v_{1} \downarrow v_{2})\} \nvdash (\neg\neg v_{1} \downarrow v_{2})$ , ebenso umgekehrt. Da jede Markierung der doppelten Negation den Wert $1$ gibt, muss die Ersetzung postuliert werden.
  Verwendet: 1. System, Ableitung und Identität. Stützt sich auf: A (Eindeutige Lesbarkeit und Rekursion), B (Starke Induktion), C (Axiome von Łukasiewicz). Bewiesen in: Formale Deduktionssysteme.
Abschnitt 2 Die vier Techniken und die neue Regel
- Ein Ergebnis aus Prämissen in ein Theorem und in eine Regel umwandeln, die unter jeder Prämissenmenge anwendbar ist.
- Implikationen verketten, Antezedenzien umordnen, doppelte Negationen setzen und entfernen und die Form der Kontraposition wählen, die zu jeder Implikation passt.
- Die Regel der Ersetzung der doppelten Negation anwenden, dabei die Vorkommen finden, die die Abkürzungen verbergen, und sie in jeder Kopie wiederholen, die eine Negation erzeugt.
- Mit der Markierung erklären, warum die Regel postuliert wird, und beweisen, dass das Deduktionstheorem mit ihr gilt.
1. Vom Ergebnis zur Regel. Wenn $\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta$ , dann folgt aus $\Gamma \vdash \alpha_{1}$ , $\ldots$ , $\Gamma \vdash \alpha_{n}$ auch $\Gamma \vdash \beta$ , und es gilt $\vdash (\alpha_{1} \rightarrow (\alpha_{2} \rightarrow \cdots (\alpha_{n} \rightarrow \beta) \cdots))$ ; insbesondere gilt, wenn $\alpha \dashv\vdash \alpha'$ , dass $\Gamma \vdash \alpha$ genau dann, wenn $\Gamma \vdash \alpha'$ .
  Verwendet: 2. Strukturelle Eigenschaften. Stützt sich auf: E (Deduktionstheorem). Bewiesen in: Vier Ableitungstechniken.
2. Hypothetischer Syllogismus und Vertauschung. $\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi)$ , mit einer Ableitung von sieben Zeilen aus A1 und A2; und $\{(\varphi \rightarrow (\psi \rightarrow \chi))\} \vdash (\psi \rightarrow (\varphi \rightarrow \chi))$ .
  Verwendet: 1. System, Ableitung und Identität. Stützt sich auf: C (Axiome von Łukasiewicz), E (Deduktionstheorem), F (Vom Ergebnis zur Regel). Bewiesen in: Vier Ableitungstechniken.
3. Doppelte Negation. $\vdash (\neg\neg\varphi \rightarrow \varphi)$ , indem man A3 zweimal auf eine Implikation anwendet, die A1 aus $\neg\neg\varphi$ herstellt; $\vdash (\varphi \rightarrow \neg\neg\varphi)$ , indem man das Vorige auf $\neg\varphi$ und A3 anwendet; daher $\varphi \dashv\vdash \neg\neg\varphi$ , schon im Łukasiewicz-Kalkül.
  Stützt sich auf: C (Axiome von Łukasiewicz), E (Deduktionstheorem). Bewiesen in: Vier Ableitungstechniken.
4. Ersetzung der doppelten Negation. Die Regel EDN wird postuliert, weil die Markierung der doppelten Negation den Wert $1$ gibt, nicht aber der Ersetzung innerhalb eines Peirce-Pfeils. Entsteht $\chi'$ aus $\chi$ durch die Regel, so gilt $\chi \dashv\vdash \chi'$ ; insbesondere $(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi)$ und $(\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi)$ .
  Verwendet: 3. Deduktionstheorem und beweisbare Äquivalenz, 4. Grenze des Łukasiewicz-Kalküls. Stützt sich auf: G (Doppelte Negation). Bewiesen in: Vier Ableitungstechniken.
5. Deduktionstheorem im Kalkül des Kurses. Reflexivität, Monotonie, Schnitt und Endlichkeit gelten mit der neuen Regel, ebenso $\Gamma \cup \{\varphi\} \vdash \psi$ genau dann, wenn $\Gamma \vdash (\varphi \rightarrow \psi)$ : Im neuen Fall wird die Regel, da $(\varphi \rightarrow \chi)$ gleich $((\neg\varphi \downarrow \chi) \downarrow (\neg\varphi \downarrow \chi))$ ist, zweimal angewandt, einmal in jeder Kopie von $\chi$ . Daraus sind $\vdash ((\varphi \downarrow \psi) \rightarrow (\neg\neg\varphi \downarrow \psi))$ und seine Umkehrung Theoreme.
  Verwendet: 2. Strukturelle Eigenschaften, 3. Deduktionstheorem und beweisbare Äquivalenz. Stützt sich auf: B (Starke Induktion), D (Ersetzung der doppelten Negation). Bewiesen in: Vier Ableitungstechniken.
6. Kontraposition. $(\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \neg\varphi)$ , $(\neg\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \varphi)$ und $(\varphi \rightarrow \neg\psi) \dashv\vdash (\psi \rightarrow \neg\varphi)$ : Die Glieder wechseln die Seite, und jedes wechselt beim Übergang sein Vorzeichen.
  Verwendet: 6. Hypothetischer Syllogismus und Vertauschung. Stützt sich auf: C (Axiome von Łukasiewicz), E (Deduktionstheorem), G (Doppelte Negation), F (Vom Ergebnis zur Regel). Bewiesen in: Vier Ableitungstechniken.
Abschnitt 3 Junktoren und Ersetzung
- Die Abkürzungen auflösen, um zu entscheiden, ob zwei Ausdrücke dieselbe Zeichenkette bezeichnen oder Formeln, deren Äquivalenz eine Ableitung erfordert.
- Den Peirce-Pfeil mit dem Fundamentallemma in Negation und Implikation übersetzen.
- Eine Äquivalenz mit der Ersetzung äquivalenter Formeln ins Innere einer Formel übertragen, sie von der Regel der Ersetzung der doppelten Negation unterscheiden und Äquivalenzen verketten.
- Die fünf Symmetrien in der Reihenfolge beweisen, die die Definitionen vorgeben.
1. Fundamentallemma. $(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi)$ : Da $\neg(\neg\varphi \rightarrow \psi)$ nichts anderes als $\neg\neg(\neg\neg\varphi \downarrow \psi)$ ist, setzt die Regel EDN die innere doppelte Negation und die doppelte Negation die äußere; in umgekehrter Richtung entfernen die doppelte Negation und die Regel sie.
  Stützt sich auf: D (Ersetzung der doppelten Negation), G (Doppelte Negation). Bewiesen in: Die Symmetrien der Junktoren.
2. Ersetzung äquivalenter Formeln. Wenn $\varphi \dashv\vdash \varphi'$ , dann $\neg\varphi \dashv\vdash \neg\varphi'$ , $(\varphi \rightarrow \psi) \dashv\vdash (\varphi' \rightarrow \psi)$ und $(\psi \rightarrow \varphi) \dashv\vdash (\psi \rightarrow \varphi')$ ; mit dem Fundamentallemma dasselbe auf beiden Seiten des Peirce-Pfeils, und von dort für die Disjunktion und die Konjunktion. Anders als die Regel EDN lässt sie beliebige äquivalente Formeln zu.
  Verwendet: 6. Hypothetischer Syllogismus und Vertauschung, 10. Kontraposition, 11. Fundamentallemma. Stützt sich auf: E (Deduktionstheorem). Bewiesen in: Die Symmetrien der Junktoren.
3. Äquivalente Formen. $(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi)$ , mit zwei Anwendungen der Regel EDN, eine in jeder Kopie, die die äußere Negation erzeugt; $(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \downarrow \neg\psi)$ , durch die doppelte Negation; und $(\varphi \wedge \psi)$ ist dieselbe Zeichenkette wie $\neg(\varphi \rightarrow \neg\psi)$ .
  Stützt sich auf: D (Ersetzung der doppelten Negation), G (Doppelte Negation). Bewiesen in: Die Symmetrien der Junktoren.
4. Die fünf Symmetrien. $(\varphi \downarrow \psi) \dashv\vdash (\psi \downarrow \varphi)$ , durch das Fundamentallemma und die Kontraposition; daraus nacheinander die Symmetrien von $\vee$ , $\wedge$ , $\leftrightarrow$ und $\veebar$ , jede mit der vorigen, die bei Bedarf mit der Ersetzung unter der Negation übertragen wird.
  Verwendet: 11. Fundamentallemma, 10. Kontraposition. Stützt sich auf: H (Ersetzung äquivalenter Formeln). Bewiesen in: Die Symmetrien der Junktoren.
Abschnitt 4 Die klassischen Regeln und die Gesetze
- Mit Prämissen die Einführung und die Elimination der Disjunktion und der Konjunktion, das Tertium non datur und den Satz vom Widerspruch beweisen.
- Das Ex falso quodlibet, die Reductio ad absurdum und die Fallunterscheidung mit Prämissen beweisen und erklären, warum sie ohne Prämissen nicht genügen.
- Die De-Morgan-Gesetze, ihre Varianten und die Distributivgesetze in ihren beiden Richtungen durch Ableitung beweisen.
- Formeln mit Ketten begründeter Äquivalenzen in einfache Normalformen umformen.
1. Regeln der Junktoren. Mit jedem $\Gamma$ : Aus $\varphi$ folgt $(\varphi \vee \psi)$ ; aus $(\varphi \vee \psi)$ und $\neg\varphi$ folgt $\psi$ ; aus $\varphi$ und $\psi$ folgt $(\varphi \wedge \psi)$ ; aus $(\varphi \wedge \psi)$ folgen $\varphi$ und $\psi$ ; außerdem $\vdash (\varphi \vee \neg\varphi)$ und $\vdash \neg(\varphi \wedge \neg\varphi)$ .
  Verwendet: 1. System, Ableitung und Identität, 2. Strukturelle Eigenschaften, 6. Hypothetischer Syllogismus und Vertauschung, 10. Kontraposition, 13. Äquivalente Formen, 14. Die fünf Symmetrien. Stützt sich auf: C (Axiome von Łukasiewicz), E (Deduktionstheorem), F (Vom Ergebnis zur Regel), G (Doppelte Negation). Bewiesen in: Die Techniken der klassischen Logik.
2. Ex falso quodlibet und Reductio ad absurdum. Wenn $\Gamma \vdash \varphi$ und $\Gamma \vdash \neg\varphi$ , dann $\Gamma \vdash \psi$ für jede $\psi$ ; wenn $\Gamma \cup \{\neg\varphi\}$ sowohl $\psi$ als auch $\neg\psi$ ableitet, dann $\Gamma \vdash \varphi$ ; und wenn $\Gamma \cup \{\varphi\}$ beide ableitet, $\Gamma \vdash \neg\varphi$ .
  Verwendet: 1. System, Ableitung und Identität, 2. Strukturelle Eigenschaften, 15. Regeln der Junktoren. Stützt sich auf: C (Axiome von Łukasiewicz), E (Deduktionstheorem), G (Doppelte Negation). Bewiesen in: Die Techniken der klassischen Logik.
3. Fallunterscheidung. Wenn $\Gamma \cup \{\varphi\} \vdash \psi$ und $\Gamma \cup \{\neg\varphi\} \vdash \psi$ , dann $\Gamma \vdash \psi$ ; und wenn $\Gamma \cup \{\varphi\} \vdash \chi$ , $\Gamma \cup \{\psi\} \vdash \chi$ und $\Gamma \vdash (\varphi \vee \psi)$ , dann $\Gamma \vdash \chi$ .
  Verwendet: 2. Strukturelle Eigenschaften, 10. Kontraposition, 15. Regeln der Junktoren, 16. Ex falso quodlibet und Reductio ad absurdum. Stützt sich auf: E (Deduktionstheorem). Bewiesen in: Die Techniken der klassischen Logik.
4. De-Morgan-Gesetze. $\neg(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \vee \neg\psi)$ , durch die Definition und die doppelte Negation; $\neg(\varphi \vee \psi) \dashv\vdash (\neg\varphi \wedge \neg\psi)$ , mit einer Anwendung der Regel EDN in jedem Argument des Peirce-Pfeils; daher $(\varphi \downarrow \psi) \dashv\vdash (\neg\varphi \wedge \neg\psi)$ und $\neg(\varphi \rightarrow \psi) \dashv\vdash (\varphi \wedge \neg\psi)$ .
  Stützt sich auf: D (Ersetzung der doppelten Negation), G (Doppelte Negation), H (Ersetzung äquivalenter Formeln). Bewiesen in: De-Morgan-Gesetze und Distributivgesetze.
5. Distributivgesetze. $(\varphi \wedge (\psi \vee \chi)) \dashv\vdash ((\varphi \wedge \psi) \vee (\varphi \wedge \chi))$ und $(\varphi \vee (\psi \wedge \chi)) \dashv\vdash ((\varphi \vee \psi) \wedge (\varphi \vee \chi))$ , jedes in seinen beiden Richtungen durch Fallunterscheidung; mit den Symmetrien auch von rechts.
  Verwendet: 14. Die fünf Symmetrien, 15. Regeln der Junktoren, 17. Fallunterscheidung. Stützt sich auf: H (Ersetzung äquivalenter Formeln). Bewiesen in: De-Morgan-Gesetze und Distributivgesetze.

Auf dem Weg zur Semantik. Die Kette hält dort an, wo die Ableitung alle Techniken erreicht, mit denen die Mathematik argumentiert. Es bleibt zu klären, ob das Ableitbare genau das ist, was unter jeder Belegung wahr ist: Die nächste Einheit wird die Wahrheit definieren, und die letzte wird beide Begriffe vergleichen.

Die Abkürzungen der Begründungen

Die Ableitungen der Einheit begründen jede Zeile mit einer Abkürzung, die in allen Lektionen dieselbe ist. Sie sind hier zusammengestellt, geordnet nach der Lektion, die sie einführt. „Prämisse“ bezeichnet eine Voraussetzung der Aufgabenstellung und in den Ableitungen über Ableitungen eine Voraussetzung der Regel, die bewiesen wird. Die Zahlen in Klammern geben die Zeilen an, auf die die Regel angewandt wird; eine bereits bewiesene Äquivalenz wird ohne Zahl angeführt, wenn sie als Zeile geschrieben wird, und mit der Nummer der Zeile, die sie umformt, wenn sie auf diese Zeile angewandt wird, auch auf einen ihrer Teile mit „Ers“.

Erste Lektion: A1, A2 und A3 (die Axiomenschemata); MP $(i, j)$ (Modus ponens); Def (Auflösen oder Einführen einer Abkürzung, mit dem Junktor, der aufgelöst wird: „Def $\vee$ “, „Def $\dashv\vdash$ “); Id (Identität, das Theorem $\vdash (\varphi \rightarrow \varphi)$ ); Refl (Reflexivität: wenn $\varphi \in \Gamma$ , dann $\Gamma \vdash \varphi$ ); Mon (Monotonie); Schnitt (Abgeleitetes darf als Prämisse verwendet werden); Fin (Endlichkeit); DT (Deduktionstheorem) und UDT (seine Umkehrung).
Zweite Lektion: HS (hypothetischer Syllogismus); VP (Vertauschung der Prämissen); DN (doppelte Negation); EDN $(i)$ (Ersetzung der doppelten Negation in der Zeile $i$ ; EDN ohne Zahl führt die Äquivalenz zwischen einer Formel und derjenigen an, die aus ihr durch die Regel entsteht); KP (Kontraposition, in jeder ihrer drei Formen); „Gelöste Aufgabe $n$ “ (ein Ergebnis der gelösten Aufgabe $n$ derselben Lektion, als Zeile geschrieben).
Dritte Lektion: FL (Fundamentallemma, $(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi)$ ); Ers (Ersetzung äquivalenter Formeln, in jeder ihrer Formen, gefolgt von der angewandten Äquivalenz: „Ers, DM $(i)$ “); Äq (äquivalente Formen der Disjunktion und der Konjunktion, $(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi)$ und $(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \downarrow \neg\psi)$ ); Sym (Symmetrie eines Junktors).
Vierte Lektion: $\vee$ I und $\vee$ E (Einführung und Elimination der Disjunktion); $\wedge$ I und $\wedge$ E (Einführung und Elimination der Konjunktion); TND (Tertium non datur); SW (Satz vom Widerspruch; die Abkürzung benennt den Satz, begründet aber keine Zeile der Einheit); EFQ (Ex falso quodlibet); FU $(i, j)$ und FU $(i, j, k)$ (Fallunterscheidung, mit einer Formel und ihrer Negation oder mit einer Disjunktion); „FU ohne Prämissen“ (die Fallunterscheidung ohne Menge $\Gamma$ , die nur in einer Aufgabe vorkommt); RAA (Reductio ad absurdum, in ihren beiden Formen).
Fünfte Lektion: DM (De-Morgan-Gesetze); Dist (Distributivität); Assoz (Assoziativität der Disjunktion); Instanz $(i)$ (die Zeile $i$ , die für beliebige Formeln gilt, erneut geschrieben mit anderen Formeln an der Stelle ihrer Metavariablen; die Substitution wird angegeben).
Herausforderungen dieser Lektion: M3 (das Schema, das die dritte Herausforderung an die Stelle von A3 setzt).