Hilbert-Kalkül

aus Wikipedia, der freien Enzyklopädie
Wechseln zu: Navigation, Suche
Dieser Artikel behandelt axiomatische logische Kalküle. Für den Hilbertkalkül der Geometrie siehe Hilberts Axiomensystem der euklidischen Geometrie

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.[1]

Ein Hilbertkalkül für die klassische Aussagenlogik[Bearbeiten]

Syntax[Bearbeiten]

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[Bearbeiten]

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[Bearbeiten]

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 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 Element von M ist, gilt M ├ A (die Hypothese).

Modus (ponendo) ponens[Bearbeiten]

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[Bearbeiten]

  • 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[Bearbeiten]

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

Einzelnachweise[Bearbeiten]

  1. Einführung in die Mengenlehre: Die Mengenlehre Georg Cantors und ihre Axiomatisierung durch Ernst Zermelo, Oliver Deiser, Gabler Wissenschaftsverlage, 2009, ISBN 3642014445, eingeschränkte Vorschau in der Google-Buchsuche