# term

In mathematics , a term is a meaningful combination of numbers , variables , symbols for mathematical links and brackets . Terms can be seen as the syntactically correct formed words or groups of words in the formal language of mathematics.

In practice, the term is often used to talk about individual components of a formula or a larger term. For example, one can speak of a linear term and a constant term for the linear function . ${\ displaystyle f (x) = mx + b}$${\ displaystyle mx}$${\ displaystyle b}$

## Colloquial explanation

The term "term" is used colloquially for anything that has a meaning. In the narrower sense, mathematical structures are meant that can be calculated in principle, at least if the variables contained therein have been assigned values. For example, it is a term, because it has the variables contained therein and a value to, so the term is given a value. Instead of numbers, other mathematical objects can also come into consideration here, for example a term that receives a value when a truth value is assigned to the Boolean variables . In the normal case (single-order logic), however, the exact mathematical definition does not refer to the possible value assignments, as explained below. ${\ displaystyle (x + y) ^ {2}}$${\ displaystyle x}$${\ displaystyle y}$${\ displaystyle (p_ {1} \ vee \ neg p_ {2}) \ wedge p_ {3}}$ ${\ displaystyle p_ {1}, p_ {2}, p_ {3}}$

Roughly one can say that a term is one side of an equation or relation, e.g. B. an inequality is. The equation or relation itself is not a term, it consists of terms.

The following operations can typically be performed with terms:

• calculate (for this you first calculate the "inner" functions and then the outer ones):${\ displaystyle (2 + 3) ^ {2} = 5 ^ {2} = 25}$
• according to certain rules of calculation transform : by applying the distributive law and some other "permitted" rules.${\ displaystyle (x + y) ^ {2} = x ^ {2} + 2xy + y ^ {2}}$
• compare with each other, if relations are defined for the appropriate types: ${\ displaystyle 2xy \ leq x ^ {2} + y ^ {2}}$
• insert into each other (one term is often used instead of a variable of another term). A special form of substitution is substitution , in which a term with variables is replaced by another term with variables (usually a single variable): arises from by replacing by .${\ displaystyle (x + y) ^ {2}}$${\ displaystyle z ^ {2}}$${\ displaystyle z}$${\ displaystyle x + y}$

Often terms or partial terms are named according to their meaning in terms of content. In the term that describes the total energy of a mass point in physics , the first term is called “term of kinetic energy ” and the second “term of potential energy ”. Characteristic properties are often used for naming. So is meant by the “quadratic term” in the partial term because this is the partial term that contains the variable in squared form. ${\ displaystyle {\ tfrac {1} {2}} mv ^ {2} + mgh}$${\ displaystyle x ^ {3} + 7x ^ {2} -2x + 1}$${\ displaystyle 7x ^ {2}}$${\ displaystyle x}$

## Formal definition

The exact mathematical definition of a term, as it is given in mathematical logic , names rules according to which terms are built up. A term is then any expression that results from applying such rules:

• Each variable symbol is a term.${\ displaystyle v}$
• Every constant symbol is a term.${\ displaystyle c}$
• If there is one -place function symbol and there are terms, then is a term.${\ displaystyle f}$${\ displaystyle k}$${\ displaystyle t_ {1}, \ dotsc, t_ {k}}$${\ displaystyle f (t_ {1}, \ dotsc, t_ {k})}$

Let the set of all terms for a given signature and set of variables be simple for terms without variables ( ) . The function symbols induce links of different arity between the elements of or , with which these sets of character strings themselves become an algebraic structure , the term algebra or basic termgebra . See also elementary language: §Terms , logical formulas . ${\ displaystyle {\ boldsymbol {S}}}$${\ displaystyle {\ mathcal {V}}}$${\ displaystyle {\ boldsymbol {\ mathcal {T}}} _ {{\ boldsymbol {S}}, {\ mathcal {V}}}}$${\ displaystyle {\ mathcal {V}} = \ emptyset}$${\ displaystyle {\ boldsymbol {\ mathcal {T}}} _ {\ boldsymbol {S}}}$
${\ displaystyle {\ boldsymbol {\ mathcal {T}}} _ {{\ boldsymbol {S}}, {\ mathcal {V}}}}$${\ displaystyle {\ boldsymbol {\ mathcal {T}}} _ {\ boldsymbol {S}}}$

### Remarks

