Korrektheit (Logik)

aus Wikipedia, der freien Enzyklopädie
Dies ist eine alte Version dieser Seite, zuletzt bearbeitet am 17. August 2014 um 18:13 Uhr durch 77.23.40.181 (Diskussion) (Abschnittslink korrigiert). Sie kann sich erheblich von der aktuellen Version unterscheiden.
Zur Navigation springen Zur Suche springen

Korrektheit (englisch soundness) ist eine wichtige Eigenschaft formaler Systeme oder Kalküle und betrifft den Zusammenhang zwischen Syntax und Semantik, der umgangssprachlich lautet: Was formal ableitbar ist, ist auch wahr (innerhalb der gegebenen Semantik).

In der formalen Logik wird Ableitbarkeit durch den syntaktischen Ableitungsoperator und Schlussfolgern durch die semantischen Folgerungsrelation ausgedrückt: Ein Kalkül heißt korrekt, wenn für Aussagenmengen und aus stets folgt. Die Semantik des Schließens wird modelltheoretisch definiert. gilt genau dann, wenn jedes Modell von , auch Modell von ist.

Für die Korrektheit eines Kalküls ist hinreichend, wenn jede einzelne Ableitungsregel schlüssig ist. In einem korrekten Kalkül lässt sich keine Formel herleiten, die im gewählten Modell nicht wahr ist.

Das Gegenstück zur Korrektheit ist die Vollständigkeit eines formalen Systems. Sie besagt: Was semantisch richtig ist, lässt sich auch ableiten. Vollständigkeitssätze sind meist weitaus schwieriger zu beweisen als Korrektheitssätze; so bereitet der Beweis für die Korrektheit des Sequenzenkalküls der Prädikatenlogik keine Probleme,[1] während der Vollständigkeitssatz schwieriger ist.

Siehe auch

Einzelnachweis

  1. Ebbinghaus, Einführung in die mathematische Logik, Mannheim-Leipzig-Wien-Zürich 1992, S. 74

Quellen

  • Heinz-Dieter Ebbinghaus, Jörg Flum, Wolfgang Thomas: Einführung in die mathematische Logik, 5. Aufl., Spektrum Akademischer Verlag; 2007, ISBN 978-3827416919
  • Hans-Peter Tuschik, Helmut Wolter: Mathematische Logik – kurzgefasst. Grundlagen, Modelltheorie, Entscheidbarkeit, Mengenlehre, BI-Wiss. Verlag, Mannheim-Leipzig-Wien-Zürich 1994, ISBN 3-411-16731-9.