A e 1for Alice, denoted as e 1a
, is intended to represent a set of worlds {hw, {}i**, . . .**}. A e 2is of the form
{h**w, e**1 b i,hw
′
, e′1 b i**, . . .**}, and it is to be read as "at w, she believes Bob considers worlds from e 1 b possible but at w
′
, she believes Bob to consider worlds from e
′1 b possible". This conveys the idea that Alice has only partial information about Bob, and so at different worlds, her beliefs about what Bob knows differ.

We define a e kfor Alice, a e jfor Bob and a world w ∈ W as a (**k, j**)-model (e ka
, e j b
, w). Only sentences of a maximal a-depth of k, and a maximal b-depth of j are interpreted *wrt.* a (**k, j**)-model. The complete semantic definition is:

$$1.\,\,\,e_{a}^{k},e_{b}^{j},w\models p\,\mathrm{iff}\,\,p\in w\,\,\mathrm{and}\,\,p\,\,\mathrm{is~a~ground~atom},$$
4
2. e ka , e j b , w |= (m = n) iff m, n ∈ N and are identical, 3. e ka , e j b , w |= ¬α iff e ka , e j b , w 6|= α, 4. e ka , e j b , w |= α ∨ β iff e ka , e j b , w |= α or e ka , e j b , w |= β, 5. e ka , e j b , w |= ∀x. α iff e ka , e j b , w |= α xn for all n ∈ N , 6. e ka , e j b , w |= Laα iff for all hw ′ , ek−1 bi ∈ e ka , e ka , ek−1 b, w′|= α, 7. e ka , e j b , w |= Naα iff for all hw ′ , ek−1 bi 6∈ e ka , e ka , ek−1 b, w′|= α
And since Oaα syntactically denotes Laα ∧ Na¬α, it follows from the semantics that

8. e
ka
, e
j
b
, w |= Oaα iff for all worlds w
′
, for all e
k−1for Bob, hw
$$\langle w^{\prime},e_{b}^{k-1}\rangle\in e_{a}^{k}\;\mathrm{iff}$$
iff e
$$e_{a}^{k},e_{b}^{k-1},w^{\prime}\vDash$$
(The semantics for Lbα and Nbα are given analogously.) A formula α (of a-depth of k and of b-depth of j) is *satisfiable* iff there is a (**k, j**)-model such that e ka
, e j b
, w |= α. The formula is *valid* (|= α) iff α is true at all (**k, j**)-models. Satisfiability is extended to a set of formulas Σ (of maximal **a, b**-depth of **k, j**) in the manner that there is a (**k, j**)-model e ka
, e j b
, w such that e ka
, e j b
, w |= α
′
for every α
′ ∈ Σ.

We write Σ |= α to mean that for every (**k, j**)-model e ka
, e j b
, w, if e ka
, e j b
, w |= α
′
for all α
′ ∈ Σ, then e ka
, e j b
, w |= α.

Validity is not affected if models of a depth greater than that needed are used. This is to say, if α is true *wrt.* all (**k, j**)-models, then α is true *wrt.* all (k
′
, j′)-models for k
′ ≥ **k, j**′ ≥ j. We obtain this result by constructing for every e k
′

a
, a k-structure ea↓
k
′

k
, such that they agree on all formulas of maximal a-depth k. Analogously for e j
′

b
.

```
Definition 2.3: Given e
                        k
                         ′
                         
                        a
                          , we define ea↓
                                         k
                                          ′
                                          
                                         k
                                           for k
                                                ′ ≥ k ≥ 1:

```

1. ea↓
11 = e 1a
,

2. $e_{a}\downarrow_{1}^{k^{\prime}}=\{\langle w,\{\}\rangle\mid\langle w,e_{b}^{k^{\prime}-1}\rangle\in e_{a}^{k^{\prime}}\}$, 3. $e_{a}\downarrow_{k}^{k^{\prime}}=\{\langle w,e_{b}\downarrow_{k-1}^{k^{\prime}-1}\rangle\mid\langle w,e_{b}^{k^{\prime}-1}\rangle\in e_{a}^{k^{\prime}}\}$.  