• If one considers the addition marked with +, according to the above formal definition is a term, but not. Nevertheless, the more easily readable form is preferred; the latter is an alternative, advantageous notation for the correct term . Accordingly, the character string is a name for a term, that is, a metalinguistic expression for a term. As long as it is clear that such character strings could be translated back into the formally correct spelling at any time, if one wanted, there would be no difficulties here.${\ displaystyle + (x, y)}$${\ displaystyle x + y}$${\ displaystyle x + y}$${\ displaystyle + (x, y)}$${\ displaystyle x + y}$
• Some functions (for example the power function, multiplication with variables) are represented by positioning the terms to one another instead of a separate function symbol (for example or )${\ displaystyle x ^ {y}}$${\ displaystyle xy}$
• In the case of nested brackets, [] and {} are sometimes used to make it clearer that the brackets belong together, e.g. B.${\ displaystyle [2 (x + y)] ^ {2}}$
• There are also notation without brackets, such as the Polish notation , but these are usually not that easy to read. The third definition line above is in this notation (compare: first-order predicate logic §Term ):
o   If a k -place function symbol and are terms, then is a term.${\ displaystyle f}$${\ displaystyle t_ {1}, \ dotsc, t_ {k}}$${\ displaystyle ft_ {1}, \ dotsc, t_ {k}}$
• Occasionally the constants are subsumed as zero-digit functions, which is particularly evident in the bracket-free notation.
• There is no mention of a possible insertion of values ​​in the variables, as it occurred in the above slang description. "Term" is a purely syntactic term here, because it only has to comply with certain structure rules. Terms are given a semantic meaning in retrospect by restricting the possible values ​​of variables in so-called models . The terms and are initially different as character strings. However, if one considers these terms in the model of real numbers, it becomes apparent that they always assume the same values. The equality of terms is then to be understood to mean that equality exists for all . This can be wrong for other models, such as the set of - matrices .${\ displaystyle (x + y) ^ {2}}$${\ displaystyle x ^ {2} + 2xy + y ^ {2}}$${\ displaystyle (x + y) ^ {2} = x ^ {2} + 2xy + y ^ {2}}$${\ displaystyle x, y \ in \ mathbb {R}}$${\ displaystyle 2 {\ times} 2}$
• The definition given here does not include terms with bound variables, such as multi-part sums , integrals, or limit values . Since when quantifiers are included in expressions (see below) there are also bound variables, this gives an example of how this could be done. As with expressions, terms without free variables will then be called closed . Your value assignment then does not depend on the variable assignment (see below § Term evaluation ).${\ displaystyle \ sum _ {i = 1} ^ {n} i ^ {2}}$ ${\ displaystyle \ int _ {a} ^ {b} \ sin (k \ cdot t) dt}$ ${\ displaystyle \ lim _ {n \ to \ infty} (2 \ cdot n + 3) / n}$
• Recently, the tree representation of terms has become increasingly important. A detailed description can be found in Kleine Büning (2015).

### example

${\ displaystyle {\ tfrac {xy} {4}}}$ is a term because

• ${\ displaystyle x}$and are terms (as variables),${\ displaystyle y}$
• ${\ displaystyle 4}$ is a term (as a constant),
• ${\ displaystyle xy}$is a term (" "),${\ displaystyle \ operatorname {multiply} (x, y)}$
• ${\ displaystyle {\ tfrac {xy} {4}}}$is a term (the division symbol is the fraction bar ( ) same as , " ")${\ displaystyle -}$${\ displaystyle xy: 4}$${\ displaystyle \ operatorname {divide} (\ operatorname {multiply} (x, y), 4)}$

## Applications

If one forms a term with variables, one often intends in applications to replace these variables with certain values ​​that come from a certain basic set or definition set . For the concept of the term itself, it is not necessary to specify such a set according to the above formal definition. One is then no longer interested in the abstract term, but in a function defined by this term in a certain model.

This is a rule of thumb for calculating the stopping distance (braking distance plus reaction distance) of a car in meters . This string is a term. We intend to substitute for the speed of the car in km per hour, in order to use the value that the term then takes as the braking distance in meters. For example, if a car drives 160 km / h, the formula gives a stopping distance of 304 m. ${\ displaystyle \ left ({\ tfrac {x} {10}} \ right) ^ {2} + \ left ({\ tfrac {x} {10}} \ cdot 3 \ right)}$${\ displaystyle x}$${\ displaystyle \ left ({\ tfrac {160} {10}} \ right) ^ {2} + \ left ({\ tfrac {160} {10}} \ cdot 3 \ right)}$

We use the term here to define the allocation rule of a function , . ${\ displaystyle f \ colon \ mathbb {R} _ {0} ^ {+} \ to \ mathbb {R} _ {0} ^ {+}}$${\ displaystyle x \ mapsto \ left ({\ tfrac {x} {10}} \ right) ^ {2} + \ left ({\ tfrac {x} {10}} \ cdot 3 \ right)}$

Terms themselves are neither true nor false and have no values. Only in a model, that is, with the specification of a basic set for the occurring variables, can terms take on values.

## Algebraic Transformations

Long, complicated terms can often be simplified by applying arithmetic rules to them that leave the value of the term unchanged, for example the commutative law , associative law, or distributive law :

