« previous section | next section » |
In this subsection we introduce more formal approach to predicate
calculus, carefully separating the syntax of the language from the
meaning of its expressions, i.e. we precisely define the language and
its semantics.
Let V0 be the set of propositional variables, V be the set of individual variables (variables which cross domain is different than {true, false}), Ρ - the set of names for relations and Φ - the set of names for functions. The well-formed expressions of the predicate language are terms (that correspond to algebraic expressions) and formulas (that correspond to Boolean expressions or propositional functions).
Definition 7.4.1
The set of terms is the smallest set including V and such that, if f is a name of an n-argument function and t1, ..., tn are terms, then f(t1, ...,tn) is a term.
The set of formulas is the smallest set of expressions including the set of propositional variables V0 and such that
Remark. In the case of the two-argument function's or relation' s name, its symbol is traditionally placed between the arguments e.g. we write (x+y) instead of +(x,y), as in the above definition.
Example 7.4.1
If x and y are individual variables, "<" is a symbol of the
two-argument relation and "+", "*" are symbols of the two-argument
operations, then ((x+y)*x) is a term and ((x+y)* x)<(x+y)), ( ∀
x) ((x+y)* x)<(x+y)), ( ∃
x) (x>x*x ∨ ( ∀
y)((x+y)* x<(x+y)) ) are formulas.
In order to calculate the value of a propositional formula it is necessary and enough to know the values of all its propositional variables. The formulas of predicate calculus are constructed with variables, functions and relations. Usually we cannot estimate the value of the formula without knowing the meaning of these symbols. The question about the value of the expression ( ∀ x)( ∃ y) (x ⊕ y > x) must wait for an answer until we establish the space of values for individual variables x, y and the interpretation of the operation ⊕ and the relation >.
Thus, in order to define semantics of predicate calculus we firstly need to determine a domain for individual variables and an interpretation of functional and predicate symbols in this set. A set together with the interpretation of functional and relational symbols in it, we call an algebraic structure (the lecture 10 is devoted to the issue of algebraic structures). A sequence of values for the variables is called a valuation. For convenience, we treat the valuations as functions which ascribe values to the variables from the set V0 ∪ V. Because every formula has a finite number of variables, then not all values of variables are crucial for us to calculate its value.
Let STR be some arbitrary algebraic structure. Let us denote by tSTR(v) the value of the term t interpreted in the structure STR at the valuation v. We assume the following recursive definition of the term's meaning:
tSTR(v) = v(x), if t is just the individual variable x and
tSTR(v) = fSTR(t1(v),..., tn(v)), when t is of the form f(t1,..., tn) and fSTR is an n-argument operation in STR being interpretation of functional symbol f.
Example 7.4.2
Let's consider the term ((x ⊕ y) ⊗ z) in which x, y, z are individual variables and ⊕, ⊗ are two-argument operations. If we interpret this term over the structure of real numbers, then assuming that ⊕ is the sum operator and ⊗ is the multiplication symbol, and v is a valuatuion such that v(x)=2, v(y)= 3, v(z)=5, the final value of the considered term is 25. We may check it:
((x ⊕ y) ⊗ z)R(v) = (x ⊕ y) R(v) * z R(v) = (x R(v) + y R(v))* z R(v) = (2+3)*5 = 25.
However, if we interpret the same term in the structure of P(N) (all subsets of the set of natural numbers) and adopt the following interpretation: ⊕ - set union, ⊗ - set intersection, and if we take the valuation v(x)={2}, v(y)={3}, v(z)={5}, then the term value is the empty set, i.e.
((x ⊕ y) ⊗ z)P(N)(v)
= (x ⊕ y)P(N)(v) ∩ zP(N)(v) = (xP(N)(v) ∪ yP(N)(v)) ∩
{5} =
({2} ∪ {3}) ∩
{5} = {2,3} ∩ {5} = ∅.
Similarly, by induction on formula's form, we define the semantics of predicate calculus formulas. Let STR denote an arbitrary algebraic structure in which we interpret the functional and relational symbols and let v be an arbitrary valuation. The expression STR, v |= α(x) denotes that the value of the formula α(x) interpreted over the structure STR at the valuation v is true. In this case we say that the formula α(x) is satisfied by the valuation v in the structure STR. The concept of satisfiability can be defined recursively in the following manner:
STR, v |= p if and only if v(p)=1 when p is a propositional variable,
STR, v |= r(t1,..., tn) if and only if rSTR(tiSTR(v),..., tnSTR(v)) holds
STR, v |= ¬ α(x) if and only if STR, v |= α(x) does not hold
STR, v |= (α(x) ∨ β(x)) if and only if STR, v |= α(x) or STR, v |= β(x)
STR, v |= (α(x) ∧ β(x)) if and only if STR, v |= α(x) and STR, v |= β(x)
STR, v |= (α(x) → β(x)) if and only if STR, v |= ¬ α(x) or STR, v |= β(x)
STR, v |= ( ∀x) α(x) if and only if STR, v(a/x) |= α(x) for all a ∈ STR
STR, v |= ( ∃x) α(x) if and only if STR, v(a/x) |= α(x) for some a ∈ STR.
Let's look closer at the definition of satisfiability for the formulas with quantifiers. The formula ( ∀x) α(x) is satisfied by the valuation v over the structure STR if and only if every valuation v(a/x) obtained from v by replacing the variable x with any element a, satisfies the formula α(x). The formula ( ∃x) α(x) is satisfied at the valuation v in the structure STR if and only if at least one valuation v(a/x) obtained from v by replacing the variable x with any element a, satisfies the formula α(x).
We say that a formula α is true over the structure STR if and only if it is satisfied by any valuation in this structure, i.e. when for every v, STR,v|= α(x). This fact can be shortly denoted by STR|= α.
Example 7.4.3
N|= ( ∀ z) ( ∃ x) ( ∃ y)(x + y >z ).
R|= ( ∃ x)( ∃ y)( ¬ ((x + y) >2)).
It follows that there exists such a value for the variable z that the formula ( ∃ x)( ∃ y)( ¬ ((x + y) >z)) takes the value true in R. Thus, for the valuation v such that v(z)=2 we have R,v|= ( ∃ x)( ∃ y)( ¬ ((x + y) >z)). It is easy to notice that the formula ( ∃ x)( ∃ y)( ¬ ((x + y) >z)) is satisfied in R, regardless of the value of the variable z. Therefore,
R|= ( ∀ z) ( ∃ x)( ∃ y)( ¬ ((x + y) >z)).
Question 7.4.1 Write down the following propositions as the predicate calculus formulas and try to check their satifiability in the set of real numbers.
« previous section | next section » |