# Kalkül

Als der oder das Kalkül (französisch calcul „Rechnung“; von lateinisch calculus „Rechenstein“, „Spielstein“) versteht man in den formalen Wissenschaften wie Logik und Mathematik ein formales System von Regeln, mit denen sich aus gegebenen Aussagen (Axiomen) weitere Aussagen ableiten lassen. Kalküle, auf eine Logik selbst angewandt, werden auch Logikkalküle genannt.
Das Wort Kalkül im logischen und mathematischen Sinn ist ein Maskulinum (der Kalkül). Kalkül im umgangssprachlichen Sinn wird auch als Neutrum (das Kalkül, deshalb auch „ins Kalkül ziehen“) in der Bedeutung von „Berechnung“ oder „Überlegung“ verwendet.

## Bestandteile

Ein Kalkül besteht aus folgenden Bestandteilen:
* Bausteine, also Grundelemente (Grundzeichen), aus denen komplexere Ausdrücke zusammengesetzt werden. Die Gesamtheit der Bausteine des Kalküls wird auch sein Alphabet genannt. Für einen Kalkül der Aussagenlogik z. B. wählt man als Bausteine Satzbuchstaben (Satzvariablen), einige Konnektive (z. B. →, ∧, ∨ und ¬) und gegebenenfalls Gliederungszeichen (Klammern). In Analogie zu natürlichen Sprachen kann man die Liste der Bausteine als „Wörterbuch“ (im Sinn einer Wörterliste) des Kalküls bezeichnen.
* Formationsregeln, mit denen festgelegt wird, wie die Bausteine zu komplexen Objekten, die auch wohlgeformte Formeln genannt werden, zusammengesetzt werden dürfen. Die Gesamtheit der von den Formationsregeln gebildeten, wohlgeformten Ausdrücke wird auch Satzmenge des Kalküls genannt und ist eine formale Sprache über den Bausteinen. Ein Kalkül für die Aussagenlogik könnte zum Beispiel festlegen, dass man aus zwei bestehenden Sätzen einen neuen Satz bilden darf, indem man die beiden mit einem zweistelligen Konnektiv verbindet. So sind die Formationsregeln in Analogie zur natürlichen Sprache die „Grammatik“ des Kalküls.
* Transformationsregeln (Ableitungsregeln, Deduktionsregeln), die angeben, wie bestehende wohlgeformte Objekte (Ausdrücke, Sätze) des Kalküls umgeformt werden dürfen, um neue Objekte daraus zu erzeugen. In einem logischen Kalkül sind die Transformationsregeln Schlussregeln, die angeben, wie man aus bestehenden Sätzen auf neue Sätze schließen kann. Ein Beispiel für eine Schlussregel ist der Modus ponens, der erlaubt, von zwei Sätzen der Form „A → B“ und „A“ auf den Satz der Form „B“ zu schließen.
* Axiome sind Objekte (Ausdrücke), die nach den Formationsregeln des Kalküls gebildet sind und die ohne weitere Rechtfertigung, d. h., ohne eine Transformationsregel auf bereits bestehende Ausdrücke anzuwenden, verwendet werden dürfen.
Von diesen Bestandteilen ist nur der letzte (die Axiome) optional. Ein Kalkül, der Axiome beinhaltet – egal wie viele oder wie wenige –, wird axiomatischer Kalkül (auch „axiomatischer Regelkalkül“) genannt. Kalküle, die ohne Axiome auskommen, dafür aber meistens mehr Transformationsregeln beinhalten, werden oft als Regelkalküle (auch Schlussregelkalküle) bezeichnet.
Ein Kalkül ordnet weder seinen Bausteinen noch den daraus erzeugten zusammengesetzten Objekten eine Bedeutung zu. Gibt man für die von einem Kalkül erzeugten Zeichenreihen eine Interpretation an, d. h., legt man für sie eine Bedeutung fest, spricht man von einem interpretierten Kalkül, ansonsten von einem uninterpretierten Kalkül.
Ein Kalkül bildet sozusagen einen fest abgeschlossenen Handlungsspielraum. Das Schachspiel mit den Figuren (Axiome) und Zugregeln (Schlussregeln) bietet, wie Spiele im Allgemeinen, ein anschauliches Beispiel. Ein vorgegebenes Ziel (z. B. Gewinn des Spiels, Lösung eines – politischen – Konflikts, Finden eines Weges aus dem Labyrinth) gehört jedoch nicht zum Kalkül.

