| Ground Expression |
Article Index for Ground |
Website Links For Ground |
Information AboutGround Expression |
| CATEGORIES ABOUT GROUND EXPRESSION | |
| mathematical logic | |
|
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 . DON'T MIX UP ... ... ''ground expression''s and ''ground pieces of an expression''. The upper is an expression of the language, and its existence don't depend on an interpretation. The ground piece of an expression 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 of 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 term''s. But this is more or less correct, 'cause these expressions are parts of the language, sith universe of a Herbrand-interpretation is (telling it inexactly) primarily the set of the constant symbols of the language. CLASSIFYING GROUND EXPRESSIONS Because of expressions of a language can be divided into terms and formulae, we can classify ground expressions in a similar way, so there are: # ground terms, expressions what don't contain logical variables (only constant signs) and predicate symbols, # ground formulae contain predicate symbols, but no individuum variable. EXAMPLES E.g. above the FOL describing Natural Number s, if 0 signs the Zero constant, s(x) the function of "direct following" (you know s(x) = x+1), + the addition, then
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. FORMAL DEFINITION We give this in first-order languages. Given an FOL, with the sets of constant symbols, individuum variables, functional operators, predicate symbols. Ground terms We can apply logical recursion (formula-recursion): # elements of C are GT-s; # If f∈F n-ary function symbol and α1, α2 , ..., αn are GT-s, then f(α2 , ..., αn) is a GT, too. # Every GT can be given by finite applying those two rules. Ground formulae Applying syntactic recursion we can define the idea of ground formula like this: # If p∈P n-ary predicate symbol and α1, α2 , ..., αn are Ground Terms , then p(α1, α2 , ..., αn) is a ground formula; # If p and q are ground formulae, then ¬(p), (p)∨(q), (p)∧(q), (p)→(q) 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 this three rules. |
|
|