ψ is valid, and since M" =  I : I = ob(P, N) , it follows that (M', M) = Bψ ob(P, N)
iff (M", M) = Bψ.

Now suppose that, for each modal atom ξ of depth i, ( M ′, M ) = ξ iff ( M ′′, M ) = ξ, and let (P', N') denote the partition of the modal atoms in MA(E) of depth less or equal to i induced by ( M ′ , M ).  First, consider a modal atom not ψ of depth i + 1.  Then, by Lemma 4.6, (M',M) = not ψ iff (M',M) = not(ψ(P',N')) and, by the inductive hypothesis and Lemma 4.6, (M", M) = not ψ iff (M", M) = not(ψ(P', N')).  Then, since ψ has depth i, ψ(P ′ , N ′ ) is a propositional formula, hence (M ′ , M ) = not(ψ(P ′ , N ′ )) iff there exists an interpretation I = M such that I = ψ(P I , N I ), which immediately implies that ( M ′ , M ) = not ψ iff ( M ′′ , M ) = not ψ .  Now consider a modal atom Bψ of depth i + 1. Then, by Lemma 4.6, (M',M) = Bψ iff (M',M) = B(ψ(P',N')) and, by the inductive hypothesis and Lemma 4.6, (M",M) = B¥ iff (M",M) = B(¥(P',N')). By Definition 4.3, (M', M) = B¥ iff the propositional formula ob(P, N)    ψ(P', N') is valid, and since M n = I : I = ob(P, N) , it follows that (M', M) = B¥ iff (M", M) = B¥,
which proves the thesis.

D
We are now ready to prove correctness of the algorithm MBNF-Not-Entails.

## Theorem 4.15 Let Σ

M, P
B. Then, MBNF-Not-Entails(σ,φ) returns true iff 0 If part.  Suppose σ = MBNF ϕ . Then, there exists a pair ( I, M ) such that ( I, M ) is Proof.

an MBNF model for σ and ( I , M , M ) = ϕ . Let ( P , N ) be the partition of M A(Σ) induced by ( M, M ).  By Theorem 4.7, M =  I : I = ob( P, N ) .  Therefore, by Definition 4.8, (P, N) = Prt(X, ob(P, N)). Then, since (I, M, M) = ϕ, by Theorem 4.10 it follows that I = ϕ( ob ( P i N )), and since ( I , M i M ) = σ i by Lemma 4.6 I = σ( P i N ), therefore I =
σ(P, N)
ϕ(ob(P, N )). Now suppose there exists a partition (P', N') of M A(Σ) such that
(P ′ , N ′ ) = (P ′ N ) and none of conditions (c1), (c2), and (c3) holds. Then, since σ(P ′ , N ′ ) is satisfiable, there exists an interpretation J such that J = σ( P ′ , N ′ ), and since ( P ′ , N ′ ) =
Prt(E, ob(P', N'), ob(P, N)), from Lemma 4.6 it follows that there exists an interpretation J such that ( J, M ′ , M ) = σ, where M ′ =  I : I = σδ(P ′ , N ′ ) . Then, since condition (c3)
does not hold, the propositional formula ob ( P, N )   ob ( P ′ , N ′ ) is valid, which implies that M = M . Now, if M ′ = M ′ then ( P ′ , N ′ ) would be the partition induced by ( M ′ M ), thus contradicting the hypothesis ( P ′ , N ′ ) = ( P ′ N ). Hence, M ′ M ′ and since ( J ′ M ′ , M ′ ) = σ ′
it follows that ( I , M ) is not an MBNF model for σ .  Contradiction.  Consequently, condition
(c) in the algorithm holds, therefore MBNF-Not-Entails( σ, ϕ) returns true.

Only-if part. Suppose MBNF-Not-Entails( σ, ϕ) returns true. Then, there exists a partition ( P, N ) of MA(Σ) such that conditions (a), (b), and (c) hold. Let M =  I : I = ob(P, N) . Since (P, N) = Prt(E, ob(P, N)), by Definition 4.8 (P, N) is the partition induced by ( M, M ). And since σ( P, N ) an interpretation I such that I = σ(P,N) and I = ϕ(ob(P,N)), hence, by Lemma 4.6,
(I, M, M) = σ and (I, M, M) = ϕ. Now suppose (I, M) is not an MBNF model for σ.

Then, there exists a set M ′ and an interpretation J such that M ′ M and ( J, M ′ , M ) = σ .

Let (P', N') be the partition of MA() induced by (M', M). Since M = I : I = ob(P, N) , it follows that M ′ contains at least one interpretation J which does not satisfy ob (P, N),
and since ob (P, N) = Λ Bψερ ψ(P, N), J does not satisfy at least one formula of the form