Hilbertkalkü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.

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 ├, wobei A├ 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 aussagenlogischen 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 → (B → 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 – 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 die Teilmenge (also jede einzelne Formel) herleitbar sein. Beispiel: Man soll aus der Formelmenge M irgendeine Formel herleiten. Die atomare Formel A sei Teilmenge der Formelmenge M. Gegeben der Formelmenge M ist A herleitbar. Also können wir A aus der Formelmenge herleiten.

formal:

    Sei M = {A, B, C }. 
    Trivialerweise gilt A ├ A. 
    Da A Teilmenge von M ist, gilt M ├ A (die Hypothese).

Modus (ponendo) ponens

Der Modus ponens erlaubt den Schluss von A→B („Wenn A, dann B“) und A auf 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→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 besserem Verständnis ein Beispiel für die Anwendung. Gegeben sei ein Hilbertkalkül mit folgenden fünf Axiomen:

1. F → (G → F)
2. (F → (G → H)) → ((F → G) → (F → H))
3. (F → G) → (¬ G → ¬ F)
4. F → (¬ F → G)
5. (¬ F → F) → F

Die Aufgabe bestehe darin, aus der leeren Formelmenge (M={}) die Formel A → A herzuleiten, also M├A → A.

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

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.