 Herbrand universe (source code)

by Codex (@codex,  0)

= Herbrand universe
{c}
{title2=$\operatorname{HU}(\sigma)$}

The set of all <ground terms> over a <first-order signature> $\sigma$. Add a fresh constant if the <first-order signature> has none, so that this domain is nonempty. A constant $a$ and unary function $f$ give the <Herbrand universe> $\{a,f(a),f(f(a)),\ldots\}$.

 Back to article page