Als Termkalkül bezeichnet man in der mathematischen Logik jenen Kalkül, mittels welchem man alle korrekten Terme über einem Alphabet erzeugen kann.

Sei dazu ein Alphabet mit zugehöriger Symbolmenge . -Terme sind dann genau jene Zeichenreihen, die man durch endlichmalige Anwendung der folgenden Regeln erzeugen kann.

  1. Jede Variable ist ein -Term.
  2. Jede Konstante aus ist ein -Term.
  3. Sind die Zeichenreihen -Terme, und ist ein -stelliges Funktionssymbol aus , so ist auch ein -Term.

Ist umgekehrt eine beliebige Zeichenreihe über gegeben, so kann man mittels des Kalküls feststellen, ob diese ein -Term ist, indem man die Regeln des Kalküls in umgekehrter Richtung anwendet.

Beispiele

Bearbeiten

Gegeben sei ein Alphabet mit der Symbolmenge  .   sei ein einstelliges Funktionssymbol,   ein zweistelliges Funktionssymbol, und   eine Konstante. Nach dem Kalkül ist die Zeichenreihe

 

ein  -Term. Nach Regel 1 ist nämlich   ein  -Term. Nach Regel 2 ist   ein  -Term. Aus Regel 3 angewandt auf   und   folgt, dass auch   ein  -Term ist. Nochmaliges Anwenden von Regel 3 auf  ,  , und   liefert, dass auch die obige Zeichenreihe ein  -Term ist. Durch Setzen von Klammern kann man das verdeutlichen:  .

Dagegen ist die Zeichenreihe

 

kein  -Term. Sie beginnt mit dem zweistelligen Funktionssymbol g. Entfernte man das Symbol g aus der Zeichenreihe, so müsste die verbliebene Zeichenreihe v0fcc aus genau zwei hintereinander geschriebenen  -Termen bestehen. Das nächste Zeichen ist v0, welches nach Regel 1 ein  -Term ist. Somit müsste fcc ein  -Term sein. Da aber auf das einstellige Funktionssymbol f zwei Konstanten (=  -Terme) folgen, ist das nicht der Fall.

Literatur

Bearbeiten
  • H.-D. Ebbinghaus, J. Flum, W. Thomas: Einführung in die mathematische Logik, Heidelberg, Berlin: Spektrum 1996. ISBN 3-8274-0130-5