Theorem 6.2. *For all* α **∈ ON L**+
n t, AX′n ⊢ Sat(α) iff α is AX+
n t*-consistent.*
Proof: It is helpful to have the following variant of Lemma 4.17 at hand, and a corollary thereof.

Lemma 9.1: *Suppose* φ, ψ **∈ ON L**+
n t−1are i*-objective* AX+
n t-consistent formulas, and |= φ∨ψ*. Then* Liφ ∧ Niψ is AX+
n t*-consistent.*
Proof: Suppose not. Then AX+
n t⊢ ¬(Laφ∧Naψ), that is AX+
n t⊢ ¬Laφ∨¬Naψ. Then, by Lemma 6.1, |= ¬Laφ ∨ ¬Naψ. Let Wφ = {w | w |= φ}. Let e ka = Wφ × E
k−1 be a e kfor Alice. Then clearly, e ka
, {}, w 6|= ¬Laφ. It must be then that e ka
, {}, w |= ¬Naψ. Then there is some hw
′
, ek−1 b**i 6∈** e ka such that e ka
, ek−1 b, w′|= ¬ψ. And clearly, for all hw
′
, ek−1 b**i 6∈** e ka
, e ka
, ek−1 b, w′|= ¬φ (by construction). It follows that there is a hw
′
, ek−1 b**i 6∈** e ka where e ka
,
e k−1 b, w′|= ¬(φ ∨ ψ), contradicting the validity of φ ∨ ψ.

Corollary 9.2: *Suppose* α, β1, . . . βk, γ, δ1, . . . δm **∈ ON L**+
n t−1, are i*-objective* AX+
n t-consistent formulas, and |= α ∨ γ*. Then* Liα ∧ ¬Li¬β1 . . . ∧ ¬Li¬βk ∧ Niγ ∧ ¬Niδ1 . . . ∧ ¬Ni¬δm is AX+
n tconsistent.

Returning to Theorem 6.2: Proof on the *length* of the derivative, using induction on t. Let α be a consistent propositional formula. Then, by V2, AX′n ⊢ Sat(α). Since it is a consistent propositional formula, it is also AX+
n t-consistent. Assume theorem holds for α **∈ ON L**+
n t−1. Suppose we have Sat(α ∧ βk), Sat(γ ∧ δm),¬Sat(¬(α ∨ γ)) **∈ ON L**+
n t−1then by V3, AX′n ⊢ Sat(Liα ∧ ¬Li¬βk ∧
Niγ ∧ ¬Ni¬δm). By hypothesis α ∧ βk, γ ∧ δm are AX+
n t-consistent. And ¬(α ∨ γ) is not AX+
n tconsistent, and so AX+
n t⊢ α∨γ. By Lemma 6.1, |= α∨γ. Clearly, by Corollary 9.2, Liα∧ ¬Li¬βk ∧
Niγ ∧ ¬Ni¬δm is AX+
n t-consistent. Finally, suppose that you have Sat(α) for some i-objective α and Sat(β) for some i-subjective β, then by V4, AX′n ⊢ Sat(α ∧ β). By induction hypothesis, α and β are AX+
n t-consistent. By Lemma 6.1, α is satisfiable and β is satisfiable, and so is α ∧ β. By Lemma 6.1, α ∧ β is AX+
n t-consistent. The other direction is symmetric.

Theorem 6.3. AX′n ⊢ α iff AX+
n t⊢ α*, for* α **∈ ON L**+
n t.

Proof: Since axioms A1n − A4n, MP, NEC, NECVal are common to both, their use is not discussed. To show that AX′n ⊢ α ⇒ AX+
n t⊢ α, suppose you had Sat(¬α) for some i-objective α **∈ ON L**+
n t−1then using A5′n
, one could show that Niα ⊃ ¬Liα. From Theorem 6.2, we also know ¬α is AX+
n t−1-consistent. Then, we can show Niα ⊃ ¬Liα as well using A5tn
. V2, V3, V4 follow immediately from Theorem 6.2. Assuming now that the proof holds for base cases, using V1, if AX′n ⊢ Val(α) and AX′n ⊢ Val(α ⊃ β) then AX′n ⊢ Val(β). Now, by induction hypothesis, AX+
n t⊢ Val(α) iff by Lemma 6.1 |= Val(α), and so |= α. Similarly, |= α ⊃ β, and thus, |= β and |= Val(β) by the semantics. By Lemma 6.1, AX+
n t⊢ Val(β).

To show that AX+
n t⊢ α ⇒ AX′n ⊢ α, suppose ¬α **∈ ON L**+
n t−1is i-objective and AXt−1 nconsistent, then one can prove Niα ⊃ ¬Liα. Now, ¬α is also AX+
n t-consistent and by Theorem 6.2, AX′n ⊢ Sat(¬α). Then we can prove Niα ⊃ ¬Liα, as desired.