Moderne Termlogik: Einleitung: Kalküle


Moderne Termlogik Bearbeiten

Einleitung Bearbeiten

Kalküle Bearbeiten

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:  
    • Variable:  
    • Formationsregel: alle beliebigen Zeichenketten aus Atomen und Variablen sind zulässig
  • Axiom: +
  • Transformationsregeln:
    • (R1)  
    • (R2)  


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"   wie folgt herleiten:

 

Die Tatsache, dass   im Kalkül ableitbar ist, bezeichnen wir mit  .

  • Allgemein schreiben wir  , wenn im Kalkül der Ausdruck   unter Verwendung von   abgeleitet werden kann.

Ein Beispiel: Es gilt im obigen Kalkül

 ,

was die folgende Ableitung zeigt:

 .