Die Symmetrien der Junktoren

Was verwendet wird und was zu beweisen ist

Die Lektion über formale Deduktionssysteme hat den Łukasiewicz-Kalkül festgelegt: die Axiome A1, A2 und A3 und den Modus ponens. Sie hat außerdem die Reflexivität (Refl: Wenn $\varphi \in \Gamma$, dann $\Gamma \vdash \varphi$), die Monotonie (Mon), den Schnitt (Schnitt: Wenn $\Gamma \vdash \varphi_{i}$ für jedes $i$ und $\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{n}\} \vdash \psi$, dann $\Gamma \vdash \psi$), das Deduktionstheorem (DT) und seine Umkehrung (UDT) sowie die beweisbare Äquivalenz $\varphi \dashv\vdash \psi$ bereitgestellt, die bedeutet, dass $\{\varphi\} \vdash \psi$ und $\{\psi\} \vdash \varphi$; und sie hat mit einer Markierung, die die Axiome und der Modus ponens erhalten, gezeigt, dass dieser Kalkül gewisse Formeln über den Peirce-Pfeil nicht ableitet. Die Lektion über die vier Ableitungstechniken hat den hypothetischen Syllogismus (HS: $\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi)$), die Vertauschung der Prämissen (VP), die doppelte Negation (DN: $\varphi \dashv\vdash \neg\neg\varphi$, mit ihren beiden Theoremen $\vdash (\neg\neg\varphi \rightarrow \varphi)$ und $\vdash (\varphi \rightarrow \neg\neg\varphi)$) und die Kontraposition (KP) in ihren drei Formen hinzugefügt:

Nachdem die doppelte Negation bewiesen war, hat dieselbe Lektion den Kalkül des Kurses um eine zweite primitive Regel ergänzt, die Ersetzung der doppelten Negation (EDN): Entsteht $\chi'$ aus $\chi$, indem man ein Vorkommen einer Teilformel $\theta$ durch $\neg\neg\theta$ oder ein Vorkommen einer Teilformel $\neg\neg\theta$ durch $\theta$ ersetzt, dann wird aus $\chi$ auf $\chi'$ geschlossen. Die so aus der Zeile $i$ gewonnene Zeile wird mit EDN$(i)$ begründet. Von da an bezieht sich $\vdash$ auf den Kalkül des Kurses (A1 bis A3, der Modus ponens und EDN), in dem Refl, Mon, Schnitt, DT und UDT weiterhin gelten. Die Regel wirkt auf die Zeichenkette der Grundsprache, sodass sie auch die Vorkommen erreicht, die eine Abkürzung verbirgt, und zwar in jedem der beiden Argumente eines Peirce-Pfeils; zu ihren unmittelbaren Folgerungen gehören

und allgemein $\chi \dashv\vdash \chi'$, sooft $\chi'$ aus $\chi$ durch EDN entsteht. Eine Äquivalenzzeile dieser Form wird mit „EDN“ begründet, ohne Zeilennummer, so wie eine Zeile „DN“ oder „KP“ eine bereits bewiesene Äquivalenz anführt. Wie dort kann ein bereits bewiesenes Theorem als Zeile einer Ableitung geschrieben werden, weil sich seine eigene Ableitung an dieser Stelle einfügen lässt; und nach dem Lemma „Vom Ergebnis zur Regel“ jener Lektion wird jede Technik auch als Regel unter einer beliebigen Prämissenmenge $\Gamma$ angewandt und mit den Nummern der Zeilen angeführt, auf die sie angewandt wird, wie KP$(i)$ oder HS$(i, j)$. In Ableitungen über Ableitungen bezeichnet „Prämisse“ eine Voraussetzung der Regel, die bewiesen wird.

Die offiziellen Abkürzungen, festgelegt in der Lektion über die Sprache der Aussagenlogik, sind die einzigen Definitionen der Junktoren:

Eine mit „Def“ begründete Zeile leitet nichts ab: Sie schreibt dieselbe Formel unter einem anderen Namen, und die Anmerkung sagt, welche Abkürzung aufgelöst oder eingeführt wird („Def $\rightarrow$“, „Def $\vee$“). Es lohnt sich, an das Phänomen zu erinnern, das in der Lektion über die Formalisierung der natürlichen Sprache beobachtet wurde: Ein und dieselbe Formel lässt mehrere Namen zu, sodass eine Konjunktion als Zeichenkette auch eine Disjunktion ist. Löst man zum Beispiel die Implikation mit $\neg\varphi$ an der Stelle von $\varphi$ auf, so erhält man

und die doppelte Negation, die vor $\varphi$ erscheint und von der Abkürzung verborgen wird, ist der Grund, weshalb die Regel EDN in allem Folgenden eingreifen wird.

Die beweisbare Äquivalenz als Gleichheit

Die Beweise dieser Lektion sind fast alle Ketten von Äquivalenzen: $\varphi_{1} \dashv\vdash \varphi_{2}$, $\varphi_{2} \dashv\vdash \varphi_{3}$ und so fort. Damit man aus einer Kette auf $\varphi_{1} \dashv\vdash \varphi_{n}$ schließen kann, muss sich die beweisbare Äquivalenz wie eine Gleichheit verhalten, und genau das hat die Proposition über die Eigenschaften der beweisbaren Äquivalenz in der Lektion über formale Deduktionssysteme festgestellt: Die Relation ist reflexiv ($\varphi \dashv\vdash \varphi$), symmetrisch (wenn $\varphi \dashv\vdash \psi$, dann $\psi \dashv\vdash \varphi$) und transitiv (wenn $\varphi \dashv\vdash \psi$ und $\psi \dashv\vdash \chi$, dann $\varphi \dashv\vdash \chi$), und zwei beweisbar äquivalente Formeln sind als Konklusionen austauschbar (wenn $\Gamma \vdash \varphi$ und $\varphi \dashv\vdash \varphi'$, dann $\Gamma \vdash \varphi'$, für jede Formelmenge $\Gamma$). Es lohnt sich, daran zu erinnern, wie die beiden letzten bewiesen wurden, denn die ganze Lektion ruht auf ihnen: Von $\{\varphi\} \vdash \varphi'$ gelangt man durch Monotonie zu $\Gamma \cup \{\varphi\} \vdash \varphi'$, und von dieser und von $\Gamma \vdash \varphi$ durch Schnitt zu $\Gamma \vdash \varphi'$; die Transitivität ergibt sich, indem man dies mit $\Gamma = \{\varphi\}$ in der einen Richtung und mit $\Gamma = \{\chi\}$ in der anderen anwendet.

Von nun an wird der Schritt, der eine Kette von Äquivalenzen zu einer einzigen zusammenfasst, mit „Schnitt“ begründet, dem Instrument jener Proposition. Nun enthält jedes Glied $\varphi_{i} \dashv\vdash \varphi_{i+1}$ die beiden Ableitungen, die Hin- und die Rückrichtung; also beweist eine Kette von Äquivalenzen zugleich beide Richtungen ihrer Konklusion, und nichts bleibt „als Übung“.