Termkalkül

Als Termkalkül bezeichnet m​an in d​er mathematischen Logik j​enen Kalkül, mittels welchem m​an alle korrekten Terme über e​inem Alphabet erzeugen kann.

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

1. Jede Variable ist ein ${\displaystyle S}$ -Term.
2. Jede Konstante aus ${\displaystyle S}$ ist ein ${\displaystyle S}$ -Term.
3. Sind die Zeichenreihen ${\displaystyle t_{1},\ldots ,t_{n}}$ ${\displaystyle S}$ -Terme, und ist ${\displaystyle f}$ ein ${\displaystyle n}$ -stelliges Funktionssymbol aus ${\displaystyle S}$ , so ist auch ${\displaystyle ft_{1},\ldots ,t_{n}}$ ein ${\displaystyle S}$ -Term.

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

Beispiele

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

${\displaystyle gv_{0}fc}$

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

Dagegen i​st die Zeichenreihe

${\displaystyle gv_{0}fcc}$

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