Vier Ableitungstechniken

Die Ausgangswerkzeuge

In der Lektion über formale Deduktionssysteme wurde der Łukasiewicz-Kalkül festgelegt. Seine Sprache ist die Sprache der Kreise und Scheiben, geschrieben mit den offiziellen Abkürzungen der Lektion über die Sprache der Aussagenlogik; seine Axiome sind alle Instanzen der folgenden drei Schemata, wobei $\varphi$, $\psi$ und $\chi$ beliebige Formeln sind, und seine einzige Regel ist der Modus ponens.

• A1: $(\varphi \rightarrow (\psi \rightarrow \varphi))$.
• A2: $((\varphi \rightarrow (\psi \rightarrow \chi)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \chi)))$.
• A3: $((\neg\psi \rightarrow \neg\varphi) \rightarrow (\varphi \rightarrow \psi))$.
• MP: Aus $\varphi$ und $(\varphi \rightarrow \psi)$ wird $\psi$ abgeleitet.

Eine Ableitung von $\varphi$ aus einer Menge $\Gamma$ von Formeln ist eine endliche Folge von Formeln, die mit $\varphi$ endet und in der jede Formel ein Axiom, ein Element von $\Gamma$ oder das Ergebnis der Anwendung des Modus ponens auf zwei frühere Formeln ist; gibt es eine, so schreibt man $\Gamma \vdash \varphi$, und wenn $\Gamma$ leer ist, $\vdash \varphi$, und man sagt, $\varphi$ sei ein Theorem. In derselben Lektion wurden die Metatheoreme bewiesen, die wir hier verwenden: die Reflexivität (Refl: Wenn $\varphi \in \Gamma$, dann $\Gamma \vdash \varphi$), die Monotonie (Mon: Wenn $\Gamma \subseteq \Delta$ und $\Gamma \vdash \varphi$, dann $\Delta \vdash \varphi$), der Modus ponens zwischen Ableitungen (wenn $\Gamma \vdash \varphi$ und $\Gamma \vdash (\varphi \rightarrow \psi)$, dann $\Gamma \vdash \psi$), der Schnitt (Schnitt: Wenn $\Gamma \vdash \varphi_{i}$ für jedes $i$ von $1$ bis $n$ und $\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{n}\} \vdash \psi$, dann $\Gamma \vdash \psi$), die Endlichkeit (wenn $\Gamma \vdash \varphi$, genügt eine endliche Teilmenge von $\Gamma$), das Deduktionstheorem (DT: Wenn $\Gamma \cup \{\varphi\} \vdash \psi$, dann $\Gamma \vdash (\varphi \rightarrow \psi)$) und seine Umkehrung (UDT) sowie das Theorem $\vdash (\varphi \rightarrow \varphi)$, das wir in den Begründungen mit Id abkürzen. Schließlich bedeutet $\varphi \dashv\vdash \psi$ (beweisbare Äquivalenz), dass $\{\varphi\} \vdash \psi$ und $\{\psi\} \vdash \varphi$.

Es sei daran erinnert, dass $\neg$ und $\rightarrow$ keine Zeichen der Grundsprache sind, sondern Abkürzungen: $\neg\varphi$ ist die Zeichenkette $(\varphi \downarrow \varphi)$, und $(\varphi \rightarrow \psi)$ ist $(\neg\varphi \vee \psi)$, das heißt $\neg(\neg\varphi \downarrow \psi)$. Die drei Axiome sprechen nur von Negationen und Implikationen, und dieselbe Lektion hat mit einer Markierung durch $0$ und $1$, die sie und der Modus ponens erhalten, die Grenze gezeigt, die daraus folgt: Im Łukasiewicz-Kalkül ist aus $(v_{1} \downarrow v_{2})$ nicht $(\neg\neg v_{1} \downarrow v_{2})$ ableitbar, und der Peirce-Pfeil bleibt zum Teil außerhalb seiner Reichweite. Diese Lektion geht daher in zwei Schritten vor. Bis einschließlich zur doppelten Negation bezieht sich $\vdash$ auf den Łukasiewicz-Kalkül, und nichts von dem, was bewiesen wird, hängt davon ab, die Abkürzungen aufzulösen. Nachdem die doppelte Negation bewiesen ist, wird dem Kalkül eine zweite primitive Regel hinzugefügt, die Ersetzung der doppelten Negation, die auf der aufgelösten Zeichenkette wirkt; von da an bezieht sich $\vdash$ auf den Kalkül des Kurses, den Łukasiewicz-Kalkül zusammen mit dieser Regel. Da jede Ableitung des ersten auch eine Ableitung des zweiten ist, geht nichts von dem zuvor Bewiesenen verloren.

