Encyclopedia

Ground expression

Term that does not contain any variables

Wikipedia contributorsAdapted for Fathomly · View authors

2 min read
Source updated May 10, 2025

In mathematical logic, a ground term of a formal system is a term that does not contain any variables. Similarly, a ground formula is a formula that does not contain any variables.

In first-order logic with identity with constant symbols $a$ and $b$ , the sentence $Q(a)\lor P(b)$ is a ground formula. A ground expression is a ground term or ground formula.

01Examples

Consider the following expressions in first order logic over a signature containing the constant symbols $0$ and $1$ for the numbers 0 and 1, respectively, a unary function symbol $s$ for the successor function and a binary function symbol $+$ for addition.

$s(0),s(s(0)),s(s(s(0))),\ldots$ are ground terms;
$0+1,\;0+1+1,\ldots$ are ground terms;
$0+s(0),\;s(0)+s(0),\;s(0)+s(s(0))+0$ are ground terms;
$x+s(1)$ and $s(x)$ are terms, but not ground terms;
$s(0)=1$ and $0+0=0$ are ground formulae.

02Formal definitions

What follows is a formal definition for first-order languages. Let a first-order language be given, with $C$ the set of constant symbols, $F$ the set of functional operators, and $P$ the set of predicate symbols.

Ground term

A ground term is a term that contains no variables. Ground terms may be defined by logical recursion (formula-recursion):

Elements of $C$ are ground terms;
If $f\in F$ is an $n$ -ary function symbol and $\alpha _{1},\alpha _{2},\ldots ,\alpha _{n}$ are ground terms, then $f\left(\alpha _{1},\alpha _{2},\ldots ,\alpha _{n}\right)$ is a ground term.
Every ground term can be given by a finite application of the above two rules (there are no other ground terms; in particular, predicates cannot be ground terms).

Roughly speaking, the Herbrand universe is the set of all ground terms.

Ground atom

A ground predicate, ground atom or ground literal is an atomic formula all of whose argument terms are ground terms.

If $p\in P$ is an $n$ -ary predicate symbol and $\alpha _{1},\alpha _{2},\ldots ,\alpha _{n}$ are ground terms, then $p\left(\alpha _{1},\alpha _{2},\ldots ,\alpha _{n}\right)$ is a ground predicate or ground atom.

Roughly speaking, the Herbrand base is the set of all ground atoms, while a Herbrand interpretation assigns a truth value to each ground atom in the base.

Ground formula

A ground formula or ground clause is a formula without variables.

Ground formulas may be defined by syntactic recursion as follows:

A ground atom is a ground formula.
If $\varphi$ and $\psi$ are ground formulas, then $\lnot \varphi$ , $\varphi \lor \psi$ , and $\varphi \land \psi$ are ground formulas.

Ground formulas are a particular kind of closed formulas.

Watch videos about Ground expressionExplainers and documentaries on YouTube (opens in a new tab)

Sources and credits

This article is adapted from the Wikipedia article “Ground expression”, written by its contributors and licensed under CC BY-SA 4.0. Fathomly has changed the layout, removed citation markers, navigation and maintenance notices, and adjusted punctuation. This adapted version is shared under the same license. For references, see the original article.

Fathomly is not affiliated with or endorsed by the Wikimedia Foundation. Spotted a problem? Tell us.