Added to Favorites

Related Searches

Definitions

Nearby Words

A ground expression in mathematical logic is an expression of a logical language (mainly, of a first-order language) that doesn't contain variables, but only logical constants. For example, any expression of a zero-order language is ground.

Expressively, as an intuitive or everyday-interpretation, we can imagine that a ground expression signs the „concrete”, „well-determined” and „fixed” things and judgements, and a non-ground expression signs an indeterminate or general thing or proposition. But this is only fuzzy philosophy, the exact definition of ground expressions can be found below.

The terms "ground expression", "ground term" and "ground formula" are sometimes used for expressions that contain no free variables. In this weaker sense, a lambda expression like is a ground term. For formulae of a logic, the term "sentence" is also used for this.

... ground expressions and ground pieces of an expression. The former is an expression of the language, and its existence doesn't depend on an interpretation. The latter is a formal expression too, but it's not part of the original language, because it contains symbols of universe elements (where the universe is the universe of the interpretation). Because simple things entropically have to become complicated, in the theory of Herbrand interpretations, ground pieces of a term above the set of the constant symbols of the language are called simple ground terms. But this is more or less correct, because these expressions are parts of the language, with universe of a Herbrand-interpretation is (telling it inexactly) primarily the set of the constant symbols of the language.

Because expressions of a language can be divided into terms, atoms and formulae, we can classify ground expressions in a similar way. There are:

- ground terms, expressions which do not contain variables (only constant signs) and functions,
- ground atoms, which are predicates consisting only of ground terms
- ground formulae which are composed from ground atoms.

None of these contain variables or are composed from variables.

Consider the first order logic describing the natural numbers, where 0 signs the zero constant, and s(x) is the function of "direct following", s(x) = x+1, where + denotes addition. Then

- 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.

What follows is a formal definition for first-order languages. Let a first-order 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.

- 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.

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:

- 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 connectives, 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.

Wikipedia, the free encyclopedia © 2001-2006 Wikipedia contributors (Disclaimer)

This article is licensed under the GNU Free Documentation License.

Last updated on Monday September 15, 2008 at 16:30:14 PDT (GMT -0700)

View this article at Wikipedia.org - Edit this article at Wikipedia.org - Donate to the Wikimedia Foundation

This article is licensed under the GNU Free Documentation License.

Last updated on Monday September 15, 2008 at 16:30:14 PDT (GMT -0700)

View this article at Wikipedia.org - Edit this article at Wikipedia.org - Donate to the Wikimedia Foundation

Copyright © 2015 Dictionary.com, LLC. All rights reserved.