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_{1},\ldots ,t_{n}$ $S$-Terme, und ist $f$ ein $n$-stelliges Funktionssymbol aus $S$, so ist auch $ft_{1},\ldots ,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=\lbrace f,g,c\rbrace$. $f$ sei ein einstelliges Funktionssymbol, $g$ ein zweistelliges Funktionssymbol, und $c$ eine Konstante. Nach dem Kalkül ist die Zeichenreihe

$gv_{0}fc$

ein $S$-Term. Nach Regel 1 ist nämlich $v_{0}$ 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_{0}$, und $fc$ liefert, dass auch die obige Zeichenreihe ein $S$-Term ist. Durch Setzen von Klammern kann man das verdeutlichen: $gv_{0}fc=g(v_{0}f(c))$.

Dagegen ist die Zeichenreihe

$gv_{0}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