The rest of the paper is organized as follows. We review Levesque's notions,3and define a semantics with so-called k-*structures*. We then compare the framework to earlier attempts. Following that, we introduce a sound and complete axiomatization for the propositional fragment. In the last sections, we sketch the multi-agent (first-order) generalization of AEL, and prove that k-structures and
[Halpern & Lakemeyer 2001] agree on valid sentences, for an enriched language. Then, we conclude and end.

## 2 The K-Structures Approach

The non-modal part of Levesque's logic4 **ON L** consists of standard first-order logic with = and a countably infinite set of standard names N .

5 To keep matters simple, function symbols are not considered in this language. We call a predicate other than =, applied to first-order variables or standard names, an atomic formula. We write α xn to mean that the variable x is substituted in α by a standard name. If all the variables in a formula α are substituted by standard names, then we call it a *ground* formula. Here, a world is simply a set of ground atoms, and the semantics is defined over the set of all possible worlds W. The standard names are thus *rigid designators*, and denote precisely the same entities in all worlds.

ON L also has two modal operators: L and N. While Lα is to be read as "at least α is known", Nα is to be read as "at most ¬α is known". A set of possible worlds is referred to as the agent's *epistemic* state e. Defining a model to be the pair (**e, w**) for w ∈ W, components of **ON L**'s meaning of truth are:
1. **e, w** |= p iff p ∈ w and p is a ground atom, 2. **e, w** |= (m = n) iff m and n are identical standard names, 3. **e, w** |= ¬α iff **e, w** 6|= α, 4. **e, w** |= α ∨ β iff e, w |= α or **e, w** |= β, 5. e, w |= ∀**x. α** iff **e, w** |= α xn for all standard names n, 6. **e, w** |= Lα iff for all w
′ ∈ e, **e, w**′|= α, and 7. **e, w** |= Nα iff for all w
′ 6∈ e, **e, w**′|= α.

The main idea is that α is (at least) believed iff it is true at all worlds considered possible, while (at most) α is believed to be false iff it is true at all worlds considered *impossible*. So, an agent is said to only-know α, syntactically expressed as Lα ∧ N¬α, when worlds in e are precisely those where α is true. Halpern and Lakemeyer ([2001]) underline three features of the semantical framework of **ON L**,
the intuitions of which we desire to maintain in the many agent setting:
1. Evaluating Nα does *not affect* the epistemic possibilities. Formally, in **ON L**, after evaluating formulas of the form Nα the agent's epistemic state is still given by e.