# 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 ${\displaystyle Q(a)\lor P(b)}$ is a ground formula, with ${\displaystyle a}$ and ${\displaystyle b}$ being constant symbols. A ground expression is a ground term or ground formula.

## Examples

Consider the following expressions in first order logic over a signature containing a constant symbol ${\displaystyle 0}$  for the number ${\displaystyle 0,}$  a unary function symbol ${\displaystyle s}$  for the successor function and a binary function symbol ${\displaystyle +}$  for addition.

• ${\displaystyle s(0),s(s(0)),s(s(s(0))),\ldots }$  are ground terms,
• ${\displaystyle 0+1,\;0+1+1,\ldots }$  are ground terms,
• ${\displaystyle x+s(1)}$  and ${\displaystyle s(x)}$  are terms, but not ground terms,
• ${\displaystyle s(0)=1}$  and ${\displaystyle 0+0=0}$  are ground formulae,

## Formal definition

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

### Ground terms

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

1. Elements of ${\displaystyle C}$  are ground terms;
2. If ${\displaystyle f\in F}$  is an ${\displaystyle n}$ -ary function symbol and ${\displaystyle \alpha _{1},\alpha _{2},\ldots ,\alpha _{n}}$  are ground terms, then ${\displaystyle f\left(\alpha _{1},\alpha _{2},\ldots ,\alpha _{n}\right)}$  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, ground atom or ground literal is an atomic formula all of whose argument terms are ground terms.

If ${\displaystyle p\in P}$  is an ${\displaystyle n}$ -ary predicate symbol and ${\displaystyle \alpha _{1},\alpha _{2},\ldots ,\alpha _{n}}$  are ground terms, then ${\displaystyle p\left(\alpha _{1},\alpha _{2},\ldots ,\alpha _{n}\right)}$  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 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 ${\displaystyle \lnot p}$  are the same as those of ${\displaystyle p.}$  The free variables of ${\displaystyle p\lor q,p\land q,p\to q}$  are those free variables of ${\displaystyle p}$  or free variables of ${\displaystyle q.}$
3. The free variables of ${\displaystyle \forall x\;p}$  and ${\displaystyle \exists x\;p}$  are the free variables of ${\displaystyle p}$  except ${\displaystyle x.}$