${\ displaystyle (x + y) (xy)}$    Multiply out
${\ displaystyle = x ^ {2} -xy + yx-y ^ {2}}$     Apply commutative law
${\ displaystyle = x ^ {2} -y ^ {2}}$

According to the definition above, the concept of the term does not provide for such transformations, it is a matter of different terms. With these algebraic transformations it is always meant that the values ​​that a term can assume when a certain basic set is chosen, do not change through these transformations. That depends on the basic amount! The above transformations are only correct in those basic sets in which the laws used, such as the commutative law, apply.

Such algebraic transformations are still called term transformations , because according to the rules that apply in the agreed basic set, one can move from one term to another without changing its possible values. The following objectives are pursued:

• Simplification of terms
• Inflating terms to create the desired structures, such as the square extension
• Preparation of the desired partial terms such as the Cardan formula :${\ displaystyle (u + v) ^ {3} = u ^ {3} + v ^ {3} + 3uv (u + v)}$

## Delimitation to expression

### Expressions

An expression is like a term a formal character; their structure is defined according to logic, e.g. B. the predicate logic. In first order predicate logic with equality one defines:

1. Are terms, then is an expression.${\ displaystyle t_ {1}, t_ {2}}$${\ displaystyle t_ {1} = t_ {2}}$
2. Are terms and is a -place relation symbol, then is an expression.${\ displaystyle t_ {1}, \ dotsc, t_ {k}}$${\ displaystyle R}$${\ displaystyle k}$${\ displaystyle Rt_ {1} \ dotso t_ {k}}$
3. Are and expressions, so are , , , , and expressions.${\ displaystyle \ varphi}$${\ displaystyle \ psi}$${\ displaystyle (\ varphi \ land \ psi)}$${\ displaystyle (\ varphi \ lor \ psi)}$${\ displaystyle (\ varphi \ rightarrow \ psi)}$${\ displaystyle (\ varphi \ leftrightarrow \ psi)}$${\ displaystyle (\ exists x \ varphi)}$${\ displaystyle (\ forall x \ varphi)}$

This means that any number of complex expressions can be built up by repeatedly applying these educational laws. According to this definition, terms can roughly be described as what can be on one side of an equation or put in a relation; Terms are precisely these components of expressions.

The exact definition of the expression depends on the logic under consideration; in the second level predicate logic , for example, one also adds the insertion of terms in relation variables and quantifications via relations.

### example

To describe the real numbers one uses the link symbol for the multiplication and the relation symbol for the inequality , furthermore constants like 0, 1, 2, ... If variables are, then by definition also are ${\ displaystyle \ cdot}$${\ displaystyle \ leq}$${\ displaystyle x, y}$

${\ displaystyle x \ cdot x}$, the constant 0 and terms.${\ displaystyle y}$

By definition of the term are

${\ displaystyle x \ cdot x = y}$ and ${\ displaystyle 0 \ leq y}$

Expressions, because the first string is the equality of two terms; the second is a relation in which two terms have been inserted. So that's too

${\ displaystyle 0 \ leq y \ rightarrow (\ exists x (x \ cdot x = y))}$

an expression and finally

${\ displaystyle \ forall y (0 \ leq y \ rightarrow (\ exists x (x \ cdot x = y)))}$

This expression is true in the real number model. It is important to understand that the above structure of the expression is not a proof; it is just a matter of forming a character string according to certain rules. An accompanying statement can only be true or false in a model, where it can be proven if necessary. The above statement is known to be false in the model of the rational numbers, because the rational number is , but there is no rational number that satisfies. ${\ displaystyle y = 2}$${\ displaystyle \ geq 0}$${\ displaystyle x}$${\ displaystyle x \ cdot x = y}$

## Terms in multifaceted logic

When looking at heterogeneous structures such as vector spaces , one likes to divide the objects into different sorts , for example vectors and scalars in vector spaces. The terms that occur are then to be differentiated according to these types. As a further component of the theory, there are therefore a number of variety designators. ${\ displaystyle T}$

Due to the multi-faceted signature , the symbols are not only assigned a simple arithmetic number, but (for relations and functions) a sequence (tuple) of argument types and (for constants and functions) a value type. ${\ displaystyle {\ boldsymbol {S}}}$

With regard to the types of variables, there are essentially two approaches in the literature:

1. A single set of variables is provided. A (possibly only partial) mapping that assigns a variety to variable identifiers is called a variable declaration ; a variable from the domain of the variable declaration is called declared . During the interpretation, this can be replaced by a local variant (locally modified variable declaration) in the scope (area of ​​effect) of the respective quantifier${\ displaystyle {\ mathcal {V}}}$${\ displaystyle \ nu: {\ mathcal {V}} \ not \ to T}$
2. Other authors, on the other hand, strictly delimit the sets of symbols for the variables of different types and use a separate set of variable symbols for each type. The variables are z. B. characterized by a variety index. The assignment of a variety to a variable is fixed and is not modified locally.${\ displaystyle \ nu}$

