any i-objective ¬α **∈ ON L**+
n t−1that is consistent with A1n − A5t−1 n. Then, the semantics above is characterized by the proof theory AX+
n tdefined (inductively) for **ON L**+
n t, consisting of AXtn
(A1n −
A5tn
, MP, NEC) with NECVal as an additional inference rule.

Lemma 6.1: *For all* α **∈ ON L**+
n t, AX+
n t⊢ α iff |= α.

The proof of this lemma, and those of the following theorems are given in the appendix. We proceed to show that Sat(α) is provable from AX′n iff α is AX+
n t-consistent.

Theorem 6.2: *For all* α **∈ ON L**+
n t, AX′n ⊢ Sat(α) iff α is AX+
n t*-consistent.*
This allows us to show that AX′n and AX+
n tagree on provable sentences.

Theorem 6.3: *For all* α **∈ ON L**+
n t, AX′n ⊢ α iff AX+
n t⊢ α.

Lemma 6.4: *For all* α **∈ ON L**+
n t, |= α iff α *is valid in*
[Halpern & Lakemeyer 2001].

Proof: AX′n is sound and complete for [Halpern & Lakemeyer 2001], and AX+
n tis sound and complete for |=.

Since it can be shown that every α **∈ ON L**+
n is provably equivalent to some α
′ **∈ ON L**n [Halpern & Lakemeyer 2001],
we also obtain the following corollary.

Corollary 6.5: *For all* α **∈ ON L**tn
, |= α iff α *is valid in [Halpern & Lakemeyer 2001].*

## 7 Conclusions

This paper has the following new results. We have a first-order modal logic for multi-agent onlyknowing that we show, for the first time, generalizes Levesque's semantics. Unlike all attempts so far, we neither make use of proof-theoretic notions of maximal consistency nor Kripke structures [Waaler & Solhaug 2005]. The benefit is that the semantic proofs are straightforward, and we understand possible worlds precisely as Levesque meant. We then analyzed a propositional subset, and showed first that the axiom system from Lakemeyer ([1993]) is sound and complete for a restricted language. We used this result to devise a new proof theory that does not require us axiomatize any semantic notions [Halpern & Lakemeyer 2001].

Our axiomatization was shown to be sound and complete for the semantics, and its use is straightforward on formulas involving the nesting of *at most* operators. In the process, we revisited the features of only-knowing and compared the semantical framework to other approaches. Its behavior seems to coincide with our intuitions, and it also captures a multi-agent generalization of Moore's AEL. Finally, although the axiomatization of Halpern and Lakemeyer ([2001]) is not natural, we showed that they essentially capture the desired properties of multi-agent only-knowing, but at much expense.

## 8 Acknowledgements

The authors would like to thank the reviewers for helpful suggestions and comments. The first author is supported by a DFG scholarship from the graduate school GK 643.