Korrektheit (Logik)

Korrektheit ist eine Eigenschaft formaler Systeme bzw. Kalküle. Man unterscheidet semantische Korrektheit („Alles, was beweisbar ist, ist wahr.“) und klassische Korrektheit („In keinem Fall ist $A$ und $\neg A$ zugleich beweisbar.“). Ein korrekter Kalkül ist insbesondere widerspruchsfrei, denn in einem Kalkül, der nicht widerspruchsfrei ist, d. h. in dem ein Widerspruch beweisbar ist, ist insbesondere alles, was falsch ist, beweisbar.

Korrektheit ist das Pendant zur Vollständigkeit, in dem Sinn, dass ein Kalkül vollständig ist, wenn in ihm jede wahre Aussage formal ableitbar ist. („Alles, was wahr ist, ist beweisbar.“) Wenn ein Kalkül korrekt und vollständig ist und terminiert, können in ihm genau alle wahren Aussagen abgeleitet werden. Kurt Gödel bewies, dass die Prädikatenlogik erster Stufe korrekt und vollständig ist (Vollständigkeitssatz).