151
Supported Model Semantics
5.1.17 Theorem Let P be a Φ-accessible program with model I and level
mapping l such that P satisfies (F) with respect to I ∪ ¬(B P \ I) and l.
Then T P is strictly contracting on the spherically complete dislocated generalized ultrametric space (I P , �), where for all J, K ∈ I P we have �(J, K) =
max{d l (J, I), d l (I, K)}. In particular, P has a unique supported model.
Proof: By Proposition 4.8.23, we have that (I P , �) is a spherically complete
dislocated generalized ultrametric space.
In order to show that T P is strictly contracting, let J, K ∈ I P , and assume
that �(J, K) = 2
−α . Then J, K and I agree on all ground atoms of level less
than α. We show that T P (J) and I agree on all ground atoms of level less
than or equal to α. A similar argument shows that T P (K) and I agree on all
ground atoms of level less than or equal to α, and this suffices.
Let A ∈ T P (J) with l(A) ≤ α. Then there must be a clause A ← L 1 , . . . , L n
in ground(P ) such that J |= L 1 ∧ · · · ∧ L n . Since I and J agree on all ground
atoms of level less than α, (Fii) cannot hold, because if I |= L i with l(A) >
l(L i ), then J |= L i and consequently J |= L 1 ∧· · ·∧L n , which is a contradiction.
Therefore, (Fi) holds, and so A ∈ T P (I) = I. Hence, A ∈ I.
Conversely, suppose that A ∈ I. Since I = T P (I), there must be a clause
A ← L 1 , . . . , L n in ground(P ) such that I |= L 1 ∧ · · · ∧ L n . Thus, (Fi) must
hold, and so we can assume that A ← L 1 , . . . , L n also satisfies l(A) > l(L i )
for i = 1, . . . , n. Since I and J agree on all ground atoms of level less than α,
we have J |= L 1 ∧ · · · ∧ L n , and hence A ∈ T P (J), as required.
Applying Theorem 4.5.1 now yields a unique fixed point M of the operator
T P , that is, a unique supported model for P .
•
The proof of Theorem 4.5.1 yields, moreover, that there must be an ordinal
α such that �(M, M ) = 0. Since the only point of X which has non-zero
distance from itself is I, we conclude that I = M is the unique supported
model for P . This is somewhat unfortunate,
7 since I was needed in order to
construct �.
5.2 Three-Valued Supported Models
Recall from Section 2.4 that the three-valued supported models for a program P are exactly the fixed points of the corresponding Fitting operator,
while the least fixed point of the operator, that is, the least three-valued supported model for the program, is called its Fitting model. In this section, we
will study variants of the Fitting operator and relate them to the classes of
programs studied in Section 5.1. Thus, in the present section, unless otherwise
7 We have argued in [Hitzler and Seda, 2003] that self-distance can be understood as a
measure of a priori knowledge, but this needs to be substantiated further.
Supported Model Semantics
5.1.17 Theorem Let P be a Φ-accessible program with model I and level
mapping l such that P satisfies (F) with respect to I ∪ ¬(B P \ I) and l.
Then T P is strictly contracting on the spherically complete dislocated generalized ultrametric space (I P , �), where for all J, K ∈ I P we have �(J, K) =
max{d l (J, I), d l (I, K)}. In particular, P has a unique supported model.
Proof: By Proposition 4.8.23, we have that (I P , �) is a spherically complete
dislocated generalized ultrametric space.
In order to show that T P is strictly contracting, let J, K ∈ I P , and assume
that �(J, K) = 2
−α . Then J, K and I agree on all ground atoms of level less
than α. We show that T P (J) and I agree on all ground atoms of level less
than or equal to α. A similar argument shows that T P (K) and I agree on all
ground atoms of level less than or equal to α, and this suffices.
Let A ∈ T P (J) with l(A) ≤ α. Then there must be a clause A ← L 1 , . . . , L n
in ground(P ) such that J |= L 1 ∧ · · · ∧ L n . Since I and J agree on all ground
atoms of level less than α, (Fii) cannot hold, because if I |= L i with l(A) >
l(L i ), then J |= L i and consequently J |= L 1 ∧· · ·∧L n , which is a contradiction.
Therefore, (Fi) holds, and so A ∈ T P (I) = I. Hence, A ∈ I.
Conversely, suppose that A ∈ I. Since I = T P (I), there must be a clause
A ← L 1 , . . . , L n in ground(P ) such that I |= L 1 ∧ · · · ∧ L n . Thus, (Fi) must
hold, and so we can assume that A ← L 1 , . . . , L n also satisfies l(A) > l(L i )
for i = 1, . . . , n. Since I and J agree on all ground atoms of level less than α,
we have J |= L 1 ∧ · · · ∧ L n , and hence A ∈ T P (J), as required.
Applying Theorem 4.5.1 now yields a unique fixed point M of the operator
T P , that is, a unique supported model for P .
•
The proof of Theorem 4.5.1 yields, moreover, that there must be an ordinal
α such that �(M, M ) = 0. Since the only point of X which has non-zero
distance from itself is I, we conclude that I = M is the unique supported
model for P . This is somewhat unfortunate,
7 since I was needed in order to
construct �.
5.2 Three-Valued Supported Models
Recall from Section 2.4 that the three-valued supported models for a program P are exactly the fixed points of the corresponding Fitting operator,
while the least fixed point of the operator, that is, the least three-valued supported model for the program, is called its Fitting model. In this section, we
will study variants of the Fitting operator and relate them to the classes of
programs studied in Section 5.1. Thus, in the present section, unless otherwise
7 We have argued in [Hitzler and Seda, 2003] that self-distance can be understood as a
measure of a priori knowledge, but this needs to be substantiated further.