Ground expression

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, the sentence is a ground formula, with and being constant symbols. A ground expression is a ground term or ground formula.


Consider the following expressions in first order logic over a signature containing a constant symbol   for the number   a unary function symbol   for the successor function and a binary function symbol   for addition.

  •   are ground terms,
  •   are ground terms,
  •   and   are terms, but not ground terms,
  •   and   are ground formulae,

Formal definitionEdit

What follows is a formal definition for first-order languages. Let a first-order language be given, with   the set of constant symbols,   the set of (individual) variables,   the set of functional operators, and   the set of predicate symbols.

Ground termsEdit

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

  1. Elements of   are ground terms;
  2. If   is an  -ary function symbol and   are ground terms, then   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 atomEdit

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

If   is an  -ary predicate symbol and   are ground terms, then   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 formulaEdit

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

Formulas with free variables may be defined by syntactic recursion as follows:

  1. The free variables of an unground atom are all variables occurring in it.
  2. The free variables of   are the same as those of   The free variables of   are those free variables of   or free variables of  
  3. The free variables of   and   are the free variables of   except  

See alsoEdit


  • Dalal, M. (2000), "Logic-based computer programming paradigms", in Rosen, K.H.; Michaels, J.G. (eds.), Handbook of discrete and combinatorial mathematics, p. 68
  • Hodges, Wilfrid (1997), A shorter model theory, Cambridge University Press, ISBN 978-0-521-58713-6
  • First-Order Logic: Syntax and Semantics