\section*{Notes}}
\newcommand{\Exer}{
\bigskip\markright{EXERCISES}
\section*{Exercises}}
\newcommand{D_G}{D_G}
\newcommand{{\rm S5}_m}{{\rm S5}_m}
\newcommand{{\rm S5C}_m}{{\rm S5C}_m}
\newcommand{{\rm S5I}_m}{{\rm S5I}_m}
\newcommand{{\rm S5CI}_m}{{\rm S5CI}_m}
\newcommand{Mart\'\i n\ }{Mart\'\i n\ }
\newcommand{\end{enumerate}\setlength{\itemsep}{-\parsep}}{\end{enumerate}\setlength{\itemsep}{-\parsep}}
\newcommand{\setlength{\itemsep}{0pt}\begin{itemize}}{\setlength{\itemsep}{0pt}\begin{itemize}}
\newcommand{\end{description}\setlength{\itemsep}{-\parsep}}{\end{description}\setlength{\itemsep}{-\parsep}}
\newcommand{\end{itemize}\setlength{\itemsep}{-\parsep}}{\end{itemize}\setlength{\itemsep}{-\parsep}}
\newtheorem{fthm}{Theorem}
\newtheorem{flem}[fthm]{Lemma}
\newtheorem{fcor}[fthm]{Corollary}
\newcommand{\slidehead}[1]{
\eject
\Huge
\begin{center}
{\bf #1 }
\end{center}
\vspace{.5in}
\LARGE}

\newcommand{_G}{_G}
\newcommand{{\bf if}}{{\bf if}}

\newcommand{{\tt \ at\_time\ }}{{\tt \ at\_time\ }}
\newcommand{\skew6\hat\ell\,}{\skew6\hat\ell\,}
\newcommand{{\bf then}}{{\bf then}}
\newcommand{{\bf until}}{{\bf until}}
\newcommand{{\bf else}}{{\bf else}}
\newcommand{{\bf repeat}}{{\bf repeat}}
\newcommand{{\cal A}}{{\cal A}}
\newcommand{{\cal E}}{{\cal E}}
\newcommand{{\cal F}}{{\cal F}}
\newcommand{{\cal I}}{{\cal I}}
\newcommand{{\cal N}}{{\cal N}}
\newcommand{{\cal R}}{{\cal R}}
\newcommand{{\cal S}}{{\cal S}}
\newcommand{B^{\scriptscriptstyle \cN}}{B^{\scriptscriptstyle {\cal N}}}
\newcommand{B^{\scriptscriptstyle \cS}}{B^{\scriptscriptstyle {\cal S}}}
\newcommand{{\cal W}}{{\cal W}}
\newcommand{E_G}{E_G}
\newcommand{C_G}{C_G}
\newcommand{C_\cN}{C_{\cal N}}
\newcommand{E_\cS}{E_{\cal S}}
\newcommand{E_\cN}{E_{\cal N}}
\newcommand{C_\cS}{C_{\cal S}}

\newcommand{\mbox{{\it attack}}}{\mbox{{\it attack}}}
\newcommand{\mbox{{\it attacking}}}{\mbox{{\it attacking}}}
\newcommand{\mbox{{\it delivered}}}{\mbox{{\it delivered}}}
\newcommand{\mbox{{\it exist}}}{\mbox{{\it exist}}}
\newcommand{\mbox{{\it decide}}}{\mbox{{\it decide}}}
\newcommand{{\it clean}}{{\it clean}}
\newcommand{{\it diff}}{{\it diff}}
\newcommand{{\it failed}}{{\it failed}}
\newcommand\eqdef{=_{\rm def}}
\newcommand{\mbox{{\it false}}}{\mbox{{\it false}}}

\newcommand{D_{\cN}}{D_{{\cal N}}}
\newcommand{D_{\cS}}{D_{{\cal S}}}
\newcommand{{\it time}}{{\it time}}
\newcommand{f}{f}

\newcommand{{\rm K}_n}{{\rm K}_n}
\newcommand{{\rm K}_n^C}{{\rm K}_n^C}
\newcommand{{\rm K}_n^D}{{\rm K}_n^D}
\newcommand{{\rm T}_n}{{\rm T}_n}
\newcommand{{\rm T}_n^C}{{\rm T}_n^C}
\newcommand{{\rm T}_n^D}{{\rm T}_n^D}
\newcommand{{\rm S4}_n}{{\rm S4}_n}
\newcommand{{\rm S4}_n^C}{{\rm S4}_n^C}
\newcommand{{\rm S4}_n^D}{{\rm S4}_n^D}
\newcommand{{\rm S5}_n}{{\rm S5}_n}
\newcommand{{\rm S5}_n^C}{{\rm S5}_n^C}
\newcommand{{\rm S5}_n^D}{{\rm S5}_n^D}
\newcommand{{\rm KD45}_n}{{\rm KD45}_n}
\newcommand{{\rm KD45}_n^C}{{\rm KD45}_n^C}
\newcommand{{\rm KD45}_n^D}{{\rm KD45}_n^D}
\newcommand{{\cal L}_n}{{\cal L}_n}
\newcommand{{\cal L}_n^C}{{\cal L}_n^C}
\newcommand{{\cal L}_n^D}{{\cal L}_n^D}
\newcommand{{\cal L}_n^{CD}}{{\cal L}_n^{CD}}
\newcommand{{\cal M}_n}{{\cal M}_n}
\newcommand{{\cal M}_n^r}{{\cal M}_n^r}
\newcommand{\M_n^{\mbox{\scriptsize{{\it rt}}}}}{{\cal M}_n^{\mbox{\scriptsize{{\it rt}}}}}
\newcommand{\M_n^{\mbox{\scriptsize{{\it rst}}}}}{{\cal M}_n^{\mbox{\scriptsize{{\it rst}}}}}
\newcommand{\M_n^{\mbox{\scriptsize{{\it elt}}}}}{{\cal M}_n^{\mbox{\scriptsize{{\it elt}}}}}
\renewcommand{\mbox{${\cal L}_n$}}{\mbox{${\cal L}_{n} (\Phi)$}}
\renewcommand{\mbox{${\cal L}_n^D$}}{\mbox{${\cal L}_{n}^D (\Phi)$}}
\newcommand{{\rm S5}_n^{DU}}{{\rm S5}_n^{DU}}
\newcommand{{\cal L}_n^D}{{\cal L}_n^D}
\newcommand{{\rm S5}_n^U}{{\rm S5}_n^U}
\newcommand{{\rm S5}_n^{CU}}{{\rm S5}_n^{CU}}
\newcommand{{\cal L}^{U}_n}{{\cal L}^{U}_n}
\newcommand{{\cal L}_n^{CU}}{{\cal L}_n^{CU}}
\newcommand{{\cal L}_n^{DU}}{{\cal L}_n^{DU}}
\newcommand{{\cal L}_n^{CU}}{{\cal L}_n^{CU}}
\newcommand{{\cal L}_n^{DU}}{{\cal L}_n^{DU}}
\newcommand{{\cal L}_n^{\it CDU}}{{\cal L}_n^{\it CDU}}
\newcommand{\C_n}{{\cal C}_n}
\newcommand{\I_n^{oa}(\Phi')}{{\cal I}_n^{oa}(\Phi')}
\newcommand{\C_n^{oa}(\Phi)}{{\cal C}_n^{oa}(\Phi)}
\newcommand{\C_n^{oa}}{{\cal C}_n^{oa}}
\newcommand{OA$_{n,\Phi}$}{OA$_{n,\Phi}$}
\newcommand{OA$_{n,{\Phi}}'$}{OA$_{n,{\Phi}}'$}
\newcommand{U}{U}
\newcommand{\, U \,}{\, U \,}
\newcommand{{\rm a.m.p.}}{{\rm a.m.p.}}
\newcommand{\commentout}[1]{}
\newcommand{\msgc}[1]{ @ #1 }
\newcommand{{\C_n^{\it amp}}}{{{\cal C}_n^{\it amp}}}
\newcommand{\begin{itemize}}{\begin{itemize}}
\newcommand{\end{itemize}}{\end{itemize}}
\newcommand{\begin{enumerate}}{\begin{enumerate}}
\newcommand{\end{enumerate}}{\end{enumerate}}
\newcommand{\stackrel{r}{\rightarrow}}{\stackrel{r}{\rightarrow}}
\newcommand{\mbox{\it ack}}{\mbox{\it ack}}
\newcommand{\G_0}{{\cal G}_0}
\newcommand{\itemsep 0pt\partopsep 0pt}{\itemsep 0pt\partopsep 0pt}
\def\seealso#1#2{({\em see also\/} #1), #2}
\newcommand{\cents}{\hbox{\rm \rlap{/}c}}
\newcommand{\mathcal{ONL}_n}{\mathcal{ONL}_n}
\newcommand{\mathcal{ONL}_n}{\mathcal{ONL}_n}
\newcommand{\mathcal{ONL}_n^-}{\mathcal{ONL}_n^-}
\newcommand{\mathcal{ONL}}{\mathcal{ONL}}

\newcommand{{e'}}{{e'}}
\newcommand{{e^*}}{{e^*}}
\newcommand{{e^\bullet}}{{e^\bullet}}

\newcommand{\mathitbf{N}_j}{\mathitbf{N}_j}
\newcommand{\mathbf{A5}_n}{\mathbf{A5}_n}
\newcommand{{AX}_n}{{AX}_n}

\newcommand{\models^{kj}}{\models^{kj}}
\newcommand{{\textsf{K45}}_{n}}{{\textsf{K45}}_{n}}
\newcommand{{e_a^k}^w, {e_b^j}^w, w}{{e_a^k}^w, {e_b^j}^w, w}
\newcommand{\ebullet_b^{k-1}}%  {e_b^{k-1}^\bullet}{{e^\bullet}_b^{k-1}

\newcommand{e_b^{j-1}}{e_b^{j-1}}
\newcommand{e_b^k}%{e_{(b,k)}}{e_b^k
\newcommand{\models^{k+1}}{\models^{k+1}}
\newcommand{\estar_a^{k+1}} %{e_{(a,k+1)}^*}{{e^*}_a^{k+1}}
\newcommand{e_a^{k-1}} %{e_{(a,k-1)}}{e_a^{k-1}}

\newcommand{S_{k''}}{S_{k''}}
\newcommand{e_{b}^{k+1}}{e_{b}^{k+1}}
\newcommand{S_{k+1}}{S_{k+1}}

\newcommand{e_a^{k+1}}%{e_{(a,k+1)}}{e_a^{k+1}
\newcommand{\estar_b^k}{{e^*}_b^k}
\newcommand{S_{k-1}}{S_{k-1}}

\newcommand{\( k \)-structure}{\( k \)-structure}
\newcommand{S_j}{S_j}
\newcommand{e^k}{e^k}
\newcommand{\kminstr}{S_{k-1}}
\newcommand{\noindent}{\noindent}
\newcommand{$\mathcal{ES}$}{$\mathcal{ES}$}
\newcommand{$\mathcal{GL}$}{$\mathcal{GL}$}
\newcommand{$\mathcal{GL}$}{$\mathcal{GL}$}
\newcommand{$(k,j)$-model}{$(k,j)$-model}
\newcommand{\langle}{\langle}
\newcommand{\rangle}{\rangle}

\newcommand{e_a^{k-2}} %{e_{(a,k-2)}}{e_a^{k-2}}
\newcommand{M^c}{M^c}
\newcommand{\mathcal{K}^c_a}{\mathcal{K}^c_a}
\newcommand{\mathcal{K}^c_i}{\mathcal{K}^c_i}
\newcommand{\mathcal{K}^c_b}{\mathcal{K}^c_b}
\newcommand{e_b^{k-2}}%{e_{(b,k-2)}}{e_b^{k-2}
\newcommand{\textit{obj}_a}{\textit{obj}_a}

\newcommand{w_{\Sigma}}{w_{\Sigma}}

\newcommand{\mathitbf{O}}{\mathitbf{O}}
\newcommand{\mathitbf{O}_i}{\mathitbf{O}_i}
\newcommand{\aknow}{\mathitbf{L}_{a}}
\newcommand{\aoknow}{\mathitbf{O}_{a}}
\newcommand{\bknow}{\mathitbf{L}_{b}}
\newcommand{\mathitbf{O}_{b}}{\mathitbf{O}_{b}}
\newcommand{\mathcal{M}^{1,j}}{\mathcal{M}^{1,j}}
\newcommand{\mathitbf{L}_i}{\mathitbf{L}_i}
\newcommand{\mathitbf{L}_i}{\mathitbf{L}_i}
\newcommand{\mathitbf{L}}{\mathitbf{L}}
\newcommand{{\mathitbf{N}}}{{\mathitbf{N}}}
\newcommand{\mathitbf{N}_i}{\mathitbf{N}_i}
\newcommand{\mathitbf{N}_a}{\mathitbf{N}_a}
\newcommand{\mathitbf{L}_a}{\mathitbf{L}_a}
\newcommand{\mathitbf{N}_b}{\mathitbf{N}_b}
\newcommand{{\mathcal{W}}_p}{{\mathcal{W}}_p}
\newcommand{{\mathcal{W}}_{\bar{p}}}{{\mathcal{W}}_{\bar{p}}}
\newcommand{e_b^1}% {e_{(b,1)}}{e_b^1

\newcommand{\varphi_{a0}}{\varphi_{a0}}
\newcommand{\varphi_{aj}}{\varphi_{aj}}
\newcommand{\varphi_{a1}}{\varphi_{a1}}
\newcommand{\varphi_{a2}}{\varphi_{a2}}
\newcommand{\psi_{a0}}{\psi_{a0}}
\newcommand{\psi_{aj}}{\psi_{aj}}
\newcommand{\psi_{a1}}{\psi_{a1}}
\newcommand{\psi_{a2}}{\psi_{a2}}

\newcommand{\oasubj}{\textit{subj}_a}
\newcommand{\oaObj}{{\bar{O}\textit{bj}}_a}
\newcommand{\canaObj}{\textit{Obj}_a}
\newcommand{\textit{Sat}}{\textit{Sat}}
\newcommand{e_b^{k''}} %{e_{(b,k'')}}{e_b^{k''}}
\newcommand{\ebullet_b^{k''}}{{e^\bullet}_b^{k''}}
\newcommand{\onl^+}{\mathcal{ONL}_n^+}
\newcommand{\axioms^+}{{AX}_n^+}
\newcommand{\onl^t}{\mathcal{ONL}_n^t}
\newcommand{{\onl^+}}{{\mathcal{ONL}_n^+}}
\newcommand{{\onl^+}^t}{{\mathcal{ONL}_n^+}^t}

\newcommand{\onl^{k+1}}{\mathcal{ONL}_n^{t+1}}
\newcommand{\axioms^t}{{AX}_n^t}
\newcommand{\models^{k}}{\models^{k}}
\newcommand{{k-1}}{{k-1}}
\newcommand{\onl^{k-1}}{\mathcal{ONL}_n^{k-1}}
\newcommand{\axioms^{k-1}}{{AX}_n^{k-1}}
\newcommand{\axioms^{t+1}}{{AX}_n^{t+1}}

\newcommand{\mathcal{W}}{\mathcal{W}}
\newcommand{\textit{subj}_i^+}{\textit{subj}_i^+}
\newcommand{\textit{obj}_i^+}{\textit{obj}_i^+}
\newcommand{\textit{subj}_a^+}{\textit{subj}_a^+}
\newcommand{\textit{obj}_a^+}{\textit{obj}_a^+}
\newcommand{\textit{subj}_b^+}{\textit{subj}_b^+}
\newcommand{\textit{obj}_b^+}{\textit{obj}_b^+}
\newcommand{{O}{bj}^+_i}{{O}{bj}^+_i}
\newcommand{{O}{bj}^+_a}{{O}{bj}^+_a}
\newcommand{{O}{bj}^+_b}{{O}{bj}^+_b}
\newcommand{\mathbf{M}_i}{\mathbf{M}_i}
\newcommand{e_b^{j'}}{e_b^{j'}}
\newcommand{e_a^1}% {e_{(a,1)}}{e_a^1
	\newcommand{e^{i}_{(b,k-1)}}{e^{i}_{(b,k-1)}}
	\newcommand{e^{\bar{i}}_{(b,k-1)}}{e^{\bar{i}}_{(b,k-1)}}
	\newcommand{\estar_b^{k-1}} %{e^{*}_{(b,k-1)}}{{e^*}_b^{k-1}}
\newcommand{e_a^{k'}}%{e_{(a,k')}}{e_a^{k'}
\newcommand{M^*}{M^*}
\newcommand{M^{\bullet}}{M^{\bullet}}
\newcommand{\estar_a^k}{{e^*}_a^k}
\newcommand{\ebullet_a^k}{{e^\bullet}_a^k}
\newcommand{\estar_b^j}{{e^*}_b^j}
\newcommand{\ebullet_b^j}{{e^\bullet}_b^j}
\newcommand{w^{*}}{w^{*}}
\newcommand{{w^{\bullet}}}{{w^{\bullet}}}
\newcommand{e_a^2}{e_a^2}
\newcommand{\mathbb{S}_k}{\mathbb{S}_k}
\newcommand{[\![}{\llbracket
\newcommand{]\!]}{\rrbracket}

\newcommand{\mathitbf{L}_j}{\mathitbf{L}_j}
\newcommand{e_{b}^{k'-1}}{e_b^{k'-1}}
\newcommand{e_b^{K-1}}{e_b^{K-1}}
\newcommand{e_b^{K'-1}}{e_b^{K'-1}}
\newcommand{e_a^{K'}}{e_a^{K'}}
	\newcommand{e_a^K}{e_a^K}
\newcommand{\textit{HL}~}{\textit{HL}~}
	\newcommand{\bigvee \gamma_a}{\bigvee \gamma_a}
	\newcommand{\bigvee \gamma_b}{\bigvee \gamma_b}
	\newcommand{e_a^{j+1}}{e_a^{j+1}}
\newcommand{e_b^{2k}}{e_b^{2k}}
\newcommand{\ebullet^{2k}_b}{{e^\bullet}^{2k}_b}
\newcommand{\textit{Val}}{\textit{Val}}

\newcommand{\mathbb{S}_{k-1}}{\mathbb{S}_{k-1}}
\newcommand{e_a^k}{e_a^k}
\newcommand{e_b^{k-1}}{e_b^{k-1}}
\newcommand{\emph{wrt.}~}{\emph{wrt.}~}
\newcommand{\mathcal{N}}{\mathcal{N}}

\newcommand{{\dl w \dr}}{{[\![ w ]\!]}}
\newcommand{{\dl w' \dr}}{{[\![ w' ]\!]}}
\newcommand{{e_{\dl w \dr}}}{{e_{[\![ w ]\!]}}}
\newcommand{\edash_b^{k-1}}{{e'}_b^{k-1}}
\newcommand{{e_{\dl w' \dr}}}{{e_{[\![ w' ]\!]}}}
\newcommand{e_{\dl w'' \dr}}{e_{[\![ w'' ]\!]}}

\newcommand{{\ew}_a^{k'}}{{{e_{\dl w \dr}}}_a^{k'}}

\newcommand{{\ew}_a^k}{{{e_{\dl w \dr}}}_a^k}
\newcommand{{\ew}_a^{j+1}}{{{e_{\dl w \dr}}}_a^{j+1}}
\newcommand{{\ew}_a^{k+1}}{{{e_{\dl w \dr}}}_a^{k+1}}
\newcommand{{\ew}_a^{K}}{{{e_{\dl w \dr}}}_a^{K}}
\newcommand{\estar_a^{j+1}}{{e^*}_a^{j+1}}
\newcommand{{\ew}_b^j}{{{e_{\dl w \dr}}}_b^j}
\newcommand{{\ew}_b^J}{{{e_{\dl w \dr}}}_b^J}
\newcommand{{\ewdash}_a^k}{{{e_{\dl w' \dr}}}_a^k}
\newcommand{{\ewdash}_b^j}{{{e_{\dl w' \dr}}}_b^j}

\newcommand{{\ewdash}_b^{k-1}}{{{e_{\dl w' \dr}}}_b^{k-1}}
\newcommand{{\ewdashdash}_a^{k-2}}{{e_{\dl w'' \dr}}_a^{k-2}}

\newcommand{e_b^j}{e_b^j}
\newcommand{\eak, \ebj, w}{e_a^k, e_b^j, w}

\newcommand{\hgap}{\hspace{0.5cm}}
\newcommand{\todo}[1]{\marginpar{\tiny\textcolor{orange}{#1}}}

\section{Introduction}
\label{sec:introduction}

Levesque's notion of only-knowing is a single agent monotonic logic that was
proposed with the intention of capturing certain types of nonmonotonic
reasoning. Levesque (\citeyear{77758}) already showed that there is a close connection to
Moore's (\citeyear{2781}) autoepistemic logic (AEL). Recently, Lakemeyer and Levesque
(\citeyear{lakemeyer2005only}) showed that only-knowing can be adapted to capture default logic as
well. The main benefit of using Levesque's logic is that, via simple semantic
arguments, nonmonotonic conclusions can be reached without the use of
meta-logical notions such as fixpoints \cite{330786,levesque2001logic} . Only-knowing is then naturally of
interest in a many agent context, since agents capable of non-trivial
nonmonotonic behavior should believe other agents to also be equipped with
nonmonotonic mechanisms. For instance, if all that Bob knows is that Tweety is
a bird and a default that birds typically fly, then Alice, if she knows all
that Bob knows, concludes that Bob believes Tweety can fly.\footnote{We use
the terms "knowledge" and "belief" interchangeably in the paper.} Also, the
idea of only-knowing a collection of sentences is useful for modeling the beliefs of a
knowledge base (KB), since sentences that are not logically entailed by the KB
are taken to be precisely those not believed. If many agents are involved, and
suppose Alice has some beliefs on Bob's KB, then she could capitalize on Bob's
knowledge to collaborate on tasks, or plan a strategy against him.

As a logic, Levesque's construction is unique in the sense that in addition to
a classical epistemic operator for belief, he introduces a modality to denote
what is \emph{at most} known. This new modality has a subtle relationship to
the belief operator that makes extensions to a many agent case non-trivial.
Most extensions so far make use of arbitrary Kripke structures, that already
unwittingly discard the simplicity of Levesque's semantics. They also have
some undesirable properties, perhaps invoking some caution in their usage. For
instance, in a canonical model (Lakemeyer 1993), certain types of epistemic
states cannot be constructed. In another Kripke approach (Halpern 1993), the
modalities do not seem to interact in an intuitive manner. Although an approach
by Halpern and Lakemeyer (\citeyear{1029713}) does indeed successfully model
multi-agent only-knowing, it forces us to have the semantic notion of validity
directly in the language and has proof-theoretic constructs in the semantics
via maximally consistent sets. Precisely for this reason, that proposal is not
natural, and it is matched with a proof theory that has a set of new axioms to
deal with these new notions. It is also not clear how one can extend their
semantics to the first-order case. Lastly, an approach by Waaler (\citeyear{DBLP:conf/aiml/Waaler04}) avoids such an axiomatization of validity, but the model theory also has problems \cite{DBLP:conf/tark/WaalerS05}. Technical discussions on their semantics are deferred to later.

The goal of this paper is to show that there is indeed a natural semantics for
multi-agent only-knowing for the quantified language with equality. For the
propositional subset, there is also a sound and complete axiomatization that
faithfully generalizes Levesque's proof theory.\footnote{The proof theory for
a quantified language is well known to be \emph{incomplete} for the single
agent case. It is also known that any complete axiomatization cannot be
\emph{recursive} \cite{204824,levesque2001logic}.} We also differ from Halpern
and Lakemeyer in that we do not enrich the language any more than necessary
(modal operators for each agent), and we do not make use of canonical Kripke
models. And while canonical models, in general, are only workable semantically
and can not be used in practice, our proposal has a computational appeal to
it. We also show that if we do enrich the language with a modal operator for
\emph{validity}, but only to establish a common language with \cite{1029713},
then we agree on the set of valid sentences. Finally, we obtain a
first-order multi-agent generalization of AEL, defined solely using notions of
classical logical entailment and theoremhood.

The rest of the paper is organized as follows. We review Levesque's notions,\footnote{There are other notions of "all I know", which will not be discussed here \cite{101989,ben1989all}. Also see \cite{330786}.} and
define a semantics with so-called \( k \)-\emph{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 \cite{1029713} agree on valid sentences, for an enriched language. Then, we conclude and end.

\newcommand{\mathcal{ONL}}{\mathcal{ONL}}

\section{The \( k \)-structures Approach}
\label{sec:the_logic}

The non-modal part of Levesque's logic\footnote{We name the logic following \cite{1029713} for ease of comparisons later on. It is referred to as \( \mathcal{OL} \) in \cite{204824,levesque2001logic}.} \( \mathcal{ONL} \) consists of standard
first-order logic with \( = \) and a countably infinite set of standard names \(
\mathcal{N} \).\footnote{More precisely, we have logical connectives \( \lor
  \), \( \forall \) and \( \neg \). Other connectives are taken for their usual syntactic
  abbreviations.}  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 \emph{atomic} formula. We write \(
\alpha^x_n \) to mean that the variable \( x \) is substituted in \( \alpha \) by a standard
name. If all the variables in a formula \( \alpha \) are substituted by standard
names, then we call it a \emph{ground} formula. Here, a world is simply a set of ground atoms, and the semantics is defined over the set of all possible worlds \( \mathcal{W} \).
The standard names are thus \emph{rigid designators}, and denote
  precisely the same entities in all worlds. \( \mathcal{ONL} \) also has two modal
operators: \( \mathitbf{L} \) and \( {\mathitbf{N}} \). While \( \mathitbf{L} \alpha \) is
to be read as "at least \( \alpha \) is known", \( {\mathitbf{N}} \alpha \) is to be
read as "at most \( \neg \alpha \) is known". A set of possible worlds is
referred to as the agent's \emph{epistemic state} \( e \). Defining a model to
be the pair \( (e,w) \) for \( w \in \mathcal{W} \), components of \( \mathcal{ONL} \)'s
meaning of truth are: \begin{enumerate}
	\item \( e,w\models p \) iff \( p \in w \) and \( p \) is a ground atom,

	\item \( e,w \models (m = n) \) iff \( m \) and \( n \) are identical standard names,

	\item \( e, w\models \neg \alpha \) iff \( e,w\not\models \alpha \),

	\item \( e, w\models \alpha \lor \beta \) iff \(  e,w \models \alpha \) or \( e,w\models \beta \),

	\item \( e,w\models \forall x.~\alpha \) iff \( e,w\models \alpha^x_n \) for all standard names \( n \),

	\item \( e,w \models \mathitbf{L} \alpha \) iff for all \( w' \in e \), \( e, w' \models \alpha \), and

	\item \( e,w\models {\mathitbf{N}} \alpha \) iff for all \( w' \not\in e \), \( e,w' \models \alpha \).
\end{enumerate}

\noindent The main idea is that \( \alpha \) is (at least) believed iff it is true at all worlds considered possible, while (at most) \( \alpha \) is believed to be false iff it is true at all worlds considered \emph{impossible}. So, an agent is said to only-know \( \alpha \), syntactically expressed as \( \mathitbf{L} \alpha \land {\mathitbf{N}} \neg \alpha \), when worlds in \( e \) are precisely those where \( \alpha \) is true. Halpern and Lakemeyer (\citeyear{1029713}) underline three features of the semantical framework of \( \mathcal{ONL} \), the intuitions of which we desire to maintain in the many agent setting: \begin{enumerate}
	\item Evaluating \( {\mathitbf{N}}\alpha \) does \emph{not affect} the epistemic possibilities.  Formally, in \( \mathcal{ONL} \), after evaluating formulas of the form \( {\mathitbf{N}}\alpha   \) the agent's epistemic state is still given by \( e \).

	\item A union of the agent's possibilities, that evaluate \( \mathitbf{L} \),
and the impossible worlds that evaluate \( {\mathitbf{N}} \), is \emph{fixed} and
\emph{independent} of \( e \), and is the set of all \emph{conceivable}
states. Formally, in \( \mathcal{ONL} \), \( \mathitbf{L}\alpha \) is evaluated \emph{wrt.}~ worlds
\( w\in e \), and \( {\mathitbf{N}}\alpha \) is evaluated \emph{wrt.}~ worlds \( w\in
\mathcal{W} -e \); the union of which is \( \mathcal{W} \). The intuition is that the
exact complement of an agent's possibilities is used in evaluating \(
{\mathitbf{N}} \).

	\item Given any set of possibilities, there is always a model where \emph{precisely} this set is the epistemic state. Formally, in \( \mathcal{ONL} \), any subset of \( \mathcal{W} \) can be defined as the epistemic state.
\end{enumerate}

\noindent Although these notions seem clear enough in the single agent case, generalizing them to the many agent case is non-trivial \cite{1029713}. We shall return to analyze the features shortly. Let us begin by extending the language. Let \( \mathcal{ONL}_n \) be a first-order modal language that enriches the non-modal subset of \( \mathcal{ONL} \) with modal operators \( \mathitbf{L}_i \) and \( \mathitbf{N}_i \) for \( i = a,b \). For ease of exposition, we only have two agents \( a \) (Alice) and \( b \) (Bob). Extensions to more agents is straightforward. We freely use \( \mathitbf{O}_i \), such that \( \mathitbf{O}_i \alpha \) is an abbreviation for \( \mathitbf{L}_i \alpha \land \mathitbf{N}_i \neg \alpha	 \), and is read as "all that \( i \) knows is \( \alpha \)". Objective and subjective formulas are understood as follows.

\begin{definition} The \( i \)-depth of a formula \( \alpha \), denoted \( |\alpha|_i \), is defined inductively as (\( \Box_i \) denotes \( \mathitbf{L}_i \) or
 \( \mathitbf{N}_i \)):	\begin{enumerate}
		\item \( |\alpha|_i = 1 \) for atoms,

		\item \( |\neg \alpha|_i = |\alpha|_i \),

		\item \( |\forall x.~\alpha|_i = |\alpha|_i \),

		\item \( |\alpha \lor \beta|_i = \textrm{max}(|\alpha|_i, |\beta|_i) \),

		\item \( |\Box_i \alpha|_i = |\alpha|_i \) ,

		\item \( |\Box_j\alpha|_i = |\alpha|_j + 1 \), for \( j \neq i \)
	\end{enumerate}
	A formula has a depth \( k \) if max(\( a \)-depth,\( b \)-depth) = \( k \). A formula is called \( i \)-objective if all epistemic operators which do not occur within the scope of another epistemic operator are of the form $\Box_j$ for $i\ne j$. A formula is called \( i \)-subjective if every atom is in the scope of an epistemic operator and all epistemic operators which do not occur within the scope of another epistemic operator are of the form $\Box_i.$
\end{definition}

 For example, a formula of the form \( \aknow \bknow \aknow p \lor \bknow q\) has a depth of \( 4 \), a \( a \)-depth of \( 3 \) and a \( b \)-depth of \( 4 \).  \( \bknow q \) is both \( b \)-subjective and \( a \)-objective. A formula is called \emph{objective} if it does not mention any modal operators. A formula is called \emph{basic} if it does not mention any \( \mathitbf{N}_i \) for \( i = a,b \). We now define a notion of epistemic states using \( k \)-\emph{structures}. The main intuition is that we keep separate the worlds Alice believes from the worlds she considers Bob to believe, to depth \( k \).

\begin{definition} A \( k \)-structure{} (\( k \geq 1 \)), say \( e^k \), for an agent is defined inductively as: \begin{itemize}

	\item[$-$] \( e^1 \subseteq \mathcal{W} \times\{ \{\}\}, \)

	\item[$-$] \( e^k \subseteq \mathcal{W} \times \mathbb{E}^{k-1},  \) where \( \mathbb{E}^{m} \) is the set of all \( m\)-structures.

\end{itemize}

\end{definition}

\noindent A \( e^1 \) for Alice, denoted as \( e_a^1}% {e_{(a,1)} \), is intended to represent a set of worlds \( \{ \langle w, \{\} \rangle, \ldots \} \). A \( e^2 \) is of the form \( \{ \langle w, e_b^1 \rangle, \langle w', {e'}_b^1 \rangle, \ldots \} \), and it is to be read as "at \( w \), she believes Bob considers worlds from \( e_b^1 \) possible but at \( w' \), she believes Bob to consider worlds from \( {e'}_b^1 \) 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^k \) for Alice, a \( e^j \) for Bob and a world \( w \in \mathcal{W} \) as a \( (k,j) \)-model \( (e_a^k, e_b^j,w) \). Only sentences of a maximal \( a \)-depth of \( k \), and a maximal \( b \)-depth of \( j \) are interpreted \emph{wrt.}~{}a \( (k,j) \)-model. The complete semantic definition is:

\begin{enumerate}
	\item \( \eak, \ebj, w \models p \) iff \( p \in w \) and \( p \) is a ground atom,

	\item \( \eak, \ebj, w \models (m = n) \) iff \( m,n \in \mathcal{N} \) and are identical,
\item \( \eak, \ebj, w \models \neg \alpha \) iff \( \eak, \ebj, w \not\models \alpha \),
\item \( \eak, \ebj, w \models \alpha \vee \beta \) iff  \( \eak, \ebj, w \models \alpha \) or \( \eak, \ebj, w \models \beta \),

\item \( \eak, \ebj, w \models \forall x.~\alpha \) iff \( \eak, \ebj, w \models \alpha^x_n \) for all \( n \in \mathcal{N} \),
\item \( \eak, \ebj, w \models \aknow \alpha \) iff for all \( \langle w', {e_b^{k-1}} \rangle \in {e_a^k} \),\\ \( {e_a^k}, {e_b^{k-1}}, w' \models \alpha \),
\item\label{i:nknow} \( \eak, \ebj, w \models \mathitbf{N}_a \alpha \) iff for all \( \langle w', {e_b^{k-1}} \rangle \not\in {e_a^k} \),\\ \( {e_a^k}, {e_b^{k-1}}, w' \models \alpha \)
\end{enumerate}

\noindent And since \( \aoknow \alpha  \) syntactically denotes \( \aknow \alpha \land \mathitbf{N}_a \neg \alpha \), it follows from the semantics that
\begin{enumerate}
	\item[8.] \( \eak, \ebj, w \models \aoknow \alpha \) iff for all worlds \( w' \),
	for all \( e^{k-1} \) for Bob,
	\( \langle w', {e_b^{k-1}} \rangle \in {e_a^k} \) iff \( {e_a^k}, {e_b^{k-1}}, w' \models \alpha \)
\end{enumerate}

\noindent (The semantics for \( \bknow\alpha \) and \( \mathitbf{N}_b \alpha \) are given analogously.) A formula \( \alpha \) (of \( a \)-depth of \( k \) and of
\( b \)-depth of \( j \)) is \emph{satisfiable} iff there is a \( (k,j)
\)-model such that \( e_a^k, e_b^j,w \models \alpha \). The formula is
\emph{valid} (\( \models \alpha \)) iff \( \alpha \) is true at all \( (k,j) \)-models. Satisfiability is extended to a set of formulas \( \Sigma \) (of maximal \( a,b \)-depth of \( k,j \)) in the manner that there is a \( (k,j) \)-model \( \eak, \ebj, w \) such that \( \eak, \ebj, w \models \alpha' \) for every \( \alpha' \in \Sigma \). We write \( \Sigma \models \alpha \) to mean that for every \(
(k,j) \)-model \( \eak, \ebj, w \), if \( \eak, \ebj, w \models \alpha' \) for all \( \alpha' \in
\Sigma \), then \( \eak, \ebj, w \models \alpha \).

\newcommand{{e_a}{\downarrow}_k^{k'}}{{e_a}{\downarrow}_k^{k'}}
\newcommand{{e_b}{\downarrow^{k'-1}_{k-1}}}{{e_b}{\downarrow}_{k-1}^{k'-1}}
\newcommand{{e_a}{\downarrow}_0^{k'}}{{e_a}{\downarrow}_0^{k'}}

Validity is not affected if models of a depth greater than that needed are used. This is to say, if \( \alpha \) is true \emph{wrt.}~all \( (k,j) \)-models, then \( \alpha \) is true \emph{wrt.}~all \( (k',j') \)-models for  \( k'\geq k,j'\geq j \). We obtain this result by constructing for every \( e_a^{k'}}%{e_{(a,k')} \), a \( k \)-structure \( {e_a}{\downarrow}_k^{k'} \), such that they agree on all formulas of maximal \( a \)-depth \( k \). Analogously for \( e_b^{j'} \).

\newcommand{{e_a}{\downarrow^{k'}_1}}{{e_a}{\downarrow^{k'}_1}}

\begin{definition} Given \( e_a^{k'}}%{e_{(a,k')} \), we define \( {e_a}{\downarrow}_k^{k'} \) for
  $k'\ge k \geq 1$: \begin{enumerate}

  \item  \( {e_a}{\downarrow^1_1} = e_a^1}% {e_{(a,1)} \),

  \item \( {e_a}{\downarrow^{k'}_1} = \{ \langle w, \{\} \rangle \mid \langle w, e_{b}^{k'-1} \rangle \in e_a^{k'}}%{e_{(a,k')} \} \),
	\item \( {e_a}{\downarrow}_k^{k'} = \{ \langle w, {e_b}{\downarrow^{k'-1}_{k-1}} \rangle \mid \langle w, e_{b}^{k'-1} \rangle \in e_a^{k'}}%{e_{(a,k')} \} \).
\end{enumerate}

\end{definition}

\newcommand{{e_b}{\downarrow}^{j'}_j}{{e_b}{\downarrow}^{j'}_j}
\newcommand{{e_a}{\downarrow}_{k-1}^{k'}}{{e_a}{\downarrow}_{k-1}^{k'}}
\newcommand{{e_b}{\downarrow^{k'-1}_{j-1}}}{{e_b}{\downarrow^{k'-1}_{j-1}}}
\newcommand{{e_a}{\downarrow_1^{k'}}}{{e_a}{\downarrow_1^{k'}}}
\newcommand{{e_b}{\downarrow_1^{k'-1}}}{{e_b}{\downarrow_1^{k'-1}}}
\newcommand{{e_a}{\downarrow_2^{k'}}}{{e_a}{\downarrow_2^{k'}}}
\newcommand{{e_b}{\downarrow_2^{j'}}}{{e_b}{\downarrow_2^{j'}}}

\begin{lemma}\label{lem:satisfiability_higher_structures} For all formulas \( \alpha \) of maximal \( a,b \)-depth of \( k,j \), \( e_a^{k'}}%{e_{(a,k')}, e_b^{j'}, w \models \alpha \) iff \( {e_a}{\downarrow}_k^{k'}, {e_b}{\downarrow}^{j'}_j, w \models \alpha \), for \( k' \geq k,j'\geq j \).
\end{lemma}

\begin{proof} By induction on the depth of formulas.~The proof immediately holds for atomic formulas, disjunctions and negations since we have the same world \( w \). Assume that the result holds for formulas of \( a,b \)-depth \( 1 \). Let \( \alpha \) such a formula, and suppose \( e_a^{k'}}%{e_{(a,k')}, e_b^{j'}, w\models \aknow \alpha \) (where \( \aknow \alpha \) has \( a,b \)-depth of \( 1,2 \)). Then, for all \( \langle w', e_{b}^{k'-1} \rangle \in e_a^{k'}}%{e_{(a,k')} \), \( e_a^{k'}}%{e_{(a,k')}, e_{b}^{k'-1}, w'\models \alpha \) iff (by induction hypothesis) \( {e_a}{\downarrow_1^{k'}}, {e_b}{\downarrow_1^{k'-1}}, w'\models \alpha \) iff \( {e_a}{\downarrow_2^{k'}}, \{\}, w\models \aknow \alpha \). By construction, we also have \( {e_a}{\downarrow_1^{k'}}, \{\},w\models \aknow \alpha \). Lastly, since \( \aknow \alpha  \) is \( a \)-subjective, \( b \)'s structure is irrelevant, and thus, \( {e_a}{\downarrow_1^{k'}}, {e_b}{\downarrow_2^{j'}}, w\models \aknow\alpha \).

For the reverse direction, suppose \( {e_a}{\downarrow_1^{k'}}, {e_b}{\downarrow_2^{j'}}, w\models \aknow \alpha \). Then for all \( w' \in {e_a}{\downarrow_1^{k'}} \), \( {e_a}{\downarrow_1^{k'}}, \{\}, w' \models \alpha \) iff (by construction) for all \( \langle w', e_{b}^{k'-1} \rangle \in e_a^{k'}}%{e_{(a,k')} \), \( e_a^{k'}}%{e_{(a,k')}, e_{b}^{k'-1}, w' \models \alpha \) iff \( e_a^{k'}}%{e_{(a,k')}, \{\}, w \models \aknow \alpha \). Since \( b \)'s structure is irrelevant, we have \( e_a^{k'}}%{e_{(a,k')}, e_b^{j'}, w \models \aknow \alpha  \). The cases for \( \bknow \alpha \), \( \mathitbf{N}_a \alpha \) and \( \mathitbf{N}_b \alpha \) are completely symmetric.
	\eprf \end{proof}

\begin{theorem} For all formulas \( \alpha \) of \( a,b \)-depth of \(
  k,j \), if \( \alpha \) is true at all \( (k,j) \)-models, then \( \alpha \)
  is true at all \( (k',j') \)-models with $k'\ge k$ and $j'\ge j$.

\end{theorem}

\begin{proof} Suppose \( \alpha \) is true at all \( (k,j) \)-models. Given any \( (k',j') \)-model, by assumption \( {e_a}{\downarrow}_k^{k'}, {e_b}{\downarrow}^{j'}_j, w\models \alpha \) and by Lemma \ref{lem:satisfiability_higher_structures}, \( e_a^{k'}}%{e_{(a,k')}, e_b^{j'}, w\models \alpha \).
	\eprf \end{proof}

\noindent Knowledge with \( k \)-structures satisfy \emph{weak} \( \textsf{S5} \) properties, and the Barcan formula \cite{nla.cat-vn2004742}.
\begin{lemma} If \( \alpha \) is a formula, the following are valid \emph{wrt.}~ models of appropriate depth (\( \Box_i \) denotes \( \mathitbf{L}_i \) or \( \mathitbf{N}_i \)): \begin{enumerate}
	\item \( \Box_i \alpha \land \Box_i(\alpha \supset \beta) \supset \Box_i \beta \),

	\item \( \Box_i \alpha \supset \Box_i\Box_i \alpha \),

	\item \( \neg \Box_i \alpha \supset \Box_i \neg \Box_i \alpha \),

	\item \( \forall \mathitbf{x}.~\Box_i \alpha \supset \Box_i(\forall \mathitbf{x}.~\alpha) \).
\end{enumerate}

\end{lemma}

\begin{proof} The proofs are similar. For item 3, wlog let \( \Box_i \) be \( \aknow \). Suppose \( e_a^k, e_b^j, w \models \neg \aknow \alpha \). There is some \( \langle w',e_b^{k-1} \rangle \in e_a^k \) such that \( e_a^k, e_b^{k-1}, w' \models \neg \alpha \). Let \( w'' \) be any world such that \( \langle w'', \edash_b^{k-1} \rangle \in e_a^k \). Then, \( e_a^k, \edash_b^{k-1}, w'' \models \neg \aknow \alpha \). Thus, \( e_a^k, e_b^j, w\models \aknow \neg \aknow \alpha \). The case of \( \mathitbf{N}_a \) is analogous.
	\eprf \end{proof}

\newcommand{\textit{true}}{\textit{true}}

\noindent Before moving on, let us briefly reflect on the fact that $k$-structures
have finite depth. So suppose \( a \) only-knows KB, of depth \( k \). Using
\( k \)-structures allows us to reason about what is believed, up to depth \(
k \). Also, if we construct epistemic states from \( k' \)-structures where \(
k'\geq k \), then the logic correctly captures non-beliefs beyond the depth \(
k \). To illustrate, let \( \textit{true} \) (depth \( 1 \)) be all that \( a \)
knows. Then, it can easily be shown that both the sentences \( \aoknow(\textit{true})
\supset \neg \aknow\neg \bknow \alpha \) and \( \aoknow(\textit{true}) \supset \neg
\aknow \bknow \alpha \) are valid sentences in the logic, by considering any
\( e^2 \) (and higher) for \( a \). For most purposes, this restriction of
having a parameter \( k \) seems harmless in the sense that agents usually
have a finite knowledge base with sentences of some maximal depth $k$ and they
should not be able to conclude anything about what is known at depths higher
than $k$, with one exception. If we were to include a notion of common
knowledge \cite{reasoning:about:knowledge}, then we would get entailments
about what is believed at arbitrary depths. With our current model, this
cannot be captured, but we are willing to pay that price because in return we
get, for the first time, a very simple possible-world style account of
only-knowing. Similarly,
we have nothing to say about (infinite) knowledge bases with unbounded depth.

\section{Multi-Agent Only-Knowing}
\label{sec:multi_agent_only_knowing}

In this section, we return to the features of only-knowing discussed earlier
and verify that the new semantics reasonably extends them to the
multi-agent case.  We also briefly discuss earlier attempts at capturing these features.  Halpern (\citeyear{DBLP:conf/aaai/Halpern93}), Lakemeyer (\citeyear{Lakemeyer1993}), and Halpern and Lakemeyer (\citeyear{1029713}) independently attempted to
extend \( \mathcal{ONL} \) to the many agent case.\footnote{For space reasons, we do not review all
aspects of these approaches.} There are some subtle differences in
their approaches, but the main restriction is they only allow a propositional
language. Henceforth, to make the comparison feasible, we shall also speak of
the propositional subset of \( \mathcal{ONL}_n \) with the understanding that the
semantical framework is now defined for propositions (from an infinite set \(
\Phi \)) rather than ground atoms.

The main component in these features is the notion of
\emph{possibility}.
In the single agent case, each world represents a
possibility. Thus, from a logical viewpoint, a possibility is simply the set of
objective formulas true at some world. Further, the set of epistemic possibilities is given
by \( \{ \{\textrm{objective formulas true at}~w \} \mid w\in e\} \). Halpern and
Lakemeyer (\citeyear{1029713}) correctly argue that the appropriate generalization of
the notion of possibility in the many agent case are \( i \)-objective
formulas. Intuitively, a possible state of affairs according to \( a \)
include the state of the world (objective formulas), as well as what \( b \)
is taken to believe.
The earlier attempts by Halpern and Lakemeyer use Kripke
structures with accessibility relations \( \mathcal{K}_i \) for each agent \( i \). Given a Kripke structure \( M \), the notion of possibility is defined as the set of \( i \)-objective formulas true at some Kripke world, and the set of epistemic possibilities is obtained from the \( i \)-objective formulas true at all \( i	 \)-accessible worlds. Formally, the set of epistemic possibilities true at \( (M,w) \), where \( w \) is a world in \( M \), is defined as \( \{ \textit{obj}_i^+(M,w') \mid
w' \in \mathcal{K}_i(w) \} \), where \( \textit{obj}_i^+(M,w') \) is a set consisting of
\( i \)-objective formulas true at \( (M,w') \).\footnote{The superscript \( +
\) denotes that the set includes non-basic formulas. Given \( X^+ \), we let
\( X = \{ \phi ~\textrm{is basic}~ \mid \phi \in X^+ \} \). } Although intuitive, note that, even
for the propositional subset of \( \mathcal{ONL} \), a Kripke world is a completely
different entity from what Levesque supposes. Perhaps, one consequence is that
the semantic proofs in earlier approaches are very involved. In contrast, we
define worlds exactly as Levesque supposes. And, our notion of possibility is obtained from the set of \( a
\)-objective formulas true at each \( \langle w, e_b^{k-1} \rangle \) in \( e_a^k \).

\newcommand{e_a^{j-1}}{e_a^{j-1}}

\begin{definition} Suppose \(M = (\eak, \ebj, w) \) is a \( (k,j) \)-model. \begin{enumerate}

\item  let \( \textit{obj}_i^+(M) = \{ \textrm{\( i \)-objective \( \phi \)} \mid M \models \phi \} \),

\item  let \( {O}{bj}^+_a({e_a^k}) = \{ \textit{obj}_a^+(\{\}, {e_b^{k-1}}, w) \mid \langle w, {e_b^{k-1}} \rangle \in {e_a^k} \} \),

\item let \( {O}{bj}^+_b(e_b^j) = \{ \textit{obj}_b^+(e_a^{j-1}, \{\}, w) \mid \langle w, e_a^{j-1} \rangle \in e_b^j \} \).
\end{enumerate}

\end{definition}

\noindent All the \( a \)-objective formulas true at a model \( M \), essentially the objective formulas true \emph{wrt.}~\( w \) and the \( b \)-subjective formulas true w\emph{rt.}~\( e_b^j \), are given by \( \textit{obj}_a^+(M) \). Note that these formulas do not strictly correspond to \( a \)'s possibilities. Rather, we define \( {O}{bj}^+_a \) on her epistemic state \( e_a^k \), and this gives us  all the \( a \)-objectives formulas that \( a \) considers possible. We shall now argue that the intuition of all of Levesque's properties is maintained.\footnote{It is interesting to note that such a formulation of Levesque's properties is not straightforward in the first-order case. That is, for the quantified language, it is known that there are epistemic states that can not be  characterized using only objective formulas \cite{levesque2001logic}. Thus, it is left open how one must correctly generalize the features of first-order \( \mathcal{ONL} \). } \\

\noindent \textbf{Property 1.}~In the single agent case, this property ensured that an agent's epistemic possibilities are not affected on evaluating \( {\mathitbf{N}} \). This is immediately the case here. Given a model, say \( (\eak, \ebj, w) \), \( a \)'s epistemic possibilities are determined by \( {O}{bj}^+_a({e_a^k}) \). To evaluate \( \mathitbf{N}_a\alpha \), we consider all models \(  ({e_a^k}, {e_b^{k-1}}, w' ) \) such that \( \langle w', {e_b^{k-1}} \rangle \not\in {e_a^k}	  \). Again, \( a \)'s possibilities are given by \( {O}{bj}^+_a({e_a^k}) \) for all these models, and does not change. \\[1ex]
\noindent \textbf{Property 2.} In the single agent case, this property ensured that evaluating \( \mathitbf{L}\alpha \) and \( {\mathitbf{N}}\alpha \) is always \emph{wrt.}~ the set of all possibilities, and completely independent of \( e \). As discussed, in the many agent case, possibilities mean \( i \)-objective formulas and analogously, if \( \alpha \) is a possibility in \( a \)'s view, say an \( a \)-objective formula of maximal \( b \)-depth of \( k \), then we should interpret \( \aknow \alpha \) and \( \mathitbf{N}_a \alpha \) \emph{wrt.}~all \( a \)-objective possibilities of max.~depth \( k \): the set of \( (k+1) \)-structures. Clearly then, the result is fixed and independent of the corresponding \( e^{k+1} \). The following lemma is a direct consequence of the definition of the semantics.

\begin{lemma} Let \( \alpha \) be a \( i \)-objective formula of \( j \)-depth \( k \), for \( j \neq i \). Then, the set of \( k\!+\!1 \)-structures that evaluate \( \mathitbf{L}_i \alpha \) and \( \mathitbf{N}_i \alpha \) is \( \mathbb{E}^{k+1} \).

\end{lemma}

\noindent \textbf{Property 3.} The third property ensures that one can characterize
epistemic states from any set of \( i \)-objective formulas. Intuitively,
given such a set, we must have a model where \emph{precisely} this set is the
epistemic state. Earlier attempts at clarifying this property involved
constructing a \emph{set} of maximally \( {\textsf{K45}}_{n} \)-consistent sets of basic \(
i \)-objective formulas, and showing that there exist an epistemic state that precisely corresponds to this set. But, defining possibilities via \( {\textsf{K45}}_{n} \)
proof-theoretic machinery inevitably leads to some limitations, as we shall
see. We instead proceed semantically, and go beyond basic formulas. Let \(
\Omega \) be a satisfiable set of \( i \)-objective formulas, say of maximal
\( j \)-depth \( k \), for \( j\neq i \). Let \( \Omega' \) be a set obtained by adding a \( i
\)-objective formula \( \gamma \) of maximal \( j \)-depth \( k \) such that \(
\Omega' \) is also satisfiable. By considering all \( i \)-objective formulas
of maximal \( j \)-depth \( k \), let us construct \( \Omega' \), \( \Omega'' \), \(
\ldots \) by adding formulas iff the resultant set remains satisfiable. When
we are done, the resulting \( \Omega^\ast \) is what we shall call a maximally
satisfiable \( i \)-objective set.\footnote{A maximally satisfiable set is to
be understood as a semantically characterized \emph{complete} description of a
possibility, analogous to a proof theoretically characterized notion of
maximally consistent set of formulas.} Naturally, there may be many such sets
corresponding to \( \Omega \). We show that given a \emph{set} of maximally
satisfiable \( i \)-objective sets, there is a model where precisely this set
characterizes the epistemic state.

\begin{theorem}\label{thm:iset-theorem}
Let \( S_i \) be a set of maximally satisfiable sets of \( i \)-objective formulas, and \( \sigma \) a satisfiable objective formula. Suppose \( S_a \) is of max.~\( b \)-depth \( k-1 \) and \( S_b \) is of max.~\( a \)-depth \( j-1 \). Then there is a model \( M^* = \langle \estar_a^k, \estar_b^j, w^{*} \rangle \) such that \( M^* \models \sigma \), \( S_a = {O}{bj}^+_a(\estar_a^k) \) and \( S_b = {O}{bj}^+_b(\estar_b^j) \).

\end{theorem}

\begin{proof}
	 Consider \( S_a \). Each \( S' \in S_a \) is a maximally satisfiable \( a \)-objective set, and thus by definition, there is a \( k \)-structure \( \langle w', e_b^{k-1} \rangle \) such that \( \{\}, e_b^{k-1}, w' \models S' \). Define such a set of \( k \)-structures \( \{ \langle w', e_b^{k-1} \rangle \} \), corresponding to each \( S' \in S_a \), and let this be \( \estar_a^k \). It is immediate to verify that \( {O}{bj}^+_a(\estar_a^k) = S_a \). Analogously, for \( \estar_b^j \) using \( S_b \). Finally, there is clearly some world \( w^{*} \) where \( \sigma \) holds.
	\eprf \end{proof}

\subsection{On Validity}
\label{sub:on_validity}

How does the semantics compare to earlier approaches? In particular, we are
interested in valid formulas.
Lakemeyer (\citeyear{Lakemeyer1993}) proposes a semantics using \( {\textsf{K45}}_{n} \)-canonical models, but
he shows that the formula \(\neg \aoknow \neg \mathitbf{O}_{b} p \) 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 \( \neg \aoknow \neg \mathitbf{O}_{b} p \) is unintuitive. After all,
Bob could \emph{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 (\citeyear{DBLP:conf/aaai/Halpern93}), called the \( i \)-set approach.\footnote{In his original formulation, Halpern (\citeyear{DBLP:conf/aaai/Halpern93}) constructs \emph{trees}. We build on discussions in \cite{1029713}.} It is
also satisfiable in the \( k \)-structure semantics. Interestingly, the \( i
\)-set approach and \( k \)-structures agree on one more notion. The formula
\( \aknow \bot \supset \neg \mathitbf{N}_a \neg \mathitbf{O}_{b} \neg \aoknow p \)~(\( \zeta \)) is valid in both, while \( \neg \zeta \) is satisfiable
\emph{wrt.}~Lakemeyer (\citeyear{Lakemeyer1993}). (It turns out that the validity of \( \zeta \)
in our semantical framework is implicitly related to the satisfiability of \(
\mathitbf{O}_{b} \neg \aoknow p \), 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, \( \mathitbf{N}_a \neg \mathitbf{O}_{b} p \land \aknow \neg \mathitbf{O}_{b} p \)~(\(
\lambda \)) is satisfiable in Halpern (\citeyear{DBLP:conf/aaai/Halpern93}). Recall that, in this property, the
union of models that evaluate \( \mathitbf{N}_i \alpha \) and \( \mathitbf{L}_i \alpha \) must
lead to all conceivable states. So, the satisfiability of \( \lambda \) leaves open
the question as to why \( \mathitbf{O}_{b} p \) is not considered since \( \neg \mathitbf{O}_{b}
p \) is true at all conceivable states. We show that, in contrast, \(
\lambda \) is not satisfiable in the \( k \)-structures approach. Lastly, \cite{1029713}
involves enriching the language, the intuitions of which are perhaps best
explained after reviewing the proof theory, and so we defer discussions to
later.\footnote{An approach by
\cite{DBLP:conf/aiml/Waaler04,DBLP:conf/tark/WaalerS05} is also motivated by
the proof theory. Discussions are deferred.}

\begin{theorem}\label{lem:iset_validity} The following are properties of the semantics: \begin{enumerate}
	\item  \( \aoknow \neg \mathitbf{O}_{b} p \), for any \( p \in \Phi \), is satisfiable.

	\item \( \models \aknow \bot \supset \neg \mathitbf{N}_a \neg \mathitbf{O}_{b} \neg \aoknow p \).

	\item \( \mathitbf{N}_a\neg\mathitbf{O}_{b} p \land \aknow \neg\mathitbf{O}_{b} p \) is not satisfiable.
\end{enumerate}

\end{theorem}

\begin{proof} \textbf{Item 1.} Let \( {\mathcal{W}}_p = \{ w \mid w \models p \} \) and let \( E \) be all subsets of \( \mathcal{W} \) except the set \( {\mathcal{W}}_p \). It is easy to see that if \( e_b^1}% {e_{(b,1)} \in E \), then \( \{\}, e_b^1}% {e_{(b,1)}, w \not\models  \mathitbf{O}_{b} p \), for any world \( w \). Now, define a \( e^2 \) for \( a \) that has all of \( \mathcal{W} \times E \). Thus, \( e_a^2,
\{\}, w \models \aoknow \neg \mathitbf{O}_{b} p\).

\textbf{Item 2.}  Suppose \( e_a^k, \{\},
w\models \aknow \bot \) for any \( w \in \mathcal{W} \). Then, for all \(
\langle w', e_b^{k-1} \rangle \in e_a^k \), \( e_a^k, e_b^{k-1}, w' \models \bot \), and thus,
\( e_a^k = \{\} \). Suppose  now \( e_a^k, \{\}, w\models \mathitbf{N}_a \neg \mathitbf{O}_{b} \neg \aoknow p \). Then, \emph{wrt.}~ all of \( \langle w', e_b^{k-1} \rangle \not\ine_a^k \) i.e.~all of \( \mathbb{E}^k \), \( \neg \mathitbf{O}_{b} \neg \aoknow p \) must hold. That is, \( \neg \mathitbf{O}_{b} \neg \aoknow p \) must be valid. From above, we know this is not the case.

\textbf{Item 3.}  Suppose \( e_a^k, \{\}, w \models \aknow \neg \mathitbf{O}_{b}  p \), for any \( w \). Then, for all \( \langle w', e_b^{k-1} \rangle \in e_a^k \), \( e_a^k, e_b^{k-1}, w' \models \neg \mathitbf{O}_{b} p \). Since \( \mathitbf{O}_{b} p \) is satisfiable, there is a \( \estar_b^{k-1}} %{e^{*}_{(b,k-1)} \) such that \( \{\}, \estar_b^{k-1}} %{e^{*}_{(b,k-1)}, w^{*} \models \mathitbf{O}_{b} p \), and  \( \langle w^{*}, \estar_b^{k-1}} %{e^{*}_{(b,k-1)} \rangle \not\in e_a^k \). Then, \( e_a^k, \{\}, w \models \neg \mathitbf{N}_a \neg \mathitbf{O}_{b} p \).              \eprf \end{proof}

\noindent Thus, \( k \)-structures seem to satisfy our intuitions on the behavior of only-knowing. To understand why, notice that  \( \neg \aoknow \neg \mathitbf{O}_{b} p \) and \( \lambda \) involve the nesting of \( \mathitbf{N}_i \) operators. Lakemeyer (\citeyear{Lakemeyer1993}) makes an unavoidable technical commitment. A (\( i \)-objective) possibility is formally a maximally \( {\textsf{K45}}_{n} \)-consistent set of \emph{basic} \( i \)-objective formulas. The restriction to basic formulas is an artifact of a semantics based on the canonical model. Unfortunately, there is more to agent \( i \)'s possibility than just basic formulas. In the case of Halpern (\citeyear{DBLP:conf/aaai/Halpern93}), the problem seems to be that \( \mathitbf{N}_i \) and \( \mathitbf{L}_i \) do not interact naturally, and that the full complement of epistemic possibilities is not considered in interpreting \( \mathitbf{N}_i \). In contrast, Theorem \ref{thm:iset-theorem} shows that we allow non-basic formulas and by using a strictly semantic notion, we avoid problems that arise from the proof-theoretic restrictions. And, since the semantics faithfully complies with the second property, \( \lambda \) is not satisfiable.

The natural question is if there are axioms that characterize the semantics. We begin, in the next section, with a proof theory by Lakemeyer (\citeyear{Lakemeyer1993}) that is known to be sound and complete for all attempts so far, but for a restricted language.

\section{Proof Theory}
\label{sec:proof_theory}
In the single agent case, \( \mathcal{ONL} \)'s proof theory consists of axioms of
propositional logic, axioms that treat \( \mathitbf{L} \) and \( {\mathitbf{N}} \) as
a classical belief operator in \( \textsf{K45} \), an axiom that allows us to use
\( {\mathitbf{N}} \) and \( \mathitbf{L} \) freely on subjective formulas, modus ponens (\( \mathbf{MP} \)) and
 necessitation (\( \mathbf{NEC} \)) for both \( \mathitbf{L} \) and \(
{\mathitbf{N}} \) as inference rules, and the following axiom:\footnote{Strictly speaking, this is not the proof theory introduced in~\cite{77758}, where an axiom replaces the inference rule \( \mathbf{NEC} \).
Here, we consider an equivalent formulation by Halpern and Lakemeyer~(\citeyear{1029713}).}  \begin{itemize}
	\item[] \( \mathbf{A5}. \) \( {\mathitbf{N}} \alpha \supset \neg \mathitbf{L} \alpha \)
	if \( \neg \alpha \) is a propositionally consistent\\\qquad \mbox{}\qquad \mbox{} objective formula.
\end{itemize}

\noindent As we shall see, only the axiom
\( \mathbf{A5} \) is controversial, since extending any objective \( \alpha \)
to \emph{any} \( i \)-objective \( \alpha \) is problematic. Mainly, the soundness of the axiom in the single agent case relies on propositional logic. But in the multi-agent case, since we go beyond propositional formulas establishing this consistency is non-trivial, and even circular. To this end, Lakemeyer~(\citeyear{Lakemeyer1993}) proposes to resolve this consistency by relying on the existing logic \( {\textsf{K45}}_{n} \). As a consequence, his proof theoretic formulation appropriately generalizes all of Levesque's axioms, except for \( \mathbf{A5} 	 \) where its application is restricted to only basic \( i \)-objective consistent formulas. We use \( \vdash \) to denote provability.

\begin{definition} \( \mathcal{ONL}_n^- \) consists of all formulas \( \alpha \) in \(
\mathcal{ONL}_n \) such that no \( \mathitbf{N}_j \) may occur in the scope of a \( \mathitbf{L}_i \) or
a \( \mathitbf{N}_i \), for \( i \neq j \).

\end{definition}

\noindent The following axioms, along with \( \mathbf{MP} \) and \( \mathbf{NEC} \) (for \( \mathitbf{L}_i \) and \( \mathitbf{N}_i \)) is an axiomatization that we refer to as \( {AX}_n \). \( {AX}_n \) is sound and complete for the canonical model and the \( i \)-set approach for formulas in \( \mathcal{ONL}_n^- \).

\begin{itemize}

	\item[]  \( \mathbf{A1}_n. \) All instances of propositional logic,

	\item[]  \( \mathbf{A2}_n. \) \( \mathitbf{L}_i(\alpha \supset \beta) \supset (\mathitbf{L}_i \alpha \supset \mathitbf{L}_i \beta) \),

	\item[] \( \mathbf{A3}_n. \) \( \mathitbf{N}_i(\alpha \supset \beta) \supset (\mathitbf{N}_i \alpha \supset \mathitbf{N}_i \beta) \),

	\item[]   \( \mathbf{A4}_n. \) \( \sigma \supset \mathitbf{L}_i \sigma \land \mathitbf{N}_i \sigma \) for \( i \)-subjective \( \sigma \),

	\item[] \( \mathbf{A5}_n.~\mathitbf{N}_i \alpha \supset \neg \mathitbf{L}_i \alpha
	 \) if \( \neg \alpha \) is a \( {\textsf{K45}}_{n} \)-consistent\\\qquad \mbox{}\qquad \mbox{} \( i \)-objective basic formula.
\end{itemize}

\noindent Observe that, as discussed, the soundness of \( \mathbf{A5}_n \) is built on \( {\textsf{K45}}_{n} \)-consistency. Since our semantics is not based on Kripke structures, proving that every \( {\textsf{K45}}_{n} \)-consistent formula is satisfiable in some \( (k,j) \)-model is not immediate. We propose a construction called the \( (k,j) \)-\emph{correspondence model}. In the following, in order to disambiguate \( \mathcal{W} \) from Kripke worlds, we shall refer to our worlds as propositional valuations.

\begin{definition} The \( {\textsf{K45}}_{n} \) canonical model \( M^c = \langle \mathcal{W}^c, \pi^c, \mathcal{K}^c_a, \mathcal{K}^c_b \rangle \)  is defined as follows: \begin{enumerate}

		\item \( \mathcal{W}^c = \{ w \mid w \) is a (basic) maximally consistent set \( \} \)

	\item for all \( p \in \Phi\) and worlds \( w \), \( \pi^c(w)(p) = \textrm{true} \) iff \( p \in w \)

	\item \( (w,w') \in \mathcal{K}^c_i \) iff \( w\backslash \mathitbf{L}_i \subseteq w' \), \( w\backslash \mathitbf{L}_i = \{ \alpha \mid \mathitbf{L}_i\alpha \in w\} \)
\end{enumerate}

\end{definition}

\begin{definition} Given \( M^c \), define a set of propositional valuations \( \mathcal{W} \) such that for each world \( w \in \mathcal{W}^c \), there is a valuation \( [\![ w ]\!] \in \mathcal{W} \), \( [\![ w ]\!] = \{ p \mid p \in w \} \).
\end{definition}

\newcommand{{e_{\dl w \dr}}_a^1}{{e_{[\![ w ]\!]}}_a^1}

\begin{definition}\label{defn:correspondence_model} Given  \( M^c \) and a world \( w \in \mathcal{W}^c \), construct a $(k,j)$-model{} \( \langle {\ew}_a^k, {\ew}_b^j, [\![ w ]\!] \rangle \) from valuations \( \mathcal{W} \) inductively: \begin{enumerate}
	\item \( {e_{\dl w \dr}}_a^1 = \{ \langle [\![ w' ]\!], \{\} \rangle \mid w' \in \mathcal{K}^c_a(w) \} \),

	\item \( {\ew}_a^k = \{ \langle [\![ w' ]\!], {\ewdash}_b^{k-1} \rangle \mid w' \in \mathcal{K}^c_a(w) \} \),

	\item[] where \( {\ewdash}_b^{k-1} = \{ \langle [\![ w'' ]\!], {\ewdashdash}_a^{k-2} \rangle \mid w'' \in \mathcal{K}^c_b(w') \} \).
\end{enumerate}

\noindent Further, \( {\ew}_b^j \) is constructed analogously. Let us refer to this model as the \( (k,j) \)-correspondence model of \( (M^c, w) \).
\end{definition}

\noindent Roughly, Defn.~\ref{defn:correspondence_model} is a construction of a \(
(k,j) \)-model that appeals to the accessibility relations in the canonical
model.\footnote{The construction is somewhat similar to the notion of \emph{generated submodels} of Kripke frames \cite{hughes1984companion}.} Thus, a \( e_a^1}% {e_{(a,1)} \) for Alice \emph{wrt.}~\( w \) has precisely the
valuations of Kripke worlds \(w' \in \mathcal{K}^c_a(w) \). Quite analogously, a \(
e_a^k \) is a set \( \{ \langle [\![ w' ]\!], e^{k-1} \rangle \} \), where \( w' \in
\mathcal{K}^c_a(w) \) as before, but \( e^{k-1} \) is an epistemic state for Bob and
hence refers all worlds \( w'' \in \mathcal{K}^c_b(w') \). By a induction on the depth
of a \emph{basic} formula \( \alpha \), we obtain a theorem that \( \alpha \)
of maximal \( a,b \)-depth \( k,j \) is satisfiable at \( (M^c,w) \) iff
the \( (k,j) \)-correspondence model satisfies the formula.

\begin{theorem}\label{thm:basicformulas_canon_iff_kjmodel} For all basic formulas \( \alpha \) in \( \mathcal{ONL}_n^- \) and of maximal \( a,b \)-depth of \( k,j \), \\
	\qquad \mbox{}\qquad \mbox{}\qquad \mbox{}\( M^c, w \models \alpha \) iff \( {\ew}_a^k, {\ew}_b^j, [\![ w ]\!] \models \alpha \).

\end{theorem}

\begin{proof} By definition, the proof holds for propositional formulas,
disjunctions and negations. So let us say the result holds for formulas of \(
a,b \)-depth \( 1 \). Suppose now \( M^c,w \models \aknow\alpha \), where
\( \aknow \alpha \) has \( a,b \)-depth of \( 1,2 \). Then for all \( w'\in
\mathcal{K}^c_a(w) \), \( M^c, w'\models \alpha \) iff (by induction hypothesis) \(
{e_{\dl w' \dr}}_a^1, {e_{\dl w' \dr}}_b^1, {\dl w' \dr} \models \alpha \) iff \( {e_{\dl w \dr}}_a^2, \{\}, {\dl w \dr}
\models \aknow \alpha \). By construction, we also have \( {e_{\dl w \dr}}_a^1, \{\}, {\dl w \dr} \models
\aknow \alpha \). Since \( b \)'s structure is irrelevant, we get \( {e_{\dl w \dr}}_a^1,
{e_{\dl w \dr}}_b^2, {\dl w \dr} \models \aknow \alpha \) proving the hypothesis.

	 	For the other direction, suppose \( {e_{\dl w \dr}}_a^1, {e_{\dl w \dr}}_b^2, {\dl w \dr} \models \aknow
\alpha \). For all \( {\dl w' \dr} \in {e_{\dl w \dr}}_a^1 \), \( {e_{\dl w \dr}}_a^1, \{\},
{\dl w' \dr} \models \alpha \) iff (by hyp.) \( M^c, w'\models \alpha \)
for all \( w' \in \mathcal{K}^c_a(w) \) iff \( M^c,w\models \aknow \alpha \).\eprf \end{proof}

\begin{lemma}\label{lem:every_kffn_consistent_is_sat} Every \( {\textsf{K45}}_{n} \)-consistent basic formula \( \alpha \) is satisfiable wrt.~some $(k,j)$-model.

\end{lemma}

\begin{proof}
	It is a property of the canonical model that every \( {\textsf{K45}}_{n} \)-consistent basic formula is satisfiable \emph{wrt.}~the canonical model. Supposing that the formula has a \( a,b \)-depth of \( k,j \) then from Thm \ref{thm:basicformulas_canon_iff_kjmodel}, we know there is at least the correspondence  $(k,j)$-model{} that also satisfies the formula.
	\eprf \end{proof}

	                 \begin{theorem}\label{thm:soundness_onlmin}

		 For all \( \alpha \in \mathcal{ONL}_n^- \), if \( {AX}_n \vdash \alpha \) then \( \models \alpha \).

	\end{theorem}

	\begin{proof}		The soundness is easily shown to hold for \( \mathbf{A1}_n - \mathbf{A4}_n \). The soundness of \( \mathbf{A5}_n \) is shown by induction on the depth. Suppose \( \alpha \) is a propositional formula, and say \( \neg \alpha \) is a consistent  propositional formula (and hence \( {\textsf{K45}}_{n} \)-consistent). Then there is a world \( w^{*} \) such that \( \{\},\{\}, w^{*}\models \neg \alpha \). Given a \( e_a^k \), if \( \langle w^{*}, e_b^{k-1} \rangle \in e_a^k \) for some \( e_b^{k-1} \), then \( e_a^k, \{\}, w \models \neg \aknow \alpha \) for any world \( w \). If not, then \( e_a^k, \{\}, w\models \neg \mathitbf{N}_a \alpha \). Thus,  \( e_a^k, \{\}, w\models \mathitbf{N}_a \alpha \supset \neg \aknow \alpha \). Wlog, assume the proof holds for \( a\)-objective  formulas of max.~\( b \)-depth \( k-1 \).  Suppose now, \( \alpha   \) is such a formula, and \( \neg \alpha \) is \( {\textsf{K45}}_{n} \)-consistent. By Lemma \ref{lem:every_kffn_consistent_is_sat}, there is \( \langle w^{*}, \estar_b^{k-1}} %{e^{*}_{(b,k-1)} \rangle \), such that \( \{\}, \estar_b^{k-1}} %{e^{*}_{(b,k-1)}, w^{*} \models \neg \alpha \). Again, if \( \langle w^{*}, \estar_b^{k-1}} %{e^{*}_{(b,k-1)} \rangle \in e_a^k \), then \( e_a^k, \{\}, w\models \neg \aknow \alpha \) and if not, then \( e_a^k, \{\}, w\models \neg \mathitbf{N}_a \alpha \).
		\eprf \end{proof}

\noindent We proceed with the completeness over the following definition, and lemmas.

\begin{definition} A formula \( \psi \) is said to be \emph{independent} of the formula \( \phi \) wrt. an axiom system \( AX \), if neither \( AX \vdash \phi \supset \psi \) nor \( AX \vdash \phi \supset \neg \psi \).

\end{definition}

\begin{lemma}[Halpern and Lakemeyer, 2001]\label{lem:existence_independent}
If \( \phi_1, \ldots, \phi_m \) are \( {\textsf{K45}}_{n} \)-consistent basic \( i
\)-objective formulas then there exists a basic \( i \)-objective formula \(
\psi \) of the form \( \mathitbf{L}_j \psi' \) (\( j \neq i \)) that is independent of \( \phi_1,
\ldots, \phi_m \) wrt. \( {\textsf{K45}}_{n} \).

\end{lemma}

\begin{lemma}\label{lem:depth_of_independent_formula} In the lemma above, if \( \phi_i \) are \( i  \)-objective and of maximal \( j \)-depth \( k \) for \( j\neq i \), then there is a \( \psi \) of \( j \)-depth \( 2k+2 \).

\end{lemma}

\begin{lemma}[Halpern and Lakemeyer, 2001]\label{lem:phi_or_psi_is_valid_basic} If \( \phi \) and \( \psi \) are \( i \)-objective basic formulas, and if \( \mathitbf{L}_i \phi \land \mathitbf{N}_i \psi \) is \( {AX}_n \)-consistent, then \( \phi \lor \psi \) is valid.

\end{lemma}

\begin{lemma}[Halpern and Lakemeyer, 2001] Every formula \( \alpha \in \mathcal{ONL}_n \) is provably equivalent to one in the normal form \emph{(}written below for \( n = \{a,b\} \)\emph{):}   \\[1ex]
\noindent \( \bigvee(\sigma \land \aknow \varphi_{a0} \land \neg \aknow \varphi_{a1}  \ldots \land \neg \aknow \varphi_{a{m_1}}  \land \bknow 	\varphi_{b0} \ldots \land \neg \bknow \varphi_{b{m_2}}  \land
 \mathitbf{N}_a \psi_{a0} \ldots \land \neg \mathitbf{N}_a \psi_{a{n_1}}   \land \mathitbf{N}_b \psi_{b0} \ldots \land \neg \mathitbf{N}_b \psi_{bn_2} ) \) \\[1ex]
\noindent where \( \sigma \) is a propositional formula, and \( \varphi_{im} \) and \( \psi_{in} \) are \( i \)-objective. If \( \alpha \in \mathcal{ONL}_n^- \), \( \varphi_{im} \) and \( \psi_{in} \) are basic.

\end{lemma}

\begin{theorem}\label{thm:completeness_onlmin} For all formulas \( \alpha \in \mathcal{ONL}_n^- \), if \(\models \alpha \) then \( {AX}_n \vdash \alpha \).

\end{theorem}

\begin{proof}
	It is sufficient to prove that every \( {AX}_n \)-consistent
formula \( \xi \) is satisfiable \emph{wrt.}~ some $(k,j)$-model. If \( \xi \) is basic,
then by Lemma \ref{lem:every_kffn_consistent_is_sat}, the statement holds. If
\( \xi \) is not basic, then wlog, it can be
considered in the normal form: \\[1ex]
	   \noindent \( \bigvee(\sigma \land \aknow \varphi_{a0} \land \neg \aknow \varphi_{a1}  \ldots \land \neg \aknow \varphi_{a{m_1}}  \land \bknow 	\varphi_{b0} \ldots \land \neg \bknow \varphi_{b{m_2}}  \land
	 \mathitbf{N}_a \psi_{a0} \ldots \land \neg \mathitbf{N}_a \psi_{a{n_1}}   \land \mathitbf{N}_b \psi_{b0} \ldots \land \neg \mathitbf{N}_b \psi_{bn_2} ) \) \\[1ex]
\noindent where \( \sigma \) is a propositional formula, and \( \varphi_{im} \)
and \( \psi_{in} \) are \( i \)-objective and basic. Since \( \sigma \) is
propositional and consistent, there is clearly a world \( w^{*} \) such that
\( w^{*} \models \sigma \). We construct a \( k' \)-structure such that it
satisfies all the \( a \)-subjective formulas in the normal form above.
Following that, a \( j' \)-structure for all the \( b \)-subjective formulas
is constructed identically. The resulting \( (k',j') \)-model (with \( w^{*}
\)) satisfies \( \xi \).

Let \( A \) be all \( {\textsf{K45}}_{n} \)-consistent formulas of the form \( \varphi_{a0} \land
\psi_{a0} \land \neg \varphi_{aj} \) (for \( j \geq 1 \)) or the form \( \varphi_{a0} \land \psi_{a0}
\land \neg \psi_{aj} \). Let \( \gamma \) be independent of all formulas in \( A
\), as in Lemma \ref{lem:existence_independent} and
\ref{lem:depth_of_independent_formula}. Note that, while we take \( \xi
\) itself to be of maximal \( a,b \)-depth of \( k,j \), the depth of \( \varphi_{a0},
\ldots \) being \( a \)-objective are of maximal \( b \)-depth \( k-1 \), and hence
\( \gamma \) is of \( b	 \)-depth \( 2k \) (Lemma
\ref{lem:depth_of_independent_formula}). Given a consistent set of
formulas, the standard Lindenbaum construction can be used to construct a
maximally consistent set of formulas, all of a maximal \( b \)-depth \( k-1 \). That is,
a formula is considered in the construction only if it has a maximal \( b \)-depth
\( k-1 \). Now, let \( S_a \) be a set of all maximally consistent sets of
formulas, constructed by only considering formulas of maximal \( b \)-depth \( k-1 \), and containing \( \varphi_{a0} \land (\neg
\psi_{a0} \lor (\psi_{a0} \land \gamma)) \). Since each of these consistent sets are
basic and \( a \)-objective, they are satisfiable by
Lemma~\ref{lem:every_kffn_consistent_is_sat}.  Thus the sets \( S' \in S_a \) are
satisfiable \emph{wrt.}~ \( 2k \)-structures \( \langle w, e_b^{2k} \rangle \). Let \( k'
=2k+1 \). By constructing a \( k' \)-structure for Alice, say \( e_a^{k'}}%{e_{(a,k')} \),
from each \( \langle w, e_b^{2k} \rangle \) for every \( S' \in S_a \), we have that
\( \canaObj(e_a^{k'}}%{e_{(a,k')}) = S_a \). We shall show that all the \( a \)-subjective
formulas in the normal form are satisfied \emph{wrt.}~ \( \langle {e_a^{k'}}%{e_{(a,k')}}, \{\}, w^{*}
\rangle \).

Since for all \( S' \in S_a \), we have \( \varphi_{a0} \in S' \) we get that \(
{e_a^{k'}}%{e_{(a,k')}}, \{\}, w^{*} \models \aknow \varphi_{a0} \). Now, since \( \aknow \varphi_{a0}
\land \neg \aknow \varphi_{aj} \) is consistent, it must be that \( \varphi_{a0} \land \neg
\varphi_{aj} \) is consistent. For suppose not, then \( \neg \varphi_{a0} \lor \varphi_{aj} \) is
provable and thus, we have \( \varphi_{a0} \supset \varphi_{aj} \). We then prove \( \aknow
\varphi_{a0} \supset \aknow \varphi_{aj} \), and since we have \( \aknow \varphi_{a0} \) we prove \(
\aknow \varphi_{aj} \), clearly inconsistent with \( \aknow \varphi_{a0}
\land\neg \aknow \varphi_{aj} \). Now that
\( \varphi_{a0} \land \neg \varphi_{aj} \) is consistent, we either have that \( \varphi_{a0} \land
\neg \varphi_{aj} \land \psi_{a0} \) or \( \varphi_{a0} \land \neg \varphi_{aj} \land \neg \psi_{a0} \) is
consistent. With the former, we also have that \( \varphi_{a0} \land \neg \varphi_{aj} \land
\psi_{a0} \land \gamma \) is consistent. There are maximally consistent sets that
contain one of them, both of which contain \( \neg \varphi_{aj} \). This means that,
\( {e_a^{k'}}%{e_{(a,k')}}, \{\}, w^{*} \models \neg \aknow \varphi_{aj} \).

Now, consider some \( k' \)-structure \( \langle {w^{\bullet}}, \ebullet^{2k}_b \rangle \not
\in {e_a^{k'}}%{e_{(a,k')}} \). One of the following \( a \)-objective formulas must hold \emph{wrt.}~
this \( k' \)-structure: (a) \( \varphi_{a0} \land \psi_{a0} \), (b) \( \varphi_{a0} \land \neg
\psi_{a0} \), (c) \( \neg \varphi_{a0} \land \psi_{a0} \) or (d) \( \neg \varphi_{a0} \land \neg \psi_{a0}
\). It can not be (d), since \( \aknow \varphi_{a0} \land \mathitbf{N}_a \psi_{a0} \) is
consistent, and this implies that \( \varphi_{a0} \lor \psi_{a0} \) is valid (by Lemma
\ref{lem:phi_or_psi_is_valid_basic}). It certainly cannot be (b), for it would
be in some \( S' \in S_a \). This leaves us with options (c) and (a), both of
which have \( \neg \psi_{a0} \). Since the \( k' \)-structure was arbitrary, we
must have for all \( \langle w, e_b^{2k} \rangle \not\in {e_a^{k'}}%{e_{(a,k')}} \), \( \{\},
{e_b^{2k}}, w \models \psi_{a0} \). Thus, \( {e_a^{k'}}%{e_{(a,k')}}, \{\}, w^{*} \models
\mathitbf{N}_a \psi_{a0} \).

Finally, since \( \mathitbf{N}_a \psi_{a0} \land \neg \mathitbf{N}_a \psi_{aj} \) is consistent, it
must be that \( \psi_{a0} \land \neg \psi_{aj} \) is consistent. Further, either \(
\psi_{a0} \land \neg \psi_{aj} \land \varphi_{a0} \) or \( \psi_{a0} \land \neg \psi_{aj} \land \neg
\varphi_{a0} \) is consistent. If the former, then \( \psi_{a0} \land \neg \psi_{aj} \land
\varphi_{a0} \land \neg \gamma \) is also consistent. Let \( \beta \) be that which is
consistent. Note that \( \neg \beta \land (\varphi_{a0} \land (\neg \psi_{a0} \lor (\psi_{a0}
\land \gamma))) \) is consistent, and hence part of all \( S' \in S_a \). This
means that \( {e_a^{k'}}%{e_{(a,k')}}, \{\}, w^{*} \models \aknow(\neg \beta) \). But
since \( \beta \) itself is consistent, there is a \( k' \)-structure such
that \( \{\}, e_{(b,2k)}^\bullet, {w^{\bullet}} \models \beta \). And this \( k'
\)-structure can not be in \( {e_a^{k'}}%{e_{(a,k')}} \). This means that \( {e_a^{k'}}%{e_{(a,k')}},
\{\}, w^{*} \models \neg \mathitbf{N}_a \psi_{aj} \). Thus, all the \( a \)-subjective
formulas in the normal form above are satisfiable \emph{wrt.}~ \( {e_a^{k'}}%{e_{(a,k')}} \).
\eprf \end{proof}

\noindent  Now, observe that, although \( \aknow \bot \supset \neg \mathitbf{N}_a \neg \mathitbf{O}_{b} \neg \aoknow p \)~(\( \zeta \)) from Theorem \ref{lem:iset_validity} is valid, yet it is not derivable from \( {AX}_n \). In fact, the soundness result is easily extended to the full language \( \mathcal{ONL}_n \). Then, the proof theory cannot be complete for the full language since there is \( \zeta \in \mathcal{ONL}_n \) such that \( \not\vdash \zeta \) and \( \models \zeta \). Similarly, the validity of non-provable formulas \( \neg \aoknow \neg \mathitbf{O}_{b} p \) and \( \zeta \) \emph{wrt.}~the canonical model and the \( i \)-set approach respectively, show that although \( {AX}_n \) is also sound for the full language in these approaches, it cannot be compelete. Mainly, axiom \( \mathbf{A5}_n \) has to somehow go beyond basic formulas. As Halpern and Lakemeyer (\citeyear{1029713}) discuss, the problem is one of circularity. We would like the axiom to hold for any \( \alpha \) such that it is a consistent \( i \)-objective formula, but to deal with consistency we have to clarify what the axiom system looks like.

The approach taken by Halpern and Lakemeyer is to introduce \emph{validity} (and its dual satisfiability) directly into the language. Formulas in the new language, \( \onl^+ \), are shown to be provably equivalent to \( \mathcal{ONL}_n \). Some new axioms involving validity and satisfiability are added to the axiom system, and the resultant proof theory \( \axioms^+ \) is shown to be sound and complete for formulas in \( \onl^+ \), \emph{wrt.}~an \emph{extended} canonical model. (An extended canonical model follows the spirit of the canonical model construction but by considering maximally \( \axioms^+ \)-consistent sets, and treat \( \mathitbf{L}_i \) and \( \mathitbf{N}_i \) as two independent modal operators.) So, one approach is to show that for formulas in the extended language the set of valid formulas overlap in the extended canonical model and \( k \)-structures. But then, as we argued, axiomatizing validity is not natural. Also, the proof theory is difficult to use. And in the end, we would still understand the axioms to characterize a semantics bridged on proof-theoretic elements.

Again, what is desired is a generalization of Levesque's axiom \( \mathbf{A5} \), and nothing more. To this end, we propose a new axiom system, that is subtly related to the structure of formulas as are parameters \( k \) and \( j \). The axiom system has an additional \( t \)-axioms, and is to correspond to a sequence of languages \(
\onl^t \).\footnote{The idea was also suggested by a reviewer in \cite{1029713} for an axiomatic characterization of the extended canonical model, although its completeness was left open.}

\begin{definition} Let \( \mathcal{ONL}_n^1 = \mathcal{ONL}_n^- \). Let \( \onl^{k+1} \) be all Boolean combinations of formulas of \( \onl^t \) and formulas of the form \( \mathitbf{L}_i \alpha \) and \( \mathitbf{N}_i \alpha \) for \( \alpha \in \onl^t \).

\end{definition}

\noindent It is not hard to see that \( \onl^{k+1} \supseteq \onl^t \). Note that \( t \)
here does not correspond to the depth of formulas. Indeed, a formula of the
form \( (\bknow\aknow)^{k+1}p \) is already in \( \mathcal{ONL}_n^- \). Let \( \axioms^{t+1} \)
be an axiom system consisting of \( \mathbf{A1}_n-\mathbf{A4}_n \), \( \mathbf{MP} \), \( \mathbf{NEC} \) and \( \mathbf{A5}_n^1-\mathbf{A5}_n^{t+1} \) defined inductively as: \begin{itemize}
	\item[]  \( \mathbf{A5}_n^1. ~\mathitbf{N}_i \alpha	 \supset \neg \mathitbf{L}_i \alpha	 \), if \( \neg \alpha \) is a \( {\textsf{K45}}_{n} \)-consistent \\
	\qquad \mbox{}\qquad \mbox{}\( i \)-objective basic formula.

	\item[] \(  \mathbf{A5}_n^{t+1}. ~\mathitbf{N}_i \alpha \supset \neg \mathitbf{L}_i \alpha	 \), if \( \neg \alpha \in \onl^t \), is \( i \)-objective,\\
	\qquad \mbox{}\qquad \mbox{} and consistent \emph{wrt.}~\( \mathbf{A1}_n-\mathbf{A4}_n \), $\mathbf{A5}_n^1-\mathbf{A5}_n^t$ .
\end{itemize}

\begin{theorem}\label{thm:soundness_full_lang} For all \( \alpha \in \onl^t \), if \( \axioms^t \vdash \alpha \) then \( \models \alpha \).

\end{theorem}

\begin{proof}
	We prove by induction on \( t \). The case of \( {AX}_n^1 \) is
identical to Theorem \ref{thm:soundness_onlmin}. So, for the induction hypothesis,
let us assume that \emph{wrt.}~ \( \axioms^t \), if \( \axioms^t \vdash \beta \) for \(
\beta \in \onl^t \) then \( \models\beta \). Now, suppose that \( \neg \alpha
\) is consistent \emph{wrt.}~ \( \axioms^t \) and is \( a \)-objective. This implies
that \( \not \models \alpha \). Thus, there is some \( k \)-structure \( \langle
w^{*}, \estar_b^k \rangle \) such that \( \{\}, \estar_b^k, w^{*} \models \neg
\alpha \). Suppose now \( \langle w^{*}, \estar_b^k \rangle \in {e_a^{k+1}}%{e_{(a,k+1)}} \) then \(
{e_a^{k+1}}%{e_{(a,k+1)}}, \{\}, w' \models \neg \aknow \alpha \) and if not then \( {e_a^{k+1}}%{e_{(a,k+1)}},
\{\}, w' \models \neg \mathitbf{N}_a \alpha \). Thus, \( {e_a^{k+1}}%{e_{(a,k+1)}}, \{\}, w' \models
\mathitbf{N}_a \alpha \supset \neg \aknow \alpha \), demonstrating the soundness of
\( \axioms^{t+1} \).
\eprf \end{proof}

\noindent We establish completeness in a manner identical to Theorem \ref{thm:completeness_onlmin}, and thus it necessary to ensure that Lemma  \ref{lem:existence_independent}, \ref{lem:depth_of_independent_formula} and \ref{lem:phi_or_psi_is_valid_basic} hold for non-basic formulas.

\begin{lemma} If \( \phi_1, \ldots, \phi_m \) are \( \axioms^t \)-consistent \( i \)-objective formulas, then there is a basic formula \( \psi \) of the form \( \mathitbf{L}_j \psi \) (\( j \neq i \)) that is independent of \( \phi_1, \ldots, \phi_m \) \emph{\emph{wrt.}~ }\( \axioms^t \).

\end{lemma}

\begin{proof}
	Suppose that \( \phi_i \) are \( a \)-objective and of maximal \( b \)-depth \( k \). A formula \( \psi \) of the form \( (\bknow \aknow)^{k+1}p \) (where \( p \in \Phi \) is in the scope of \( k+1 \) \( \bknow \aknow \)) is shown to be independent of \( \phi_1, \ldots, \phi_m \). Let us suppose we can derive a \( \gamma \) of the form \( \bknow \aknow \bknow \aknow \ldots p \) of maximal depth \( k \), to show that neither \( \vdash \gamma \supset \psi \) nor \(  \vdash \gamma \supset \neg \psi \). Given any formula, the only axioms in \( \axioms^t \) that can introduce \( \gamma \) in the scope of modal operators is \( \mathbf{A4}_n \) and \( \mathbf{A5}_n^{t} \). Applying \( \mathbf{A4}_n \) gives \(\bknow \gamma \) or \(  \mathitbf{N}_b \gamma \), and then using the axiom again we have \( \bknow \bknow \gamma \) or \( \bknow \mathitbf{N}_b \gamma \). It is easy to see that the resulting formulas are clearly independent from \( \psi \). Applying \( \mathbf{A5}_n^t \) on the other hand, allows us to derive \( \vdash \gamma \supset \mathitbf{N}_a \gamma \) or \(  \vdash \gamma \supset \neg \aknow \gamma \) (\( \gamma \) is consistent \emph{wrt.~}\( \axioms^t \) and hence also \emph{wrt.~}\( \mathbf{A5}_n^{t-1} \)). Again, we could show \( \vdash \gamma \supset \neg \bknow \neg \aknow \gamma \). Continuing this way, it might only be possible to derive \( \neg \bknow \neg \aknow \ldots \bknow \aknow \ldots p \) of depth \( 2k+2 \), that is indeed independent of \( \psi \).
	\eprf \end{proof}

\begin{lemma}\label{lem:phi_or_psi_is_valid} If \( \phi \) and \( \psi \) are \( i \)-objective formulas, \( \phi, \psi \in \onl^t \) and \( \mathitbf{L}_i \phi \land \mathitbf{N}_i \psi \) is  \( \axioms^{t+1} \)-consistent then \( \models \phi \lor \psi \).

\end{lemma}

\begin{proof}
	Suppose not. Then \( \neg \phi \land \neg \psi \) is \( \axioms^t \)-consistent, and by \( \mathbf{A5}_n^{t+1} \) we prove \( \mathitbf{N}_a (\phi \lor \psi) \supset \neg \aknow (\phi \lor \psi) \), and thus, \( \mathitbf{N}_a \psi \supset \neg \aknow \phi \), and this is not \( \axioms^{t+1} \)-consistent with \( \aknow \phi \land \mathitbf{N}_a \psi \).
	\eprf \end{proof}

\begin{theorem}\label{thm:completeness_onlk} For all \( \alpha \in \onl^t \), if \( \models \alpha \) then \( \axioms^t \vdash \alpha \).

\end{theorem}

\begin{proof}
	Proof by induction on \( t \). It is sufficient to show that if a formula \( \beta \in \onl^{k+1} \) is \( \axioms^{t+1} \)-consistent then it is satisfiable \emph{wrt.}~some model. We already have the proof for \( \mathcal{ONL}_n^1 \) (see Theorem \ref{thm:completeness_onlmin}). Let us assume the proof holds for all formulas \( \alpha \in \onl^t \). Particularly, this means that any formula that is \( \axioms^t \)-consistent is satisfiable \emph{wrt.}~some \( (k',j') \)-model. Let \( \alpha \in \onl^{k+1} \) (say of maximal \( a,b \)-depth of \( k+1,j+1 \)), and suppose that \( \alpha \) is consistent \emph{wrt.}~\( \axioms^{t+1} \). It is sufficient to show that \( \alpha \) is satisfiable. Wlog, we take it in the normal form: \\[1ex]
	%
		  \noindent \( \bigvee(\sigma \land \aknow \varphi_{a0} \land \neg \aknow \varphi_{a1}  \ldots \land \neg \aknow \varphi_{a{m_1}}  \land \bknow 	\varphi_{b0} \ldots \land \neg \bknow \varphi_{b{m_2}}  \land
	 \mathitbf{N}_a \psi_{a0} \ldots \land \neg \mathitbf{N}_a \psi_{a{n_1}}   \land \mathitbf{N}_b \psi_{b0} \ldots \land \neg \mathitbf{N}_b \psi_{bn_2} ). \) \\[1ex]
\noindent Note that, by definition, it must be that all of \( \varphi_{im}, \psi_{in} \)~are at most in \( \onl^t \) (i.e.~they may also be in \( \mathcal{ONL}_n^{t-1}, \ldots
\)), and \( i \)-objective. We proceed as we did for Theorem \ref{thm:completeness_onlmin} but without restricting to basic formulas. Let \( A
\) be all \( \axioms^t \)-consistent formulas of the form \( \varphi_{a0} \land
\psi_{a0} \land \neg \varphi_{aj} \) or \( \varphi_{a0} \land \psi_{a0} \land \neg \psi_{aj} \) (they are of maximal \( b \)-depth \( k \)). Let \(
\gamma \) be independent of all formulas in \( A \). Let \( S_a \) be the set of all (\(
\axioms^t \)-) maximally consistent sets of formulas, constructed from formulas of maximal \( b \)-depth \( k \), and containing \( \varphi_{a0} \land (\neg
\psi_{a0} \lor (\psi_{a0} \land \gamma)) \), and hence by induction hypothesis they are satisfiable in some model. Note that all formulas in \( S_a \) are
in \( \onl^t \). The \( b \)-depth is maximally \( 2k+2 \). Letting \( k''=2k+2 \),
we have that for all \( S' \in S_a \), there is a \( \langle w, e_b^{k''}} %{e_{(b,k'')} \rangle
\) such that \( \{\}, e_b^{k''}} %{e_{(b,k'')}, w \models S' \). Let \( k'=k''+1 \).
Letting \( {e_a^{k'}}%{e_{(a,k')}} \) be all such \( k' \)-structures \( \langle w, e_b^{k''}} %{e_{(b,k'')} \rangle \) for each \( S' \in S_a \) makes \(
{O}{bj}^+_a({e_a^{k'}}%{e_{(a,k')}}) = S_a \) (in contrast, for Thereom \ref{thm:completeness_onlmin} we dealt with \( \canaObj \)). We claim that this \( k' \)-structure for
Alice, a \( j' \)-structure for Bob constructed similarly, and a world where
\( \sigma \) holds (there is such a world since \( \sigma \) is propositional
and consistent) is a model where \( \alpha \) is satisfied. The proof proceeds
as in Theorem \ref{thm:completeness_onlmin}. We show the case of \(
\neg \aknow \varphi_{aj} \).

Since \( \aknow \varphi_{a0} \land \neg \aknow \varphi_{aj} \) is consistent \emph{wrt.}~\( \axioms^{t+1}
\), it must be that \( \varphi_{a0} \land \neg \varphi_{aj} \) is consistent \emph{wrt.}~\(
\axioms^{t+1} \). Further, since \( \varphi_{a0}, \varphi_{aj} \in \onl^t \), they must consistent be \emph{wrt.}~\( \axioms^t \) (for if not, they cannot by definition be consistent \emph{wrt.}~\( \axioms^{t+1} \)). This means that either \( \varphi_{a0} \land \neg \varphi_{aj} \land \psi_{a0} \)
or \( \varphi_{a0} \land \neg \varphi_{aj} \land \neg \psi_{a0} \) is consistent. If the former
is, then so is \( \varphi_{a0} \land \neg \varphi_{aj} \land \psi_{a0} \land \gamma \). Since \(
S_a \) consist of all \( \axioms^t \)-consistent formulas containing \(
\varphi_{a0} \land (\neg \psi_{a0} \land (\psi_{a0} \land \gamma)) \), there is clearly a \(
S' \in S_a \) such that \( \neg \varphi_{aj} \in S' \). Consequently, it can not be
that \( {e_a^{k'}}%{e_{(a,k')}}, \{\}, w' \models \aknow \varphi_{aj} \). Thus, \( e_a^{k'}}%{e_{(a,k')}, \{\},
w' \models \neg \aknow \varphi_{aj} \).
\eprf \end{proof}

\noindent Thus, we have a sound and complete axiomatization for the propositional
fragment of \( \mathcal{ONL}_n \). In comparison to Lakemeyer (\citeyear{Lakemeyer1993}), the
axiomatization goes beyond a language that restricts the nesting of \( \mathitbf{N}_i
\). In contrast to Halpern and Lakemeyer (\citeyear{1029713}), the axiomatization does not
necessitate the use of semantic notions in the proof theory. A third
axiomatization by \cite{DBLP:conf/aiml/Waaler04,DBLP:conf/tark/WaalerS05}
proposes an interesting alternative to deal with the circularity in a generalized \(
\mathbf{A5} \). The idea is to first define consistency by formulating a
fragment of the axiom system in the sequent calculus. Quite analogous to having
\( t \)-axioms, they allow us to apply \( \mathbf{A5}_n \) on \( i \)-objective
formulas of a lower depth, thus avoiding circularity without the need to
appeal to satisfiability as in \cite{1029713}.
Waaler and Solhaug~(\citeyear{DBLP:conf/tark/WaalerS05}) also define a
semantics for multi-agent only-knowing which does not appeal to
canonical models. Instead, they define a class of Kripke structures which need
to satisfy certain constraints. Unfortunately, these constraints are quite
involved and, as the authors admit, the nature of these models ``is complex
and hard to penetrate.''

To get a feel of the axiomatization, let us consider a well studied example from \cite{1029713} to see where we differ. Suppose Alice assumes the following default: unless I know that Bob knows my secret then he does not know it. If the default is all that she knows, then she \emph{nonmonotonically} comes to believe that Bob does not know her secret. Let \(
\gamma \) be a proposition that denotes Alice's secret, and we want to show that \( \vdash \aoknow(\delta) \supset \aknow \neg \bknow \gamma \), where \( \delta = \neg \aknow \bknow \gamma \supset \neg \bknow \gamma \). We write (Def.)~to mean \( \aoknow \alpha \equiv \aknow \alpha   \land \mathitbf{N}_a \neg \alpha \), and we freely reason with propositional logic (PL) or \( {\textsf{K45}}_{n} \).
 \begin{enumerate
	\item \( \aoknow(\delta) \supset \aknow \neg \aknow \bknow \gamma \supset \aknow \neg \bknow \gamma  \) \hfill Def.,PL,\( \mathbf{A2}_n \)

	\item \( \aoknow(\delta)\supset \mathitbf{N}_a\neg \aknow \bknow \gamma \land \mathitbf{N}_a\bknow \gamma \) \hfill Def.,PL,\( {\textsf{K45}}_{n} \)

	\item \( \mathitbf{N}_a \bknow \gamma \supset \neg \aknow \bknow \gamma \) \hfill \( \mathbf{A5}_n^1 \)

	\item  \( \neg \aknow \bknow \gamma \supset \aknow \neg \aknow \bknow \gamma \) \hfill \( \mathbf{A4}_n \)

	\item \( \aoknow(\delta) \supset \aknow \neg \aknow \bknow \gamma \) \hfill 2,3,4,PL

	\item \( \aoknow(\delta) \supset \aknow \neg \bknow \gamma \) \hfill 1,5,PL
\end{enumerate}

\noindent We use \( \mathbf{A5}_n^1 \), and it is applicable because \( \neg \bknow \gamma \) is \( a \)-objective and \( {\textsf{K45}}_{n} \)-consistent. Now, suppose Alice is cautious. She changes her default to assume that if she does not believe Bob to only-know some set of facts \( \theta \in \Phi \), then \( \theta \) is not all that he knows. We would like to show
 \[ \vdash \aoknow(\neg \aknow \mathitbf{O}_{b} \theta \supset \neg \mathitbf{O}_{b} \theta) \supset \aknow \neg \mathitbf{O}_{b} \theta \]
Of course, this default is different from \( \delta \) in containing \( \mathitbf{O}_{b} \theta \) rather than \( \bknow \gamma \). The proof is identical, except that we use \( \mathbf{A5}_n^2 \), since \( \neg \mathitbf{O}_{b} \theta \in \mathcal{ONL}_n^1 \) is \( a \)-objective and \( {AX}_n^1 \)-consistent. The latter proof requires reasoning with the \emph{satisfiability} modal operator in Halpern and Lakemeyer (\citeyear{1029713}), and is not provable with the axioms of Lakemeyer (\citeyear{Lakemeyer1993}).

\section{Autoepistemic Logic}
\label{sec:autoepistemic_logic}

Having examined the properties of multi-agent only-knowing, in terms of a semantics for both the first-order and propositional case, and an axiomatization for the propositional case, in the current section we discuss how the semantics also captures autoepistemic logic (AEL). AEL, as originally developed by Moore (\citeyear{2781}), intends to allow agents to draw conclusions, by making observations of their own epistemic states. For instance, Alice concludes that she has no brother because if she did have one then she would have known about it, and she does not know about it \cite{2781}. The characterization of such beliefs are defined using fixpoints called \emph{stable expansions}. In the single agent case, Levesque (\citeyear{77758}) showed that the beliefs of an agent who only-knows \( \alpha \) is \emph{precisely} the stable expansion of \( \alpha \). Of course, the leverage with the former is that it is specified using regular entailments. In Lakemeyer (\citeyear{Lakemeyer1993}), and Halpern and Lakemeyer (\citeyear{1029713}), a many agent generalization of AEL is considered in the sense of a stable expansion for every agent, and relating this to what the agent only-knows. But their generalizations are only for the propositional fragment, while Levesque's definitions involved first-order entailments. In contrast, we obtain the corresponding quantificational multi-agent generalization of AEL. We state the main theorems below. The proofs are omitted since they follow very closely from the ideas for the single agent case~\cite{levesque2001logic}.

\begin{definition} Let \( A \) be a set of formulas, and \( \Gamma \) is the \( i \)-stable expansion of \( A \) iff it the set of first-order implications of \( A \cup \{\mathitbf{L}_i \beta \mid \beta \in \Gamma \} \cup \{\neg\mathitbf{L}_i\beta \mid \beta \not\in\Gamma \} \).

\end{definition}

\newcommand{\boldsymbol e_a^+}{\boldsymbol e_a^+}

\begin{definition}[Maximal structure] If \( e_a^k \) is a \( k \)-structure, let \( \boldsymbol e_a^+ \) be a \( k \)-structure with the addition of all \( \langle w', e_b^{k-1} \rangle \not \in e_a^k \) such that for every \( \alpha  \in \mathcal{ONL}_n^-	\) of maximal \( a,b \)-depth \( k,k-1 \), if \( e_a^k, \{\}, w \models \aknow \alpha \) for any world \( w \) then \( e_a^k, e_b^{k-1}, w' \models \alpha \). Define \( \Gamma = \{ \beta \mid \beta ~\textrm{is basic and}~ \boldsymbol e_a^+, \{\}, w \models \aknow \beta \}  \) as the belief set of \( \boldsymbol e_a^+ \).

\end{definition}

\begin{theorem}\label{thm:onlyknowing_is_stable} Let \( M = \langle \boldsymbol e_a^+, e_b^j, w \rangle \) be a model, where \( \boldsymbol e_a^+ \) is a maximal structure for \( a \). Let \( \Gamma \) be the belief set of \( \boldsymbol e_a^+ \), and suppose \( \alpha \in \mathcal{ONL}_n^- \) is of maximal \( a,b \)-depth \( k,k-1 \). Then,
	 \( M \models \aoknow\alpha \) iff \( \Gamma \) is the \( a \)-stable expansion of \( \alpha \).

\end{theorem}

\noindent Theorem \ref{thm:onlyknowing_is_stable} essentially says that the complete set of basic beliefs at a \emph{maximal} epistemic state where \( \alpha \) is all that \( i \) knows, precisely coincides with the \( i \)-stable expansion of \( \alpha \).

\section{Axiomatizing Validity}
\label{sec:axiomatizing_validity}

Extending the work in \cite{Lakemeyer1993} and \cite{DBLP:conf/aaai/Halpern93}, which was only restricted to formulas in \( \mathcal{ONL}_n^- \), Halpern and Lakemeyer~(\citeyear{1029713}) proposed a multi-agent only-knowing logic that handles the nesting of \( \mathitbf{N}_i \) operators. But as discussed, there are two undesirable features. The first is a semantics based on canonical models, and the second is a proof theory that axiomatizes validity. Although such a construction is far from natural,  we show in this section that they do indeed capture the desired properties of only-knowing. This also instructs us that our axiomatization avoids such problems in a reasonable manner.

Recall that the language of \cite{1029713} is \( {\onl^+} \), which is \( \mathcal{ONL}_n \) and a modal operator for validity, \( \textit{Val} \). A modal operator \( \textit{Sat} \), for satisfiability, is used freely such that \( \textit{Val}(\alpha) \) is syntactically equivalent to \( \neg \textit{Sat}(\neg \alpha) \). To enable comparisons, we present a variant of our logic, that has all its main features, but has additional notions to handle the extended language. We then show that this logic and \cite{1029713} agree on the set of valid sentences from \( {\onl^+} \) (and also \( \mathcal{ONL}_n \)).

The main feature of \cite{1029713} is the proof theory \( {AX}_n' \), and a semantics that is sound and complete for \( {AX}_n' \) via the extended canonical model. \( {AX}_n' \) consists of \( \mathbf{A1}_n-\mathbf{A4}_n \), \( \mathbf{MP} \), \( \mathbf{NEC} \) and the following:

\begin{itemize}

\item[] \( \mathbf{A5}_n'. \) \( \textit{Sat}(\neg \alpha) \supset (\mathitbf{N}_i \alpha \supset \neg \aknow \alpha) \), if \( \alpha \) is \( i \)-objective.

\item[]  \( \mathbf{V1}. \) \( \textit{Val} (\alpha) \land \textit{Val}(\alpha \supset \beta) \supset \textit{Val}(\beta) \).

\item[]  \( \mathbf{V2}. \) \( \textit{Sat}(p_1 \land \ldots p_n) \), if \( p_i \)'s are literals and \( p_1 \land \ldots p_n \) is \\\qquad \mbox{}\qquad \mbox{}  propositionally consistent.

\item[] \( \mathbf{V3}. \) \( \textit{Sat}(\alpha \land \beta_1) \land \ldots \textit{Sat}(\alpha \land \beta_k) \land \textit{Sat}(\gamma \land \delta_1) \ldots \land \\\qquad \mbox{}\qquad \mbox{} \textit{Sat}(\gamma \land \delta_m) \land \textit{Val}(\alpha \lor \gamma) \supset \textit{Sat}(\mathitbf{L}_i \alpha \land \neg \mathitbf{L}_i \neg \beta_1 \ldots \land \\\qquad \mbox{}\qquad \mbox{}\mathitbf{N}_i \gamma \land  \neg \mathitbf{N}_i \neg \delta_1 \ldots) \), if \( \alpha, \beta_i, \gamma, \delta_i \) are \( i \)-objective.

\item[]  \( \mathbf{V4}. \) \( \textit{Sat}(\alpha) \land \textit{Sat}(\beta) \supset \textit{Sat}(\alpha \land \beta) \), if \( \alpha \) is \( i \)-objective \\\qquad \mbox{}\qquad \mbox{}and \( \beta \) is \( i \)-subjective.

\item[]       \( \mathbf{NEC}_\textit{Val}. \) From \( \alpha \) infer \( \textit{Val}(\alpha) \).

\end{itemize}

\noindent The essence of our new logic, in terms of a notion of depth (with \( |\textit{Val}(\alpha)|_i = |\alpha|_i \)) and a semantical account over possible worlds, is as before. The complete semantic definition for formulas in \( {\onl^+} \) of maximal \( a,b \)-depth of \( k,j \) is: \begin{itemize}
	\item[1.] -8.~as before,

	\item[9.] \( e_a^k, e_b^j, w \models \textit{Val}(\alpha) \) if \( e_a^k, e_b^j, w\models \alpha \) for all \( e_a^k, e_b^j,w \).
\end{itemize}

\noindent {Satisfiability} and {validity} (\( \models \)) are understood analogously.\footnote{Note that \( \textit{Val} \) corresponds precisely to how validity is defined.} Let \( {\onl^+} ^1 \),  \( \ldots \) \( {\onl^+}^t \) be also defined analogously. Further, let axioms \( \mathbf{A1}_n-\mathbf{A5}_n^{t} \) be defined for \( {\onl^+}^{t} \). For instance, \( \mathbf{A5}_n^{t} \) is defined for any \( i \)-objective \( \neg \alpha \in {\onl^+}^{t-1} \) that is consistent with \( \mathbf{A1}_n-\mathbf{A5}_n^{t-1} \). Then, the semantics above is characterized by the proof theory \( {{AX}_n^+}^t \) defined (inductively) for \( {\onl^+}^t \),
consisting of \( {AX}_n^t \) (\( \mathbf{A1}_n-\mathbf{A5}_n^t \), \( \mathbf{MP} \), \( \mathbf{NEC} \)) with \( \mathbf{NEC}_\textit{Val} \) as an additional inference rule.

\begin{lemma}\label{lem:completeness_onlpk} For all \( \alpha \in {\onl^+}^t \), \( {{AX}_n^+}^t \vdash \alpha \) iff \( \models \alpha \).

\end{lemma}

\noindent The proof of this lemma, and those of the following theorems are given in the appendix.
We proceed to show that \( \textit{Sat}(\alpha) \) is provable from \( {AX}_n' \) iff \( \alpha \) is \( {{AX}_n^+}^t \)-consistent.
\begin{theorem}\label{thm:sat_means_consistent} For all \( \alpha \in {\onl^+}^t \), \( {AX}_n '\vdash \textit{Sat}(\alpha) \) iff \( \alpha \) is \( {{AX}_n^+}^t \)-consistent.

\end{theorem}

\noindent This allows us to show that \( {AX}_n' \)  and \( {{AX}_n^+}^t \) agree on provable sentences.

\begin{theorem}\label{thm:provable_sentences} For all \( \alpha \in {\onl^+}^t \), \( {AX}_n' \vdash \alpha \) iff \( {{AX}_n^+}^t \vdash \alpha \).

\end{theorem}

\begin{lemma}\label{cor:final} For all \( \alpha \in {\onl^+} ^t \), \( \models \alpha \) iff \( \alpha  \) is valid in\\~\cite{1029713}.

\end{lemma}

\begin{proof}
	\( {AX}_n' \) is sound and complete for \cite{1029713}, and \( {{AX}_n^+}^t \) is sound and complete for \( \models \).
	\eprf \end{proof}

\noindent Since it can be shown that every \( \alpha \in {\onl^+} \) is provably equivalent to some \( \alpha' \in \mathcal{ONL}_n \) \cite{1029713}, we also obtain the following corollary.

\begin{corollary}For all \( \alpha \in \mathcal{ONL}_n ^t \), \( \models \alpha \) iff \( \alpha  \) is valid in ~\cite{1029713}.

\end{corollary}

\section{Conclusions}
\label{sec:conclusions}

This paper has the following new results. We have a first-order modal logic for multi-agent only-knowing 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 \cite{DBLP:conf/tark/WaalerS05}.
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 (\citeyear{Lakemeyer1993}) 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 \cite{1029713}.
Our axiomatization was shown to be sound and complete for the semantics, and its use is straightforward on formulas involving the nesting of \emph{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~(\citeyear{1029713}) is not natural, we showed that they essentially  capture the desired properties of multi-agent only-knowing, but at much expense.

\section{Acknowledgements}
\label{sec: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.

\bibliographystyle{jas99}