The type of logical truth values ​​has a special meaning - if available - and is indicated here with . Relations can be understood as predicates according to their characteristic function . In particular, zero-digit relations correspond to logical constants, just as zero-digit functions of an image type correspond to the constants of this type. ${\ displaystyle \ {\ operatorname {false}, \ operatorname {true} \}}$${\ displaystyle \ operatorname {logical}}$

In the recursive definition of the terms, reference is made to their sortness in order to achieve the syntactic properties mentioned in the introduction: Incorrect sort relationships appear as syntax errors.

## Expressions in polyvalent logic

Similar to multi-site terms, given a multi-site signature, the sorts of the arguments and image values ​​are taken into account. The recursive definition of first atomic and then general formulas (expressions) takes place according to this stipulation. Incorrect type assignments are therefore shown as syntax errors.

In the case of flexible variable declarations, it should be noted that locally modified variable declarations are used in the scope (scope) of the quantifiers. In this way, the same variables can be used for different varieties in this case. In the event that a variable is already declared outside the quantifiers, i. H. if the declaration is already in the original definition area , it is overwritten locally. ${\ displaystyle x}$${\ displaystyle x}$${\ displaystyle \ nu}$

## Term evaluation

Given a structure with an interpretation function , the stock of variable names. In the multi-faceted case, there is also a variable declaration by means of a (possibly only partial) mapping . ${\ displaystyle {\ boldsymbol {S}}}$${\ displaystyle {\ mathcal {A}}}$${\ displaystyle \ alpha}$${\ displaystyle {\ mathcal {V}}}$${\ displaystyle \ nu {:} \ {\ mathcal {V}} \ not \ to T}$

Let there be a variable assignment (also variable assignment ) . In the one-sorted case, this is a (possibly only partial) figure , in vielsortigen case was for each variable (assigned any) an element of the value range of the declared grade the image: . ${\ displaystyle \ beta}$${\ displaystyle \ beta {:} \ {\ mathcal {V}} \ not \ to A}$${\ displaystyle x}$${\ displaystyle \ beta (x) \ in A _ {\ nu (x)}}$

The variable assignment assigns a value to the terms as follows: ${\ displaystyle \ beta}$${\ displaystyle t}$${\ displaystyle [\! [t] \!]}$

• ${\ displaystyle [\! [\ color {blue} x \ color {black}] \!] = \ beta (\ color {blue} x \ color {black})}$for variables ,${\ displaystyle \ color {blue} x \ color {black} \ in {\ mathcal {V}}}$
• ${\ displaystyle [\! [\ color {blue} f (t_ {1}, \ dots t_ {n}) \ color {black}] \!] = \ alpha (\ color {blue} f \ color {black} ) ([\! [\ color {blue} t_ {1} \ color {black}] \!], \ dots [\! [\ color {blue} t_ {n} \ color {black}] \!]) }$for a function symbol of arity .${\ displaystyle \ color {blue} f \ color {black}}$${\ displaystyle n = \ sigma (\ color {blue} f \ color {black})}$

Characters and character strings above the entire alphabet are highlighted in blue for clarity:

• On the left is the evaluation of a term, i.e. a character string (finite sequence of symbols).
• On the right side a function (link) is applied to its arguments .${\ displaystyle \ alpha (f)}$${\ displaystyle [\! [t_ {1}] \!], [\! [t_ {2}] \!], \ dots}$

Constants can be understood as zero-digit functions, is explicit

• ${\ displaystyle [\! [c] \!] = \ alpha (c)}$for constants .${\ displaystyle c}$

The mapping is called term evaluation or term assignment . ${\ displaystyle [\! [\] \!]}$

In the multi-site case, the evaluation of a term of the (non-logical) variety results in an object (element) of the range of values . ${\ displaystyle t}$${\ displaystyle s}$${\ displaystyle A_ {s} = \ alpha (s)}$

The term evaluation is a continuation of the variable assignment and the constant interpretation that is compatible with the function interpretation . Term evaluation is defined by two parameters: ${\ displaystyle \ alpha | _ {\ mathcal {F}}}$${\ displaystyle \ beta}$${\ displaystyle \ alpha | _ {\ mathcal {C}}}$${\ displaystyle [\! [\] \!]}$

1. the interpretation function (stands for the structure) and${\ displaystyle \ alpha}$
2. the variable assignment ${\ displaystyle \ beta}$

Assuming that the value ranges are disjoint in pairs, the types of the assigned variables are uniquely determined by their value , so that in this case the additional specification of the variable declaration is not necessary. Therefore, there are also notations in the way   instead . ${\ displaystyle A_ {s}}$${\ displaystyle s = \ nu (x)}$${\ displaystyle x}$${\ displaystyle \ beta (x) \ in A_ {s}}$${\ displaystyle [\! [\] \!] _ {\ alpha, \ beta}}$${\ displaystyle [\! [\] \!]}$

## Validity of expressions

Just as terms with a given structure (expressed by ) and variable assignment ( ) can be evaluated for their value of a (non-logical) variety , expressions can be evaluated for their logical value. Instead of for this validity of expressions (also called truth value or formula assignment ) the notation is usual. This validity is implicitly defined by the following rules: ${\ displaystyle t}$${\ displaystyle \ alpha}$${\ displaystyle \ beta}$${\ displaystyle s}$${\ displaystyle \ varphi}$${\ displaystyle [\! [\ varphi] \!] _ {\ alpha, \ beta}}$${\ displaystyle (\ alpha, \ beta) \ models \ varphi}$

• ${\ displaystyle (\ alpha, \ beta) \ models \ color {blue} x \ color {black} \ Leftrightarrow \ beta (\ color {blue} x \ color {black})}$   possibly for logical variables ${\ displaystyle \ color {blue} x \ color {black} \ in {\ mathcal {V}}}$
• ${\ displaystyle (\ alpha, \ beta) \ models \ color {blue} t_ {1} = t_ {2} \ color {black} \ Leftrightarrow [\! [\ color {blue} t_ {1} \ color {black }] \!] _ {\ alpha, \ beta} \ color {red} = \ color {black} [\! [\ color {blue} t_ {2} \ color {black}] \!] _ {\ alpha , \ beta}}$ for terms ${\ displaystyle \ color {blue} t_ {1} \ color {black}, \ color {blue} t_ {2} \ color {black}}$
• ${\ displaystyle (\ alpha, \ beta) \ models \ color {blue} R (t_ {1}, \ dots t_ {k}) \ color {black} \ Leftrightarrow ([\! [\ color {blue} t_ { 1} \ color {black}] \!] _ {\ Alpha, \ beta}, \ dots [\! [\ Color {blue} t_ {k} \ color {black}] \!] _ {\ Alpha, \ beta}) \ in \ alpha (\ color {blue} R \ color {black})}$   for a relation symbol of arity and terms , in particular${\ displaystyle \ color {blue} R \ color {black}}$${\ displaystyle k = \ sigma (\ color {blue} R \ color {black})}$${\ displaystyle \ color {blue} t_ {1} \ color {black}, \ dots \ color {blue} t_ {k} \ color {black}}$
${\ displaystyle (\ alpha, \ beta) \ models \ color {blue} R \ color {black} \ Leftrightarrow \ epsilon \ in \ alpha (\ color {blue} R \ color {black}) \ Leftrightarrow \ alpha (\ color {blue} R \ color {black}) \ neq \ emptyset \ Leftrightarrow \ alpha (\ color {blue} R \ color {black})}$   possibly for logical constants, d. H. zero-digit relations
• ${\ displaystyle (\ alpha, \ beta) \ models \ color {blue} \ neg \ varphi \ color {black} \ \ \ Leftrightarrow \ \ \ color {red} \ neg \ color {black} (\ alpha, \ beta ) \ models \ color {blue} \ varphi \ color {black}}$ for expressions ${\ displaystyle \ varphi}$
• ${\ displaystyle (\ alpha, \ beta) \ models \ color {blue} \ varphi \ lor \ psi \ color {black} \ \ \ Leftrightarrow \ \ ((\ alpha, \ beta) \ models \ color {blue} \ varphi \ color {black}) \ \; \ color {red} \ lor \ color {black} \ \; ((\ alpha, \ beta) \ models \ color {blue} \ psi \ color {black})}$ for expressions ${\ displaystyle \ color {blue} \ varphi \ color {black}, \ color {blue} \ psi \ color {black}}$
• ${\ displaystyle (\ alpha, \ beta) \ models \ color {blue} \ varphi \ land \ psi \ color {black} \ \ \ Leftrightarrow \ \ ((\ alpha, \ beta) \ models \ color {blue} \ varphi \ color {black}) \ \; \ color {red} \ land \ color {black} \ \; ((\ alpha, \ nu) \ models \ color {blue} \ psi \ color {black})}$
• ${\ displaystyle (\ alpha, \ beta) \ models \ color {blue} \ varphi \ to \ psi \ color {black} \ \ \ Leftrightarrow \ \ ((\ alpha, \ beta) \ models \ color {blue} \ varphi \ color {black}) \ \; \ color {red} \ to \ color {black} \ \; ((\ alpha, \ beta) \ models \ color {blue} \ psi \ color {black})}$
• ${\ displaystyle (\ alpha, \ beta) \ models \ color {blue} \ varphi \ leftrightarrow \ psi \ color {black} \ \ \ Leftrightarrow \ \ ((\ alpha, \ beta) \ models \ color {blue} \ varphi \ color {black}) \ \; \ color {red} \ leftrightarrow \ color {black} \ \; ((\ alpha, \ beta) \ models \ color {blue} \ psi \ color {black})}$
• ${\ displaystyle (\ alpha, \ beta) \ models \ color {blue} \ forall \; x: s \ \ varphi \ color {black} \ \ \ Leftrightarrow \ \ \ color {red} \ forall \ color {black} \; a \ in A _ {\ color {blue} s \ color {black}} \ color {red}: \ color {black} (\ alpha, \ beta _ {\ langle x \ mapsto a \ rangle}) \ models \ color {blue} \ varphi}$, where is a variety, a variable symbol and an expression in which the local variable of the variety occurs.${\ displaystyle \ color {blue} s \ color {black} \ in T}$${\ displaystyle \ color {blue} x \ color {black} \ in {\ mathcal {V}}}$${\ displaystyle \ color {blue} \ varphi \ color {black}}$${\ displaystyle \ color {blue} x \ color {black}}$${\ displaystyle \ color {blue} s \ color {black}}$
• ${\ displaystyle (\ alpha, \ beta) \ models \ color {blue} \ exists \; x: s \ \ varphi \ color {black} \ \ \ Leftrightarrow \ \ \ color {red} \ exists \ color {black} \; a \ in A _ {\ color {blue} s \ color {black}} \ color {red}: \ color {black} (\ alpha, \ beta _ {\ langle x \ mapsto a \ rangle}) \ models \ color {blue} \ varphi}$, where , and as before.${\ displaystyle \ color {blue} s \ color {black}}$${\ displaystyle \ color {blue} x \ color {black}}$${\ displaystyle \ color {blue} \ varphi \ color {black}}$

