Seite parallel anzeigen





Der Hilbert-Typ-Kalkül

(Aussagenlogik Kapitel 7.2.2)

Diese Seite nimmt Bezug auf

(Seite parallel anzeigen)
Liste überspringen
Zum Seitenanfang

Ein Hilbert-Typ-Kalkül (oder kurz "Hilbert-Kalkül") hat typischerweise viele Axiome und meist nur den so genannten "Modus Ponens" als Schlussregel. Wir wollen hier eine einfache Version für aussagenlogische Formeln betrachten, wobei wir annehmen, dass alle materialen Äquivalenzen eliminiert wurden.
 
Der (hier vorgestellte) Hilbert-Typ-Kalkül enthält
  • die Axiomenschemata
    1. γ->(δ->γ)
    2. (γ->(δ->λ))->((γ->δ)->(γ->λ))
    3. γ->γ|δ
    4. δ->γ|δ
    5. (γ->λ)->((δ->λ)->((γ|δ)->λ))
    6. γ->(δ->γ&δ)
    7. γ&δ->γ
    8. γ&δ->δ
    9. (!γ->!δ)->(!γ->δ->γ)
    10. F->γ
  • 1 Schlussregel (die Sequente oberhalb des Striches sind die Voraussetzungen für die Regelanwendung, das Sequent unterhalb des Striches das Ergebnis der Regelanwendung):
    Modus Ponens:
    γ     γ->δ
    δ

Beispiel - Eine Ableitung im Hilbert-Kalkül

Wir wollen die Tautologie a->a ableiten:
Beschreibung der Ableitungsschritte
  • Wir bilden eine Instanz des 1. Axioms und
  • des 2. Axioms und
  • wenden den Modus Ponens an.
  • Dann fügen wir eine weitere Instanz des 1. Axioms hinzu,
  • wenden den Modus Ponens an und
  • erhalten die gewünschte Formel.
Ableitung (fahre mit der Maus über die Formeln, um etwas über ihre Herleitung zu erfahren)
a->(a->a->a) (a->(a->a->a))->(a->(a->a)->(a->a))
a->(a->a) a->(a->a)->(a->a)
a->a
Diser Hilbert-Typ-Kalkül hat folgende Eigenschaften:
  • Er hat viele komplexe Axiomenschemata.
  • Er hat nur 1 Regel.
  • Er ist vollständig und korrekt.
  • Er ist durch die Formel γ im Modus Ponens nicht analytisch.
  • Wie das obige Beispiel zeigt, sind auch Beweise einfacher Formeln kompliziert.