Finally, since Naψa0 ∧ ¬Naψaj is consistent, it must be that ψa0 ∧ ¬ψaj is consistent. Further, either ψa0 ∧ ¬ψaj ∧ ϕa0 or ψa0 ∧ ¬ψaj ∧ ¬ϕa0 is consistent. If the former, then ψa0 ∧ ¬ψaj ∧ ϕa0 ∧ ¬γ is also consistent. Let β be that which is consistent. Note that ¬β ∧ (ϕa0 ∧ (¬ψa0 ∨ (ψa0 ∧ γ))) is consistent, and hence part of all S
′ ∈ Sa. This means that e k
′

a
, {}, w∗|= La(¬β). But since β itself is consistent, there is a k
′
-structure such that {}, e•
(b,2k)
, w•|= β. And this k
′
-structure can not be in e k
′

a
.

This means that e k
′

a
, {}, w∗|= ¬Naψaj . Thus, all the a-subjective formulas in the normal form above are satisfiable *wrt.* e k
′

a
.

Now, observe that, although La**⊥ ⊃ ¬**Na¬Ob¬Oap (ζ) from Theorem 3.4 is valid, yet it is not derivable from AXn. In fact, the soundness result is easily extended to the full language **ON L**n. Then, the proof theory cannot be complete for the full language since there is ζ **∈ ON L**n such that 6⊢ ζ and |= ζ.

Similarly, the validity of non-provable formulas ¬Oa¬Obp and ζ *wrt.* the canonical model and the i-set approach respectively, show that although AXn is also sound for the full language in these approaches, it cannot be compelete. Mainly, axiom A5n has to somehow go beyond basic formulas. As Halpern and Lakemeyer ([2001]) discuss, the problem is one of circularity. We would like the axiom to hold for any α such that it is a consistent i-objective formula, but to deal with consistency we have to clarify what the axiom system looks like.

The approach taken by Halpern and Lakemeyer is to introduce *validity* (and its dual satisfiability)
directly into the language. Formulas in the new language, **ON L**+
n
, are shown to be provably equivalent to **ON L**n. Some new axioms involving validity and satisfiability are added to the axiom system, and the resultant proof theory AX+
n is shown to be sound and complete for formulas in **ON L**+
n
, *wrt.* an extended canonical model. (An extended canonical model follows the spirit of the canonical model construction but by considering maximally AX+
n
-consistent sets, and treat Li and Ni as two independent modal operators.) So, one approach is to show that for formulas in the extended language the set of valid formulas overlap in the extended canonical model and k-structures. But then, as we argued, axiomatizing validity is not natural. Also, the proof theory is difficult to use. And in the end, we would still understand the axioms to characterize a semantics bridged on proof-theoretic elements.

Again, what is desired is a generalization of Levesque's axiom A5, and nothing more. To this end, we propose a new axiom system, that is subtly related to the structure of formulas as are parameters k and j. The axiom system has an additional t-axioms, and is to correspond to a sequence of languages ON Ltn
.

14 Definition 4.14: Let ON L1n = **ON L**−
n
. Let **ON L**t+1 nbe all Boolean combinations of formulas of ON Ltn and formulas of the form Liα and Niα for α **∈ ON L**tn
.

It is not hard to see that **ON L**t+1 n **⊇ ON L**tn
. Note that t here does not correspond to the depth of formulas. Indeed, a formula of the form (LbLa)
k+1p is already in **ON L**−
n
. Let AXt+1 n be an axiom system consisting of A1n − A4n, MP, NEC and A51n − A5t+1 n defined inductively as:
A51n
. Niα ⊃ ¬Liα, if ¬α is a K45n-consistent i-objective basic formula.