54
Mathematical Aspects of Logic Programming Semantics
model consistently with respect to N α , we obtain that there must be some A i
with ¬A i ∈ H, and, by definition of l P , we obtain l P (A) = l P (A i ) = (α, ω)
and, hence, also l P (A i / ) ≤ l P (A i ) for all i
' = i. Furthermore, since P/N α is
definite, we obtain that ¬B j ∈ N α for all j, and hence l P (B j ) < l P (A) for all
j. So, condition (WSiib) is satisfied.
(2) Suppose that I is a non-empty three-valued model for P and that l
is an I-partial level mapping such that P satisfies (WS) with respect to I
and l. First, note that for all models M , N of P with M ⊆ N , we have
(P/M )/N = P/(M ∪ N ) = P/N and (P/N )/∅ = P/N .
Let I α denote I restricted to the atoms which are not undefined in N α ∪R α .
It suffices to show the following: for all α > 0, we have I α ⊆ N α ∪ R α , and
I \ M P = ∅.
We show next by induction that if α > 0 is an ordinal, then the following
statements hold. (a) The bottom stratum of P/N α is non-empty and consists
of trivial components only. (b) The bottom layer of P/N α is definite. (c)
I α ⊆ N α ∪ R α . (d) P/N α+1 satisfies (WS) with respect to I \ N α+1 and
l| Nα+1 .
Note that P satisfies the hypothesis of Lemma 2.5.12 and, hence, also its
conclusions. So, on taking α = 1, we have that P/N 1 = P/∅ satisfies (WS)
with respect to I \N 1 and l| N1 , and by application of Lemma 2.5.12, we obtain
that statements (a) and (b) hold. For (c), note that no atom in R 1 can be true
in I, because no atom in R 1 can appear as head of a clause in P , and now apply
Lemma 2.5.12 (c). For (d), apply Lemma 2.5.12, noting that P/N 2 � N2 P .
For α a limit ordinal, we can show, exactly as in the proof of Lemma 2.5.12
(d), that P satisfies (WS) with respect to I \ N α and l| Nα . So, Lemma 2.5.12
is applicable, and statements (a) and (b) follow. For (c), let A ∈ R α . Then
every clause in P with head A contains a body literal which is false in N α . By
the induction hypothesis, this implies that no clause with head A in P can
have a body which is true in I. So, A ∈ I. Together with Lemma 2.5.12 (c),
this proves statement (c). For (d), apply again Lemma 2.5.12 (d), noting that
P/N α+1 � Nα+1 P .
For α = β + 1 a successor ordinal, we obtain by the induction hypothesis
that P/N β satisfies the hypothesis of Lemma 2.5.12. So, again statements (a)
and (b) follow immediately from this lemma, and (c) and (d) follow as in the
case when α is a limit ordinal.
It remains to show that I \ M P = ∅. Indeed, by the transfinite induction
argument just given, we obtain that P/M P satisfies (WS) with respect to
I \ M P and l| M P . If I \ M P is non-empty, then by Lemma 2.5.12 the bottom
stratum S(P/M P ) is non-empty, and the bottom layer L(P/M P ) is definite
and has model M corresponding to the least two-valued model for L(P/M P ).
Hence, by definition of the weakly perfect model M P for P , we must have that
M ⊆ M P , which contradicts the fact that M is the least model for L(P/M P ).
Hence, I \ M P must be empty, and this concludes the proof.
•
The following corollary follows immediately as a special case.
Mathematical Aspects of Logic Programming Semantics
model consistently with respect to N α , we obtain that there must be some A i
with ¬A i ∈ H, and, by definition of l P , we obtain l P (A) = l P (A i ) = (α, ω)
and, hence, also l P (A i / ) ≤ l P (A i ) for all i
' = i. Furthermore, since P/N α is
definite, we obtain that ¬B j ∈ N α for all j, and hence l P (B j ) < l P (A) for all
j. So, condition (WSiib) is satisfied.
(2) Suppose that I is a non-empty three-valued model for P and that l
is an I-partial level mapping such that P satisfies (WS) with respect to I
and l. First, note that for all models M , N of P with M ⊆ N , we have
(P/M )/N = P/(M ∪ N ) = P/N and (P/N )/∅ = P/N .
Let I α denote I restricted to the atoms which are not undefined in N α ∪R α .
It suffices to show the following: for all α > 0, we have I α ⊆ N α ∪ R α , and
I \ M P = ∅.
We show next by induction that if α > 0 is an ordinal, then the following
statements hold. (a) The bottom stratum of P/N α is non-empty and consists
of trivial components only. (b) The bottom layer of P/N α is definite. (c)
I α ⊆ N α ∪ R α . (d) P/N α+1 satisfies (WS) with respect to I \ N α+1 and
l| Nα+1 .
Note that P satisfies the hypothesis of Lemma 2.5.12 and, hence, also its
conclusions. So, on taking α = 1, we have that P/N 1 = P/∅ satisfies (WS)
with respect to I \N 1 and l| N1 , and by application of Lemma 2.5.12, we obtain
that statements (a) and (b) hold. For (c), note that no atom in R 1 can be true
in I, because no atom in R 1 can appear as head of a clause in P , and now apply
Lemma 2.5.12 (c). For (d), apply Lemma 2.5.12, noting that P/N 2 � N2 P .
For α a limit ordinal, we can show, exactly as in the proof of Lemma 2.5.12
(d), that P satisfies (WS) with respect to I \ N α and l| Nα . So, Lemma 2.5.12
is applicable, and statements (a) and (b) follow. For (c), let A ∈ R α . Then
every clause in P with head A contains a body literal which is false in N α . By
the induction hypothesis, this implies that no clause with head A in P can
have a body which is true in I. So, A ∈ I. Together with Lemma 2.5.12 (c),
this proves statement (c). For (d), apply again Lemma 2.5.12 (d), noting that
P/N α+1 � Nα+1 P .
For α = β + 1 a successor ordinal, we obtain by the induction hypothesis
that P/N β satisfies the hypothesis of Lemma 2.5.12. So, again statements (a)
and (b) follow immediately from this lemma, and (c) and (d) follow as in the
case when α is a limit ordinal.
It remains to show that I \ M P = ∅. Indeed, by the transfinite induction
argument just given, we obtain that P/M P satisfies (WS) with respect to
I \ M P and l| M P . If I \ M P is non-empty, then by Lemma 2.5.12 the bottom
stratum S(P/M P ) is non-empty, and the bottom layer L(P/M P ) is definite
and has model M corresponding to the least two-valued model for L(P/M P ).
Hence, by definition of the weakly perfect model M P for P , we must have that
M ⊆ M P , which contradicts the fact that M is the least model for L(P/M P ).
Hence, I \ M P must be empty, and this concludes the proof.
•
The following corollary follows immediately as a special case.