Hilbert-Kalkül

Hilbertkalküle sind axiomatische Kalküle für die klassische Aussagenlogik oder die Prädikatenlogik erster Stufe, das heißt Kalküle, in denen sich Theoreme und Argumente der Aussagenlogik oder der Prädikatenlogik erster Stufe herleiten lassen. Die beiden Hauptmerkmale von Hilbertkalkülen sind das Vorhandensein etlicher Axiome oder Axiomenschemata sowie die geringe Anzahl von Schlussregeln – im Fall der Angabe von Axiomenschemata oft nur einer einzigen Regel, des Modus ponendo ponens, und im Fall der Angabe von Axiomen zusätzlich einer Substitutionsregel.

Die Bezeichnung „Hilbertkalkül“ geht auf den Mathematiker David Hilbert zurück, der die als Hilbertprogramm bekannt gewordene und später durch den Gödelschen Unvollständigkeitssatz als unlösbar erwiesene Forderung aufstellte, die gesamte Mathematik und Logik auf ein gemeinsames einheitliches und vollständiges Axiomensystem aufzubauen. In einem engeren Sinn werden gelegentlich nur von Hilbert selbst angegebene Kalküle als Hilbertkalküle bezeichnet, insbesondere der gemeinsam mit Paul Bernays 1934 im Werk „Grundlagen der Mathematik“ angegebene axiomatische aussagenlogische Kalkül.

Da die Arbeiten von Hilbert wiederum auf der Begriffsschrift von Gottlob Frege basieren, werden diese Kalküle gelegentlich auch als „Frege-Kalküle“ bezeichnet.

Ein Hilbertkalkül für die klassische Aussagenlogik

Syntax

Neben den Aussagenvariabeln und logischen Konstanten der Objektebene enthält der hier dargestellte Kalkül das metasprachliche Zeichen $\vdash$, wobei $A\vdash B$ gelesen wird als „$B$ ist aus $A$ herleitbar“.

In einem Hilbertkalkül wird im Wesentlichen mit Hilfe von drei elementaren Operationen Beweis geführt. Handlung (1) ist das Erstellen einer Instanz eines Axiomenschemas. Handlung (2) ist das Aufstellen einer Hypothese, und Handlung (3) ist das Verwenden des Modus ponens.

Axiome

Zu Handlung (1): Ein Hilbertkalkül benutzt als Axiomenschemata aussagenlogische Tautologien, also Formeln, die unter jeder Zuordnung von Wahrheitswerten zu den in ihnen vorkommenden Satzvariablen den Wert „wahr“ annehmen. Eine derartige Tautologie ist zum Beispiel die Aussage $A\rightarrow (B\rightarrow A)$, die in vielen Hilbertkalkülen als Axiom oder als Axiomenschema verwendet wird. Verwendet man sie als Axiomenschema, dann fungieren A und B darin als Platzhalter, die gegen jede andere beliebige atomare Formel ausgetauscht werden können; verwendet man sie als Axiom, dann benötigt man zusätzlich eine Schlussregel, die es erlaubt, die Satzvariablen A und B durch andere Formeln zu ersetzen, also eine Substitutionsregel.

Hypothese

Zu Handlung (2): Als Aufstellen einer Hypothese bezeichnet man die Handlung, die aus einer gegebenen Formelmenge eine Formel herleitet, die in dieser Formelmenge bereits enthalten ist. Da die gegebene Formelmenge bereits herleitbar ist, muss auch jede einzelne Formel, die Element der Menge ist, herleitbar sein. Beispiel: Man soll aus der Formelmenge M irgendeine Formel herleiten. Die atomare Formel A sei Element der Formelmenge M. Gegeben die Formelmenge M, ist A herleitbar. Also können wir A aus der Formelmenge herleiten.

Formal:

    Sei $M=\{A,B,C\}$.
    Trivialerweise gilt $A\vdash A$.
    Da $A$ Element von $M$ ist, gilt $M\vdash A$ (die Hypothese).

Modus (ponendo) ponens

Der Modus ponens erlaubt den Schluss auf $B$ aus $A$ und $A\rightarrow B$ („wenn A, dann B“). Im hier dargestellten Kalkül präsentiert sich diese Regel wie folgt:

