In the following, we say that an occurrence of a subformula ψ in a formula φ M 
strict if it does not lie within the scope of a modal operator. E.g., let σ = B ϕ not ( B ψ f ).

The occurrence of B ϕ in σ is strict, while the occurrence of B ψ is not strict.

Theorem 3.5  Let E
B. Then, M is an AEL model for Σ iff, for each I , ( I , M ) is an MBNF model of τ(Σ).

Proof.

If part.  Suppose ( I, M ) is an MBNF model of τ(Σ).  Then, for each M'
M,
(M', M) = r(E). Since r(E) is a set of formulas of the form B ϕ , where ϕ does not contain any occurrence of the operator B, it follows that, for each subformula of the form not ϕ occurring in r(E), (M', M) = not ϕ iff (M, M) = not ϕ . Now let Bϕ   r(Σ), let ϕ  denote the propositional formula obtained from ϕ by replacing each strict occurrence in ϕ of a formula of the form not ψ with true if ( M , M ) = not ψ and with false otherwise, and let E' = Q : B Q
r(E) . Now suppose there exists an interpretation J such that J = E'
and J M. Then, from the definition of satisfiability in MBNF structures it follows that
(M) = T(X), thus contradicting the hypothesis that (I, M) is an MBNF model for r(E). Hence, M = I : I = E' . Now consider a pair (J, M): again, from the definition of satisfiability in MBNF structures it follows immediately that ( J, M ) = ∑ iff J = ∑ ′ . And since M contains all the interpretations satisfying Σ ′ , it follows that, for each interpretation M , (J, M) = Σ, therefore by Proposition 3.4 it follows that M is an AEL model for Σ.

J
Only-if part.  Suppose M  is an AEL model for Σ.  Then, by Proposition 3.4, for each interpretation I    M , ( I , M ) = Σ and, for each interpretation J    M , ( J , M ) = Σ . For Σ, let φ ′′ denote the propositional formula obtained from φ by replacing each strict each w occurrence of a formula of the form Bψ with true if M = Bψ and with false otherwise, and let Σ" = φ" : φ Σ . Then, suppose there exists an interpretation J such that J = Σ ′′
and J M. Then, from the definition of satisfiability in MBNF structures it follows that
(J, M) = E, thus contradicting the hypothesis that M is an AEL model for E. Hence, M =  I : I = Y" . Now suppose that, for some interpretation I, (I, M) is not an MBNF model for r(E). Then, there exists M' M such that (M', M) = r(E). From the definition of r( ), it follows that each interpretation in M ′ satisfies Σ ′′ , and, since M ′     M , there exists M such that J = Σ ′′ . Contradiction. Therefore, ( I, M ) is an MBNF model for Σ.

J
o We remark that the above theorem could alternatively be proved from the fact that the K-free fragment of the logic MKNF (Lifschitz, 1991) is equivalent to AEL, which is stated (although without proof) by Schwarz and Truszczynski (1994, page 123), and from the correspondence between MBNF and MKNF (Lifschitz, 1994).

The previous theorem implies that the interpretation of the modality not in MBNF and of the modal operator in autoepistemic logic are the same. This property extends previous results relating MBNF with AEL (Lin & Shoham, 1992; Schwarz & Lifschitz, 1993; Chen, 1994), and has interesting consequences both in the logic programming framework and in nonmonotonic reasoning. In particular, since MBNF generalizes the stable model semantics for logic programs (Gelfond & Lifschitz, 1988), the above result strengthens the idea that AEL is the true logic of negation as failure (as interpreted according to the stable model semantics). Moreover, positive theories have the same interpretation both in MBNF and in the logic of minimal knowledge S5 G (Halpern & Moses, 1985): consequently, the logic MBNF generalizes both Halpern and Moses' S5 G and Moore's AEL.