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.
... 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.
Because expressions of a language can be divided into terms, atoms and formulae, we can classify ground expressions in a similar way. There are:
None of these contain variables or are composed from variables.
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.
What follows is a formal definition for first-order languages. Let a first-order language be given, with the the set of constant symbols, the set of (individual) variables, the set of functional operators, and the set of predicate symbols.
Roughly speaking, the Herbrand universe is the set of all ground terms.
If p∈P is an n-ary predicate symbol and α1, α2 , ..., αn are ground terms, then p(α1, α2 , ..., αn) is a ground predicate or ground atom.
Ground formulae may be defined by syntactic recursion as follows: