Theorem 4.5: *For all basic formulas* α in **ON L**−
n and of maximal **a, b***-depth of* **k, j**,
Mc, w |= α iff eJwK
k a
, eJwK
j b
, JwK |= α.

Proof: By definition, the proof holds for propositional formulas, disjunctions and negations. So let us say the result holds for formulas of **a, b**-depth 1. Suppose now Mc, w |= Laα, where Laα has **a, b**-depth of 1, 2. Then for all w
′ ∈ Kca
(w), Mc, w′|= α iff (by induction hypothesis) eJw′K
1 a
, eJw′K
1 b
, Jw
′
K |= α iff eJwK
2 a
, {}, JwK |= Laα. By construction, we also have eJwK
1 a
, {}, JwK |= Laα. Since b's structure is irrelevant, we get eJwK
1 a
, eJwK
2 b
, JwK |= Laα proving the hypothesis.

For the other direction, suppose eJwK
1 a
, eJwK
2 b
, JwK |= Laα. For all Jw
′
K ∈ eJwK
1 a
, eJwK
1 a
, {}, Jw
′
K |= α iff (by hyp.) Mc, w′|= α for all w
′ ∈ Kca(w) iff Mc, w |= Laα.

Lemma 4.6: *Every* K45n-consistent basic formula α *is satisfiable wrt. some* (**k, j**)*-model.* Proof: It is a property of the canonical model that every K45n-consistent basic formula is satisfiable wrt. the canonical model. Supposing that the formula has a **a, b**-depth of **k, j** then from Thm 4.5, we know there is at least the correspondence (**k, j**)-model that also satisfies the formula.

## Theorem 4.7:

For all α **∈ ON L**−
n
, if AXn ⊢ α *then* |= α.

Proof: The soundness is easily shown to hold for A1n − A4n. The soundness of A5n is shown by induction on the depth. Suppose α is a propositional formula, and say ¬α is a consistent propositional formula (and hence K45n-consistent). Then there is a world w
∗
such that {}, {}, w∗|= ¬α. Given a e ka
, if hw
∗
, ek−1 bi ∈ e ka for some e k−1 b, then e ka
, {}, w |= ¬Laα for any world w. If not, then e ka
, {}, w |=
¬Naα. Thus, e ka
, {}, w |= Naα ⊃ ¬Laα. Wlog, assume the proof holds for a-objective formulas of max. b-depth k−1. Suppose now, α is such a formula, and ¬α is K45n-consistent. By Lemma 4.6, there is hw
∗
, e∗k−1 bi, such that {}, e∗k−1 b, w∗|= ¬α. Again, if hw
∗
, e∗k−1 bi ∈ e ka
, then e ka
, {}, w |= ¬Laα and if not, then e ka
, {}, w |= ¬Naα.

We proceed with the completeness over the following definition, and lemmas.

Definition 4.8: A formula ψ is said to be *independent* of the formula φ wrt. an axiom system AX, if neither AX ⊢ φ ⊃ ψ nor AX ⊢ φ ⊃ ¬ψ.

Lemma 4.9: *[Halpern and Lakemeyer, 2001] If* φ1**, . . . , φ**m are K45n-consistent basic i-objective formulas then there exists a basic i-objective formula ψ *of the form* Ljψ
′
(j 6= i*) that is independent of* φ1**, . . . , φ**m *wrt.* K45n.

Lemma 4.10: In the lemma above, if φi are i-objective and of maximal j-depth k for j 6= i, then there is a ψ of j*-depth* 2k + 2.

Lemma 4.11: [Halpern and Lakemeyer, 2001] If φ and ψ are i*-objective basic formulas, and if* Liφ ∧
Niψ is AXn-consistent, then φ ∨ ψ *is valid.*