Zwei Stile der Ableitung

Es gibt zwei Arten, eine Ableitung zu schreiben, und beide werden verwendet. Die erste ist die eigentliche Ableitung, eine Folge von Formeln, in der jede Zeile ein Axiom, eine Prämisse oder das Ergebnis des Modus ponens ist; jede Zeile wird mit A1, A2, A3, Prämisse oder MP$(i, j)$ begründet, wobei die Zeile $i$ das Antezedens ist und die Zeile $j$ die Implikation, deren Antezedens genau die Zeile $i$ ist (und, sobald die neue Regel eingeführt ist, EDN$(i)$). Die zweite ist die Ableitung über Ableitungen, deren Zeilen keine Formeln sind, sondern Aussagen der Form $\Gamma \vdash \varphi$; jede wird mit einem bereits bewiesenen Metatheorem begründet, und die ganze Folge ist ein Schluss in der Metasprache, der garantiert, dass eine Ableitung des ersten Stils existiert, auch wenn er sie nicht hinschreibt. Die Begründungen dieses zweiten Stils sind wie folgt zu lesen.

• Refl: Die Formel rechts gehört zur Menge links.
• A1, A2, A3: Die Formel rechts ist eine Instanz des Schemas; eine Instanz eines Axioms wird aus jedem $\Gamma$ mit einer Ableitung von einer einzigen Zeile abgeleitet.
• MP$(i, j)$: der Modus ponens zwischen Ableitungen, angewandt auf die Zeile $i$, $\Gamma \vdash \varphi$, und auf die Zeile $j$, $\Gamma \vdash (\varphi \rightarrow \psi)$, mit demselben $\Gamma$.
• DT$(i)$ und UDT$(i)$: das Deduktionstheorem oder seine Umkehrung, angewandt auf die Zeile $i$.
• Der Name eines bereits bewiesenen Theorems, etwa Id oder DN: Die Formel rechts ist eine Instanz dieses Theorems und wird aus jedem $\Gamma$ durch Monotonie abgeleitet, weil die leere Menge in $\Gamma$ enthalten ist.
• Prämisse, in einer Ableitung über Ableitungen: Die Zeile ist eine der Voraussetzungen der Regel, die gerade bewiesen wird.

Jedes Ergebnis dieser Lektion wird mit Metavariablen formuliert und gilt daher für beliebige Formeln: Sein Beweis ist ein Schema, und substituiert man darin jede Metavariable durch eine Formel, so erhält man einen anderen Beweis, weil die Instanzen eines Axiomenschemas Instanzen bleiben und jeder Modus ponens ein Modus ponens bleibt (dasselbe wird für jede Anwendung der neuen Regel gelten). So folgt aus $\vdash (\varphi \rightarrow \varphi)$ die Aussage $\vdash (\neg\psi \rightarrow \neg\psi)$, mit $\neg\psi$ an Stelle von $\varphi$. Dieses Mittel, ein Ergebnis auf eine komplexere Formel als die der Aussage anzuwenden, ist dasjenige, das im Folgenden am meisten einbringt.

Vom Ergebnis zur Regel

Die Techniken dieser Lektion werden aus festen Prämissen bewiesen, etwa $\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi)$; verwendet werden sie aber mitten in Ableitungen mit anderen Prämissen, in denen $(\varphi \rightarrow \psi)$ und $(\psi \rightarrow \chi)$ keine Prämissen sind, sondern bereits abgeleitete Formeln. Das folgende Lemma, eine direkte Folge der Monotonie und des Schnitts, erlaubt diesen Gebrauch ein für alle Mal.

Daraus folgt, dass jede aus Prämissen bewiesene Technik drei Gestalten hat: das Ergebnis selbst, das Theorem, das man durch Entladen seiner Prämissen erhält, und die Regel, die unter jedem $\Gamma$ angewandt wird. In einer Ableitung über Ableitungen wird die Regel mit dem Namen der Technik und den Nummern der Zeilen aufgerufen, auf die sie angewandt wird, etwa HS$(3, 4)$, und das Lemma garantiert, dass der Schritt legitim ist.