Aussagenkalkül

Ein Aussagenkalkül ist ein Kalkül für die Aussagenlogik. Er leitet aus einer gegebenen Menge von Aussagen neue Aussagen her, die aus den gegebenen Aussagen aussagenlogisch folgen. Allgemein werden die Aussagen, aus denen hergeleitet wird, Prämissen genannt; die hergeleiteten Aussagen werden Konklusionen genannt. Die Herleitung einer Konklusion aus einer Menge von Prämissen wird als Argument bezeichnet.

Prinzipiell wird unterschieden:

• Semantische Gültigkeit (Folgerung): Für die klassische Aussagenlogik ist semantische Gültigkeit folgendermaßen definiert: Ein Argument ist genau dann semantisch gültig, wenn unter der Voraussetzung, dass alle Prämissen wahr sind, auch die Konklusion wahr ist.
• Syntaktische Gültigkeit (Herleitung): Ein Argument ist genau dann syntaktisch gültig, wenn sich die Konklusion mit Hilfe der Axiome und Schlussregeln des gewählten Aussagenkalküls aus den Prämissen herleiten lässt.

Ein Kalkül ist korrekt, wenn in ihm nur Folgerungen ableitbar sind. Ein Kalkül ist vollständig, wenn in ihm alle Folgerungen ableitbar sind. Für die klassische Aussagenlogik lassen sich Kalküle angeben, die korrekt und vollständig sind.

Verschiedene Aussagenkalküle sind zudem Entscheidungsverfahren für die Gültigkeit von Argumenten, das heißt, sie erlauben es, für jedes beliebige Argument innerhalb endlicher Zeit festzustellen, ob das Argument gültig ist oder nicht. Aussagenkalküle, die Entscheidungsverfahren sind, sind zum Beispiel der aussagenlogische Baumkalkül oder der aussagenlogische Resolutionskalkül.

Konkrete Aussagenkalküle sind in folgenden Artikeln angegeben:

• Im Artikel Aussagenlogik ist ein axiomatischer Aussagenkalkül angegeben.
• Im Artikel Baumkalkül ist ein Aussagenkalkül nach Beth, ein Widerlegungskalkül, angegeben.
• Im Artikel Existential Graphs ist der graphische aussagenlogische Kalkül der Alphagraphen angegeben.
• Im Artikel Resolution (Logik) wird ein Widerlegungskalkül angegeben, der vor allem für das automatische Beweisen bedeutsam ist.
• In den Artikeln Systeme natürlichen Schließens und Sequenzenkalkül sind Regelkalküle angegeben.