Das Kefk Network Wiki befindet sich im Testbetrieb.
Hilbert-Kalkül
Aus Kefk.
Ein Hilbertkalkül ist ein syntaktischer Kalkül zur Entscheidung der Gültigkeit logischer Schlüsse. Wichtiges Merkmal eines Hilbertkalküls ist die geringe Anzahl von Schlussregeln (oftmals nur eine) und Axiomen.
Inhaltsverzeichnis |
Hilbertkalkül für die klassische Aussagenlogik
Syntax
Neben den Aussagenvariabeln und logischen Konstanten der Objektebene enthält der Kalkül das metasprachliche Zeichen ├, wobei A├ B gelesen wird als „B folgt aus A“.
Im Hilbert-Kalkül wird im Wesentlichen mit Hilfe von drei elementaren Operationen Beweis geführt. Handlung (1) ist das Erstellen einer Instanz eines Axioms. Handlung (2) ist das Aufstellen einer Hypothese, und Handlung (3) ist das Verwenden des Modus Ponens.
Axiome
Zunächst zu Handlung (1). Der Hilbert-Kalkül befleißigt sich gewisser aussagenlogischer Tautologien, also Formeln, die angewandt in allen Fällen den Wahrheitswert 1 zurückliefern. Eine derartige Tautologie ist zum Beispiel: A → (B → A) und wird im Hilbert-Kalkül als Axiom vorausgesetzt. A und B fungieren in dieser Formel als Platzhalter, und können gegen jede andere beliebige atomare Formel ausgetauscht werden.
Hypothese
Nun 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. Und da die gegebene Formelmenge bereits erfüllbar ist, so muss auch die Teilmenge (also jede einzelne Formel) erfüllbar sein. Bsp.: Man soll aus der Formelmenge M irgendeine Formel herleiten. Die atomare Formel A sei Teilmenge der Formel M. Und da M erfüllbar ist, wissen wir, dass auch A erfüllbar ist. Also können wir A aus der Formelmenge herleiten.
formal:
M = {A, B, C }
M ├ A Hypothese
Modus Ponens
Der Modus Ponens (auch Schnittregel engl. cut), ist das Schließen auf die Herleitbarkeit einer Teilformel, der sich aufgrund des anderen Teils dieser Formel, und einer weiteren bereits hergeleiteten Formel ziehen lässt.
Bsp.:
M sei eine Formelmenge ; A, B seien atomare Formeln
wenn M ├ A
und M ├ A → B gilt
dann gilt auch M ├ B
zum besserem Verständnis ein Beispiel für die Anwendung des Hilbert Kalküls
Gegeben seien folgende 5 Axiome
- (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 zu A, G zu (B → A)) |
| 2 | M├ (A → ((B → A) → A))→ ((A → (B → A)) → (A → A)) | Instanz von Axiom (2) (F zu A, G zu (B → A), H zu A) |
| 3 | M├ (A → (B → A)) → (A → A) | Modus Ponens aus Schritt 1. & 2. |
| 4 | M├ A → (B → A) | Instanz von Axiom (1) (F zu A, G zu B) |
| 5 | M├ A → A | Modus Ponens aus Schritt 3. & 4. |
 | Dieses Dokument entstammt in seiner ersten oder einer späteren Version der deutschsprachigen Wikipedia. Es ist dort zu finden unter dem Stichwort Hilbert-Kalk%C3%BCl, die Liste der bisherigen Autoren befindet sich in der Versionsliste; die Originalfassung kann dort auch bearbeitet werden. Alle Texte der Wikipedia und ihre Derivate stehen unter der GNU-Lizenz für freie Dokumentation. |
