Ground expression

From Wikipedia, the free encyclopedia

Ground expression in mathematical logic is an expression of a logical language (mainly, of a first-order language) what doesn't contain logical (individual-) variables. E.g. all 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.

Contents 1 Don't mix up ... 2 Classifying ground expressions 3 Examples 4 Formal definition 4.1 Ground terms 4.2 Ground formulae

[edit] Don't mix up ...

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

[edit] Classifying ground expressions

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

1. ground terms, expressions which do not contain logical variables (only constant signs) and predicate symbols,
2. ground formulae contain predicate symbols, but no individual variables.

[edit] Examples

E.g. above the FOL describing natural numbers, if 0 signs the zero constant, s(x) the function of "direct following" (you know s(x) = x+1), + the addition, then

• s(0), s(s(0)), s(s(s(0))) ... stb. are GT-s;
• 0+1, 0+1+1, ... are GT-s too.
• x+s(1) and s(x) are terms, but not ground terms;
• s(0)=1 és 0+0=0 are ground formulae;
• but then s(z)=1 and ∀x: (s(x)+1=s(s(x))) aren't ground expressions.

The last example ∀x: (s(x)+1=s(s(x))) shows that albeit a ground expression must be closed, but not v. versa. ∀x: (s(x)+1=s(s(x))) is a closed formula, but not a ground formula, 'cause contains logical variable, despite of that this is not free.

[edit] Formal definition

We give this in first-order languages.

Given an FOL, with the sets of C constant symbols, V individuum variables, F functional operators, P predicate symbols.

[edit] Ground terms

We can apply logical recursion (formula-recursion):

1. elements of C are GT-s;
2. If f∈F n-ary function symbol and α₁, α₂ , ..., α_n are GT-s, then f(α₂ , ..., α_n) is a GT, too.
3. Every GT can be given by finite applying those two rules.

[edit] Ground formulae

Applying syntactic recursion we can define the idea of ground formula like this:

1. If p∈P n-ary predicate symbol and α₁, α₂ , ..., α_n are ground terms, then p(α₁, α₂ , ..., α_n) is a ground formula;
2. If p and q are ground formulae, then ¬(p), (p)∨(q), (p)∧(q), (p)→(q) are ground formulae, too.
3. 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.
4. We can get all ground formulae applying this three rules.