$M$ und $N$ seien Formelmengen und $A$ und $B$ seien Formeln.

Wenn nun aus der Formelmenge $M$ die Formel $A$ herleitbar ist und wenn aus der Formelmenge $N$ die Formel $A\rightarrow B$ herleitbar ist, dann ist aus der Vereinigung von $M$ und $N$ die Formel $B$ herleitbar; in formaler Schreibweise:

$M\vdash A$

$N\vdash A\rightarrow B$

$M\cup N\vdash B$

Zum besseren Verständnis ein Beispiel für die Anwendung. Gegeben sei ein Hilbertkalkül mit folgenden fünf Axiomen:

1. $F\rightarrow (G\rightarrow F)$
2. $(F\rightarrow (G\rightarrow H))\rightarrow ((F\rightarrow G)\rightarrow (F\rightarrow H))$
3. $(F\rightarrow G)\rightarrow (\neg G\rightarrow \neg F)$
4. $F\rightarrow (\neg F\rightarrow G)$
5. $(\neg F\rightarrow F)\rightarrow F$

Die Aufgabe bestehe darin, aus der leeren Formelmenge $M=\{\}$ die Formel $A\rightarrow A$ herzuleiten, also $M\vdash A\rightarrow A$.

Schritt	Formel	Erläuterung
1	$M\vdash A\rightarrow ((B\rightarrow A)\rightarrow A)$	Instanz von Axiom (1) ($F$ ersetzt durch $A$, $G$ ersetzt durch $(B\rightarrow A)$)
2	$M\vdash (A\rightarrow ((B\rightarrow A)\rightarrow A))\rightarrow ((A\rightarrow (B\rightarrow A))\rightarrow (A\rightarrow A))$	Instanz von Axiom (2) ($F$ ersetzt durch $A$, $G$ ersetzt durch $(B\rightarrow A)$, $H$ ersetzt durch $A$)
3	$M\vdash (A\rightarrow (B\rightarrow A))\rightarrow (A\rightarrow A)$	Modus Ponens aus Schritt 1 und 2.
4	$M\vdash A\rightarrow (B\rightarrow A)$	Instanz von Axiom (1) ($F$ ersetzt durch $A$, $G$ ersetzt durch $B$)
5	$M\vdash A\rightarrow A$	Modus Ponens aus Schritt 3 und 4.

Verhältnis zu anderen Logik-Kalkülen

Die Beweisführung innerhalb eines Hilbert-Kalküls ist oftmals sehr aufwendig und es ist nicht trivial ersichtlich, wie eine aussagenlogische oder prädikatenlogische Formel aus dem Kalkül abgeleitet werden kann. Im Gegensatz dazu stehen Systeme des Natürlichen Schließens, unter anderem das von Gentzen entwickelte System oder der Fitch-Kalkül. In derartigen formalen Systemen ist die Beweisführung sehr viel ähnlicher der des üblichen deduktiv-mathematischen Argumentierens. Systeme des Natürlichen Schließens sind regelbasiert; sie haben keine Axiome, dafür allerdings eine große Anzahl von Schlussregeln. Konträr dazu haben Axiomensysteme in der Regel viele (möglicherweise sogar unendlich viele) Axiome und nur eine Schlussregel. Der zweite Unterschied besteht darin, dass Systeme des Natürlichen Schließens es erlauben, Aussagen zum Zwecke der Beweisführung kurzfristig anzunehmen und diese später wieder zu verwerfen.

Literatur

• David Hilbert, Paul Bernays: Grundlagen der Mathematik. Band 1 Berlin 1934, Band 2 Berlin 1939
• H. Ehrig, B. Mahr, F. Cornelius, M. Grosse-Rhode, P. Zeitz: Mathematisch-strukturelle Grundlagen der Informatik. Springer-Verlag, Berlin et al. 2001, ISBN 3-540-41923-3. 

Weblinks

• Formale Prädikatenlogik (PDF; 508 kB), eine Zusammenstellung von Axiomen, Regeln und Propositionen mit formalen Beweisen im Stil von Hilbert