Proof: Consider Sa. Each S
′ ∈ Sa is a maximally satisfiable a-objective set, and thus by definition, there is a k-structure hw
′
, ek−1 bi such that {}, ek−1 b, w′|= S
′
. Define such a set of k-structures
{hw
′
, ek−1 bi}, corresponding to each S
′ ∈ Sa, and let this be e
∗k a
. It is immediate to verify that Obj+
a
(e
∗k a
) = Sa. Analogously, for e
∗j b using Sb. Finally, there is clearly some world w
∗ where σ holds.

## 3.1 On Validity

How does the semantics compare to earlier approaches? In particular, we are interested in valid formulas. Lakemeyer ([1993]) proposes a semantics using K45n-canonical models, but he shows that the formula ¬Oa¬Obp for any proposition p is valid. Intuitively, it says that all that Alice knows is that Bob does not only know p, and as Lakemeyer argues, the validity of ¬Oa¬Obp is unintuitive. After all, Bob could *honestly* tell Alice that he does not only know p. The negation of this formula, on the other hand, is satisfiable in a Kripke structure approach by Halpern ([1993]), called the i-set approach.10 It is also satisfiable in the k-structure semantics. Interestingly, the i-set approach and k-structures agree on one more notion. The formula La**⊥ ⊃ ¬**Na¬Ob¬Oap (ζ) is valid in both, while ¬ζ is satisfiable wrt. Lakemeyer ([1993]). (It turns out that the validity of ζ in our semantical framework is implicitly related to the satisfiability of Ob¬Oap, so this property is not unreasonable.)
However, we immediately remark that the i-set approach and k-structures do not share too many similarities beyond those presented above. In fact, the i-set approach does not truly satisfy Levesque's second property. For instance, Na¬Obp ∧ La¬Obp (λ) is satisfiable in Halpern ([1993]). Recall that, in this property, the union of models that evaluate Niα and Liα must lead to all conceivable states. So, the satisfiability of λ leaves open the question as to why Obp is not considered since ¬Obp is true at all conceivable states. We show that, in contrast, λ is not satisfiable in the k-structures approach. Lastly,
[Halpern & Lakemeyer 2001] involves enriching the language, the intuitions of which are perhaps best explained after reviewing the proof theory, and so we defer discussions to later.11 Theorem 3.4: The following are properties of the semantics:
1. Oa¬Obp, for any p ∈ Φ, is satisfiable.

2. |= La**⊥ ⊃ ¬**Na¬Ob¬Oap.

3. Na¬Obp ∧ La¬Obp *is not satisfiable.*
Proof: Item 1. Let Wp = {w | w |= p} and let E be all subsets of W except the set Wp. It is easy to see that if e 1 b ∈ E, then {}, e1 b
, w 6|= Obp, for any world w. Now, define a e 2for a that has all of W ×E.

Thus, e 2a
, {}, w |= Oa¬Obp.

Item 2. Suppose e ka
, {}, w |= La⊥ for any w ∈ W. Then, for all hw
′
, ek−1 bi ∈ e ka
, e ka
, ek−1 b, w′|= ⊥,
and thus, e ka = {}. Suppose now e ka
, {}, w |= Na¬Ob¬Oap. Then, *wrt.* all of hw
′
, ek−1 b**i 6∈** e ka i.e. all of E

k, ¬Ob¬Oap must hold. That is, ¬Ob¬Oap must be valid. From above, we know this is not the case.

10In his original formulation, Halpern ([1993]) constructs *trees*. We build on discussions in [Halpern & Lakemeyer 2001].

11An approach by [Waaler 2004; Waaler & Solhaug 2005] is also motivated by the proof theory. Discussions are deferred.