ss given by ( P t N ), the propositional formula ob ( P t N ) constrains the interpretations of M t since in each such structure the propositional formula ob ( P, N ) must be satisfied by each interpretation J   M, i.e. J = ob(P, N). Example 4.4 Let

$\sigma=(Ba\quad not(b\quad c))\quad d\quad\quad B(\quad f\quad g)$  $at(b\quad c),B(\quad f\quad g)$ . Now suppose that . 
Then, MA(o) = Ba, not(b), B( f g) . Now suppose that

$$\begin{array}{r c l}{{P}}&{{=}}&{{B a\,,\,n o t\,{\bigl(}\,b\quad c\,{\bigr)}}}\\ {{N}}&{{=}}&{{B{\bigl(}\quad f\quad g\,{\bigr)}}}\end{array}$$

Then, σ(P, N) = (true)   d false (which is equivalent to d), and ob(P,N) = a. 

Definition 4.5 We say that a pair of sets of interpretations (M, M ′ ) induces the partition (P, N) of MA(σ) if, for each modal atom ξ   MA(σ), ξ   P iff (M, M') = ξ .

Lemma 4.6 Let ϕ and let (P,N) be the partition induced by (M,M') on a set of modal atoms S.  Then, (I, M, M') = ϕ iff (I, M, M') = ϕ(P, N).

Follows immediately from Definitions 4.2 and 4.5, and from the definition of Proof, satisfiability in MBNF structures.

D
We now show that, if ( I , M ) is an MBNF model for σ which induces the partition ( P , N )
of MA(X), then the formula ob(P,N) completely characterizes the set of interpretations M.

Theorem 4.7  Let σ partition of MA(σ) induced by (M, M). Then, M =  J : J = ob(P, N). Proof.   Let M ′ =  J : J = ob ( P ′ N ) .  Since ( M ′ M ) induces the partition ( P ′ N ), by Definition 4.5 it follows that each interpretation in M must satisfy ob ( P , N ), hence M
M  .

Now suppose M M M ′ , and consider the structure ( I , M ′ , M ). We prove that each modal atom ξ   M A(σ) belongs to P iff (I, M', M) = ξ . The proof is by induction on the depth of formulas in MA(σ).

First, consider a modal atom not ψ such that ψ      : from the definition of satisfiability of a formula in an MBNF structure, it follows immediately that not ψ   P iff ( I, M ′ , M ) =
not ψ . Then, consider a modal atom Bψ such that ψ      : if Bψ    P, then, by definition of ob(P, N), the propositional formula ob(P, N)   ψ is valid, therefore (I, M', M) = Bψ. If B$ N, then there exists an interpretation J in M such that J = $, and since M'
M ,
it follows that ( I , M ′ , M ) = B ψ . Hence, each modal atom ξ   MA(σ) of depth 1 belongs to P iff (I, M', M) = ξ .

Suppose now that ξ    P iff ( I , M ′ , M ) = ξ for each modal atom ξ in M A( σ ) of depth less or equal to i . Consider a modal atom B ψ of M A(σ) of depth i + 1: by the induction hypothesis, and by Lemma 4.6, (I, M', M) = B¥ iff M' = B(¥(P, N)). Now, if B¥