imported>Josef J. Jarosch am 6. November 2025 um 20:07 Uhr

2025-11-06T20:07:17Z

Neue Seite

{{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ül]]e für die klassische [[Aussagenlogik]] oder die [[Prädikatenlogik erster Stufe]], das heißt Kalküle, in denen sich [[Theorem]]e und [[Argument]]e der Aussagenlogik oder der Prädikatenlogik erster Stufe [[Ableitung (Logik)|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 ponens|Modus ponendo ponens]], und im Fall der Angabe von Axiomen zusätzlich einer [[Substitution (Logik)|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ödelscher Unvollständigkeitssatz|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.<ref>Einführung in die Mengenlehre: Die Mengenlehre Georg Cantors und ihre Axiomatisierung durch Ernst Zermelo, Oliver Deiser, Gabler Wissenschaftsverlage, 2009, ISBN 3-642-01444-5, {{Google Buch |BuchID=J8TBXux80G0C |Seite=456 |Hervorhebung=Frege}}</ref>

== 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 <math>\vdash</math>, wobei <math>A \vdash B</math> als „<math>B</math> ist aus <math>A</math> herleitbar“ gelesen wird.

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 [[Tautologie (Logik)|Tautologien]], also Formeln, die unter jeder Zuordnung von [[Wahrheitswert]]en zu den in ihnen vorkommenden Satzvariablen den Wert „wahr“ annehmen. Eine derartige Tautologie ist zum Beispiel die Aussage <math>A \rightarrow (B \rightarrow A)</math>, 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 <math>M = \{A, B, C\}</math>.
Trivialerweise gilt <math>A \vdash A</math>.
Da <math>A</math> Element von <math>M</math> ist, gilt <math>M \vdash A</math> (die Hypothese).

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

: <math>M</math> und <math>N</math> seien Formelmengen und <math>A</math> und <math>B</math> seien Formeln.
: Wenn nun aus der Formelmenge <math>M</math> die Formel <math>A</math> herleitbar ist und wenn aus der Formelmenge <math>N</math> die Formel <math>A \rightarrow B</math> herleitbar ist, dann ist aus der Vereinigung von <math>M</math> und <math>N</math> die Formel <math>B</math> herleitbar; in formaler Schreibweise:
: <math>M \vdash A</math>
: <math>N \vdash A \rightarrow B</math>
: <math>M \cup N \vdash B</math>

Zum besseren Verständnis ein Beispiel für die Anwendung. Gegeben sei ein Hilbertkalkül mit folgenden fünf Axiomen:
# <math>F \rightarrow (G \rightarrow F)</math>
# <math>(F \rightarrow (G \rightarrow H)) \rightarrow ((F \rightarrow G) \rightarrow (F \rightarrow H))</math>
# <math>(F \rightarrow G) \rightarrow (\neg G \rightarrow \neg F)</math>
# <math>F \rightarrow (\neg F \rightarrow G)</math>
# <math>(\neg F \rightarrow F) \rightarrow F</math>

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

{| border="1" cellpadding="2" cellspacing="0"
!Schritt
!Formel
!Erläuterung
|-
|1
|<math>M \vdash A \rightarrow ((B \rightarrow A) \rightarrow A)</math>
|Instanz von Axiom (1) (<math>F</math> ersetzt durch <math>A</math>, <math>G</math> ersetzt durch <math>(B \rightarrow A)</math>)
|-
|2
|<math>M \vdash (A \rightarrow ((B \rightarrow A) \rightarrow A)) \rightarrow ((A \rightarrow (B \rightarrow A)) \rightarrow (A \rightarrow A))</math>
|Instanz von Axiom (2) (<math>F</math> ersetzt durch <math>A</math>, <math>G</math> ersetzt durch <math>(B \rightarrow A)</math>, <math>H</math> ersetzt durch <math>A</math>)
|-
|3
|<math>M \vdash (A \rightarrow (B \rightarrow A)) \rightarrow (A \rightarrow A)</math>
|Modus Ponens aus Schritt 1 und 2.
|-
|4
|<math>M \vdash A \rightarrow (B \rightarrow A)</math>
|Instanz von Axiom (1) (<math>F</math> ersetzt durch <math>A</math>, <math>G</math> ersetzt durch <math>B</math>)
|-
|5
|<math>M \vdash A \rightarrow A</math>
|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 [[Systeme natürlichen Schließens|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.<ref> [https://www.logicmatters.net/resources/pdfs/ProofSystems.pdf Logic Matters - Proof Systems] Peter Smith: ''Axioms, rules, and what logic is all about'' In: ''Types of Proof System'' 2010, S. 2.</ref>

== Literatur ==

* David Hilbert, Paul Bernays: ''Grundlagen der Mathematik''. Band 1 Berlin 1934, Band 2 Berlin 1939
* {{Literatur
|Autor= H. Ehrig, B. Mahr, F. Cornelius, M. Grosse-Rhode, P. Zeitz
|Titel= Mathematisch-strukturelle Grundlagen der Informatik
|Verlag= Springer-Verlag
|Ort= Berlin et al.
|Jahr= 2001
|ISBN=3-540-41923-3
}}

== Weblinks ==
* [http://www.qedeq.org/current/doc/math/qedeq_formal_logic_v1_de.pdf Formale Prädikatenlogik] (PDF; 508 kB), eine Zusammenstellung von Axiomen, Regeln und Propositionen mit formalen Beweisen im Stil von Hilbert

== Einzelnachweise ==
<references />

{{SORTIERUNG:Hilbertkalkul}}
[[Kategorie:Logikkalkül]]
[[Kategorie:David Hilbert als Namensgeber]]

Hilbert-Kalkül - Versionsgeschichte

imported>Josef J. Jarosch am 6. November 2025 um 20:07 Uhr