Proof The monotonicity of TK follows directly from Props. C.7 and **A.10. Now since** I
is the minimal element of (M, ≤**), we obtain** T
0 K(I) = I ≤ T
1 K(I). By n **times**
applying the monotonicity of TK **we obtain** T
n K(I) ≤ T
n+1 K (I**) which is equivalent**
to T
n K(I) ⊇ T
n+1 K (I).

The following proposition shows that each definite P**-ground hybrid knowledge**
base either has no model at all, or, similarly as definite logic programs, **it has the** greatest S5 model that coincides with its unique MKNF model. It also shows how this model can be computed by iterating the TK **operator starting from** I.

Proposition C.9 Let K = hO,Pi be a definite P-ground hybrid knowledge base. Then either K has no S5 model or it has the greatest S5 model that also coincides with its single MKNF model. Furthermore, the set

$$\operatorname{mod}(\mathcal{K})=\bigcap_{n\geq0}T_{\mathcal{K}}^{n}(\mathcal{I})$$

is empty if K **has no S5 model and otherwise coincides with its unique MKNF** model.

## Proof

First we will prove an auxiliary claim: M ⊆ TK(M**) holds for any S5 model** M of K. Suppose M is an S5 model of K **and recall that**
TK(M) = mod (**O ∪ {** H
∗(r) | r **∈ P ∧** M |= B(r) })
Let's take some formula φ ∈ O. We know that M |= φ because M **is an S5 model of**
K. Now consider some rule r ∈ P such that M |= B(r). Since M **is an S5 model of**
K, we obtain M |= H∗(r). Consequently, M |= H∗(r) for every such r. So M **is an**
S5 model of O ∪ { H∗(r) | r ∈ P ∧ M |= B(r) } and since TK(M**) is by definition of**
mod(·) the greatest S5 model of O∪{ H∗(r) | r ∈ P ∧ M |= B(r) }**, we can conclude**
that M ⊆ TK(M).

Now we will proceed with the main part of the proof. Let

## Mk =\ N≥0 T N K(I)

Then, by Corollary C.7 and Theorem A.12, MK is the least fixed point of TK**. First**
we will show that MK contains every S5 model of K**. Assume, to the contrary, that**
M is an S5 model of K such that M * MK. Then by definition M ⊆ I = T
0 K(I**). It**
cannot be the case that M ⊆ T
n K(I) for all n ≥ **0 because that would be in conflict**
with M * MK**. So let**
n0 **= max** { n ≥ 0 | M ⊆ T
n K(I) } .

Now we have M ⊆ T
n0 K (I**) and by the auxiliary claim proved above, we obtain**
M ⊆ TK(M) which together with the monotonicity of TK (Corollary **C.8) yields**
M ⊆ TK(M) ⊆ TK(T
n0 K (I**)) =** T
n0+1 K (I**). However, this is in conflict with the**
definition of n0, so no S5 model M of K with M * MK can exist.