Ground expression
Encyclopedia
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 first-order logic
all closed terms are ground terms, but in lambda calculus
the closed term 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 first-order logic with identity, the sentence x (x=x) is not a ground formula.
A ground expression is a ground term or ground formula.
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.
the set of constant symbols, 
the set of (individual) variables, 
the set of functional operators, and 
the set of predicate symbols.
that contain no variables. They may be defined by logical recursion (formula-recursion):
Roughly speaking, the Herbrand universe is the set of all ground terms.
all of whose terms are ground terms. That is,
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.
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 formulae may be defined by syntactic recursion as follows:
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, a ground term of a formal system
Formal system
In formal logic, a formal system consists of a formal language and a set of inference rules, used to derive an expression from one or more other premises that are antecedently supposed or derived . The axioms and rules may be called a deductive apparatus...
is a term
Term (logic)
In mathematical logic, universal algebra, and rewriting systems, terms are expressions which can be obtained from constant symbols, variables and function symbols...
that does not contain any variables at all, and a closed term is a term that has no free variables. In first-order logic
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
all closed terms are ground terms, but in lambda calculus
Lambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...
the closed term 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 first-order logic with identity, the sentence x (x=x) is not a ground formula.
A ground expression is a ground term or ground formula.
Examples
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.- 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 the set of constant symbols, the set of (individual) variables, the set of functional operators, and the set of predicate symbols.Ground terms
Ground terms are termsTerm (logic)
In mathematical logic, universal algebra, and rewriting systems, terms are expressions which can be obtained from constant symbols, variables and function symbols...
that contain no variables. They may be defined by logical recursion (formula-recursion):
- elements of C are ground terms;
- If f∈F is an n-ary function symbol and α1, α2 , ..., αn are ground terms, then f(α1, α2 , ..., αn) is a ground term.
- 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 formulaAtomic formula
In mathematical logic, an atomic formula is a formula with no deeper propositional structure, that is, a formula that contains no logical connectives or equivalently a formula that has no strict subformulas. Atoms are thus the simplest well-formed formulas of the logic...
all of whose terms are ground terms. That is,
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.
Roughly speaking, the Herbrand base is the set of all ground atoms, while a Herbrand interpretation
Herbrand interpretation
In mathematical logic, a Herbrand interpretation is an interpretation in which all constants and function symbols are assigned very simple meanings. Specifically, every constant is interpreted as itself, and every function symbol is interpreted as the function that applies it...
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:
- A ground atom is a ground formula; that is, if p∈P is an n-ary predicate symbol and α1, α2 , ..., αn are ground terms, then p(α1, α2 , ..., αn) is a ground formula (and is a ground atom);
- If p and q are ground formulae, then ¬(p), (p)∨(q), (p)∧(q), (p)→(q), formulas composed with logical connectiveLogical connectiveIn logic, a logical connective is a symbol or word used to connect two or more sentences in a grammatically valid way, such that the compound sentence produced has a truth value dependent on the respective truth values of the original sentences.Each logical connective can be expressed as a...
s, are ground formulae, too. - 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.
- We can get all ground formulae applying these three rules.