15
Order and Logic
In the converse direction, suppose that u is any valuation on X. Let M
denote the set of all finite valuations v such that v [ u. Let v 1 , v 2 ∈ M
and suppose that x ∈ X is such that not both v 1 (x) and v 2 (x) are equal to
the bottom element (there are only finitely many such x, of course). Noting
that approx(u(x)) in T is directed, that v 1 (x), v 2 (x) ∈ approx(u(x)) and by
considering one-point valuations (namely, those valuations w such that w(x)
is not equal to the bottom element at at most one value of x), we see that
there is v 3 (x) ∈ approx(u(x)) such that both v 1 (x) ≤ v 3 (x) and v 2 (x) ≤ v 3 (x).
It follows that there is an element v 3 of M such that v 1 [ v 3 and v 2 [ v 3 and,
hence, that M is directed. Moreover, given x ∈ X and any a ∈ approx(u(x)),
let v
x
a denote the one-point valuation which satisfies v
x
a (x) = a and v
x
a (y) = ⊥
for all y = x. Then v
M = u.
x
a ∈ M , and {v
x
a (x) | a ∈ approx(u(x))} = u(x). Thus,
It now follows from the observations just made that if u is compact, then
there is v ∈ M such that u [ v, and hence the set {x ∈ X | u(x) = ⊥} is finite.
We claim that u(x) is a compact element in (T , ≤) for each x ∈ X. Suppose
otherwise, that is, that there is x 0 ∈ X with u(x 0
) non-compact in (T , ≤).
Then there is a directed set N in T with u(x 0 ) ≤ N for which there is no
n ∈ N with u(x 0 ) ≤ n. Define the family N n consisting of the elements u n of
I(X, T ), n ∈ N , by setting u n (x) = u(x) for all x = x 0 and setting u n (x 0 ) = n.
Then N n is directed and u [ {u n | n ∈ N }, yet we do not have u [ u n
for any n ∈ N . This contradicts the fact that u is a compact element, and
hence, for each x ∈ X, u(x) is a compact element. Thus, the compact elements
are indeed the finite valuations, and, moreover, we now see that approx(u) is
directed and that approx(u) = u for each valuation u ∈ I(X, T ).
Finally, if u 1 and u 2 are two consistent finite elements in I(X, T ), then
the valuation v defined by v(x) = {u 1 (x), u 2 (x)}, for each x ∈ X, is the
supremum of u 1 and u 2 (and is, in fact, a finite element). This completes the
proof.
•
1.3.2 Valuations in Two-Valued and Other Logics
The most prominent declarative semantics for logic programs employ classical two-valued logic, three-valued logic, or, to a lesser extent, four-valued
logic. The corresponding truth sets T for these logics are T W O, T HREE,
and FOU R, as already discussed. We examine these cases next in some detail in light of Theorem 1.3.2 and also introduce some convenient notation
for these special cases. We begin by considering the orderings involved on the
three sets of truth values that we are currently discussing.
In the case of classical two-valued logic, the ordering usually taken is the
truth ordering. This is the partial ordering ≤ t satisfying f < t t and is often
denoted just by ≤; it turns T W O into a complete lattice with f as the bottom
element.
For three-valued logic, there are two natural orderings usually considered:
Order and Logic
In the converse direction, suppose that u is any valuation on X. Let M
denote the set of all finite valuations v such that v [ u. Let v 1 , v 2 ∈ M
and suppose that x ∈ X is such that not both v 1 (x) and v 2 (x) are equal to
the bottom element (there are only finitely many such x, of course). Noting
that approx(u(x)) in T is directed, that v 1 (x), v 2 (x) ∈ approx(u(x)) and by
considering one-point valuations (namely, those valuations w such that w(x)
is not equal to the bottom element at at most one value of x), we see that
there is v 3 (x) ∈ approx(u(x)) such that both v 1 (x) ≤ v 3 (x) and v 2 (x) ≤ v 3 (x).
It follows that there is an element v 3 of M such that v 1 [ v 3 and v 2 [ v 3 and,
hence, that M is directed. Moreover, given x ∈ X and any a ∈ approx(u(x)),
let v
x
a denote the one-point valuation which satisfies v
x
a (x) = a and v
x
a (y) = ⊥
for all y = x. Then v
M = u.
x
a ∈ M , and {v
x
a (x) | a ∈ approx(u(x))} = u(x). Thus,
It now follows from the observations just made that if u is compact, then
there is v ∈ M such that u [ v, and hence the set {x ∈ X | u(x) = ⊥} is finite.
We claim that u(x) is a compact element in (T , ≤) for each x ∈ X. Suppose
otherwise, that is, that there is x 0 ∈ X with u(x 0
) non-compact in (T , ≤).
Then there is a directed set N in T with u(x 0 ) ≤ N for which there is no
n ∈ N with u(x 0 ) ≤ n. Define the family N n consisting of the elements u n of
I(X, T ), n ∈ N , by setting u n (x) = u(x) for all x = x 0 and setting u n (x 0 ) = n.
Then N n is directed and u [ {u n | n ∈ N }, yet we do not have u [ u n
for any n ∈ N . This contradicts the fact that u is a compact element, and
hence, for each x ∈ X, u(x) is a compact element. Thus, the compact elements
are indeed the finite valuations, and, moreover, we now see that approx(u) is
directed and that approx(u) = u for each valuation u ∈ I(X, T ).
Finally, if u 1 and u 2 are two consistent finite elements in I(X, T ), then
the valuation v defined by v(x) = {u 1 (x), u 2 (x)}, for each x ∈ X, is the
supremum of u 1 and u 2 (and is, in fact, a finite element). This completes the
proof.
•
1.3.2 Valuations in Two-Valued and Other Logics
The most prominent declarative semantics for logic programs employ classical two-valued logic, three-valued logic, or, to a lesser extent, four-valued
logic. The corresponding truth sets T for these logics are T W O, T HREE,
and FOU R, as already discussed. We examine these cases next in some detail in light of Theorem 1.3.2 and also introduce some convenient notation
for these special cases. We begin by considering the orderings involved on the
three sets of truth values that we are currently discussing.
In the case of classical two-valued logic, the ordering usually taken is the
truth ordering. This is the partial ordering ≤ t satisfying f < t t and is often
denoted just by ≤; it turns T W O into a complete lattice with f as the bottom
element.
For three-valued logic, there are two natural orderings usually considered: