Term (logic)

In mathematical logic, a term denotes a mathematical object while a formula denotes a mathematical fact. In particular, terms appear as components of a formula. This is analogous to natural language, where a noun phrase refers to an object and a whole sentence refers to a fact. A first-order term is recursively constructed from constant symbols, variables and function symbols. An expression formed by applying a predicate symbol to an appropriate number of terms is called an atomic formula, which evaluates to true or false in bivalent logics, given an interpretation. For example, (x+1)*(x+1) is a term built from the constant 1, the variable x, and the binary function symbols + and ; it is part of the atomic formula (x+1)(x+1) \ge 0 which evaluates to true for each real-numbered value of x. Besides in logic, terms play important roles in universal algebra, and rewriting systems. Given a set V of variable symbols, a set C of constant symbols and sets Fn of n-ary function symbols, also called operator symbols, for each natural number n ≥ 1, the set of (unsorted first-order) terms T is recursively defined to be the smallest set with the following properties: every variable symbol is a term: V ⊆ T, every constant symbol is a term: C ⊆ T, from every n terms t1,...,tn, and every n-ary function symbol f ∈ Fn, a larger term f(t1, ..., tn) can be built. Using an intuitive, pseudo-grammatical notation, this is sometimes written as: t ::= x | c | f(t1, ..., tn). The signature of the term language describes which function symbol sets Fn are inhabited. Well-known examples are the unary function symbols sin, cos ∈ F1, and the binary function symbols +, −, ⋅, / ∈ F2. Ternary operations and higher-arity functions are possible but uncommon in practice. Many authors consider constant symbols as 0-ary function symbols F0, thus needing no special syntactic class for them. A term denotes a mathematical object from the domain of discourse. A constant c denotes a named object from that domain, a variable x ranges over the objects in that domain, and an n-ary function f maps n-tuples of objects to objects.