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

1. Jede Variable ist ein S-Term.
2. Jede Konstante aus S ist ein S-Term.
3. Sind die Zeichenreihen t₁, ... , t_n S-Terme, und ist f ein n-stelliges Funktionssymbol aus S, so ist auch ft₁...t_n ein S-Term.

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

Beispiele

Gegeben sei ein Alphabet mit der Symbolmenge S = {f,g,c}. f sei ein einstelliges Funktionssymbol, g ein zweistelliges Funktionssymbol, und c eine Konstante. Nach dem Kalkül ist die Zeichenreihe

gv₀fc

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

Dagegen ist die Zeichenreihe

gv₀fcc

kein S-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 S-Termen bestehen. Das nächste Zeichen ist v₀, welches nach Regel 1 ein S-Term ist. Somit müsste fcc ein S-Term sein. Da aber auf das einstellige Funktionssymbol f zwei Konstanten (=S-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