Characters and character strings above the entire alphabet are highlighted in blue for clarity, in particular the joiners and quantifiers on the left ( object language ). The red marked on the right side are abbreviations for the logical connections etc. of the common language ( metalanguage ) with which the facts are presented, i.e. for "and", "or", "there is one", "for all", “Is the same”, etc. To distinguish it from the quantifier symbols of the object language, z. B. can also be used. ${\ displaystyle \ color {blue} \ forall \ color {black} \ dots, \ color {blue} \ exists \ color {black} \ dots}$${\ displaystyle \ color {red} \ textstyle \ bigwedge \ limits _ {\ color {black} \ dots} \ color {black}, \ color {red} \ textstyle \ bigvee \ limits _ {\ color {black} \ dots }}$

The truth value of sentences ( closed expressions, i.e. without free variables) does not depend on the variable assignment.

In the second level predicate logic with relation variables, two more rules are added, in a multi-faceted normal case these are:

• ${\ displaystyle (\ alpha, \ beta) \ models \ color {blue} \ forall \; X: t \ \ varphi \ color {black} \ \ \ Leftrightarrow \ \ \ color {red} \ forall \ color {black} \; R \ subseteq \ textstyle \ prod A \ circ {\ color {blue} t \ color {black}} \ color {red}: \ color {black} (\ alpha, \ beta _ {\ langle X \ mapsto R \ rangle}) \ models \ color {blue} \ varphi}$, where is the argument type, a relation variable symbol and an expression in which the local relation variable of type occurs.${\ displaystyle \ color {blue} t \ color {black} \ in T ^ {*}}$${\ displaystyle \ color {blue} X \ color {black} \ in {\ mathcal {R}}}$${\ displaystyle \ color {blue} \ varphi \ color {black}}$${\ displaystyle \ color {blue} X \ color {black}}$${\ displaystyle \ color {blue} t}$
• ${\ displaystyle (\ alpha, \ beta) \ models \ color {blue} \ exists \; X: t \ \ varphi \ color {black} \ \ \ Leftrightarrow \ \ \ color {red} \ exists \ color {black} \; R \ subseteq \ textstyle \ prod A \ circ {\ color {blue} t \ color {black}} \ color {red}: \ color {black} (\ alpha, \ beta _ {\ langle X \ mapsto R \ rangle}) \ models \ color {blue} \ varphi}$, where , and as before.${\ displaystyle \ color {blue} t \ color {black} \ in T ^ {*}}$${\ displaystyle \ color {blue} X \ color {black}}$${\ displaystyle \ color {blue} \ varphi \ color {black}}$

