Zum Inhalt springen
Topos Uranos
Deutsch

Formale Deduktionssysteme

Zusammenfassung

Diese Lektion macht aus der Sprache der vorigen Einheit ein Instrument zum Beweisen. Sie definiert, was ein formales Deduktionssystem ist (eine Sprache, einige Axiomenschemata und einige Schlussregeln), und stellt das erste der beiden vor, mit denen der Kurs arbeitet, den Łukasiewicz-Kalkül: drei Axiomenschemata und den Modus ponens als einzige Regel. Sie definiert genau die Ableitung aus einer Prämissenmenge, das Theorem und die Relation Γ⊢φ\Gamma \vdash \varphi, leitet ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi) in fünf Zeilen ab und beweist die strukturellen Eigenschaften der Ableitbarkeit: Reflexivität, Monotonie, Modus ponens zwischen Ableitungen, Schnitt und Endlichkeit. Danach beweist sie durch starke Induktion über die Anzahl der Zeilen das Deduktionstheorem und seine Umkehrung, die es erlauben, mit Ableitungen über Ableitungen zu argumentieren, und definiert die beweisbare Äquivalenz. Schließlich zeigt sie, ohne auf Wahrheitswerte zurückzugreifen, die Grenze dieses Kalküls in einer Sprache, deren einziger Junktor der Peirce-Pfeil ist: Eine Markierung mit den Werten 00 und 11, berechnet durch Rekursion über Formeln, die die Axiome von Łukasiewicz und der Modus ponens erhalten, beweist, dass gewisse Formeln, die ableitbar sein sollten, nicht ableitbar sind, und dass man nicht einmal von (v1↓v2)(v_{1} \downarrow v_{2}) zu (¬¬v1↓v2)(\neg\neg v_{1} \downarrow v_{2}) gelangt. Daraus folgt die Notwendigkeit einer zweiten Regel, der Ersetzung der doppelten Negation, mit der die nächste Lektion den Kalkül vervollständigt.

Lernziele

  1. Die Instanzen der Schemata A1, A2 und A3 erkennen und entscheiden, ob eine Folge von Formeln eine Ableitung aus einer Prämissenmenge ist.
  2. Ableitungen im Łukasiewicz-Kalkül mit Axiomen, Prämissen und Modus ponens konstruieren, und Ableitungen über Ableitungen mit Reflexivität, Monotonie, Schnitt, dem Deduktionstheorem und seiner Umkehrung.
  3. Die strukturellen Eigenschaften der Ableitbarkeit und das Deduktionstheorem durch starke Induktion über die Anzahl der Zeilen beweisen.
  4. Beweisbare Äquivalenzen herleiten und verwenden, dass die beweisbare Äquivalenz reflexiv, symmetrisch und transitiv ist.
  5. Beweisen, dass eine Formel nicht ableitbar ist, mittels einer Markierung, die die Axiome und der Modus ponens erhalten, und mit ihr die Grenze des Łukasiewicz-Kalküls in der Sprache mit einem einzigen Junktor erklären sowie den Grund, weshalb eine zweite Regel nötig ist.

Was ein formales Deduktionssystem ist

Die vorige Einheit hat eine Sprache aufgebaut: Sie hat entschieden, welche Zeichenketten aus Kreisen und Scheiben Formeln sind, und nichts weiter. Nun behauptet und beweist eine Sprache für sich allein nichts; zum Beweisen braucht man außerdem einen Ausgangspunkt und eine Weise des Fortschreitens. Ein formales Deduktionssystem besteht daher aus drei Bestandteilen: einer formalen Sprache, die die Formeln festlegt; einer Menge von Axiomen, Formeln, die ohne Beweis zugelassen werden; und einer Menge von Schlussregeln, die angeben, welche Formel auf der Grundlage anderer, schon geschriebener Formeln geschrieben werden darf. Entscheidend ist, dass alle drei Dinge rein syntaktisch sind: Um zu prüfen, dass eine Formel ein Axiom ist oder dass eine Regel richtig angewandt wurde, genügt es, die Zeichenketten anzusehen, ohne zu fragen, was sie bedeuten. Wenn dem so ist, kann ein Beweis in einem formalen System mechanisch geprüft werden, Zeichen für Zeichen, und in dieser Möglichkeit liegt sein ganzer Wert.

Es ist von Anfang an festzuhalten, dass ein Axiom hier keine „aus sich selbst einleuchtende Wahrheit“ ist, wie im alten Gebrauch des Wortes, sondern eine als Ausgangspunkt gewählte Formel. Ob die Wahl gut ist (ob die Axiome in einem Sinn wahr sind, den die Semantik präzisieren wird, und ob sie genügen, um alles abzuleiten, was ableitbar sein soll), ist eine Frage über das System, die mit Sätzen über es beantwortet wird und nicht mit der Intuition: Die Einheit über die Metatheorie beantwortet sie, und der letzte Abschnitt dieser Lektion zeigt, dass die Frage nicht müßig ist.

Axiomenschemata und Instanzen

Die Systeme der Aussagenlogik geben ihre Axiome nicht einzeln an, weil es unendlich viele sind, sondern mittels Schemata: Ausdrücken der Metasprache, die mit Metavariablen geschrieben sind, wie (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi)). Ein Schema ist keine Formel; es ist eine Schablone. Eine Instanz des Schemas ist die Formel, die entsteht, wenn man jede Metavariable uniform durch eine Formel substituiert: Alle Vorkommen derselben Metavariablen werden durch dieselbe Formel substituiert, wobei verschiedene Metavariablen dieselbe Formel oder verschiedene Formeln erhalten dürfen.

BeispielInstanzen eines Schemas

Mit φ:=v1\varphi := v_{1} und ψ:=¬v2\psi := \neg v_{2} liefert das Schema (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi)) die Instanz (v1→(¬v2→v1))(v_{1} \rightarrow (\neg v_{2} \rightarrow v_{1})); mit φ:=(v1↓v2)\varphi := (v_{1} \downarrow v_{2}) und ψ:=(v1↓v2)\psi := (v_{1} \downarrow v_{2}) liefert es ((v1↓v2)→((v1↓v2)→(v1↓v2)))((v_{1} \downarrow v_{2}) \rightarrow ((v_{1} \downarrow v_{2}) \rightarrow (v_{1} \downarrow v_{2}))), denn nichts hindert zwei Metavariablen daran, dieselbe Formel zu erhalten. Dagegen ist (v1→(v2→v3))(v_{1} \rightarrow (v_{2} \rightarrow v_{3})) keine Instanz dieses Schemas: Das erste und das letzte Vorkommen von φ\varphi erhielten verschiedene Formeln, und die Substitution wäre nicht uniform. Jede Instanz ist, sobald die Abkürzungen aufgelöst sind, eine Zeichenkette aus Kreisen und Scheiben; das Schema dagegen lebt nur in der Metasprache.