## Kalküle in der Logik

In der Logik sind Kalküle präzise definiert: Axiome sind dort Formeln (Aussagen), Transformationsregeln sind Ersetzungsschemata über den Formeln. Der Begriff des Schließens spielt in der Logik eine zentrale Rolle, und so versucht man den semantisch definierten Folgerungsoperator $\models$ (siehe Tautologie) durch den syntaktisch definierten Ableitungsoperator $\vdash$ nachzubilden, der die Anwendung von Schlussregeln symbolisiert.
Ein Kalkül heißt

### korrekt,

    wenn sich in ihm nur semantisch gültige (allgemeingültige) Formeln ableiten lassen. (Es darf aber ohne Weiteres sein, dass es semantisch gültige Formeln gibt, die in dem Kalkül nicht ableitbar sind.)
    Formal ausgedrückt: Wenn für alle Formeln $G$ und für alle Formelmengen $\Gamma$ gilt: $(\Gamma \vdash G)\Rightarrow (\Gamma \models G)$

### vollständig,

    wenn sich in ihm alle semantisch gültigen Formeln ableiten lassen. (Es kann aber ohne Weiteres sein, dass sich in dem Kalkül auch solche Formeln ableiten lassen, die nicht semantisch gültig sind.)
    Formal ausgedrückt: Wenn für alle Formeln $G$ und für alle Formelmengen $\Gamma$ gilt: $(\Gamma \models G)\Rightarrow (\Gamma \vdash G)$

### adäquat,

    wenn er sowohl vollständig als auch korrekt ist, d. h. wenn „sich die Begriffe der Beweisbarkeit und der Ableitbarkeit im Kalkül mit den jeweiligen Begriffen der Allgemeingültigkeit und der logischen Folgerung decken“.

### widerspruchsfrei,

    wenn sich in ihm kein Widerspruch ableiten lässt (wenn es unmöglich ist, eine Formel $\varphi$ und ihre Negation $\neg \varphi$ aus nicht widersprüchlichen Prämissen abzuleiten).

### konsistent,

    wenn in ihm mindestens eine Formel nicht ableitbar ist.
    Bemerkung: Widerspruchsfreiheit und Konsistenz decken sich in der klassischen Logik und intuitionistischen Logik.
    Begründung: Wenn ein Kalkül widerspruchsfrei ist, ist es z. B. unmöglich, sowohl $\vdash P$ als auch $\vdash \neg P$ zu beweisen. Das heißt, dass es mindestens eine Formel gibt (nämlich $P$ oder $\neg P$), die nicht ableitbar ist. Wenn der Kalkül andererseits nicht widerspruchsfrei ist und sich sowohl $\varphi$ als auch $\neg \varphi$ ableiten lassen, dann lässt sich ex falso quodlibet jede beliebige Formel ableiten (diese Schlussform gilt sowohl in der klassischen als auch in der intuitionistischen Logik).
Es gibt logische Systeme bzw. allgemein formale Systeme, für die sich adäquate Kalküle aufstellen lassen, zum Beispiel die klassische Logik. Andere formale Systeme sind ihrer Natur nach so beschaffen, dass es nicht möglich ist, einen Kalkül aufzustellen, der vollständig und korrekt ist (z. B. Prädikatenlogik höherer Stufe).
Für die Aussagenlogik gibt es in Gestalt der Wahrheitstabellen ein semantisches Entscheidungsverfahren (siehe Entscheidungsproblem), mit dem sich für alle Formeln und Argumente deren aussagenlogische Gültigkeit bzw. Ungültigkeit eindeutig ermitteln lässt, ohne dass die jeweilige Formel bzw. das jeweilige Argument in einem Kalkül abgeleitet werden müsste. Insofern ist für aussagenlogische Fragestellungen die Verwendung eines Logikkalküls nicht erforderlich.
Demgegenüber gibt es schon für die allgemeine Prädikatenlogik weder semantische noch syntaktische Entscheidungsverfahren; hier ist es zum Nachweis der Gültigkeit eines Arguments daher erforderlich, es in einem geeigneten Kalkül herzuleiten. Gelingt die Ableitung, dann ist das Argument als gültig erwiesen; gelingt die Ableitung nicht, dann sagt das nichts über die Gültigkeit des Arguments aus: Es könnte ungültig sein, es könnte aber auch die Suche nach einem geeigneten Beweis nicht gründlich genug gewesen sein.
Praktische Anwendung finden logische Kalküle in der Informatik auf dem Gebiet des maschinengestützten Beweisens.

