Moderne Termlogik: Einleitung: Kalküle

Moderne Termlogik

Einleitung

Kalküle

Die Syntax der Termlogik werden wir durch einen Kalkül beschreiben. Dazu müssen die folgenden Bestandteile definiert werden:

• Bausteine, darunter:
  • Atome
  • Variable
  • Formationsregeln
• Axiome
• Transformationsregeln

Von Paul Lorenzen stammt das folgende Beispiel eines einfachen Kalküls, der hier der Illustration dieses wichtigen Begriffes dienen soll. (Den die Termlogik definierenden Kalkül werden wir im folgenden Kapitel definieren).

• Bausteine
  • Atome: $\circ ,+$
  • Variable: $a$
  • Formationsregel: alle beliebigen Zeichenketten aus Atomen und Variablen sind zulässig
• Axiom: +
• Transformationsregeln:
  • (R1) $a⟶a\circ$
  • (R2) $a⟶+a+$

Eine Ableitung in diesem Kalkül besteht darin, ausgehend von einem Axiom (einem Anfang) Transformationsregeln anzuwenden. So kann man in dem obigen kleinen Kalkül die "Figur" $++\circ +$ wie folgt herleiten:

$\begin{array}{ccc}1.& +& Axiom\\ 1\to 2.& +\circ & (R1)\\ 2\to 3.& ++\circ +& (R2)\end{array}$

Die Tatsache, dass $++\circ +$ im Kalkül ableitbar ist, bezeichnen wir mit $⊢++\circ +$.

• Allgemein schreiben wir $A_1,A_2,...,A_n⊢B$, wenn im Kalkül der Ausdruck $B$ unter Verwendung von $A_1,A_2,...,A_n$ abgeleitet werden kann.

Ein Beispiel: Es gilt im obigen Kalkül

$\circ ⊢\circ \circ \circ$,

was die folgende Ableitung zeigt:

$\begin{array}{ccc}1.& \circ & Vorauss.\\ 1\to 2.& \circ \circ & (R1)\\ 2\to 3.& \circ \circ \circ & (R1)\end{array}$.