Ground expression

---

title: "Ground expression" type: doc version: 1 created: 2026-02-28 author: "Wikipedia contributors" status: active scope: public tags: ["logical-expressions", "mathematical-logic"] description: "Term that does not contain any variables" topic_path: "science/mathematics" source: "https://en.wikipedia.org/wiki/Ground_expression" license: "CC BY-SA 4.0" wikipedia_page_id: 0 wikipedia_revision_id: 0

::summary Term that does not contain any variables ::

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.

Examples

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.

Formal 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):

1. Elements of C are ground terms;
2. 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.
3. 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:

1. A ground atom is a ground formula.
2. 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.

Notes

References

References

1. Alex Sakharov. "Ground Atom".

::callout[type=info title="Wikipedia Source"] This article was imported from Wikipedia and is available under the Creative Commons Attribution-ShareAlike 4.0 License. Content has been adapted to SurfDoc format. Original contributors can be found on the article history page. ::