In mathematical logic, a ground term of a formal system is a term that does not contain any variables at all, and a closed term is a term that has no free variables. In firstorder logic all closed terms are ground terms, but in lambda calculus the closed term λ x. x (λ y. y) is not a ground term.
Similarly, a ground formula is a formula that does not contain any variables, and a closed formula or sentence is a formula that has no free variables. In firstorder logic with identity, the sentence x (x=x) is not a ground formula.
A ground expression is a ground term or ground formula.
Contents 
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.
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 firstorder languages. Let a firstorder 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 are terms that contain no variables. They may be defined by logical recursion (formularecursion):
Roughly speaking, the Herbrand universe is the set of all ground terms.
A ground predicate or ground atom is an atomic formula all of whose terms are ground terms. That is,
If p∈P is an nary predicate symbol and α_{1}, α_{2} , ..., α_{n} are ground terms, then p(α_{1}, α_{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.
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:
