Supported Model Semantics
149
point, yielding a unique supported model for P . In order to show that T P is
strictly contracting with respect to �, we must show that for all J, K ∈ I P
with J = K we have �(T P (J), T P (K)) < �(J, K). In particular, the following
results hold.
(a) d 1 (T P (J), I) < d 1 (J, I) whenever d 1 (J, I) = 0, and d 1 (T P (J), I) = 0
whenever d 1 (J, I) = 0.
(b) f (T P (J)), f (T P (K)) < �(J, K).
(c) d 2 (T P (J), T P (K)) < �(J, K).
Indeed, it suffices to prove properties (a), (b) and (c), and we proceed to do
this next. For convenience, we identify Neg
∗ with the subset of B P containing
P
predicate symbols from Neg
∗
P .
(a) First note that d 1 (T P (J), I) = d 1 (T P − (J), I) since d 1 only depends
on the predicate symbols in Neg
∗
Let d l (J, I) = 2
−α . We show that
P .
'
'
d l (T P − (J), I) ≤ 2
−(α+1) . We know that J and I agree on all ground atoms
of level less than α and differ on an atom of level α. It suffices to show now
'
that T P − (J)
' and I agree on all ground atoms of level less than or equal to
α.
Let A be a ground atom in Neg
∗ with l(A) ≤ α, and suppose that T P − (J)
P
and I differ on A. Assume first that A ∈ T P − (J) and A ∈ I. Then there
must be a ground instance A ← L 1 , . . . , L m of a clause in P
− such that
J |= L 1 ∧ · · · ∧ L m . Since I is a fixed point of T P − , and using Definition 5.1.12,
there must also be a k such that I |= L k and l(L k ) < α. Note that the
predicate symbol in L k is contained in Neg
∗ . So we obtain I |= L k , J |
P
= L k
and l(L k ) < α, which is a contradiction to the assumption that J and I
agree on all atoms in Neg
∗ of level less than α. Now assume that A ∈ I and
P
A ∈ T P − (J). It follows that there is a ground instance A ← L 1 , . . . , L m of
a clause in P
− such that I |= L 1 ∧ · · · ∧ L m and l(A) > l(L 1 ), . . . , l(L m ) by
Definition 5.1.12. But then J |= L 1 ∧ · · · ∧ L m since J and I agree on all
atoms of level less than α and consequently A ∈ T P − (J). This contradiction
establishes the first statement in (a). The second statement in (a) follows by
'
'
a similar argument, noting that in this case J = I .
(b) It suffices to show this for K. Assume �(J, K) = 2
−α . We show that
f (T P (K)) ≤ 2
−(α+1) , for which, in turn, we have to show that, for each
A ∈ T P (K) not in Neg
∗ with l(A) ≤ α, we have A ∈ I. Assume that A ∈ I
P
for such an A. Since A ∈ T P (K), there is a ground instance A ← L 1 , . . . , L m
of a clause in P with K |= L 1 ∧ · · · ∧ L m . Since A ∈ I, there must also be a
k with I |= L k and l(A) > l(L k ) by Definition 5.1.12. If the predicate symbol
of L k belongs to Neg
∗ , then, since K and I agree on all atoms in Neg
∗ of
P
P
level less than α, we obtain K |= L k , which contradicts K |= L 1 ∧ · · · ∧ L m .
If the predicate symbol in L k does not belong to Neg
∗ , then L k is an atom,
P
and since f (K) ≤ 2
−α , we obtain I |= L k , which is again a contradiction.
(c) Let �(J, K) = 2
−α , and let A be not in Neg
∗ with l(A) ≤ α and
P
A ∈ T P (J). By symmetry, it suffices to show that A ∈ T P (K). Since A ∈
149
point, yielding a unique supported model for P . In order to show that T P is
strictly contracting with respect to �, we must show that for all J, K ∈ I P
with J = K we have �(T P (J), T P (K)) < �(J, K). In particular, the following
results hold.
(a) d 1 (T P (J), I) < d 1 (J, I) whenever d 1 (J, I) = 0, and d 1 (T P (J), I) = 0
whenever d 1 (J, I) = 0.
(b) f (T P (J)), f (T P (K)) < �(J, K).
(c) d 2 (T P (J), T P (K)) < �(J, K).
Indeed, it suffices to prove properties (a), (b) and (c), and we proceed to do
this next. For convenience, we identify Neg
∗ with the subset of B P containing
P
predicate symbols from Neg
∗
P .
(a) First note that d 1 (T P (J), I) = d 1 (T P − (J), I) since d 1 only depends
on the predicate symbols in Neg
∗
Let d l (J, I) = 2
−α . We show that
P .
'
'
d l (T P − (J), I) ≤ 2
−(α+1) . We know that J and I agree on all ground atoms
of level less than α and differ on an atom of level α. It suffices to show now
'
that T P − (J)
' and I agree on all ground atoms of level less than or equal to
α.
Let A be a ground atom in Neg
∗ with l(A) ≤ α, and suppose that T P − (J)
P
and I differ on A. Assume first that A ∈ T P − (J) and A ∈ I. Then there
must be a ground instance A ← L 1 , . . . , L m of a clause in P
− such that
J |= L 1 ∧ · · · ∧ L m . Since I is a fixed point of T P − , and using Definition 5.1.12,
there must also be a k such that I |= L k and l(L k ) < α. Note that the
predicate symbol in L k is contained in Neg
∗ . So we obtain I |= L k , J |
P
= L k
and l(L k ) < α, which is a contradiction to the assumption that J and I
agree on all atoms in Neg
∗ of level less than α. Now assume that A ∈ I and
P
A ∈ T P − (J). It follows that there is a ground instance A ← L 1 , . . . , L m of
a clause in P
− such that I |= L 1 ∧ · · · ∧ L m and l(A) > l(L 1 ), . . . , l(L m ) by
Definition 5.1.12. But then J |= L 1 ∧ · · · ∧ L m since J and I agree on all
atoms of level less than α and consequently A ∈ T P − (J). This contradiction
establishes the first statement in (a). The second statement in (a) follows by
'
'
a similar argument, noting that in this case J = I .
(b) It suffices to show this for K. Assume �(J, K) = 2
−α . We show that
f (T P (K)) ≤ 2
−(α+1) , for which, in turn, we have to show that, for each
A ∈ T P (K) not in Neg
∗ with l(A) ≤ α, we have A ∈ I. Assume that A ∈ I
P
for such an A. Since A ∈ T P (K), there is a ground instance A ← L 1 , . . . , L m
of a clause in P with K |= L 1 ∧ · · · ∧ L m . Since A ∈ I, there must also be a
k with I |= L k and l(A) > l(L k ) by Definition 5.1.12. If the predicate symbol
of L k belongs to Neg
∗ , then, since K and I agree on all atoms in Neg
∗ of
P
P
level less than α, we obtain K |= L k , which contradicts K |= L 1 ∧ · · · ∧ L m .
If the predicate symbol in L k does not belong to Neg
∗ , then L k is an atom,
P
and since f (K) ≤ 2
−α , we obtain I |= L k , which is again a contradiction.
(c) Let �(J, K) = 2
−α , and let A be not in Neg
∗ with l(A) ≤ α and
P
A ∈ T P (J). By symmetry, it suffices to show that A ∈ T P (K). Since A ∈