Hilbertkalkül

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.

Inhaltsverzeichnis

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. 

Wikimedia Foundation.

Игры ⚽ Поможем сделать НИР

Schlagen Sie auch in anderen Wörterbüchern nach:

  • 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 …   Deutsch Wikipedia

  • Berechnungsmodell — Dieser Artikel wurde auf der Qualitätssicherungsseite des Portals Mathematik eingetragen. Dies geschieht, um die Qualität der Artikel aus dem Themengebiet Mathematik auf ein akzeptables Niveau zu bringen. Dabei werden Artikel gelöscht, die nicht… …   Deutsch Wikipedia

  • Kalküle — Dieser Artikel wurde auf der Qualitätssicherungsseite des Portals Mathematik eingetragen. Dies geschieht, um die Qualität der Artikel aus dem Themengebiet Mathematik auf ein akzeptables Niveau zu bringen. Dabei werden Artikel gelöscht, die nicht… …   Deutsch Wikipedia

  • Entscheidungsverfahren (klassische Aussagenlogik) — Dieser Artikel wurde auf der Qualitätssicherungsseite des Portals Mathematik zur Löschung vorgeschlagen. Dies geschieht, um die Qualität der Artikel aus dem Themengebiet Mathematik auf ein akzeptables Niveau zu bringen. Dabei werden Artikel… …   Deutsch Wikipedia

  • Gödel'scher Vollständigkeitssatz — Der Gödelsche Vollständigkeitssatz (benannt nach Kurt Gödel) ist der Hauptsatz der mathematischen Logik. Er zeigt für ein formales System der Prädikatenlogik erster Stufe die Korrektheit und Vollständigkeit: Jeder Satz, der semantisch aus einer… …   Deutsch Wikipedia

  • Gödelscher Vollständigkeitssatz — Der Gödelsche Vollständigkeitssatz (benannt nach Kurt Gödel) ist der Hauptsatz der mathematischen Logik. Er zeigt für ein formales System der Prädikatenlogik erster Stufe die Korrektheit und Vollständigkeit: Jeder Satz, der semantisch aus einer… …   Deutsch Wikipedia

  • Kalkül — Als Kalkül (der, das, fr. calcul „Rechnung“; von lat. calculus „Rechenstein, Spielstein“) versteht man in den formalen Wissenschaften wie Logik und Mathematik ein System von Regeln, mit denen sich aus gegebenen Aussagen (Axiomen) weitere Aussagen …   Deutsch Wikipedia

  • Logik erster Ordnung — Die Artikel Prädikatenlogik und Prädikat (Logik) überschneiden sich thematisch. Hilf mit, die Artikel besser voneinander abzugrenzen oder zu vereinigen. Beteilige dich dazu an der Diskussion über diese Überschneidungen. Bitte entferne diesen… …   Deutsch Wikipedia

  • PK1 — Die Artikel Prädikatenlogik und Prädikat (Logik) überschneiden sich thematisch. Hilf mit, die Artikel besser voneinander abzugrenzen oder zu vereinigen. Beteilige dich dazu an der Diskussion über diese Überschneidungen. Bitte entferne diesen… …   Deutsch Wikipedia

  • Prädikatenkalkül — Die Artikel Prädikatenlogik und Prädikat (Logik) überschneiden sich thematisch. Hilf mit, die Artikel besser voneinander abzugrenzen oder zu vereinigen. Beteilige dich dazu an der Diskussion über diese Überschneidungen. Bitte entferne diesen… …   Deutsch Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”