Termkalkül

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 <math>A_S</math> ein Alphabet mit zugehöriger Symbolmenge <math>S</math>. <math>S</math>-Terme sind dann genau jene Zeichenreihen, die man durch endlichmalige Anwendung der folgenden Regeln erzeugen kann.

Jede Variable ist ein <math>S</math>-Term.
Jede Konstante aus <math>S</math> ist ein <math>S</math>-Term.
Sind die Zeichenreihen <math>t_1,\ldots,t_n</math> <math>S</math>-Terme, und ist <math>f</math> ein <math>n</math>-stelliges Funktionssymbol aus <math>S</math>, so ist auch <math>ft_1,\ldots,t_n</math> ein <math>S</math>-Term.

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

Beispiele

Gegeben sei ein Alphabet mit der Symbolmenge <math>S = \lbrace f,g,c \rbrace </math>. <math>f</math> sei ein einstelliges Funktionssymbol, <math>g</math> ein zweistelliges Funktionssymbol, und <math>c</math> eine Konstante. Nach dem Kalkül ist die Zeichenreihe

ein <math>S</math>-Term. Nach Regel 1 ist nämlich <math>v_0</math> ein <math>S</math>-Term. Nach Regel 2 ist <math>c</math> ein <math>S</math>-Term. Aus Regel 3 angewandt auf <math>f</math> und <math>c</math> folgt, dass auch <math>fc</math> ein <math>S</math>-Term ist. Nochmaliges Anwenden von Regel 3 auf <math>g</math>, <math>v_0</math>, und <math>fc</math> liefert, dass auch die obige Zeichenreihe ein <math>S</math>-Term ist. Durch Setzen von Klammern kann man das verdeutlichen: <math> gv_0 fc=g(v_0 f(c))</math>.

Dagegen ist die Zeichenreihe

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

Literatur

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