Term algebra

In universal algebra and mathematical logic, a term algebra or Herbrand universe is a freely generated algebraic structure. For example, in a signature consisting of a single binary relation, the term algebra over a set X of variables is exactly the free magma generated by X.

Term algebras play a role in the semantics of abstract data types, where an abstract data type declaration provides the signature of a multi-sorted algebraic structure and the term algebra is a concrete model of the abstract declaration.

The Herbrand base is analogous to the Herbrand universe, but consists of formulas. It is the set of all ground atoms.

Definition

Given a signature σ and a set X of variables, the term algebra over X (of signature σ) consists of all σ-terms that contain at most the variables in X. Formally, it is the smallest set T_σ(X) with the following properties:

• T_σ(X) contains X as a subset.
• For every n-ary function f in σ and all strings a₁, …, a_n in T_σ(X), the string f(a₁, …, a_n) is also in T_σ(X).

It follows from the second condition that T_σ(X) contains the constants of σ as a subset.

If X is empty and σ contains no constant symbols, the term algebra over X is also empty. The term algebra over X is finite if and only if σ and X are finite and σ contains no function symbols other than constant symbols.

The Herbrand universe of signature σ is the term algebra over the empty set, i.e. it consists of all ground terms of the signature. Instead of working with the term algebra over a set X, it is customary in mathematical logic to treat the elements of X as constants and use the Herbrand universe of the extended signature σ $\cup$ X. The Herbrand universe is named after Jacques Herbrand.

Decidability of term algebras

Term algebras can be shown decidable using quantifier elimination. The complexity of the decision problem is in NONELEMENTARY.

Herbrand base

The Herbrand base of signature σ consists of all ground atoms of σ: of all formulas of the form R(t₁, …, t_n), where t₁, …, t_n are terms containing no variables (i.e. elements of the Herbrand universe) and R is an n-ary relation symbol. In the case of logic with equality, it also contains all equations of the form t₁=t₂, where t₁ and t₂ contain no variables.

See also

• Domain of discourse / Universe (mathematics)
• Herbrand interpretation / Herbrand structure

References

• Anatolii Ivanovic Mal'cev: "The Metamathematics of Algebraic Systems". North-Holland, 1971. (Studies in Logic and The Foundations of Mathematics, Volume 66)
• Weisstein, Eric W. "Herbrand Universe". MathWorld.

External links

The Herbrand Universe, Herbrand Base and Herbrand Interpretations Some examples.