Ground expression

Ground expression

A ground expression in mathematical logic is an expression of a logical language (mainly, of a first-order language) that doesn't contain variables, but only logical constants. For example, any expression of a zero-order language is ground.

Expressively, as an intuitive or everyday-interpretation, we can imagine that a ground expression signs the „concrete”, „well-determined” and „fixed” things and judgements, and a non-ground expression signs an indeterminate or general thing or proposition. But this is only fuzzy philosophy, the exact definition of ground expressions can be found below.

The terms "ground expression", "ground term" and "ground formula" are sometimes used for expressions that contain no free variables. In this weaker sense, a lambda expression like is a ground term. For formulae of a logic, the term "sentence" is also used for this.

Don't confuse ...

... ground expressions and ground pieces of an expression. The former is an expression of the language, and its existence doesn't depend on an interpretation. The latter is a formal expression too, but it's not part of the original language, because it contains symbols of universe elements (where the universe is the universe of the interpretation). Because simple things entropically have to become complicated, in the theory of Herbrand interpretations, ground pieces of a term above the set of the constant symbols of the language are called simple ground terms. But this is more or less correct, because these expressions are parts of the language, with universe of a Herbrand-interpretation is (telling it inexactly) primarily the set of the constant symbols of the language.

Classifying ground expressions

Because expressions of a language can be divided into terms, atoms and formulae, we can classify ground expressions in a similar way. There are:

  1. ground terms, expressions which do not contain variables (only constant signs) and functions,
  2. ground atoms, which are predicates consisting only of ground terms
  3. ground formulae which are composed from ground atoms.

None of these contain variables or are composed from variables.


Consider the first order logic describing the natural numbers, where 0 signs the zero constant, and s(x) is the function of "direct following", s(x) = x+1, where + denotes addition. Then

  • 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(z)=1 and ∀x: (s(x)+1=s(s(x))) are expressions, but are not ground expressions.

Ground expressions are necessarily closed. The last example, ∀x: (s(x)+1=s(s(x))), shows that a closed expression is not necessarily a ground expression. So, this formula is a closed formula, but not a ground formula, because it contains a logical variable, even though that variable is not free.

Formal definition

What follows is a formal definition for first-order languages. Let a first-order language be given, with the 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 is an atomic formula all of whose terms are ground terms. That is,

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 all of whose arguments are ground atoms.

Ground formulae may be defined by syntactic recursion as follows:

  1. A ground atom is a ground formula; that is, if pP is an n-ary predicate symbol and α1, α2 , ..., αn are ground terms, then p1, α2 , ..., αn) is a ground formula (and is a ground atom);
  2. If p and q are ground formulae, then ¬(p), (p)∨(q), (p)∧(q), (p)→(q), formulas composed with logical connectives, are ground formulae, too.
  3. If p is a ground formula and we can get q from it that way some (or ) we delete or insert in the p formula, and then the result, q is well-formed and equivalent with p, then q is a ground formula.
  4. We can get all ground formulae applying these three rules.

Search another word or see Ground expressionon Dictionary | Thesaurus |Spanish
Copyright © 2015, LLC. All rights reserved.
  • Please Login or Sign Up to use the Recent Searches feature