### Beispiele

* Aussagenkalkül
* Begriffsschrift
* Beth-Tableaux
* Existential Graphs
* Fitch-Kalkül
* Gentzenkalkül bzw. Sequenzenkalkül
* Hilbertkalkül
* Hoare-Kalkül
* Lambda-Kalkül
* Prädikatenkalkül
* Relationenkalkül
* Resolutionskalkül
* Situationskalkül
* Syllogistik

## Kalküle in der Mathematik

In der Mathematik können sämtliche Regelsysteme, die, richtig angewendet, zu richtigen Ergebnissen führen, als Kalkül bezeichnet werden.

### Beispiele

* Arithmetik
* Integralrechnung
* Infinitesimalrechnung
* Kalkül der Differentialformen
* O-Kalkül
* Pi-Kalkül
* Residuenkalkül
* Stochastischer Kalkül
* Kalküle in der Bilanz-Bewertung
* wp-Kalkül

## Geschichte der Theorie des Kalküls

Die philosophischen Wurzeln des Kalküls führt man bis auf die Syllogistik von Aristoteles zurück, bei der es sich um ein formales System im modernen Sinn handelt. Die Geschichte der Theorie des Kalküls wird unterschiedlich weit zurückverfolgt. Als eigentlicher Begründer wird meist Leibniz genannt. Ziel seiner Theorie von einer characteristica universalis war es, durch reine Anwendung von vorher bestimmten Regeln mit Hilfe von Sprache neue Erkenntnisse zu gewinnen. Für andere knüpfte Leibniz damit an die ersten Ansätze eines Logikkalküls in der Kombinatorik von Raimundus Lullus an.

## Bedeutung der Kalkülisierung

Die Kalkülisierung der Logik macht in ihrem Anwendungsbereich das logische Denken zu einer Art des Rechnens. Sie ist ein Kennzeichen der modernen Logik und macht sie zur formalen, mathematischen oder symbolischen Logik. Nach Hilbert/Ackermann dient die Kalkülisierung der logischen Folgerung ihrer Zerlegung in letzte Elemente, so dass die logische Folgerung „als formale Umgestaltung der Ausgangsformeln nach gewissen Regeln, die den Rechenregeln analog sind, [erscheint]; das logische Denken findet sein Abbild in einem Logikkalkül“.
Die mit der Kalkülisierung einhergehende Mathematisierung bringt der Logik die Vorteile der Exaktheit und Überprüfbarkeit der Mathematik. Sie ist ein Phänomen der Konvergenz zum logizistischen Programm (Logizismus), d. h. zur Rückführung der Mathematik auf die Logik.
Die Kalkülisierung macht die Logik für Programmiersprachen geeignet.
Nach Paul Lorenzen besteht die Bedeutung der Kalkülisierung zunächst einmal darin, dass sie den Zirkel axiomatischer Theorien, dass sie selbst Logik voraussetzen, dadurch auflöst, dass Kalküle keine Logik voraussetzen sollen. „Für das Begründungsproblem, also für die Frage[,] mit welchem Recht man gewisse Schlüsse als logische Schlüsse anerkennt, liefert die Kalkülisierung keine Antwort.“
Als philosophisch relevant wird angegeben, dass ein (uninterpretierter) Kalkül „nichts Wirkliches“ sei, „sondern nur Regeln für unser eigenes Handeln, für das Operieren mit Figuren, enthält“.
Das Absehen von einer Interpretation bedeutet eine methodische Entlastung von semantischen Fragen und Kontroversen. Wird das Formale absolut gesetzt, birgt die Formalisierung die Gefahr eines reduktionistischen Formalismus, d. h. zu der Annahme, dass die semantische Reinterpretation und der Wirklichkeitsbezug logischer Aussagen in einem Kalkül letztendlich willkürlich bzw. nicht gegeben ist.