In the single-species case, the Cartesian product of the carrier quantities     can be simplified to with arity . Relation variables with fixed arity are usually used (these are often noted as an index), otherwise the arity must be declared: A symbolic representation of further characters is then required for the arity, so the effort is the same or about the same as in the case of several types. ${\ displaystyle \ textstyle \ prod A \ circ {\ color {blue} t \ color {black}} = A _ {\ color {blue} t_ {1} \ color {black}} \ times \ dots A _ {\ color { blue} t_ {k} \ color {black}}}$${\ displaystyle A ^ {k}}$${\ displaystyle k}$${\ displaystyle k \ in \ mathbb {N} _ {0}}$${\ displaystyle \ color {blue} i}$${\ displaystyle \ alpha (\ color {blue} i \ color {black}) = k \ in \ mathbb {N} _ {0}}$

1. See section §Terms in Versatile Logic .
2. What is meant here is an abstract Boolean algebra as a range of values. For the special case of propositional algebra : logical terms versus expressions, see below: §expressions and §expressions in many-sided logic .
3. W. Vogler (2007/2008) p. 3
4. Kruse / Borgelt (2008) p. 4
5. To do this, these terms must first be converted into a linear form (i.e. character strings). With the quantifiers this corresponds to the replacement of the notation with the symbols (similar ) by  . More s. u .: expressions as quasi 'logical terms'.${\ displaystyle \ bigwedge _ {\ dots}, \ bigvee _ {\ dots}}$${\ displaystyle \ sum _ {\ dots}, \ prod _ {\ dots}}$${\ displaystyle \ forall \ dots, \ exists \ dots}$
6. See R. Letz (2004) p. 10
7. Kleine Büning (2015), pp. 8–15
8. or formula
9. The expressions according to points 1 and 2 are called atomic .
10. W. Vogler (2007/2008) p. 5 f
11. A variable is called bound in an expression if it immediately follows the quantifier ( ), otherwise it is called a free variable. Variables can appear in the same expression both freely and bound (locally in the scope of a quantifier). An expression without free variables is called closed or a sentence . See R. Letz (2004) p. 10${\ displaystyle x \ in {\ mathcal {V}}}$${\ displaystyle \ psi}$${\ displaystyle x}$${\ displaystyle \ exists, \ forall, \ dots}$${\ displaystyle x}$
12. In the predicate logic of the second level , these two possibilities also exist in the single-order case with regard to the arity of the relation variables , here you usually find the second variant.
13. Stefan Brass (2005) p. 54
14. Stefan Brass (2005) p. 56
15. A. Oberschelp (1990) page 9ff
16. Erich Grädel (2009) p. 1
17. See Stefan Brass (2005) p. 56 and p. 66–68; and Ramharter, Eder (2015/16) p. 17.
18. C. Lutz (2010) p. 8
19. Kruse, Borgelt (2008) p. 9
20. R. Letz (2004) p. 7. The author uses the notation for the objects (elements of the value ranges of the varieties), for the interpretation function and for the assignment of variables . Instead of is noted, instead of for the term assignment it says .${\ displaystyle u}$${\ displaystyle \ iota}$${\ displaystyle \ alpha}$${\ displaystyle {\ mathcal {A}}}$${\ displaystyle \ beta}$${\ displaystyle \ beta _ {\ langle x \ mapsto a \ rangle}}$${\ displaystyle {\ mathcal {A}} _ {x} ^ {u}}$${\ displaystyle [\! [\] \!] _ {\ alpha, \ beta}}$${\ displaystyle \ iota ^ {\ mathcal {A}}}$
21. Stefan Brass (2005) p. 83
22. In order-sorted logic , the value ranges assigned to the types are not necessarily disjoint. Instead, the set of sorts is given a partial order so that the following applies to all sorts : if , then . Each constant, variable and finally each term of the variety is assigned a variety set ( above set of s), which includes all varieties with . Terms can then be combined if the intersection of the value ranges of their varieties is the value range of a defined variety , i.e. in particular is not empty. Then you write (or ). For more details see A. Oberschelp (1989) page 11ff . This type of logic is the basis of class inheritance (class hierarchy) in object-oriented programming .${\ displaystyle s \ in T}$${\ displaystyle A_ {s}}$${\ displaystyle T}$ ${\ displaystyle \ preceq}$${\ displaystyle s_ {1}, s_ {2}}$${\ displaystyle s_ {1} \ preceq s_ {2}}$${\ displaystyle A_ {s_ {1}} \ subseteq A_ {s_ {2}}}$${\ displaystyle t}$${\ displaystyle s}$${\ displaystyle = \ {r \ in T | s \ preceq r \}}$${\ displaystyle r}$${\ displaystyle s \ preceq r}$${\ displaystyle t_ {1}, t_ {2}}$${\ displaystyle r}$${\ displaystyle r = s_ {1} \ sqcap s_ {2}}$${\ displaystyle r = s_ {1} \ cap s_ {2}}$
23. Kruse, Borgelt (2008) p. 9
24. R. Letz (2004) p. 8
25. a b Stefan Brass (2005) pp. 84-88. The author uses truth tables for the logical connections marked here in color.
26. with${\ displaystyle \ nu (\ color {blue} x \ color {black}) = \ operatorname {logical}}$
27. happy is used to distinguish the equality symbol in the object language instead used.${\ displaystyle \ color {blue} \ equiv}$${\ displaystyle \ color {blue} =}$
28. with ,${\ displaystyle \ epsilon = \ emptyset}$${\ displaystyle \ emptyset = \ operatorname {false}, \ {\ emptyset \} = \ operatorname {true}}$
29. a b is the locally modified variable assignment ( variant), corresponding to the locally modified variable declaration , because of .${\ displaystyle \ beta _ {\ langle x \ mapsto a \ rangle}}$${\ displaystyle x}$${\ displaystyle \ nu _ {\ langle x \ mapsto s \ rangle}}$${\ displaystyle a \ in A_ {s} = \ alpha (s) = \ nu _ {\ langle x \ mapsto s \ rangle} (x)}$
30. R. Letz (2004) p. 10
31. a b is the locally modified relation variable assignment ( variant), corresponding to the locally modified relation variable declaration , because of .${\ displaystyle \ beta _ {\ langle X \ mapsto R \ rangle}}$${\ displaystyle X}$${\ displaystyle \ nu _ {\ langle X \ mapsto \ color {blue} t \ color {black} \ rangle}}$${\ displaystyle R \ subseteq \ textstyle \ prod A \ circ {\ color {blue} t \ color {black}} = \ textstyle \ prod A \ circ \ nu _ {\ langle X \ mapsto t \ rangle} (X) }$
32. For example (line counting) or with = length of or = character for zero, = character for increment ('+1'), or more complex a binary or decimal representation .${\ displaystyle \ color {blue} i \ color {black} = \ underbrace {\ color {blue} || \ color {black} \ dots \ color {blue} | \ color {black}} _ {k {\ text {-times}}}}$${\ displaystyle \ color {blue} i \ color {black} = \ underbrace {\ color {blue} SS \ color {black} \ dots \ color {blue} S \ color {black}} _ {k {\ text { -mal}}} \ color {blue} O \ color {black}}$${\ displaystyle k = | \ color {blue} i \ color {black} |}$${\ displaystyle \ color {blue} i \ color {black}}$${\ displaystyle \ color {blue} O}$${\ displaystyle \ color {blue} S}$

