Korrektheit (Logik)


Korrektheit (Logik)

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

In der mathematischen Sprache wird die Korrektheit mit dem syntaktischen Ableitbarkeitsoperator \vdash und dem semantischen Folgerungsoperator \models ausgedrückt: Ein Kalkül heißt korrekt, wenn aus \Sigma \vdash \Psi stets \Sigma \models \Psi folgt. Dabei wird die Semantik des Kalküls festgelegt durch eine Klasse von Modellen. \Sigma \models \Psi bedeutet, dass jede Interpretation, die Modell von \,\Sigma ist, auch Modell von \,\Psi ist.

Die Korrektheit ist eine Mindestanforderung an einen Kalkül. Sie wird hergestellt, indem jede Regel des Kalküls korrekt gewählt wird. Aus der Korrektheit folgt die Widerspruchsfreiheit des Kalküls: Man muss nur eine einzige Formel angeben, die in irgendeinem Modell falsch ist, dann kann sie in einem korrekten Kalkül auch nicht ableitbar sein. In der klassischen Logik ist ein Widerspruch A\ \and \neg A solch eine falsche Formel, in der Prädikatenlogik mit Gleichheit etwa die Formel A\neq A.

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

  • H.D. Ebbinghaus, J. Flum, W. Thomas: Einführung in die mathematische Logik. Mannheim-Leipzig-Wien-Zürich; BI-Wiss. Verlag, 1992, ISBN 3-411-15603-1
  • Hans-Peter Tuschik, Helmut Wolter: Mathematische Logik - kurzgefasst. Grundlagen, Modelltheorie, Entscheidbarkeit, Mengenlehre. Mannheim-Leipzig-Wien-Zürich; BI-Wiss. Verlag, 1994, ISBN 3-411-16731-9

Wikimedia Foundation.

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

  • Korrektheit — Das mathematische Attribut Korrektheit (von korrekt = richtig) bezeichnet: in der mathematischen Logik eine Eigenschaft mancher formaler Systeme oder Kalküle, siehe Korrektheit (Logik). in der Softwaretechnik eine Eigenschaft eines… …   Deutsch Wikipedia

  • Logik — Folgerichtigkeit; logische Korrektheit; Übereinstimmung; Stimmigkeit; Dialektik; Analytik; Gesetzmäßigkeit; Vernunft; Konsequenz * * * Lo|gik [ lo:gɪk], die; : 1 …   Universal-Lexikon

  • Hoare-Logik — Der Hoare Kalkül (auch Hoare Logik) ist ein Formales System, entwickelt von dem britischen Informatiker C. A. R. Hoare und später verfeinert von Hoare und anderen Wissenschaftlern. Er wurde 1969 in einem Artikel mit dem Titel An axiomatic basis… …   Deutsch Wikipedia

  • Vollständigkeit (Logik) — Man bezeichnet ganz unterschiedliche Eigenschaften formaler Systeme bzw. Kalküle mit dem Begriff Vollständigkeit. Zur Unterscheidung werden die Begriffe Vollständigkeit von Theorien Vollständigkeit von Sequenzenkalkülen verwendet. Daneben wird… …   Deutsch Wikipedia

  • Mathematische Logik — Die Mathematische Logik ist ein Teilgebiet der Mathematik. Oft wird sie in die Teilgebiete Modelltheorie, Beweistheorie, Mengenlehre und Rekursionstheorie aufgeteilt. Forschung im Bereich der mathematischen Logik hat zum Studium der Grundlagen… …   Deutsch Wikipedia

  • Wissensrepräsentation mit Logik — ist eine Art der Wissensrepräsentation, die auf formaler Logik basiert. Zum Aufbau wissensbasierter Systeme müssen Objekte der realen Welt in einer Sprache repräsentiert werden, die ein Computer versteht, damit er mit diesem Wissen umgehen kann.… …   Deutsch Wikipedia

  • Resolution (Logik) — Die Resolution ist ein Verfahren der formalen Logik, um eine logische Formel auf Gültigkeit zu testen. Das Resolutionsverfahren, auch Resolutionskalkül genannt, ist ein Widerlegungsverfahren: Statt direkt die Allgemeingültigkeit einer Formel zu… …   Deutsch Wikipedia

  • logische Korrektheit — Folgerichtigkeit; Logik; Übereinstimmung; Stimmigkeit …   Universal-Lexikon

  • Gödel'scher Unvollständigkeitssatz — Der gödelsche Unvollständigkeitssatz ist einer der wichtigsten Sätze der modernen Logik. Er beschäftigt sich mit der Ableitbarkeit von Aussagen in formalen Theorien. Der Satz zeigt die Grenzen der formalen Systeme ab einer bestimmten Mächtigkeit… …   Deutsch Wikipedia

  • Gödels Satz — Der gödelsche Unvollständigkeitssatz ist einer der wichtigsten Sätze der modernen Logik. Er beschäftigt sich mit der Ableitbarkeit von Aussagen in formalen Theorien. Der Satz zeigt die Grenzen der formalen Systeme ab einer bestimmten Mächtigkeit… …   Deutsch Wikipedia