Die Techniken der klassischen Logik

Die Regeln innerhalb eines Kontexts

In der Lektion über formale Deduktionssysteme wurde der Łukasiewicz-Kalkül festgelegt: die Axiomenschemata A1, A2 und A3, die Regel des Modus ponens (MP) und der Begriff der Ableitung aus einer Menge $\Gamma$ von Prämissen, mit ihren ersten Eigenschaften: der Reflexivität (Refl: Wenn $\varphi \in \Gamma$, dann $\Gamma \vdash \varphi$), der Monotonie (Mon: Wenn $\Gamma \subseteq \Delta$ und $\Gamma \vdash \varphi$, dann $\Delta \vdash \varphi$), dem Schnitt (Schnitt), dem Modus ponens zwischen Ableitungen (wenn $\Gamma \vdash \varphi$ und $\Gamma \vdash (\varphi \rightarrow \psi)$, dann $\Gamma \vdash \psi$, der ebenfalls als MP zitiert wird), dem Deduktionstheorem (DT: Wenn $\Gamma \cup \{\varphi\} \vdash \psi$, dann $\Gamma \vdash (\varphi \rightarrow \psi)$) und seiner Umkehrung (UDT). Die Lektionen über die vier Ableitungstechniken und über die Symmetrien der Junktoren fügten den hypothetischen Syllogismus (HS), die Vertauschung der Prämissen (VP), die doppelte Negation (DN), die Kontraposition (KP) in ihren drei Formen, die Ersetzung äquivalenter Formeln (Ers), die Symmetrien (Sym) und die äquivalenten Formen der Disjunktion und der Konjunktion hinzu. Die erste dieser Lektionen vervollständigte, nachdem sie die doppelte Negation bewiesen hatte, den Kalkül des Kurses außerdem um eine zweite primitive Regel, die Ersetzung der doppelten Negation (EDN): Entsteht $\chi'$ aus $\chi$, indem man ein Vorkommen einer Teilformel $\theta$ durch $\neg\neg\theta$ oder eines von $\neg\neg\theta$ durch $\theta$ ersetzt, so wird aus $\chi$ auf $\chi'$ geschlossen. Von nun an bezieht sich $\vdash$ auf diesen Kalkül (A1 bis A3, MP und EDN), in dem die Reflexivität, die Monotonie, der Schnitt, das Deduktionstheorem und seine Umkehrung weiterhin gelten; die Techniken dieser Lektion sind abgeleitete Regeln dieses Kalküls, obwohl keiner ihrer Beweise EDN unmittelbar heranzieht: Die Regel wirkt über die äquivalenten Formen und die Ersetzung äquivalenter Formeln, die die Lektion über die Symmetrien mit ihr bewiesen hat.

Nun schließt in der Mathematik niemand ohne Prämissen: Man schließt aus gewissen Axiomen, aus den Voraussetzungen eines Satzes und aus dem, was man angenommen hat, um einen Fall zu erörtern. Wenn dem so ist, ist eine Schlusstechnik nur dann nützlich, wenn sie mit einer Menge $\Gamma$ von Prämissen formuliert wird, die von Zeile zu Zeile mitgeführt wird. Daraus folgt, dass jede Regel dieser Lektion für ein beliebiges $\Gamma$ formuliert und bewiesen wird; der Fall ohne Prämissen ist der Spezialfall $\Gamma = \emptyset$, und nicht umgekehrt.

Die Beweise sind Ableitungen über Ableitungen: Jede Zeile behauptet eine Ableitbarkeit aus einer Menge, $\Gamma \vdash \varphi$, und ihre Begründung verweist auf frühere Zeilen. Darin kennzeichnet „Prämisse“ die Zeilen, die die Formulierung der Regel als gegeben voraussetzt, und der Name eines Axioms (A1, A3) oder eines bereits bewiesenen Theorems (wie Id, das Theorem $\vdash (\varphi \rightarrow \varphi)$) kennzeichnet eine Zeile $\Gamma \vdash \varphi$, in der $\varphi$ eine Instanz dieses Schemas oder dieses Theorems ist, ableitbar aus jeder beliebigen Menge.

Die Lektion über vier Ableitungstechniken bewies mit der Monotonie und dem Schnitt das Lemma „vom Ergebnis zur Regel“, das diese Arbeitsweise möglich macht: Wenn $\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta$ und $\Gamma \vdash \alpha_{i}$ für jedes $i$, dann $\Gamma \vdash \beta$. Mit $n = 1$, in jeder Richtung einer Äquivalenz $\alpha \dashv\vdash \alpha'$ angewandt, besagt es, dass $\Gamma \vdash \alpha$ genau dann gilt, wenn $\Gamma \vdash \alpha'$ gilt. Folglich lassen sich jede bereits bewiesene Regel und jede bereits bewiesene Äquivalenz auf die Zeilen einer Ableitung mit Prämissen anwenden: Lautet eine Zeile $\Gamma \vdash (\varphi \rightarrow \psi)$, so erlaubt die Kontraposition, darunter $\Gamma \vdash (\neg\psi \rightarrow \neg\varphi)$ zu schreiben und dies mit „KP“ und der Nummer der Zeile zu begründen. Für die beiden äquivalenten Formen aus der Lektion über die Symmetrien, die unablässig verwendet werden, schreibt man „Äq“:

Es ist zu betonen, dass die erste dieser Äquivalenzen keine Definition ist; die zweite ist, wie die Lektion über die Symmetrien gezeigt hat, eine Identität von Zeichenketten, wird aber zusammen mit der ersten als Äq zitiert. Nach Definition ist $(\varphi \vee \psi)$ die Zeichenkette $\neg(\varphi \downarrow \psi)$ und $(\neg\varphi \rightarrow \psi)$ die Zeichenkette $(\neg\neg\varphi \vee \psi)$, und das sind verschiedene Zeichenketten; die eine „nach Definition der Implikation“ als die andere zu lesen ist der Fehler, den diese Lektion vermeidet. „Def“ dagegen bleibt dem Fall vorbehalten, dass man dieselbe Zeichenkette unter einem anderen Namen schreibt, etwa wenn man $(\varphi \rightarrow \psi)$ als $(\neg\varphi \vee \psi)$ liest.