A1n. All instances of propositional logic, A2n. Li(α ⊃ β) ⊃ (Liα ⊃ Liβ),
A3n. Ni(α ⊃ β) ⊃ (Niα ⊃ Niβ),
A4n. σ ⊃ Liσ ∧ Niσ for i-subjective σ, A5n. Niα ⊃ ¬Liα if ¬α is a K45n-consistent i-objective basic formula.

Observe that, as discussed, the soundness of A5n is built on K45n-consistency. Since our semantics is not based on Kripke structures, proving that every K45n-consistent formula is satisfiable in some (**k, j**)-
model is not immediate. We propose a construction called the (**k, j**)-*correspondence model*. In the following, in order to disambiguate W from Kripke worlds, we shall refer to our worlds as propositional valuations.

Definition 4.2: The K45n canonical model Mc = hWc, πc, Kca
, Kc b i is defined as follows:
1. Wc = {w | w is a (basic) maximally consistent set }
2. for all p ∈ Φ and worlds w, π c(w)(p) = true iff p ∈ w 3. (w, w′) ∈ Kc i iff w\Li ⊆ w
′
, w\Li = {α | Liα ∈ w}
Definition 4.3: Given Mc, define a set of propositional valuations W such that for each world w ∈ Wc, there is a valuation JwK ∈ W, JwK = {p | p ∈ w}.

Definition 4.4: Given Mcand a world w ∈ Wc, construct a (**k, j**)-model heJwK
k a
, eJwK
j b
, JwKi from valuations W inductively:
1. eJwK
1 a
= {hJw
′
K, **{}i |** w
′ ∈ Kca
(w)},
2. eJwK
k a
= {hJw
′
K, eJw′K
k−1 bi | w
′ ∈ Kca(w)},

$\mathbb{E}^{-1}$
$${}^{-}\perp\!\!\perp v$$

where eJw′K
k−1 b= {hJw
′′K, eJw′′K
k−2 ai | w
′′ ∈ Kc b
(w
′
)}.

Further, eJwK
j b is constructed analogously. Let us refer to this model as the (**k, j**)-correspondence model of (Mc, w).

Roughly, Defn. 4.4 is a construction of a (**k, j**)-model that appeals to the accessibility relations in the canonical model.13 Thus, a e 1a for Alice *wrt.* w has precisely the valuations of Kripke worlds w
′ ∈
Kca(w). Quite analogously, a e ka is a set {hJw
′
K, ek−1i}, where w
′ ∈ Kca(w) as before, but e k−1is an epistemic state for Bob and hence refers all worlds w
′′ ∈ Kc b
(w
′
). By a induction on the depth of a basic formula α, we obtain a theorem that α of maximal **a, b**-depth **k, j** is satisfiable at (Mc, w) iff the
(**k, j**)-correspondence model satisfies the formula.

13The construction is somewhat similar to the notion of *generated submodels* of Kripke frames [Hughes & Cresswell 1984].