
## 6 Axiomatizing Validity

Extending the work in [Lakemeyer 1993] and [Halpern 1993], which was only restricted to formulas in ON L−
n
, Halpern and Lakemeyer ([2001]) proposed a multi-agent only-knowing logic that handles the nesting of Ni operators. But as discussed, there are two undesirable features. The first is a semantics based on canonical models, and the second is a proof theory that axiomatizes validity. Although such a construction is far from natural, we show in this section that they do indeed capture the desired properties of only-knowing. This also instructs us that our axiomatization avoids such problems in a reasonable manner.

Recall that the language of [Halpern & Lakemeyer 2001] is **ON L**+
n
, which is **ON L**n and a modal operator for validity, Val. A modal operator Sat, for satisfiability, is used freely such that Val(α) is syntactically equivalent to ¬Sat(¬α). To enable comparisons, we present a variant of our logic, that has all its main features, but has additional notions to handle the extended language. We then show that this logic and [Halpern & Lakemeyer 2001] agree on the set of valid sentences from **ON L**+
n
(and also ON Ln).

The main feature of [Halpern & Lakemeyer 2001] is the proof theory AX′n
, and a semantics that is sound and complete for AX′n via the extended canonical model. AX′n consists of A1n − A4n, MP,
NEC and the following:
A5′n
. Sat(¬α) ⊃ (Niα ⊃ ¬Laα), if α is i-objective.

V1. Val(α) ∧ Val(α ⊃ β) ⊃ Val(β).

V2. Sat(p1 ∧ **. . . p**n), if pi's are literals and p1 ∧ **. . . p**n is propositionally consistent.

V3. Sat(α ∧ β1) ∧ **. . .** Sat(α ∧ βk) ∧ Sat(γ ∧ δ1)**. . .** ∧
Sat(γ ∧ δm) ∧ Val(α ∨ γ) ⊃ Sat(Liα ∧ ¬Li¬β1 **. . .** ∧
Niγ ∧ ¬Ni¬δ1 **. . .**), if α, βi**, γ, δ**i are i-objective.

V4. Sat(α) ∧ Sat(β) ⊃ Sat(α ∧ β), if α is i-objective and β is i-subjective.

NECVal. From α infer Val(α).

The essence of our new logic, in terms of a notion of depth (with |Val(α)|i = |α|i) and a semantical account over possible worlds, is as before. The complete semantic definition for formulas in **ON L**+
n of maximal **a, b**-depth of **k, j** is:
1. -8. as before, 9. e ka
, e j b
, w |= Val(α) if e ka
, e j b
, w |= α for all e ka
, e j b
, w.

Satisfiability and validity (|=) are understood analogously.15 Let **ON L**+
n 1, . . . **ON L**+
n tbe also defined analogously. Further, let axioms A1n − A5tn be defined for **ON L**+
n t. For instance, A5tn is defined for 15Note that Val corresponds precisely to how validity is defined.