Termkalkül

aus Wikipedia, der freien Enzyklopädie
Zur Navigation springen Zur Suche springen

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.

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.

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