Ground atom

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

Similarly, a ground formula is a formula that does not contain any free variables. In first-order logic with identity, the sentence \forall x (x=x) is a ground formula.

A ground expression is a ground term or ground formula.


Consider the following expressions from first order logic over a signature containing a constant symbol 0 for the number 0, 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))) ... are ground terms;
  • 0+1, 0+1+1, ... 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;
  • s(1) and ∀x: (s(x)+1=s(s(x))) are ground expressions.

Formal definition

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

Ground terms

Ground terms are terms that contain no variables. They may be defined by logical recursion (formula-recursion):

  1. elements of C are ground terms;
  2. If fF is an n-ary function symbol and α1, α2, ..., αn are ground terms, then f1, α2, ..., αn) 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 or ground atom or ground literal is an atomic formula all of whose argument terms are ground terms.

If pP is an n-ary predicate symbol and α1, α2, ..., αn are ground terms, then p1, α2, ..., αn) 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 free 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 ¬p are the same as those of p. The free variables of pq, pq, pq are those free variables of p or free variables of q.
  3. The free variables of \forall x p and \exists x p are the free variables of p except x.


  • First-Order Logic: Syntax and Semantics
This article was sourced from Creative Commons Attribution-ShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for and content contributors is made possible from the U.S. Congress, E-Government Act of 2002.
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a non-profit organization.