Term calculus

As Term calculus is referred to in the mathematical logic those calculus by means of which to correct all terms over an alphabet can produce.

To do this, be an alphabet with a corresponding set of symbols . -Terms are then exactly those strings that can be generated by applying the following rules finitely. ${\displaystyle A_{S}}$ ${\displaystyle S}$ ${\displaystyle S}$

1. Each variable is a term. ${\displaystyle S}$
2. Every constant from is a term. ${\displaystyle S}$ ${\displaystyle S}$
3. If the character rows -Terme, and is a -ary function symbol , so is a -term. ${\displaystyle t_{1},\ldots ,t_{n}}$ ${\displaystyle S}$ ${\displaystyle f}$ ${\displaystyle n}$ ${\displaystyle S}$ ${\displaystyle ft_{1},\ldots ,t_{n}}$ ${\displaystyle S}$

Conversely, if any series of signs is given, then one can use the calculus to determine whether this is a term by applying the rules of the calculus in the opposite direction. ${\displaystyle A_{S}}$ ${\displaystyle S}$

Examples

Given is an alphabet with the set of symbols . be a one-digit function symbol, a two-digit function symbol, and a constant. After the calculus is the series of symbols ${\displaystyle S=\lbrace f,g,c\rbrace }$ ${\displaystyle f}$ ${\displaystyle g}$ ${\displaystyle c}$

${\displaystyle gv_{0}fc}$

a term. According to rule 1 there is a term. According to rule 2, there is a term. From rule 3 applied to and it follows that there is also a term. Repeated application of Rule 3 on , and provides that the above characters series one is -term. Enforcing brackets you can clarify this: . ${\displaystyle S}$ ${\displaystyle v_{0}}$ ${\displaystyle S}$ ${\displaystyle c}$ ${\displaystyle S}$ ${\displaystyle f}$ ${\displaystyle c}$ ${\displaystyle fc}$ ${\displaystyle S}$ ${\displaystyle g}$ ${\displaystyle v_{0}}$ ${\displaystyle fc}$ ${\displaystyle S}$ ${\displaystyle gv_{0}fc=g(v_{0}f(c))}$

Against this is the string of characters

${\displaystyle gv_{0}fcc}$

no term. It begins with the two-digit function symbol g . If the symbol g was removed from the string, the remaining string v ₀ fcc would have to consist of exactly two -terms written one behind the other . The next character is v ₀ , which according to rule 1 is a term. So fcc should be a term. However, since the one-digit function symbol f is followed by two constants (= terms), this is not the case. ${\displaystyle S}$ ${\displaystyle S}$ ${\displaystyle S}$ ${\displaystyle S}$ ${\displaystyle S}$

literature

• H.-D. Ebbinghaus, J. Flum, W. Thomas: Introduction to mathematical logic , Heidelberg, Berlin: Spectrum 1996. ISBN 3-8274-0130-5