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