Английская Википедия:Ground expression
Шаблон:Short description 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 <math>a</math> and <math>b</math>, the sentence <math>Q(a) \lor P(b)</math> is a ground formula. A ground expression is a ground term or ground formula.
Examples
Consider the following expressions in first order logic over a signature containing the constant symbols <math>0</math> and <math>1</math> for the numbers 0 and 1, respectively, a unary function symbol <math>s</math> for the successor function and a binary function symbol <math>+</math> for addition.
- <math>s(0), s(s(0)), s(s(s(0))), \ldots</math> are ground terms;
- <math>0 + 1, \; 0 + 1 + 1, \ldots</math> are ground terms;
- <math>0+s(0), \; s(0)+ s(0), \; s(0)+s(s(0))+0</math> are ground terms;
- <math>x + s(1)</math> and <math>s(x)</math> are terms, but not ground terms;
- <math>s(0) = 1</math> and <math>0 + 0 = 0</math> are ground formulae.
Formal definitions
What follows is a formal definition for first-order languages. Let a first-order language be given, with <math>C</math> the set of constant symbols, <math>F</math> the set of functional operators, and <math>P</math> the set of predicate symbols.
Ground term
A Шаблон:Visible anchor is a term that contains no variables. Ground terms may be defined by logical recursion (formula-recursion):
- Elements of <math>C</math> are ground terms;
- If <math>f \in F</math> is an <math>n</math>-ary function symbol and <math>\alpha_1, \alpha_2, \ldots, \alpha_n</math> are ground terms, then <math>f\left(\alpha_1, \alpha_2, \ldots, \alpha_n\right)</math> 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 Шаблон:Visible anchor, Шаблон:Visible anchor or Шаблон:Visible anchor is an atomic formula all of whose argument terms are ground terms.
If <math>p \in P</math> is an <math>n</math>-ary predicate symbol and <math>\alpha_1, \alpha_2, \ldots, \alpha_n</math> are ground terms, then <math>p\left(\alpha_1, \alpha_2, \ldots, \alpha_n\right)</math> is a ground predicate or ground atom.
Roughly speaking, the Herbrand base is the set of all ground atoms,[1] while a Herbrand interpretation assigns a truth value to each ground atom in the base.
Ground formula
A Шаблон:Visible anchor or Шаблон:Visible anchor is a formula without variables.
Ground formulas may be defined by syntactic recursion as follows:
- A ground atom is a ground formula.
- If <math>\varphi</math> and <math>\psi</math> are ground formulas, then <math>\lnot \varphi</math>, <math>\varphi \lor \psi</math>, and <math>\varphi \land \psi</math> are ground formulas.
Ground formulas are a particular kind of closed formulas.
See also
References