## literature

• Erich Grädel: Mathematical Logic . Mathematical Foundations of Computer Science, SS 2009. RWTH, Aachen, S. 129 ( cs.uni-dortmund.de [PDF]).
• Stefan Brass: Mathematical Logic with Database Applications . Martin Luther University Halle-Wittenberg, Institute for Computer Science, Halle 2005, p. 176 ( informatik.uni-halle.de [PDF]).
• W. Vogler: Logic for computer scientists . WS 2007/2008. Univ. Augsburg, Institute for Computer Science, Augsburg, p. 49 ( informatik.uni-augsburg.de [PDF]).
• R. Kruse, C. Borgelt: Basic concepts of predicate logic . Computational Intelligence. Otto von Guericke University, Magdeburg 2008, p. 14 ( cs.ovgu.de [PDF]).
• Reinhold Letz: Predicate logic . WS 2004/2005. Technical University of Munich, Faculty of Computer Science, Chair of Computer Science IV, Munich, p. 47 ( ifi.lmu.de [PDF]).
• Carsten Lutz: Logic . Lecture in the winter semester 2010. Part 4: Second level predicate logic . University of Bremen, AG Theory of Artificial Intelligence, 2010, p. 65 ( informatik.uni-bremen.de [PDF]).
• Esther Ramharter, Günther Eder: Second level predicate logic . WS 2015/2016. SE modal logic and other philosophically relevant logics . University of Vienna, S. 22 ( univie.ac.at [PDF]).
• Klaus Grue: Object Oriented Mathematics . University of Copenhagen, Department of Computer Science (Datalogisk Institute), 1995, p. 21 ( diku.dk [PDF] General maplet notation, also a notation for locally modified variable declaration and assignment).
• Arnold Oberschelp: Order Sorted Predicate Logic . Ed .: Karl Hans Bläsius, Ulrich Hedtstück, Claus-Rainer Rollinger. Lecture Notes in Computer Science (LNCS), Volume 418 : Sorts and Types in Artificial Intelligence, Workshop, Eringerfeld, FRG, April 24-26, 1989 Proceedings. Springer-Verlag, Berlin Heidelberg 1990, ISBN 3-540-52337-5 , p. 307 , doi : 10.1007 / 3-540-52337-6 .
• H. Kleine Büning: Types and terms . Winter semester 2015. Mod. 05 part 1. University of Paderborn, 2015, p. 15 .