Item 3. Suppose e ka
, {}, w |= La¬Obp, for any w. Then, for all hw
′
, ek−1 bi ∈ e ka
, e ka
, ek−1 b, w′|=
¬Obp. Since Obp is satisfiable, there is a e
∗k−1 bsuch that {}, e∗k−1 b, w∗|= Obp, and hw
∗
, e∗k−1 b**i 6∈** e ka
.

Then, e ka
, {}, w |= ¬Na¬Obp.

Thus, k-structures seem to satisfy our intuitions on the behavior of only-knowing. To understand why, notice that ¬Oa¬Obp and λ involve the nesting of Ni operators. Lakemeyer ([1993]) makes an unavoidable technical commitment. A (i-objective) possibility is formally a maximally K45n-consistent set of *basic* i-objective formulas. The restriction to basic formulas is an artifact of a semantics based on the canonical model. Unfortunately, there is more to agent i's possibility than just basic formulas. In the case of Halpern ([1993]), the problem seems to be that Ni and Li do not interact naturally, and that the full complement of epistemic possibilities is not considered in interpreting Ni. In contrast, Theorem 3.3 shows that we allow non-basic formulas and by using a strictly semantic notion, we avoid problems that arise from the proof-theoretic restrictions. And, since the semantics faithfully complies with the second property, λ is not satisfiable.

The natural question is if there are axioms that characterize the semantics. We begin, in the next section, with a proof theory by Lakemeyer ([1993]) that is known to be sound and complete for all attempts so far, but for a restricted language.

## 4 Proof Theory

In the single agent case, **ON L**'s proof theory consists of axioms of propositional logic, axioms that treat L and N as a classical belief operator in K45, an axiom that allows us to use N and L freely on subjective formulas, modus ponens (MP) and necessitation (NEC) for both L and N as inference rules, and the following axiom:12 A5. Nα ⊃ ¬Lα if ¬α is a propositionally consistent objective formula.

As we shall see, only the axiom A5 is controversial, since extending any objective α to any i-objective α is problematic. Mainly, the soundness of the axiom in the single agent case relies on propositional logic. But in the multi-agent case, since we go beyond propositional formulas establishing this consistency is non-trivial, and even circular. To this end, Lakemeyer ([1993]) proposes to resolve this consistency by relying on the existing logic K45n. As a consequence, his proof theoretic formulation appropriately generalizes all of Levesque's axioms, except for A5 where its application is restricted to only basic i-objective consistent formulas. We use ⊢ to denote provability.

Definition 4.1: **ON L**−
n consists of all formulas α in **ON L**n such that no Nj may occur in the scope of a Li or a Ni, for i 6= j.

The following axioms, along with MP and NEC (for Li and Ni) is an axiomatization that we refer to as AXn. AXn is sound and complete for the canonical model and the i-set approach for formulas in ON L−
n
.