1: 

2: %\documentstyle[chicago,12pt,smallsec]{article}

3: \documentstyle{article}

4: %\pagestyle{empty}

5: %jlc commands

6: \setlength{\textwidth}{130mm}

7: \setlength{\textheight}{200mm}

8:  \renewenvironment{abstract}{\section*{Abstract}\small}{}

9:        \newtheorem{definition}{Definition}[section]

10:        \newtheorem{example}[definition]{Example}

11:        \newtheorem{application}[definition]{Application}

12:        \newtheorem{theorem}[definition]{Theorem}

13:        \newtheorem{exercise}[definition]{Exercise}

14:        \newtheorem{lemma}[definition]{Lemma}

15:        \newtheorem{notation}[definition]{Notation}

16:        \newtheorem{observation}[definition]{Observation}

17:        \newtheorem{proposition}[definition]{Proposition}

18:        \newtheorem{proposal}[definition]{Proposal}

19:        \newtheorem{remark}[definition]{Remark}

20:        \newtheorem{result}[definition]{Result}

21:        \newtheorem{conjecture}[definition]{Conjecture}

22:        \newtheorem{claim}[definition]{Claim}

23:        \newtheorem{assumption}[definition]{Assumption}

24:        \newtheorem{corollary}[definition]{Corollary}

25:        \makeatletter

26:        \renewcommand{\@begintheorem}[2]{ % not in italics

27:   \trivlist\item[\hskip\labelsep{\bf #1\ #2}]}

28:        \renewcommand{\@opargbegintheorem}[3]{\trivlist

29:          \item[\hskip \labelsep{\bf #1\ #2\ (#3)}]}

30:        \makeatother

31:        \newtheorem{proof}{Proof}

32:        \renewcommand{\theproof}{}  % no numbers on proofs

33: 

34: 

35: 

36: \def \onln {\mbox{${\cal O}{\cal N}{\cal L}_n$}}

37: \newcommand{\citeyear}{\cite} 

38: %  THEOREM-LIKE ENVIRONMENTS

39:  

40:  

41: %theorem

42: \newcommand{\thm}{\begin{theorem}}

43: %lemma

44: \newcommand{\lem}{\begin{lemma}}

45: %proposition

46: \newcommand{\pro}{\begin{proposition}}

47: %definition

48: \newcommand{\dfn}{\begin{definition}}

49: %remark

50: \newcommand{\rem}{\begin{remark}}

51: %example

52: \newcommand{\xam}{\begin{example}}

53: %corollary

54: \newcommand{\cor}{\begin{corollary}}

55: %proof

56: \newcommand{\prf}{\begin{proof} }

57: %end theorem

58: \newcommand{\ethm}{\end{theorem}}

59: %end lemma

60: \newcommand{\elem}{\end{lemma}}

61: %end proposition

62: \newcommand{\epro}{\end{proposition}}

63: %end definition

64: \newcommand{\edfn}{\end{definition}}

65: %end remark

66: \newcommand{\erem}{\end{remark}}

67: %end example

68: \newcommand{\exam}{\end{example}}

69: %end corollary

70: \newcommand{\ecor}{\end{corollary}}

71: %end proof

72: \newcommand{\eprf}{\end{proof}}

73: %begin equation

74: \newcommand{\beqn}{\begin{equation}}

75: %end equation

76: \newcommand{\eeqn}{\end{equation}}

77: % white box

78: \newcommand{\wbox}{\mbox{$\sqcap$\llap{$\sqcup$}}}

79: %black box

80: \newcommand{\bbox}{\vrule height7pt width4pt depth1pt}

81: % (not)member of

82: \let\member=\in

83: \let\notmember=\notin

84: % \sub will be used for subscript.

85: \newcommand{\sub}{_}

86: % \su will be used for superscript.

87: \def\su{^}

88: %right arrow

89: \newcommand{\rarrow}{\rightarrow}

90: %left arrow

91: \newcommand{\larrow}{\leftarrow}

92: %bold face lower-case letters

93: \newcommand{\bolda}{{\bf a}}

94: \newcommand{\boldb}{{\bf b}}

95: \newcommand{\boldc}{{\bf c}}

96: \newcommand{\boldd}{{\bf d}}

97: \newcommand{\bolde}{{\bf e}}

98: \newcommand{\boldf}{{\bf f}}

99: \newcommand{\boldg}{{\bf g}}

100: \newcommand{\boldh}{{\bf h}}

101: \newcommand{\boldi}{{\bf i}}

102: \newcommand{\boldj}{{\bf j}}

103: \newcommand{\boldk}{{\bf k}}

104: \newcommand{\boldl}{{\bf l}}

105: \newcommand{\boldm}{{\bf m}}

106: \newcommand{\boldn}{{\bf n}}

107: \newcommand{\boldo}{{\bf o}}

108: \newcommand{\boldp}{{\bf p}}

109: \newcommand{\boldq}{{\bf q}}

110: \newcommand{\boldr}{{\bf r}}

111: \newcommand{\bolds}{{\bf s}}

112: \newcommand{\boldt}{{\bf t}}

113: \newcommand{\boldu}{{\bf u}}

114: \newcommand{\boldv}{{\bf v}}

115: \newcommand{\boldw}{{\bf w}}

116: \newcommand{\boldx}{{\bf x}}

117: \newcommand{\boldy}{{\bf y}}

118: \newcommand{\boldz}{{\bf z}}

119: %bold face upper-case letters

120: \newcommand{\boldA}{{\bf A}}

121: \newcommand{\boldB}{{\bf B}}

122: \newcommand{\boldC}{{\bf C}}

123: \newcommand{\boldD}{{\bf D}}

124: \newcommand{\boldE}{{\bf E}}

125: \newcommand{\boldF}{{\bf F}}

126: \newcommand{\boldG}{{\bf G}}

127: \newcommand{\boldH}{{\bf H}}

128: \newcommand{\boldI}{{\bf I}}

129: \newcommand{\boldJ}{{\bf J}}

130: \newcommand{\boldK}{{\bf K}}

131: \newcommand{\boldL}{{\bf L}}

132: \newcommand{\boldM}{{\bf M}}

133: \newcommand{\boldN}{{\bf N}}

134: \newcommand{\boldO}{{\bf O}}

135: \newcommand{\boldP}{{\bf P}}

136: \newcommand{\boldQ}{{\bf Q}}

137: \newcommand{\boldR}{{\bf R}}

138: \newcommand{\boldS}{{\bf S}}

139: \newcommand{\boldT}{{\bf T}}

140: \newcommand{\boldU}{{\bf U}}

141: \newcommand{\boldV}{{\bf V}}

142: \newcommand{\boldW}{{\bf W}}

143: \newcommand{\boldX}{{\bf X}}

144: \newcommand{\boldY}{{\bf Y}}

145: \newcommand{\boldZ}{{\bf Z}}

146: %double turnstile

147: \newcommand{\sat}{\models}

148: \newcommand{\dtur}{\models}

149: %single turnstile

150: \newcommand{\infers}{\vdash}

151: \newcommand{\stur}{\vdash}

152: %fat right arrow

153: \newcommand{\rimp}{\Rightarrow}

154: %fat left arrow

155: \newcommand{\limp}{\Leftarrow}

156: %fat double arrow

157: \newcommand{\dimp}{\Leftrightarrow}

158: %big or

159: \newcommand{\bor}{\bigvee}

160: %big and

161: \newcommand{\band}{\bigwedge}

162: %union

163: \newcommand{\union}{\cup}

164: %intersection

165: \newcommand{\inter}{\cap}

166: %bold letters

167: \newcommand{\xx}{{\bf x}}

168: \newcommand{\yy}{{\bf y}}

169: \newcommand{\uu}{{\bf u}}

170: \newcommand{\vv}{{\bf v}}

171: \newcommand{\FF}{{\bf F}}

172: \newcommand{\natnum}{{\sl N}}

173: \newfont{\sqi}{cmssqi8}

174: \newcommand{\IR}{\mbox{$I\!\!R$}}

175: \newcommand{\IP}{\mbox{$I\!\!P$}}

176: \newcommand{\IN}{\mbox{$I\!\!N$}}

177: \newcommand{\IC}{\mbox{$C\!\!\!\!\raisebox{.75pt}{\mbox{\sqi I}}$}}

178: %Use $\IC \;\;$

179: % multivalued arrow

180: \newcommand{\marrow}{\hbox{$\rightarrow$ \hskip -10pt

181: /                     $\rightarrow$ \hskip 3pt}}

182: % phi

183: \renewcommand{\phi}{\varphi}

184: %\renewcommand{\Diamond}{{\bf Large \diamond}}

185: \newcommand{\Circ}{\mbox{{\small $\bigcirc$}}}

186: \newcommand{\lt}{<}

187: \newcommand{\gt}{>}

188: \newcommand{\all}{\forall}

189: \newcommand{\infinity}{\infty}

190: %binomial coefficient:

191: \newcommand{\bc}[2]{\left( \begin{array}{c} #1 \\ #2 \end{array} \right)}

192: \newcommand{\cross}{\times}

193: \newcommand{\bigfootnote}[1]{{\footnote{\normalsize #1}}}

194: \newcommand{\medfootnote}[1]{{\footnote{\small #1}}}

195: \newcommand{\bd}{\bf}

196:  

197: % Joe's Section

198:  

199: \newcommand{\imp}{\Rightarrow}

200:  

201: %\H, \L, \O, \P and \S already taken; but we're redefining \P anyway

202: \newcommand{\A}{{\cal A}}

203: \newcommand{\B}{{\cal B}}

204: \newcommand{\C}{{\cal C}}

205: \newcommand{\D}{{\cal D}}

206: \newcommand{\E}{{\cal E}}

207: \newcommand{\F}{{\cal F}}

208: \newcommand{\G}{{\cal G}}

209: %\newcommand{\H}{{\cal H}}

210: \newcommand{\I}{{\cal I}}

211: \newcommand{\J}{{\cal J}}

212: \newcommand{\K}{{\cal K}}

213: %\newcommand{\L}{{\cal L}}

214: \newcommand{\M}{{\cal M}}

215: \newcommand{\N}{{\cal N}}

216: %\newcommand{\O}{{\cal O}}

217: \newcommand{\Ocal}{{\cal O}}

218: \newcommand{\Hcal}{{\cal H}}

219: \renewcommand{\P}{{\cal P}}

220: \newcommand{\Q}{{\cal Q}}

221: \newcommand{\R}{{\cal R}}

222: %\newcommand{\S}{{\cal S}}

223: \newcommand{\T}{{\cal T}}

224: \newcommand{\U}{{\cal U}}

225: \newcommand{\V}{{\cal V}}

226: \newcommand{\W}{{\cal W}}

227: \newcommand{\X}{{\cal X}}

228: \newcommand{\Y}{{\cal Y}}

229: \newcommand{\Z}{{\cal Z}}

230:  

231: \newcommand{\Kone}{{\cal K}_1}

232: \newcommand{\abs}[1]{\left| #1\right|}

233: \newcommand{\set}[1]{\left\{ #1 \right\}}

234: \newcommand{\Ki}{{\cal K}_i}

235: \newcommand{\Kn}{{\cal K}_n}

236: \newcommand{\st}{\, \vert \,} %puts vertical bar with space around it

237: \newcommand{\la}{\langle}

238: \newcommand{\ra}{\rangle}

239: \newcommand{\<}{\langle}

240: \renewcommand{\>}{\rangle}

241: \newcommand{\lang}{\mbox{${\cal L}_n$}}

242: \newcommand{\langd}{\mbox{${\cal L}_n^D$}}

243:  

244: %\renewcommand{\Box}{\mathbin{\vcenter{\hrule

245: %    \hbox{\vrule \kern .6em

246: %          \vbox to .6em{}\vrule}\hrule}}\hspace{.17ex}}

247: \newtheorem{nlem}{Lemma}

248: \newtheorem{Ob}{Observation}

249: \newtheorem{pps}{Proposition}

250: \newtheorem{defn}{Definition}

251: \newtheorem{crl}{Corollary}

252: \newtheorem{cl}{Claim}

253: \newcommand{\pf}{\par\noindent{\bf Proof}~~}

254: \newcommand{\eg}{e.g.,~}

255: \newcommand{\ie}{i.e.,~}

256: \newcommand{\vs}{vs.~}

257: \newcommand{\cf}{cf.~}

258: \newcommand{\etal}{et al.\ }

259: \newcommand{\resp}{resp.\ }

260: \newcommand{\respc}{resp.,\ }

261: \newcommand{\comment}[1]{\marginpar{\scriptsize\raggedright #1}}

262: \newcommand{\wrt}{with respect to~}

263: \newcommand{\re}{r.e.}

264: \newcommand{\nind}{\noindent}

265: \newcommand{\DG}{D_G}

266: \newcommand{\Sm}{{\rm S5}_m}

267: \newcommand{\Smc}{{\rm S5C}_m}

268: \newcommand{\Smi}{{\rm S5I}_m}

269: \newcommand{\Smic}{{\rm S5CI}_m}

270: \newcommand{\Martin}{Mart\'\i n\ }

271: \newcommand{\ol}{\setlength{\itemsep}{0pt}\begin{enumerate}}

272: \newcommand{\eol}{\end{enumerate}\setlength{\itemsep}{-\parsep}}

273: \newcommand{\ul}{\setlength{\itemsep}{0pt}\begin{itemize}}

274: \newcommand{\dl}{\setlength{\itemsep}{0pt}\begin{description}}

275: \newcommand{\edl}{\end{description}\setlength{\itemsep}{-\parsep}}

276: \newcommand{\eul}{\end{itemize}\setlength{\itemsep}{-\parsep}}

277: \newtheorem{fthm}{Theorem}

278: \newtheorem{flem}[fthm]{Lemma}

279: \newtheorem{fcor}[fthm]{Corollary}

280: \newcommand{\slidehead}[1]{

281: \eject

282: \Huge

283: \begin{center}

284: {\bf #1 }

285: \end{center}

286: \vspace{.5in}

287: \LARGE}

288:  

289: %chck macros

290: \newcommand{\subG}{_G}

291: \newcommand{\If}{{\bf if}}

292:  

293: \newcommand{\attime}{{\tt \ at\_time\ }}

294: \newcommand{\hatell}{\skew6\hat\ell\,}

295: \newcommand{\Then}{{\bf then}}

296: \newcommand{\Until}{{\bf until}}

297: \newcommand{\Else}{{\bf else}}

298: \newcommand{\Repeat}{{\bf repeat}}

299: \newcommand{\cA}{{\cal A}}

300: \newcommand{\cE}{{\cal E}}

301: \newcommand{\cF}{{\cal F}}

302: \newcommand{\cI}{{\cal I}}

303: %\newcommand{\IcR}{{\cal I}_{\cal R}}

304: %\newcommand{\IRca}{{\cal I}_\Rca}

305: %\newcommand{\Rca}{{\cR_{ca}}}

306: \newcommand{\cN}{{\cal N}}

307: \newcommand{\cR}{{\cal R}}

308: \newcommand{\cS}{{\cal S}}

309: \newcommand{\BN}{B^{\scriptscriptstyle \cN}}

310: \newcommand{\BS}{B^{\scriptscriptstyle \cS}}

311: \newcommand{\cW}{{\cal W}}

312: \newcommand{\EG}{E_G}

313: \newcommand{\CG}{C_G}

314: \newcommand{\CN}{C_\cN}

315: \newcommand{\ES}{E_\cS}

316: \newcommand{\EN}{E_\cN}

317: \newcommand{\CS}{C_\cS}

318: %\newcommand{\RP}{{\cR_P}}

319: %\newcommand{\IRP}{{\cal I}_\RP}

320: %\newcommand{\RSBA}{{\cR_{\it sba}}}

321: %\newcommand{\IRSBA}{{\cal I}_\RSBA}

322:  

323: \newcommand{\attack}{\mbox{{\it attack}}}

324: \newcommand{\attacking}{\mbox{{\it attacking}}}

325: \newcommand{\delivered}{\mbox{{\it delivered}}}

326: \newcommand{\exist}{\mbox{{\it exist}}}

327: \newcommand{\decide}{\mbox{{\it decide}}}

328: \newcommand{\clean}{{\it clean}}

329: \newcommand{\diff}{{\it diff}}

330: \newcommand{\Failed}{{\it failed}}

331: %\newcommand{\RF}{\cR_{\scriptscriptstyle {\cal F}}}

332: %\newcommand\eqdef{\buildrel {\rm def}\over =}

333: \newcommand\eqdef{=_{\rm def}}

334: \newcommand{\true}{\mbox{{\it true}}}

335: \newcommand{\false}{\mbox{{\it false}}}

336:  

337: %book macros

338: \newcommand{\DN}{D_{\cN}}

339: \newcommand{\DS}{D_{\cS}}

340: \newcommand{\tyme}{{\it time}}

341: \newcommand{\fp}{f}

342:  

343: %chguide macros

344: \newcommand{\Kax}{{\rm K}_n}

345: \newcommand{\Kaxc}{{\rm K}_n^C}

346: \newcommand{\Kaxd}{{\rm K}_n^D}

347: \newcommand{\Tax}{{\rm T}_n}

348: \newcommand{\Taxc}{{\rm T}_n^C}

349: \newcommand{\Taxd}{{\rm T}_n^D}

350: \newcommand{\fourax}{{\rm S4}_n}

351: \newcommand{\fouraxc}{{\rm S4}_n^C}

352: \newcommand{\fouraxd}{{\rm S4}_n^D}

353: \newcommand{\fiveax}{{\rm S5}_n}

354: \newcommand{\fiveaxc}{{\rm S5}_n^C}

355: \newcommand{\fiveaxd}{{\rm S5}_n^D}

356: \newcommand{\Dax}{{\rm KD45}_n}

357: \newcommand{\Daxc}{{\rm KD45}_n^C}

358: \newcommand{\Daxd}{{\rm KD45}_n^D}

359: \newcommand{\LP}{{\cal L}_n}

360: \newcommand{\LCP}{{\cal L}_n^C}

361: \newcommand{\LDP}{{\cal L}_n^D}

362: \newcommand{\LCDP}{{\cal L}_n^{CD}}

363: \newcommand{\MP}{{\cal M}_n}

364: \newcommand{\MPr}{{\cal M}_n^r}

365: %\newcommand{\MPrt}{{\cal M}_n^{rt}}

366: \newcommand{\MPrt}{\M_n^{\mbox{\scriptsize{{\it rt}}}}}

367: %\newcommand{\MPrst}{{\cal M}_n^{rst}}

368: \newcommand{\MPrst}{\M_n^{\mbox{\scriptsize{{\it rst}}}}}

369: %\newcommand{\MPelt}{{\cal M}_n^{elt}}

370: \newcommand{\MPelt}{\M_n^{\mbox{\scriptsize{{\it elt}}}}}

371: \renewcommand{\lang}{\mbox{${\cal L}_{n} (\Phi)$}}

372: \renewcommand{\langd}{\mbox{${\cal L}_{n}^D (\Phi)$}}

373: \newcommand{\fiveaxdu}{{\rm S5}_n^{DU}}

374: \newcommand{\LPD}{{\cal L}_n^D}

375: \newcommand{\fiveaxu}{{\rm S5}_n^U}

376: \newcommand{\fiveaxcu}{{\rm S5}_n^{CU}}

377: \newcommand{\LPU}{{\cal L}^{U}_n}

378: \newcommand{\LPCU}{{\cal L}_n^{CU}}

379: \newcommand{\LDPU}{{\cal L}_n^{DU}}

380: \newcommand{\LCPU}{{\cal L}_n^{CU}}

381: \newcommand{\LPDU}{{\cal L}_n^{DU}}

382: \newcommand{\LPCDU}{{\cal L}_n^{\it CDU}}

383: \newcommand{\Cn}{\C_n}

384: %\newcommand{\CSn}{\I_{CS}^{{n},\Phi}}

385: \newcommand{\CSn}{\I_n^{cs}(\Phi)}

386: \newcommand{\CSnp}{\I_n^{cs}(\Phi')}

387: \newcommand{\CSc}{\C_n^{cs}(\Phi)}

388: %\newcommand{\Ccs}{\C_n^{cs}}

389: \newcommand{\Ccs}{\C_n^{cs}}

390: \newcommand{\CSAX}{CS$_{{{n}},\Phi}$}

391: \newcommand{\CSAXN}{CS$_{{{n}},\Phi}'$}

392: %\newcommand{\IKB}{\I_n^{KB}}

393: \newcommand{\untill}{U}

394: \newcommand{\until}{\, U \,}

395: \newcommand{\amp}{{\rm a.m.p.}}

396: \newcommand{\commentout}[1]{}

397: \newcommand{\msgc}[1]{ @ #1 }

398: \newcommand{\Camp}{{\C_n^{\it amp}}}

399: \newcommand{\bi}{\begin{itemize}}

400: \newcommand{\ei}{\end{itemize}}

401: \newcommand{\be}{\begin{enumerate}}

402: \newcommand{\ee}{\end{enumerate}}

403: \newcommand{\rarrowr}{\stackrel{r}{\rightarrow}}

404: \newcommand{\ack}{\mbox{\it ack}}

405: \newcommand{\Gz}{\G_0}

406: \newcommand{\ampthm}{a.m.p.}

407: 

408: % Gerhard's macros

409: %

410: 

411: \newcommand{\deleted}[1]{{}}

412: \def \marg#1{\marginpar{\tiny #1}}

413: \def \md {{\mathrel|\joinrel=}}

414: \def \nmd {{\mathrel|\joinrel\neq}}

415: \def \And {\bigwedge}

416: \def \Or  {\bigvee}

417: 

418: %

419: % Setting up Proofs

420: %

421: \def \PROOF {\nopagebreak{\bf Proof$\;$: }}

422: \def \QED {\mbox{$\ \blacksquare$}\par \medskip}

423: 

424: \def \onl {\mbox{${\cal O}{\cal N}{\cal L}$}}

425: \def \onln {\mbox{${\cal O}{\cal N}{\cal L}_n$}}

426: \def \onlnminus {\mbox{${\cal O}{\cal N}{\cal L}_n^-$}}

427: \def \KFFn {\mbox{{\rm K45}$_n$}}

428: \def\tinyKFF{{\mbox{\begin{tiny}K45\end{tiny}}}}

429: \def\tinyKFFn{{\mbox{\begin{tiny}K45n\end{tiny}}}}

430: 

431: \def \notK{{\not\!\! \K}}

432: \def \Gammabar {\overline{\Gamma}}

433: 

434: \def \Mc {\mbox{$M^c$}}

435: \def \Oalpha {\mbox{$\Omega_\alpha$}}

436: \def \Salpha {\mbox{$\Sigma_\alpha$}}

437: 

438: \def\overlW{\overline{W}}

439: 

440: \def\GammaLth{{\Gamma_L^\theta}}

441: \def\GammaNth{{\Gamma_N^\theta}}

442: \def\GammaLthp{{\Gamma_L^{\theta'}}}

443: \def\GammaNthp{{\Gamma_N^{\theta'}}}

444: \def \onlp {\mbox{${\cal O}{\cal N}{\cal L}_n^+$}}

445: \newcommand{\OLNm}{{\cal ONL}_n^-}

446: \renewcommand{\LP}{{\cal L}_n}

447: %joe3: \sat_e is overloaded

448: %\newcommand{\sate}{\sat_e}

449: %joe4:

450: %\newcommand{\sate}{\sat_x}

451: %gerhard4:

452: \newcommand{\satx}{\sat^x}

453: \newcommand{\conse}{\sat^e}

454: \newcommand{\econsequence}{e-consequence}

455: \newcommand{\Wax}{\mbox{K45$_n$}}

456: %joe5: for subscripts

457: \newcommand{\sWax}{{{\rm K45}_n}}

458: \newcommand{\obji}{\mbox{{\it obj}}_i}

459: \newcommand{\objj}{\mbox{{\it obj}}_j}

460: \newcommand{\Obji}{\mbox{{\it Obj}}_i}

461: \newcommand{\Objj}{\mbox{{\it Obj}}_j}

462: \newcommand{\objsi}{\mbox{{\it ob\j}}^+_i}

463: \newcommand{\objsj}{\mbox{{\it ob\j}}^+_j}

464: \newcommand{\Objsi}{\mbox{{\it Ob\j}}^+_i}

465: \newcommand{\Objsj}{\mbox{{\it Ob\j}}^+_j}

466: \newcommand{\objei}{\mbox{{\it ob\j}}^e_i}

467: \newcommand{\Objei}{\mbox{{\it Ob\j}}^e_i}

468: \newcommand{\subji}{\mbox{{\it subj}}_i}

469: \newcommand{\subjj}{\mbox{{\it subj}}_j}

470: %joe4:

471: %\newcommand{\mdcm}{\sat}

472: \newcommand{\mdcm}{\sat^c}

473: \newcommand{\Conn}{\mbox{\em Sat}}

474: \newcommand{\Vall}{\mbox{\em Val}}

475: \newcommand{\Con}[1]{\mbox{\em Sat($#1$)}}

476: \newcommand{\Val}[1]{\mbox{\em Val($#1$)}}

477: 

478: %gerhard6:

479: %% emphasize important, newly introduced terms

480: \newcommand{\newl}[1]{\mbox{\underline{\it\smash{#1}\vphantom{\lower.1ex\hbox{x}}}}}

481: 

482: %gerhard6: new macros

483: \newcommand{\onlnzero}{\mbox{${\cal O}{\cal N}{\cal L}_n^0$}}

484: \newcommand{\onlnk}{\mbox{${\cal O}{\cal N}{\cal L}_n^k$}}

485: \newcommand{\onlnkplusone}{\mbox{${\cal O}{\cal N}{\cal L}_n^{k+1}$}}

486: \newcommand{\AXnew}{\mbox{AX$^*$}}

487: \newcommand{\Afivenewone}{\mbox{\bf A5$_n^1$}}

488: \newcommand{\Afivenewtwo}{\mbox{\bf A5$_n^2$}}

489: \newcommand{\Afivenewk}{\mbox{\bf A5$_n^k$}}

490: \newcommand{\Afivenewkplusone}{\mbox{\bf A5$_n^{k+1}$}}

491: 

492: 

493: 

494: \begin{document}

495: %joe5: made it a separate title page

496: \begin{titlepage}

497: \title{\bf Multi-Agent Only Knowing}

498: \author{{\bf Joseph Y. Halpern}\\

499: Department of Computer Science\\

500: Cornell University\\

501: Ithaca, NY 14850\\

502: halpern@cs.cornell.edu\\

503: %joe7: I added my URL; do you want to too?

504: %gerhard7: added my URL, fixed yours

505: http://www.cs.cornell.edu/home/halpern\\

506: \and {\bf Gerhard Lakemeyer}\\

507: Department of Computer Science\\

508: Aachen University of Technology\\

509: D-52056 Aachen, Germany\\

510: gerhard@cs.rwth-aachen.de\\

511: http://www-i5.informatik.rwth-aachen.de/gerhard}

512: %\date{ }

513: \maketitle

514: \thispagestyle{empty}

515: 

516: \begin{abstract}

517: Levesque introduced a notion of ``only knowing'',

518: with the goal of capturing certain types of nonmonotonic reasoning.

519: Levesque's logic dealt with only the case of a single agent.

520: Recently, both Halpern and

521: Lakemeyer independently attempted to extend Levesque's

522: logic to the multi-agent case.  Although there are a number of

523: similarities in their approaches, there are some significant

524: differences.  In this paper, we reexamine the notion of only knowing,

525: going back to first principles.  In the process,

526: %joe5

527: we simplify Levesque's completeness proof, and

528: point out some

529: problems with the earlier definitions.  This leads us to reconsider

530: what the properties of only knowing ought to be.  We provide an axiom

531: system that captures our desiderata, and show that it has a semantics

532: that corresponds to it.  The axiom system has an added feature of

533: interest: it includes a modal operator for satisfiability, and thus

534: provides a complete axiomatization for

535: satisfiability in the logic K45.

536: \end{abstract}

537: \end{titlepage}

538: %------------------------------------------------------------------------------

539: \section{Introduction}

540: %------------------------------------------------------------------------------

541: \label{intro}

542: Levesque \citeyear{Lev5} introduced a notion of ``only knowing'',

543: with the goal of capturing certain types of nonmonotonic reasoning.

544: %joe5:

545: %In particular, the hope was to capture the type of reasoning that says

546: In particular, he hoped to capture the type of reasoning that says

547: ``If all I know is that Tweety is a bird, and that birds typically fly,

548: then I can conclude that Tweety flies''.%

549: %joe2: moved footnote; we can cut it if we need space

550: \footnote{The reader should feel free to substitute ``believe''

551: anywhere we say ``know''.  Indeed, the formal logic that we use, which is

552: based on the modal logic K45, is more typically viewed as a

553: logic of belief rather than knowledge.}

554: %joe4: put the review back

555: %joe2: added

556: %We remark that we assume that the readers of this paper are familiar

557: %with basic modal logic and the systems K45, KD45, and S5.

558: %A review will be

559: %provided in the full paper.}

560: Levesque's logic dealt only with the case of a single agent.

561: It is clear that in many applications of such nonmonotonic reasoning,

562: there are several agents in the picture.

563: %joe4: put this back

564: %joe2: cut for abstract

565: For example, it may be the

566: case that all Jack knows about Jill is that Jill knows that Tweety is a

567: bird and that birds typically fly.  Jack may then want to conclude that

568: Jill knows that Tweety flies.%

569: 

570: Recently,

571: %joe5: seems less awkward

572: each of us \cite{Hal11,Lakemeyer93}

573: %both Halpern~\citeyear{Hal11} and

574: %Lakemeyer~\citeyear{Lakemeyer93}

575: independently attempted to extend

576: Levesque's

577: logic to the multi-agent case.  Although there are a number of

578: similarities in the approaches, there are some significant

579: differences.  In this paper, we reexamine the notion of only knowing,

580: going back to first principles.  In the process, we point out some

581: %joe1: rest of paragraph new

582: problems with both of the earlier definitions.  This leads us

583: to consider what the properties of only knowing ought to be.

584: We provide an axiom system that captures all our desiderata,

585: and show that it has a semantics that corresponds to it.  The axiom

586: system has an added feature of interest: it involves enriching the

587: language with a modal operator for satisfiability, and thus provides

588: an axiomatization for satisfiability in K45.

589: Unfortunately,

590: the semantics corresponding to this axiomatization

591: is not

592: %joe2

593: %so natural.

594: as natural as we might like.

595: It remains an open question whether

596: there is a natural semantics for only knowing that corresponds to this

597: %joe2

598: %semantics.

599: axiomatization.

600: 

601: The rest of this paper is organized as follows.  In the next section,

602: %joe5: cut the stuff about finite language here; it's a technical

603: %point best left to later

604: %we review the basic ideas of Levesque's logic and point out an

605: %alternative semantics followed by some remarks regarding the use of

606: %a finite language instead of an infinite one as in Levesque's case.

607: we review the basic ideas of Levesque's logic and provide an

608: alternative semantics.

609: %joe5: added

610: The use of the alternative semantics leads to a simplification of

611: Levesque's completeness proof. In

612: Section~\ref{canonical-model}, we review Lakemeyer's

613: approach, which we call the {\em

614: canonical-model} approach, and discuss some of its strengths and

615: weaknesses.

616: In

617: Section~\ref{tree-approach}, we go through the same process for

618: Halpern's

619: approach.

620: %joe5:

621: %Finally, in Section~\ref{synthesis}, we consider our new approach.

622: In Section~\ref{synthesis}, we consider our new approach.

623: %joe8: added next two sentences

624: Much of the discussion in Sections~\ref{canonical-model},

625: \ref{tree-approach}, and~\ref{synthesis} is carried out in terms of

626: three critical properties of Levesque's approach which we cull out in

627: Section~\ref{review}.  In particular, we examine to what extent each of

628: the approaches satisfies these properties.

629: %joe5: added

630: In Section~\ref{apps}, we show how the logic can be used, and discuss

631: its relationship to Moore's {\em autoepistemic logic} \cite{Moore85}.

632: Levesque showed that the single-agent version of his logic of only

633: knowing was closely connected to autoepistemic logic.  We extend his

634: result to the multi-agent case.

635: We conclude in

636: Section~\ref{discussion} with some discussion of only knowing.

637: %------------------------------------------------------------------------------

638: \section{Levesque's Logic of Only Knowing}\label{review}

639: %------------------------------------------------------------------------------

640: %In the remainder of this introduction, we discuss the issues

641: %involved at a semi-formal level.  Details can be found in

642: %the remainder of this abstract.

643: We begin by reconsidering Levesque's definition.

644: %joe5: decided to be much more careful about the set of propositions

645: Let $\Phi$ be a set of primitive propositions.

646: Let $\onl(\Phi)$ be a propositional

647: modal language

648: %with a countably infinite set of primitive propositions

649: %(as we shall see, the fact that the number of primitive propositions

650: %is countably infinite, rather than finite, has a significant impact),

651: formed by starting with the primitive propositions in $\Phi$, and

652: closing off under the classical operators $\lnot$ and $\lor$ and

653: %joe1: I'd rather make O an abbreviation

654: %three modalities $L$, $N$, and $O$.

655: two modalities, $L$ and $N$.

656: We omit the $\Phi$ whenever it is clear from context or not relevant

657: to the discussion.

658: We freely use other connectives like $\land$,

659: $\rimp$, and $\dimp$ as syntactic abbreviations of the usual kind.

660: %joe1; added

661: In addition, we take $O \alpha$ to be an abbreviation for $L \alpha

662: \land N \neg \alpha$.

663: Here $L\alpha$ should be read as ``the agent knows or believes

664: %joe1: added

665: (at least)

666: $\alpha$'', $N \alpha$ should be read as ``the agent believes at most

667: $\neg \alpha$'' (so that $N \neg \alpha$ is ``the agent believes at most

668: $\alpha$'')  and

669: $O\alpha$  should be read as ``the agent

670: %joe1:

671: %only knows $\alpha$}.

672: knows only $\alpha$''.

673: %joe1: cut

674: %(The meaning of $N\alpha$ will become clear in a moment.)

675: %gerhard6 moved from below since def. of ``objective'' needed.

676: We define an \newl{objective\/} formula to be a propositional formula

677: (\ie a formula with no modal operators),

678: a \newl{subjective\/} formula to be

679: a Boolean combination of formulas of the form $L\phi$ or $N \phi$,

680: and a \newl{basic} formula to be a formula which does not

681: mention $N$.

682: 

683: Levesque gave semantics to knowing and only knowing using the standard

684: possible-worlds approach.  In the single-agent case, we can identify a

685: \newl{situation\/} with a pair $(W,w)$, where $w$ is a possible world

686: (represented as a truth assignment to the primitive propositions)

687: and $W$ consists of a set of possible worlds.

688: Intuitively, $W$ is the set of worlds which the agent considers (epistemically)

689: possible, and $w$ describes the real world.

690: We do not require that $w \in W$ or that $W

691: \ne \emptyset$.%

692: \footnote{By requiring that $W$ is nonempty, we get the modal logic

693: KD45; by requiring that $w \in W$, we get S5.}

694: As usual, we say that the agent knows (at least) $\alpha$ if $\alpha$

695: is true in all the worlds that the agent considers possible.

696: %Gerhard2 rewritten to shorten

697: %joe4: lengthened again, so cut this.

698: %The agent is said to know at most $\lnot\alpha$ if

699: %$\alpha$ is true in all worlds the agent considers epistemically

700: %{\em impossible}. To see why this is a reasonable definition, assume

701: %$\alpha$ is true in all impossible worlds. Then $\alpha$ is at most

702: %false at all possible worlds, and perhaps not even that. Hence

703: %the agent knows at most $\lnot\alpha$.

704: %Gerhard2 rephrase since N is already added to the semantics

705: %joe4: put this back

706: Formally,

707: the semantics of the modality $L$ and the classical connectives is given

708: as follows.

709: %Formally, the semantics is given as follows.

710: %joe2:

711: %Let $p$ be a primitive proposition and let $\alpha$ and $\beta$ be

712: %arbitrary formulas of $\onl$. Then\\[1ex]

713: %

714: 

715: \begin{tabular}{l}

716:   $(W,w) \sat p$ if $w \sat p$

717: %joe2:

718: if $p$ is a primitive proposition.\\

719:   $(W,w) \sat \lnot\alpha$ if $(W,w) \nmd \alpha$.\\

720:   $(W,w) \sat \alpha \lor \beta$ if $(W,w) \sat \alpha$ or $(W,w) \sat

721: \beta$.\\

722:   $(W,w) \sat L \alpha$ if $(W,w') \sat \alpha$ for all $w' \in W$.\\

723: %joe4: cut

724: %Gerhard2

725: %  $(W,w) \sat N \alpha$ if $(W,w') \sat \alpha$ for all $w' \notin W$.

726: \end{tabular}

727: 

728: %joe4: reinstated

729: %Gerhard2

730: Notice that if $L\alpha$ holds, then the agent may know more than

731: $\alpha$.  For example, $Lp$ does not preclude $L(p \land q)$ from

732: holding.

733: %%joe2: to save space

734: %Thus,

735: %gerhard5: changes since knowing at least was introduced before

736: This is why

737: we should think of $L\alpha$ as saying that the agent knows

738: {\em at least\/} $\alpha$.

739: 

740: %joe1: added for future reference

741: It is well-known that this logic is characterized by the axiom system

742: K45.  For convenience, we describe K45 here:

743: \begin{description}

744: \item[Axioms:]\ \\[1ex]

745: \begin{tabular}{ll}

746: {\bf P}. & All instances of axioms of propositional logic.\\

747: {\bf K}. & $(L\phi \land L(\phi \rimp \psi)) \rimp L\psi$.\\

748: %\item[{\bf T}] $K_i \phi \rimp \phi$.\\

749: {\bf 4}. & $L \phi \rimp L L \phi$.\\

750: {\bf 5}. & $\neg L\phi \rimp L \neg L\phi$.\\

751: %\item[{\bf D}] $\neg K_i {\em false}$.

752: \end{tabular}

753: \item [Inference Rules:]\ \\[1ex]

754: \begin{tabular}{ll}

755: {\bf R1}. & From $\phi$ and $\phi \rimp \psi$ infer $\psi$.\\

756: {\bf R2}. & From $\phi$ infer $L\phi$.

757: \end{tabular}

758: \end{description}

759: The axioms {\bf 4} and {\bf 5} are called the {\em positive

760: introspection axiom\/} and {\em negative introspection axiom},

761: respectively.  They are appropriate for agents that are sufficiently

762: introspective so that they know what they know and do not know.

763: 

764: 

765: %Gerhard2 cut:

766: %The intuition behind $O\alpha$ is that

767: %the agent knows exactly

768: %$\alpha$; that is, he knows $\alpha$ and no more.

769: %%joe1: cut; redundant

770: %%Levesque defines $O

771: %%\alpha$ to be an abbreviation for

772: %%$L\alpha \land N\neg \alpha$.  If we think of $L \alpha$ as saying that

773: %%the agent knows at least $\alpha$, then $N \neg \alpha$ should be

774: %%viewed

775: %%as saying the agent knows at most $\alpha$.

776: %Intuitively, $N \beta$ is

777: %true if $\beta $ is true at all the worlds that the agent does {\em

778: %not\/} consider possible.  Thus, if $L \alpha \land N \neg \alpha$ is

779: %true, then $\alpha$ is true at all the worlds the agent considers

780: %possible, and $\neg \alpha$ is true at all the worlds the agent does not

781: %consider possible.  This means that

782: %$\alpha$ is true at all and only the worlds

783: %the agent considers possible.

784: 

785: %joe4: reinstated

786: How do we give precise semantics to $N$?  That is, when should we say

787: that $(W,w) \sat N \beta$?

788: Intuitively, $N \beta$ is

789: true if $\beta $ is true at all the worlds that the agent does {\em not\/}

790: consider possible.

791: It seems fairly clear from the intuition

792: that we need to evaluate the truth of $\beta$ in worlds

793: %gerhard6: added footnote due to ref2's comment

794: $w' \notin W$,\footnote{Note that, since we defined worlds extensionally as truth

795: assignments, the set of impossible worlds is well-defined and

796: fixed for a given $W$.}

797: since these are the worlds that the agent considers

798: impossible in $(W,w)$.  But if $\beta$ is a complicated formula

799: involving nested $L$ operators, then we cannot simply evaluate the truth

800: of $\beta$ at a world $w'$.  We need to have a set of worlds too.

801: In fact, the set of possible worlds we use is still $W$.  That is, while

802: evaluating the truth of $\beta$ in the impossible worlds, the agent

803: keeps the set of worlds he considers possible fixed.

804: %%joe2: to save space

805: Formally,

806: we define

807: $$\mbox{$(W,w) \sat N \alpha$ if $(W,w') \sat \alpha$ for all $w' \notin

808: W$.}$$

809: 

810: %

811: Let us stress three important features of this definition.

812: %Gerhard2 rphrase since 1st feature not yet mentioned

813: %joe4: now mentioned

814: %gerhard6: itemized for better visibility

815: \begin{itemize}

816: \item First, as we have

817: already observed, the set of possibilities is kept fixed when

818: we evaluate $N\alpha$.

819: \item Second, the set of \newl{conceivable worlds\/}---%

820: %[[GERHARD, CAN YOU

821: %COME UP WITH A BETTER PHRASE?  I LIKE CONCEIVABLE, BUT NOT CONCEIVABLE

822: %POSSIBILITIES.]]  [JOE, HOW ABOUT ``CONCEIVABLE WORLDS'' INSTEAD? I

823: %HAVE LEFT

824: %CONCEIVABLE POSSIBILITIES IN THE TEXT UNTIL WE DECIDE TO RENAME IT.]

825: the union of the set of ``possible'' worlds considered when evaluating

826: $L$ and the set of ``impossible'' worlds considered when evaluating $N$%

827: ---is fixed,

828: independent of the situation $(W,w)$; it is always the set of all truth

829: assignments.

830: \item %joe1: added

831: Finally, for every set of conceivable worlds, there is a model where

832: that set is precisely the set of worlds that the agent considers

833: possible.

834: \end{itemize}

835: 

836: %First, note that when evaluating $L\alpha$ or $N\alpha$ the set

837: %of possible worlds is kept fixed,

838: %that is, no matter which world we are in, the agent's beliefs are

839: %exactly the same.

840: %joe1: the trouble with using "conceivable world", much as I like it,

841: %is that once you go to many agents, the things that are conceivable are

842: %not worlds, but sets of formulas.  Use conceivable world here,

843: %conceivable state later.

844: 

845: %gerhard6: added

846: %joe7: added sentence

847: Roughly speaking, the first property is what is required for A4, while

848: the second property is what is required for A5.

849:  The intent of the third property is to make it

850: possible that any objective formula can be ``all you know.''

851: %joe7

852: %As we will see at the end, property 3 is a bit too strong. All we

853: As we shall see in Section~\ref{synthesis}, in a precise sense, the

854: third property is somewhat stronger than we actually need.

855: All we really need is that for any

856: %joe7: changed sentence -> formula consistently (a sentence is a

857: %first-order formula with no free variables)

858: %objective sentences the set of all

859: %worlds satisfying these sentences can be considered possible.

860: objective formulas the set of all

861: worlds satisfying these formulas can be considered possible.

862: We return to these properties for guidance when we

863: discuss possible ways of extending Levesque's semantics to the

864: multi-agent case.

865: 

866: %Finally, we obtain the semantics of only knowing as

867: %\[

868: %\mbox{$(W,w) \sat O \alpha$ if

869: %              $(W,w) \sat L\alpha$ and $(W,w) \sat N\lnot\alpha$},

870: %\]

871: %which is equivalent to

872: Since $O \alpha$ is an abbreviation for $L \alpha \land N \neg \alpha$,

873: we have that

874: \[

875: \mbox{$(W,w) \sat O \alpha$ if

876:                    for all worlds $w'$, $w'\in W$ iff $(W,w')\sat\alpha$.}

877: \]

878: 

879: 

880: %joe1: I'm not convinced it's worth keeping this material in, since

881: %we never really refer to it.  I kept it in for now though.

882: %gerhard4: stuff on maximal sets added back in since we refer to it now later

883: 

884: %joe6:

885: %the operator $N$ or, equivalently, basic formulas may mention at most

886: %the operator $N$; thus, basic formulas may mention at most

887: %the operator $L$.

888: 

889: As it stands, the semantics has the somewhat odd property that there are

890: situations that agree on all basic beliefs yet disagree on what is only

891: believed. As pointed out by Levesque~\citeyear{Lev5}, the problem is that there

892: are far too many sets of worlds than there are basic belief sets.  In order to

893: find a perfect match between the sets of basic beliefs an agent may hold and

894: sets of worlds, Levesque introduces what he calls \newl{maximal\/} sets of

895: worlds. In essence, a maximal set is the largest set in the sense that adding

896: any other world to it would change the agent's basic beliefs. Furthermore, every

897: set of worlds can be extended to a unique maximal set of worlds.  It is well

898: known that in the logic K45, an agent's beliefs are completely determined by his

899: beliefs about objective formulas (see, for example, \cite{HM4} for a proof).

900: Thus, we define a maximal set as follows:

901: 

902: %joe1: Gerhard, for consistency with my stuff, I took the labels out

903: %of definitions and theorems; we can always add them back if you really

904: %want

905: %\begin{definition}[Levesque] Maximal Sets\\

906: %\label{definition-maximal-sets}

907: \dfn If $W$ is a set of worlds, let

908: $$W^+ = \{ w\;|\; \mbox{for all objective formulas $\phi$, if

909: $(W,w)\md L\phi$ then

910: $(W,w)\md\phi$} \}.$$

911: %joe1: Moved this up

912: %\footnote{We only need to consider objective formulas because

913: %basic formulas with nested beliefs are equivalent to formulas without

914: %nested beliefs  in K45.}

915: $W$ is called {\em maximal\/} iff $W = W^+$.

916: \edfn

917: %

918: Levesque defines validity and satisfiability with

919: respect to {\em maximal\/}

920: sets only. In particular, a formula $\alpha$ is valid iff for every

921: maximal set of worlds $W$ and every world $w \in W$, we have

922: $(W,w)\md\alpha$.

923: 

924: 

925: We end this

926: %joe2: to save space

927: %brief

928: review of Levesque's logic by presenting (a slight variant

929: of) his proof theory.

930: %joe4: moved from above

931: %We define an {\em objective\/} formula to be a propositional formula

932: %(\ie a formula with no modal operators),

933: %and

934: %a {\em subjective\/} formula to be

935: %a Boolean combination of formulas of the form $L\phi$ or $N \phi$.

936: %joe4: cut; not used in this section

937: %a {\em basic\/} formula to be one

938: %that has no occurrences of the modal operator $N$.

939: %gerhard2: cut

940: %We can think of an

941: %objective formula as making a statement about the world, as opposed to

942: %the agent's knowledge of the world.

943: \begin{description}

944: \item [Axioms:]\ \\[1ex]

945: \begin{tabular}{ll}

946: \label{axioms-of-ol}

947: {\bf A1}. & All instances of axioms of propositional logic.\\

948: {\bf A2}. & $L(\alpha \rimp \beta) \rimp (L\alpha \rimp L\beta)$.\\

949: {\bf A3}. & $N(\alpha \rimp \beta) \rimp (N\alpha \rimp N\beta)$.\\

950: {\bf A4}. & $\sigma \rimp L\sigma \land N\sigma$ for every subjective

951: %joe1: added the world "formula" after subjective and objective

952: %throughout.  I hope I didn't miss any

953: formula $\sigma$.\\

954: %joe1: changed "falsifiable" to "satisfiable" (more standard, I think)

955: %{\bf A5} & $N\alpha\rimp\lnot L\alpha$ for every falsifiable objective

956: %formula $\alpha$.\\

957: {\bf A5}. & $N\alpha\rimp\lnot L\alpha$ if $\neg \alpha$ is a

958: %joe4

959: %K45-satisfiable

960: propositionally consistent

961:  objective

962: formula.\\

963: %joe1: now unnecessary

964: %{\bf A6} & $O\alpha \dimp (L\alpha \land N\lnot\alpha).$

965: \end{tabular}

966: \item [Inference Rules:]\ \\[1ex]

967: \begin{tabular}{ll}

968: {\bf MP}. & From $\alpha$ and $\alpha\rimp\beta$ infer $\beta$.\\

969: {\bf Nec}. & From $\alpha$ infer $L\alpha$ and $N\alpha$.

970: \end{tabular}

971: \end{description}

972: %Gerhard2: shortened gain

973: %joe4: expanded slightly

974: %gerhard4: changed since we can now refer to K45 axioms above

975: Axioms {\bf A2}--{\bf A4} tell us that

976: that $L$ and $N$

977: %have all the properties of K45-operators

978: separately have all the properties of K45-operators.

979: %separately are both characterized by

980: %({\bf A2}--{\bf A4}) and are,

981: %are chacterized by the axioms of the modal logic K45 (see \cite{Chellas}

982: %for more discussion).

983: Actually, {\bf A4} tells us more; it says that

984: $L$ and $N$ are mutually introspective, so that, for example, $L \phi

985: \rimp NL \phi$ is valid.

986: Perhaps the most interesting axiom is {\bf A5},

987: which gives only-knowing its desired properties.

988: Its soundness depends on the fact that

989: %%and results from

990: the union of the set of worlds considered when evaluating $L$ and

991: the set of worlds considered when evaluating $N$ is the set of all

992: conceivable worlds.%

993: \footnote{Note that, while unusual, the

994: axiom schema {\bf A5} is

995: recursive,

996: since consistency of formulas in classical

997: propositional logic is decidable.

998: %%joe1: cut

999: Hence the axioms themselves are {\em recursive}.

1000: As noted in~\cite{Lev5}, this is

1001: a problem in the first-order case, however.

1002: %no longer so in the first-order case, however.

1003: %%gerhard1: Plug for incompleteness result.

1004: In fact,

1005: %Note also that

1006: Levesque's proof theory for the first-order

1007: version of his logic was recently shown to be incomplete~\cite{HL95}.

1008: }

1009: \thm\label{levesque} {\rm \cite{Lev5}}

1010: %joe5: stressed fact that $\Phi$ has to be infinite

1011: %The proof theory is sound and complete

1012: If $\Phi$ is infinite, then

1013: Levesque's axiomatization is sound and complete

1014: %joe5:

1015: for the language $\onl(\Phi)$

1016: %with respect to the semantics.%

1017: with respect to Levesque's semantics.

1018: %Gerhard2: plug for incompleteness

1019: %joe3: to save space

1020: %\footnote{Levesque's proof theory for the first-order

1021: %version of his logic

1022: %joe4: moved this to previous footnote

1023: %\footnote{The first-order analogue of this axiom system

1024: %was recently shown to be incomplete~\cite{HL95}.}

1025: \ethm

1026: 

1027: %joe5:

1028: As we shall see, the assumption that there are infinitely many primitive

1029: propositions in $\Phi$ is crucial for Levesque's completeness result.

1030: Extra axioms are required if $\Phi$ is finite.  In addition,

1031: it is interesting to note that the assumption that $L$ and $N$ are

1032: interpreted with respect to complementary sets of worlds is not forced

1033: by the axioms. In particular,

1034: %joe2:

1035: %Axiom {\bf A5} only requires that

1036: %joe5:

1037: %for its soundness, Axiom {\bf A5} requires only that

1038: for the soundness of Axiom {\bf A5}, it suffices that

1039: the sets considered for $L$ and $N$ cover all conceivable worlds;

1040: they may overlap.

1041: The following semantics makes this

1042: %joe2:

1043: %idea

1044: precise.

1045: 

1046: %joe2: rewrote slightly

1047: %Instead of $W$ being simply a set of worlds, we now let $W$ consist of a pair

1048: %of sets of worlds $\langle W_L, W_N\rangle$ such that

1049: %$W_L\union W_N$ equals the set of all conceivable worlds.

1050: Define an \newl{extended situation} to be a triple $(W_L,W_N,w)$,

1051: where $W_L$ and $W_N$ are sets of worlds (truth assignments) such that

1052: $W_L \union W_N$ consists of all truth assignments.

1053: Define a

1054: %joe2: \sat' is overloaded (used in next section)

1055: new satisfaction relation $\satx$ that is exactly like Levesque's

1056: except for $L$- and $N$-formulas.

1057: %joe2

1058: %which now read as

1059: For them, we have

1060: 

1061: \begin{tabular}{l}

1062: $(W_L,W_N,w)

1063: \satx L \alpha$ if $(W_L,W_N,w') \satx \alpha$ for all $w' \in W_L$\\

1064: $(W_L,W_N,w)

1065: \satx N \alpha$ if $(W_L,W_N,w') \satx \alpha$ for all $w' \in W_N$.\\

1066: \end{tabular}

1067: 

1068: Note that $L$ and $N$ are now treated in a completely symmetric way.

1069: %joe2: added

1070: %Validity under this semantics is now defined as satisfaction in all

1071: %worlds $w$ and pairs of worlds $W$.

1072: %gerhard4: cut, since not quite true: need to find maximal sets

1073: % won't bother with that though and prove completeness directly

1074: %We can recover Levesque's semantics by restricting to extended

1075: %situations where $W_N$ is the complement of $W_L$.  Although

1076: %we allow more structures, all of Levesque's axioms are easily

1077: %seen to be sound under $\satx$.  Thus, it follows from

1078: %Theorem~\ref{levesque} that

1079: 

1080: \thm\label{Levthm1}

1081: %joe5:

1082: For all $\Phi$,

1083: Levesque's axiomatization is sound and complete

1084: %joe5:

1085: for the language $\onl(\Phi)$

1086: with respect to

1087: $\satx$.

1088: \ethm

1089: 

1090: \prf

1091: We omit the soundness proof, which is straightforward. Note that for axiom

1092: {\bf A5} to be sound it suffices that $W_L$ and $W_N$ together cover all worlds.  In

1093: particular, it does not matter whether or not the two sets overlap.

1094: 

1095: %joe5: added definition of maximal consistent set here.

1096: To prove completeness, we use the notion of a {\em maximal consistent\/}

1097: set.  Given an arbitrary axiom system $AX$, we say that a formula $\phi$

1098: is {\em consistent with respect to AX\/} if it is not the case that

1099: $AX \vdash \neg \phi$, where,

1100: as usual, we use $\vdash$ to denote provability.

1101: A finite set of formulas $\phi_1, \ldots,

1102: \phi_n$ is consistent with respect to $AX$ if the conjunction $\phi_1

1103: \land \ldots \land \phi_n$ is consistent with respect to $AX$.  An

1104: infinite set of formulas is consistent with respect to $AX$ if every

1105: finite subset of its formulas is consistent with respect to $AX$.

1106: Finally, given a set $F$ of formulas, a {\em maximal consistent\/}

1107: subset of $F$ is a subset $F'$ of $F$ which is consistent with respect

1108: to $AX$ such that any superset of $F'$ is not consistent with respect to

1109: $AX$.

1110: 

1111: \begin{sloppypar}

1112: In the following, provability, consistency,

1113: and maximal consistency all refer to Levesque's axiom system unless stated

1114: otherwise.

1115: To prove completeness we show that every consistent formula is

1116: satisfiable with respect to $\satx$, using a standard canonical model

1117: construction \cite{HM2,HC}.

1118: \end{sloppypar}

1119: 

1120: 

1121: Let $\Gamma_0$ be the set of all maximal consistent sets of formulas in

1122: $\onl(\Phi)$.   For $\theta\in\Gamma_0$, define  $\theta/ L =

1123:   \{\alpha\;|\; L\alpha\in\theta\}$ and

1124: $\theta/ N =   \{\alpha\;|\; N\alpha\in\theta\}$.  We then define

1125: \begin{itemize}

1126: \item $\GammaLth = \{\theta'\in\Gamma_0\;|\; \theta/ L\subseteq \theta'\}$,

1127: \item $\GammaNth = \{\theta'\in\Gamma_0\;|\; \theta/ N\subseteq \theta'\}$.

1128: \end{itemize}

1129: 

1130: If we view maximal consistent sets as worlds, then $\GammaLth$ and

1131: $\GammaNth$ represent the worlds accessible from $\theta$ for $L$ and $N$,

1132: respectively. The following lemma reflects the fact that $L$ and $N$ are

1133: both fully and mutually introspective (axiom {\bf A4}).

1134: 

1135: \begin{lemma}

1136: \label{lemma-single-ag-completeness-proof}

1137: If $\theta'\in \GammaLth\union\GammaNth$, then $\GammaLthp = \GammaLth$

1138: and $\GammaNthp = \GammaNth$.

1139: \end{lemma}

1140: \prf

1141: We prove the lemma for $\theta'\in \GammaLth$. The case $\theta'\in \GammaNth$

1142: is completely symmetric.

1143: %joe5: cut; it appears one paragraph prior

1144: %Before we prove that $\GammaLthp = \GammaLth$ recall

1145: %that

1146: %$

1147: %\begin{array}{l}

1148: %\GammaLthp = \{\theta''\in\Gamma_0\;|\;

1149: %\theta'/ L\subseteq \theta''\}\ {\rm and}\\

1150: %%\GammaLth = \{\theta^* \in\Gamma_0\;|\; \theta/ L\subseteq \theta^*\}.

1151: %\GammaLth = \{\theta'' \in\Gamma_0\;|\; \theta/ L\subseteq \theta''\}.

1152: %\end{array}

1153: %$

1154: %

1155: %To show that the two sets are equal it suffices to show

1156: To show that $\GammaLth = \GammaLthp$, it clearly suffices to show

1157: that $\theta/ L = \theta'/ L$.

1158: Let $\alpha\in \theta/ L$. Then $L\alpha\in\theta$ and

1159: also $LL\alpha\in\theta$ by axiom {\bf A4}. Thus $L\alpha\in\theta'$

1160: %joe5: added

1161: (since $\theta' \in \GammaLth$ implies that $\theta/L \subseteq \theta'$)

1162: and, hence, $\alpha\in\theta'/ L$.

1163: 

1164: For the converse, let $\alpha\in \theta'/ L$.  Thus,

1165: $L\alpha\in\theta'$.

1166: Assume that $\alpha\not\in \theta/ L$. Then $\lnot L\alpha\in\theta$

1167: %joe5:

1168: (since $\theta$ is a maximal consistent set)

1169: and, therefore, $L\lnot L\alpha\in\theta$, from which

1170: $\lnot L\alpha\in\theta'$ follows, a contradiction.

1171: 

1172: The proof that $\GammaNthp = \GammaNth$ proceeds the same way, that is,

1173: we show that $\theta/ N = \theta'/ N$.

1174: Let $\alpha\in \theta/ N$. Then $N\alpha\in\theta$ and

1175: also $LN\alpha\in\theta$ by axiom {\bf A4}. Hence $N\alpha\in\theta'$,

1176: so $\alpha\in \theta'/ N$.

1177: 

1178: For the converse, let $\alpha\in \theta'/ N$.  Thus,

1179: $N\alpha\in\theta'$. Assume that $\alpha\not\in \theta/ N$.

1180: Then $\lnot N\alpha\in\theta$

1181: and also $L\lnot N\alpha\in\theta$,

1182: from which $\lnot N\alpha\in\theta'$ follows, a contradiction.

1183: \eprf

1184: 

1185: %joe5: I didn't believe the proof of the next lemma.  I'll point out the

1186: %problem when it arises

1187: %The following lemma shows that $\GammaLth$ and $\GammaNth$, taken

1188: %together, cover all truth assignments.

1189: %We say that a maximal consistent set $\theta$ contains a truth

1190: %assignment

1191: %$w$ if for all atomic formulas $p$, $w\sat p$ iff $p\in\theta$.

1192: %

1193: %\begin{lemma}

1194: %\label{lemma-cover-all-truth-ass}

1195: %$\GammaLth\union\GammaNth$ cover all truth assignments, that is, for

1196: %every truth assignment $w$ there is a $\theta\in

1197: %\GammaLth\union\GammaNth$ which contains $w$.

1198: %\end{lemma}

1199: %\prf

1200: %Let $w$ be an arbitrary truth assignment and

1201: %$\theta'$ a maximal consistent set which contains $w$ and agrees with

1202: %$\theta$ on all subjective formulas.

1203: %joe5: this is not at all obvious to me.  Can you prove it?

1204: %Such $\theta'$ obviously exists.

1205: %We show that $\theta'\in\GammaLth\union\GammaNth$. Assume that

1206: %$\theta'\not\in\GammaLth$. To prove that $\theta'\in \GammaNth$,

1207: %we show that $\theta/ N\subseteq \theta'$.

1208: %First not that, since $\theta'\not\in\GammaLth$,

1209: %there is a $\gamma$ such that $L\gamma\in\theta$ and

1210: %$\gamma\not\in\theta'$. By a result in~\cite{Lev5} showing that

1211: %every formula is provably equivalent to one without nested modalities,

1212: %we can assume that $\gamma$ is objective.

1213: %Since $\gamma\not\in\theta'$, $\neg \gamma$ is a

1214: %propositionally consistent  objective formula.

1215: %Now let $N\alpha\in\theta$ for an arbitrary objective $\alpha$.

1216: %Then $\vdash \lnot\gamma\rimp\alpha$.

1217: %For assume otherwise, that is, assume that $\lnot(\gamma\lor\alpha)$ is consistent.

1218: %$\vdash L\gamma\rimp L(\gamma\lor\alpha)$ and, by axiom {\bf A5},

1219: %$\vdash L(\gamma\lor\alpha)\rimp\lnot N(\gamma\lor\alpha)$. In

1220: %particular,

1221: %we get $\vdash L\gamma\rimp\lnot N\alpha$, contradicting the

1222: %assumption that both $L\gamma$ and $N\alpha$ are in $\theta$.

1223: %Since $\gamma\not\in\theta'$, $\lnot\gamma\in\theta'$ and, since

1224: %$\vdash \lnot\gamma\rimp\alpha$, $\alpha\in\theta'$.

1225: %Therefore $\theta/ N\subseteq \theta'$.

1226: %\eprf

1227: 

1228: \def\WLth{{W_L^\theta}}

1229: \def\WNth{{W_N^\theta}}

1230: \def\WLthp{{W_L^{\theta'}}}

1231: \def\WNthp{{W_N^{\theta'}}}

1232: %joe5: rewrote

1233: %The following lemma establishes the connection between

1234: %maximal consistent sets and corresponding extended situations.

1235: In traditional completeness proofs using maximal consistent sets

1236: (see, for example, \cite{HM2,HC}), a situation is constructed whose

1237: worlds consists of all maximal consistent sets.  Here, we must be a

1238: little more careful.

1239: 

1240: %joe5: moved from above

1241: We say that a maximal consistent set $\theta$ contains a truth assignment

1242: $w$ if for all atomic formulas $p$, we have $w\sat p$ iff $p\in\theta$.

1243: %joe5: rewrote

1244: %For any $\theta$, let $w_\theta$ be the world contained in $\theta$.

1245: Clearly a maximal consistent set $\theta$ contains exactly one world;

1246: we denote this world by $w_\theta$.

1247: For $\theta\in\Gamma_0$,

1248: let

1249: %joe5: simplified

1250: %$\WLth = \{ w \;|\; \mbox{there is a $\theta'\in\GammaLth$ which contains $w$}\}$

1251: %and

1252: %$\WNth = \{ w \;|\; \mbox{there is a $\theta'\in\GammaNth$ which contains $w$}\}$.

1253: $\WLth = \{ w_{\theta'} \;|\; \theta'\in\GammaLth\}$ and

1254: $\WNth = \{ w_{\theta'} \;|\; \theta'\in\GammaNth\}$.

1255: %

1256: \begin{lemma}

1257: \label{completeness-max-sets-extended-sits}

1258: \begin{enumerate}

1259: \item[(a)] $(\WLth,\WNth,w_\theta)$ is an extended situation.

1260: \item[(b)] For all $\alpha$, we have $\alpha\in\theta$ iff

1261: $(\WLth,\WNth,w_\theta)\satx \alpha$. \end{enumerate}

1262: \end{lemma}

1263: \prf

1264: %\item By Lemma~\ref{lemma-cover-all-truth-ass}, $\WLth\union\WNth$

1265: %is the set of all truth assignments. Hence $(\WLth,\WNth,w_\theta)$ is

1266: %an extended situation.

1267: %joe5: new proof

1268: For part (a),

1269: to show that $(\WLth,\WNth,w_\theta)$ is an extended situation, we

1270: must show that $\WLth\union\WNth$ consists of all truth assignments.  By

1271: way of contradiction, suppose there is a truth assignment $w$ not in

1272: $\WLth\union\WNth$.

1273: Let $F_w = \{p \in \Phi \;|\; w \sat p\} \union

1274: \{\neg p \;|\; p \in \Phi, \; w \sat \neg p\}$.

1275: $F_w \union \theta/L$ cannot be consistent, for otherwise there would be

1276: some $\theta'

1277: \in \GammaLth$ that contains $F_w$, which would mean that $w \in

1278: \WLth$.  Similarly $F_w \union \theta/N$ cannot be consistent.

1279: Thus, there must be formulas $\phi_1, \phi_2, \phi_3, \phi_4$ such that

1280: $\phi_1$ and $\phi_2$ are both conjunctions of a finite number of

1281: formulas

1282: in $F_w$, $\phi_3$ is the conjunction of a finite number of formulas in

1283: $\theta/L$, and $\phi_4$ is the conjunction of a finite number of

1284: formulas in $\theta/N$, and both $\phi_1 \land \phi_3$ and $\phi_2 \land

1285: \phi_4$ are inconsistent.  Thus, we have $\vdash \phi_3 \rimp \neg

1286: \phi_1$ and $\vdash \phi_4 \rimp \neg \phi_2$.  Using standard modal

1287: reasoning ({\bf A2}, {\bf A3}, and {\bf Nec}), we have

1288: $\vdash L \phi_3 \rimp L \neg \phi_1$ and $N \phi_4 \rimp N \neg

1289: \phi_2$.  Since $L \psi \in \theta$ for each conjunct $\psi$ of

1290: $\phi_3$, standard modal reasoning shows that $L \phi_3 \in \theta$.

1291: Similarly, we have $N \phi_4 \in \theta$.  Since $\theta$ is a maximal

1292: consistent set, both $L \neg \phi_1$ and $N \neg \phi_2$ are in

1293: $\theta$.  Since $\vdash L \neg \phi_1 \rimp L(\neg \phi_1 \lor \neg

1294: \phi_2)$ and $\vdash N \neg \phi_2 \rimp N(\neg

1295: \phi_1 \lor \neg \phi_2)$, it

1296: follows that both $L (\neg \phi_1 \lor \neg \phi_2)$ and $N (\neg \phi_1

1297: \lor \neg \phi_2)$ are in $\theta$.  But this contradicts {\bf A5},

1298: since $\phi_1 \land \phi_2$ is a propositionally consistent objective

1299: formula.

1300: 

1301: For part (b),

1302: the proof proceeds by induction on the structure of $\alpha$.

1303: The statement

1304: holds trivially for atomic propositions, conjunctions, and negations.

1305: In the case of $L \alpha$, we proceed by the following chain of

1306: equivalences:

1307: 

1308: \begin{tabular}{ll}

1309: &$L\alpha\in\theta$\\

1310: iff &for all $\theta'\in\GammaLth$, we have $\alpha\in\theta'$\\

1311: iff &for all $\theta'\in\GammaLth$, we have

1312: $(\WLthp,\WNthp,w_{\theta'})\satx \alpha$ (using the induction

1313: hypothesis)\\

1314: iff &for all $w_{\theta'}\in \WLth$, we have

1315: $(\WLth,\WNth,w_{\theta'})\satx \alpha$

1316: (by Lemma~\ref{lemma-single-ag-completeness-proof})\\

1317: iff

1318: &$(\WLth,\WNth,w_{\theta})\satx L\alpha$.

1319: \end{tabular}

1320: 

1321: \noindent The case $N\alpha$ is completely

1322: symmetric. \eprf

1323: 

1324: The completeness result now follows easily.

1325: Let $\alpha$ be a consistent formula and $\theta$ a maximal consistent

1326: set of formulas containing $\alpha$.

1327: By Lemma~\ref{completeness-max-sets-extended-sits},

1328: $(\WLth,\WNth,w_{\theta})\satx \alpha$.

1329: \eprf

1330: 

1331: %joe5: rewrite

1332: %The fact that extended situations yield the same logic as Levesque's

1333: %also shows that whether or not we use maximal sets in Levesque's case

1334: %has no effect on the valid sentences of the logic.

1335: Levesque considered only maximal sets in his definition of validity.

1336: In fact, this restriction has no effect on the notion of validity.

1337: 

1338: \cor

1339: %joe5: added "\in \onl(\Phi)"

1340: A formula $\alpha \in \onl(\Phi)$ is valid iff $(W,w)\sat\alpha$ for all

1341: situations $(W,w)$ (including nonmaximal $W$).

1342: \ecor

1343: \prf

1344: %joe5: added

1345: If $\Phi$ is finite, it is easy to check that $W^+ = W$ for all sets

1346: $W$, so the result is trivially true if $\Phi$ is finite.  So suppose

1347: $\Phi$ is infinite.

1348: Notice that each situation $(W,w)$ corresponds to an extended situation

1349: $(W_L,W_N,w)$, where $W_L = W$ and $W_N$ is the complement of $W$.

1350: %joe5:

1351: %Let us call such $(W_L,W_N,w)$ an extended complementary situation.

1352: Let us call such an $(W_L,W_N,w)$ an {\em extended complementary

1353: situation}.

1354: %joe5:

1355: %The previous theorem implies that

1356: Theorems~\ref{levesque} and~\ref{Levthm1} together imply

1357: %joe7

1358: %the valid sentences obtained when considering all extended

1359: the valid formulas obtained when considering all extended

1360: situations remain the same when we restrict ourselves to

1361: complementary situations with maximal $W_L$.

1362: The corollary then follows from the fact that the set of all extended

1363: situations

1364: properly includes the set of all extended complementary situations, which

1365: in turn includes the set of all extended complementary situations with

1366: maximal $W_L$.

1367: \eprf

1368: 

1369: %joe2: rewrote

1370: %We remark that the completeness proof for the new semantics amounts to a

1371: %straightforward canonical model construction, which is considerably

1372: %simpler than Levesque's completeness proof for his semantics.

1373: %Levesque runs into complications because there are maximal sets of

1374: %formulas which have no model under his semantics. Under the new semantics

1375: %this problem does not arise.

1376: %gerhard4: deleted since now done

1377: \deleted{

1378: We can actually prove completeness of Levesque's axioms for $\satx$

1379: directly, using a standard canonical model construction (\cf

1380: Section~\ref{canonical-model}).  Moreover, as we show in the full

1381: paper, we can use our approach

1382: to give a simpler completeness proof for Levesque's semantics than

1383: the one given by Levesque.  The key idea is to find a model satisfying

1384: a formula where $W_L$ and $W_N$ may overlap, and then

1385: use the truth assignment to a primitive proposition not mentioned

1386: in the formula to force $W_L$ and $W_N$ to be disjoint.  We know

1387: that there is bound to be a primitive proposition not mentioned in

1388: the formula, given the assumption that the set of primitive

1389: propositions is infinite.

1390: %joe2: cut this

1391: %\cor

1392: %There is no finite axiomatization which characterizes precisely

1393: %those models where $L$ and $N$ are interpreted with respect to

1394: %complementary sets of worlds.

1395: %\ecor

1396: } %END DELETE

1397: 

1398: %joe5: rewrote

1399: %Interestingly, if we move to a language with only a finite set of

1400: %primitive propositions $\Phi$,

1401: %then $\sat$ and $\satx$ are no longer characterized by the

1402: %same axioms.

1403: As Theorem~\ref{Levthm1} shows, for the $\satx$ semantics, Levesque's

1404: axioms are sound and complete for all sets $\Phi$ of primitive

1405: propositions.  On the other hand,

1406: as we said earlier, Levesque's completeness proof (with respect

1407: to his semantics) depends crucially on the fact that $\Phi$ is infinite.

1408: If $\Phi$ is finite, Levesque's axioms are still sound with respect to

1409: his semantics, but they are no longer complete.

1410: %complete for $\satx$, and sound for $\sat$, but they are not complete

1411: %for $\sat$.

1412: %Levesque's completeness result depends crucially on the fact that

1413: %there are infinitely many primitive propositions in the language.

1414: %With only finitely many primitive propositions, it would appear that we need

1415: %extra axioms to characterize $\sat$.\footnote{

1416: For example,

1417: %joe5: using notation

1418: %if the language has only one primitive proposition, say $p$,

1419: if $\Phi=\{p\}$,

1420: then $\neg L \neg p \rimp N \neg p$ would be valid under $\sat$; this

1421: does not follow from the axioms given above.

1422: %joe5:

1423: %We can find an extra axiom

1424: %that gives a complete axiomatization for each finite set $\Phi$ of

1425: %primitive propositions.%

1426: In fact, for each finite set $\Phi$ of primitive propositions, we can

1427: find a new axiom scheme that, taken together with the previous axioms,

1428: gives a complete axiomatization for $\onl(\Phi)$ for Levesque's

1429: semantics if $\Phi$ is finite.%

1430: \footnote{This was also the  situation

1431: for the logic

1432: considered in \cite{FHV2}.  In that paper, a simple axiomatization was

1433: provided for the case where $\Phi$  was

1434: infinite; for each finite $\Phi$, an extra axiom was needed (that

1435: depended on $\Phi$).

1436: }

1437: %joe5: note that the new axiom also depends on $\Phi$

1438: %It turns out, however, that instead of having to add extra axioms to

1439: %capture properties like these, it suffices to replace {\bf A5} by

1440: %a much stronger version which essentially tells us that

1441: The new axiom, which subsumes axiom {\bf A5}, allows us to reduce

1442: formulas involving $N$

1443: formulas involving only $L$.

1444: %in the finite language case.

1445: 

1446: %joe5:

1447: %To make this precise,

1448: Note that worlds, which are truth assignments to the

1449: primitive propositions $\Phi$, are themselves finite if $\Phi$ is finite.

1450: Hence

1451: we can identify a world $w$ with the conjunction of all literals over $\Phi$

1452: that are true at $w$. For example, if $\Phi = \{p,q\}$ and

1453: $w$ makes $p$ true and $q$ false, then we identify $w$ with

1454: $p\land\lnot q$.

1455: %joe5: added; here is where the dependence on \Phi comes in

1456: %For any objective formula $\alpha$, let $W_\alpha$ be

1457: For any objective formula $\alpha$, let $W_{\alpha,\Phi}$ be

1458: the set of all worlds (over the primitive propositions $\Phi$) that

1459: satisfy $\alpha$.

1460: The axiom system

1461: %joe5

1462: %AX$_{fin}$

1463: AX$_{\Phi}$

1464: is then obtained from Levesque's system

1465: by replacing {\bf A5} by the following axiom:

1466: 

1467: \begin{tabular}{ll}

1468: %{\bf A5$_{fin}$}.  $N\alpha \equiv \And_{w\in W_{\lnot\alpha}} \lnot

1469: {\bf A5$_{\Phi}$}.  $N\alpha \equiv \And_{w\in W_{\lnot\alpha,\Phi}}

1470: \lnot L\lnot w$

1471: if $\neg \alpha$ is a propositionally consistent  objective formula.

1472: \end{tabular}

1473: 

1474: The axiom is easily seen to be sound since it merely expresses

1475: that $N\alpha$ holds at $W$ just in case $W$

1476: contains all worlds that satisfy $\lnot\alpha$.

1477: Note that this property depends only on the fact that $L$ and $N$ are

1478: defined with respect to complementary sets of worlds and, hence, also holds

1479: in the case of infinite $\Phi$. However, it is only in

1480: the finite case that we can express this axiomatically.

1481: Completeness is also very easy to establish.

1482: Levesque~\citeyear{Lev5}

1483: %joe5:

1484: % has already shown

1485: %that the axioms {\bf A1}--{\bf A4} prove that every formula is

1486: showed that in his system, even without {\bf A5}, every formula is

1487: provably

1488: equivalent to one without nested modalities. With {\bf A5$_{\Phi}$}, we

1489: then obtain an equivalent formula that does not mention $N$.

1490: In other words, given a formula consistent with respect to AX$_{\Phi}$,

1491: a satisfying model can be constructed with the usual technique

1492: for $K45$ alone.

1493: 

1494: \thm

1495: AX$_{\Phi}$ is sound and complete

1496: %joe5

1497: %if the number of primitive propositions is finite.

1498: %joe5:

1499: for the language $\onl(\Phi)$

1500: with respect to

1501: Levesque's semantics, if $\Phi$ is finite.

1502: \ethm

1503: 

1504: 

1505: %In the full paper, we provide an axiomatic characterization of

1506: %Levesque's semantics for any fixed set $\Phi$ of primitive

1507: %propositions.%

1508: %------------------------------------------------------------------------------

1509: \section{The Canonical-Model Approach}\label{canonical-model}

1510: %------------------------------------------------------------------------------

1511: %[NEEDS SHORTENING. SHOULD BE CUT TO ROUGHLY 2 PAGES.]

1512: 

1513: %gerhard5: modified for better glue

1514: %How do we extend this intuition to the multi-agent case?

1515: How do we extend our intuitions about only knowing to the multi-agent case?

1516: First we extend

1517: the language $\onl(\Phi)$ to the case of many agents.  That is, we now

1518: consider

1519: a language $\onln(\Phi)$, which is just like $\onl$ except that there

1520: are modalities $L_i$ and $N_i$ for each agent $i$, $1\le i\le n$, for

1521: some fixed $n$.

1522: %joe5:

1523: In the remainder of the paper, we omit the $\Phi$, just writing $\onl$

1524: and $\onln$, since the set of primitive propositions does not play a

1525: significant role.

1526: %joe1:

1527: %joe4: reinstated some stuff

1528: %gerhard2: shorten

1529: By analogy with the single-agent

1530: case,

1531: %gerhard5: added def. basic beliefs

1532: we call a formula {\em basic} if it does not mention any of the operators $N_i$

1533: ($i = 1, \ldots, n$) and

1534: %that does not mention any of the modal operators

1535: %$N_i$, $i = 1, \ldots, n$, a {\em basic\/} formula and an

1536: \newl{$i$-subjective\/} if it is  a Boolean combination of formulas

1537: of the form $L_i \phi$ and $N_i \phi$.   What should be the analogue of

1538: an objective formula? It clearly is more than just a propositional

1539: formula.  From agent 1's point of view, a formula like $L_2 p$ or even

1540: $L_2 L_1 p$ is just as ``objective'' as a propositional formula.

1541: %%In general, we can characterize the set

1542: %%of conceivable worlds as follows.

1543: We define a formula to be \newl{$i$-objective\/} if it is a Boolean

1544: combination of primitive propositions and

1545: formulas of the form $L_j\phi$ and $N_j \phi$, $j \ne i$,

1546: where $\phi$ is arbitrary.

1547: %By analogy with the single-agent

1548: %case, we call a formula {\em basic\/} if it does not mention

1549: %any of the modal operators

1550: %$N_i$, $i = 1, \ldots, n$,

1551: %{\em $i$-subjective\/} if it is a Boolean combination of formulas

1552: %of the form $L_i \phi$ and $N_i \phi$, and {\em $i$-objective\/}

1553: %if it is a Boolean

1554: %combination of primitive propositions and

1555: %formulas of the form $L_j\phi$ and $N_j \phi$, $j \ne i$,

1556: %where $\phi$ is arbitrary.

1557: %For example, from agent 1's point of view, a formula like $L_2 p$ or

1558: %even $L_2 L_1 p$ is just as ``objective'' as a propositional formula.

1559: Thus,

1560: $q \land N_2 L_1p$ is 1-objective, but

1561: $L_1 p$ and $q \land L_1p$ are not.  The $i$-objective formulas true at

1562: a world can be thought of as characterizing what is true apart from

1563: agent $i$'s subjective knowledge of the world.

1564: 

1565: 

1566: The standard

1567: model here is to have a {\em Kripke structure\/} with worlds and

1568: accessibility

1569: relations that describe what worlds the agents consider possible in

1570: each world.  Formally, a (Kripke) structure

1571: %joe1: added

1572: or model

1573: is a tuple $M = (W,\pi,

1574: \K_1, \ldots, \K_n)$, where $W$ is a set of

1575: %gerhard6 added footnote due to ref1's comment

1576: worlds,\footnote{Note that here $W$ denotes the set of {\em all}

1577: worlds of the particular model $M$,

1578: not just the (epistemically) possible ones as in Levesque's

1579: logic.}

1580: $\pi$ associates with each world a truth

1581: assignment to the primitive propositions, and

1582: $\K_i$ is agent $i$'s accessibility

1583: relation.

1584: %joe1: I didn't think this was really worth saying; Kripke structure

1585: %are pretty standard

1586: %\footnote{Note that the obvious extension, namely having a globally

1587: %accessible set of worlds for each agent, does not work since it would

1588: %make the agents mutually introspective.}

1589: %joe1: moved up from below

1590: Given such a Kripke structure $M$,

1591: let $\K_i^M(w)

1592: = \{w': (w,w') \in \K_i\}$.%

1593: \footnote{We use the superscript $M$ since we shall later need to talk

1594: about the $\K_i$ relations in more than one model at the same time.}

1595: %We similarly write $W^M$ to denote the set of worlds in structure $M$.)

1596: $\K_i^M(w)$ is the set of worlds that

1597: agent $i$ considers possible at $w$ in structure $M$.

1598: As usual, we define

1599: $$\mbox{$(M,w) \sat L_i \alpha$ if $(M,w') \sat \alpha$ for all $w' \in

1600: \K_i^M(w)$.}$$

1601: We focus on structures where the accessibility relations are Euclidean

1602: and transitive,

1603: %joe4: reinstated

1604: %which yields a model of belief which is well known to

1605: %obey the K45 axioms (generalized to $n$ agents) \cite{Chellas,HM2}.

1606: %\deleted{

1607: where a relation $R$ on $W$ is Euclidean

1608: if $(u,v) \in R$ and $(u,w) \in R$ implies that $(v,w) \in R$, and

1609: $R$ is transitive if $(u,v) \in R$ and $(v,w) \in R$ implies that $(u,w)

1610: \in R$.  We call such structures $\Wax$-structures.

1611: It is well known \cite{Chellas,HM2} that these assumptions

1612: are precisely what is required to get belief to obey the K45 axioms

1613: (generalized to $n$ agents).

1614: %For example, the multi-agent version of {\bf 4} would be

1615: %$$K_i \phi \rimp K_i K_i \phi, \ \ \ i = 1, \ldots, n.$$

1616: We say that a formula consistent with these

1617: axioms is $\Wax$-consistent.

1618: %joe4: added

1619: An infinite set of formulas is said to be $\Wax$-consistent if

1620: the conjunction of the formulas in

1621: every one of its finite subsets is $\Wax$-consistent.

1622: 

1623: %joe4: reinstated

1624: %gerhard2: cut

1625: Now the question is how to define the modal operator $N_i$.

1626: The problem in the multi-agent case is that we can

1627: no longer identify a possible world with a truth assignment.

1628: In the single-agent case, knowing the set of truth assignments that the

1629: agent considers possible completely determines his knowledge.  This is

1630: no longer true in the multi-agent case.  Somehow we must take the

1631: accessibility relations into account.

1632: A general semantics for an $N$-like operator was first given by

1633: Humberstone~\citeyear{Humberstone} and later by Ben-David and

1634: Gafni~\citeyear{BenDavid}.

1635: %joe5:

1636: %Following this approach, we provisionally define

1637: In this approach, the semantics of $N_i$ is given as follows:

1638: $$\mbox{$(M,w) \sat N_i \alpha$ if $(M,w') \sat \alpha$ for all $w'

1639: %%joe1:

1640: %%\notin \K_i^M(w)$}.$$

1641: \in W- \K_i^M(w)$}.$$

1642: The problem with this definition is that it misses out on the intuition

1643: that when evaluating $N_i \alpha$, we keep the set of worlds that agent

1644: $i$ considers possible fixed.  If $w' \in W - \K_i^M(w)$, there is

1645: certainly no reason to believe that $\K_i^M(w) = \K_i^M(w')$.

1646: 

1647: %joe1:

1648: %We solve this problem as follows.

1649: %gerhard2: briefly motivate use of i-equivalent worlds

1650: %joe4: cut (since I reinstated other stuff)

1651: %As for $N_i$, one may be tempted to identify

1652: %$i$'s epistemically impossible worlds with $W - \K_i^M(w)$.%

1653: %\footnote{See also~\cite{Humberstone,BenDavid} for

1654: %other

1655: %definitions of

1656: %$N$-like operators

1657: %%joe3:

1658: %in this spirit.}

1659: %However, on closer inspection, not all worlds in $W - \K_i^M(w)$

1660: %satisfy Levesque's first property, which requires that the

1661: %impossible worlds keep the set of possible worlds fixed.

1662: %If $w' \in W - \K_i^M(w)$, there is

1663: %certainly no reason to believe that $\K_i^M(w) = \K_i^M(w')$.

1664: One approach to solving this problem is as follows:

1665: If $w$ and $w'$ are two worlds in $M$, we write \newl{$w \approx_i w'$} if

1666: $\K_i^M(w) = \K_i^M(w')$, \ie if $w$ and $w'$ agree on the possible

1667: worlds according to agent $i$.

1668: We then define

1669: $$\mbox{$(M,w) \sat N_i \alpha$ if $(M,w') \sat \alpha$ for all $w'$

1670: %joe1:

1671: %such that $w' \notin \K_i^M(w)$ and $w \approx_i w'$.}$$

1672: such that $w' \in W - \K_i^M(w)$ and $w \approx_i w'$.}$$

1673: %joe1: lots more here

1674: 

1675: While this definition does capture the first of Levesque's properties,

1676: it does not capture the second.  To see the problem, suppose we have

1677: only one agent and a structure $M$ with only one possible world $w$.

1678: Suppose that $(w,w) \in \K_1^M$ and $p$ is true at $w$.  Then it

1679: is easy to see that $(M,w) \sat L_1 p \land N_1 p$, contradicting axiom

1680: {\bf A5}.

1681: The problem is that since the structure has only one world

1682: and it is in $\K_1^M(w)$,  there are no worlds in $W - \K_1^M(w)$.

1683: Thus, $N_1 p$ is vacuously true.

1684: Intuitively, there just aren't enough

1685: ``impossible'' worlds in this case;

1686: %gerhard2: cut

1687: %Roughly speaking, Levesque's second

1688: %property is not satisfied by this semantics.

1689: the set of conceivable

1690: worlds is not independent of the model.

1691: %joe4:

1692: %gerhard2: rewrite to shorten since people know canonical models

1693: %          rewritten stuff is just before formal def of can. model

1694: %In order to satisfy the second of Levesque's properties,

1695: To deal with this problem,

1696: we focus attention on one particular model, the

1697: {\em canonical model},

1698: %%joe1: cut

1699: %%denoted $M^c$,

1700: %%in which there is precisely one

1701: %%world corresponding to each maximal consistent set of formulas.

1702: which intuitively has ``enough'' worlds.

1703: %joe5:

1704: %To define this formally, we

1705: %first need the notion of a maximal consistent set.

1706: Its worlds consist of all the maximal consistent subsets of basic

1707: formulas.  (Recall that maximal consistent sets were defined in the

1708: proof of Theorem~\ref{Levthm1}.)  Thus, in some sense, the canonical

1709: model has as many worlds as possible.

1710: 

1711: %joe1: cut; said it earlier

1712: %Formally, we proceed as follows.  Let $\Wax$ consist of the multi-agent

1713: %version of the K45 axioms presented earlier.  Thus, for example,

1714: %%joe1: expanded

1715: %%let us assume a standard proof theory K45$_n$ with the usual

1716: %%notion of consistency (see, for example,~\cite{HM2}).

1717: %instead of {\bf K}, we have

1718: %\begin{quote}

1719: %$L_i (\phi \rimp \psi) \rimp (L_i \phi \rimp L_i \psi)$.

1720: %\end{quote}

1721: %A formula $\phi$ is $\Wax$-consistent if $\neg \phi$ is not provable

1722: %from $\Wax$.

1723: %joe1: now earlier

1724: %A {\em basic

1725: %formula\/} is

1726: %one that does not involve any $N_j$ or $O_j$ modalities, for $j = 1,

1727: %\ldots, n$.

1728: %joe5: cut; defined it earlier

1729: %\dfn

1730: %A set $\Gamma$ of basic formulas is a {\em maximal consistent set (of

1731: %basic formulas)\/} iff

1732: %$\Gamma$ is $\Wax$-consistent and no proper superset of $\Gamma$ is

1733: %$\Wax$-consistent. \edfn

1734: %joe1: cut; we never really use this

1735: %The following proposition lists some of the properties of

1736: %maximal consistent sets.

1737: %%joe1: added

1738: %A proof can be found, for example, in \cite{HM2}.

1739: %\pro

1740: %\label{properties-of-max-cons-sets}

1741: %Let $\Gamma$ be a maximal consistent set. Then

1742: %\begin{enumerate}

1743: %\item for every $\alpha$, either $\alpha\in\Gamma$ or

1744: %$\lnot\alpha\in\Gamma$.

1745: %\item $\alpha \lor \beta \in \Gamma$ iff $\alpha\in \Gamma$ or

1746: %$\beta\in\Gamma$.

1747: %\item $\alpha \land \beta\in\Gamma$ iff $\alpha\in \Gamma$ and

1748: %$\beta\in\Gamma$.

1749: %\item if $\alpha$ is provable in K45$_n$, then $\alpha\in \Gamma$.

1750: %\item if $\alpha\in\Gamma$ and $\alpha\rimp\beta\in\Gamma$, then

1751: %$\beta \in\Gamma$.

1752: %\end{enumerate}

1753: %\epro

1754: %gerhard2: rewrite to shorten

1755: %joe5:

1756: %Every maximal consistent set is satisfiable in some model.  The

1757: %canonical model is one where {\em every\/} maximal consistent set is

1758: %satisfiable at some state.

1759: %joe1: again, removed label

1760: %\begin{definition} The Canonical K45$_n$-Model $M^c$\\

1761: %

1762: %In order to satisfy the second of Levesque's properties,

1763: %we focus attention on one particular model, the

1764: %{\em canonical model} for $\Wax$, which is defined, in the usual way,

1765: %joe3;

1766: %by way of

1767: %using

1768: %sets of basic formulas which are maximally consistent with respect

1769: %to $\Wax$. The idea is that, since the canonical model satisfies every

1770: %maximally consistent set at some state, there are ``enough'' worlds

1771: %in this model.

1772: 

1773: \dfn The {\em canonical model\/} (for $\Wax$) $M^c = ( W^c, \pi^c,

1774: \K_1^c,\ldots, \K_n^c )$ is defined as follows:

1775: \begin{itemize}

1776: %Gerhard2, to save some space

1777:   \item $W^c = \{ w\;|\; \mbox{$w$ is a maximal consistent set of basic

1778: formulas \wrt K45$_n$}\}$,

1779:   \item for all primitive propositions

1780:   $p$ and $w\in W^c$, $\pi(w)(p) =$ {\bf true}

1781:   iff $p\in w$,

1782: %joe1: define w/L_i, since I use it later

1783:   \item $(w,w') \in \K_i^c$ iff $w/L_i \subseteq w'$, where

1784:   $w/L_i = \{\alpha \;|\; L_i \alpha \in w\}$.

1785: %%$L_i\alpha\in w$

1786: %  \item $W^c = \{ w\;|\; \mbox{$w$ is a maximal consistent set wrt K45$_n$}\}$.

1787: %  \item For all primitive propositions

1788: %  $p$ and $w\in W^c$, $\pi(w)(p) =$ {\bf true}

1789: %  iff $p\in w$.

1790: %%joe1: define w/L_i, since I use it later

1791: %  \item $(w,w') \in \K_i^c$ iff $w/L_i \subseteq w'$, where

1792: %  $w/L_i = \{\alpha \;|\; L_i \alpha \in w\}$.

1793: %%$L_i\alpha\in w$

1794: %%        then $\alpha\in w'$. \bbox

1795: \end{itemize}

1796: \end{definition}

1797: \deleted{

1798: Using standard techniques (see, for example, \cite{Chellas,HM2}), we

1799: can show that

1800: \thm\label{canonicalmodel}

1801: $M^c$ is a $\Wax$ structure, and for each maximal

1802: consistent set $w$, we have

1803: $(M^c,w) \sat \phi \mbox{ iff } \phi \in w$. \ethm

1804: This shows that every satisfiable formula is satisfiable in some state

1805: in $M^c$.

1806: 

1807: %The following (well known) theorem tells us that, as far as basic

1808: %formulas are concerned, nothing is lost from a logical

1809: %point of view if we confine our attention to the canonical model.

1810: %%

1811: %\begin{theorem}

1812: %\label{canonical-model-theorem}

1813: %$M^c$ is a K45$_n$-model and for every set of  basic formulas $\Gamma$,

1814: %$\Gamma$ is satisfiable iff it is satisfiable in $M^c$.

1815: %\end{theorem}df

1816: %

1817: } %%% END DELETED

1818: 

1819: 

1820: Validity in the canonical-model approach is defined with respect to

1821: the canonical model only. More precisely, a formula $\alpha$ is said to be

1822: %joe1: we're going to have more than one notion of validity

1823: {\em valid in the canonical-model approach}, denoted

1824: $\mdcm\alpha$, iff

1825: %joe5: added, for future reference

1826: %gerhard5: parentheses?

1827: %$(M^c \md \alpha$, that is, if

1828: $M^c \md \alpha$, that is, if

1829: for all worlds $w$ in the canonical model

1830: we have $(M^c,w)\md \alpha$.

1831: 

1832: \deleted{

1833: Note that, in contrast to Levesque's approach, there is no need to consider

1834: maximal sets of worlds, since the canonical model by construction provides a

1835: perfect match between the sets of basic beliefs that an agent may hold and the

1836: sets of possible worlds.

1837: %joe1: I don't like forcing breaks.

1838: %\\[1ex]

1839: }

1840: 

1841: %joe7: in response to comments by referee 2

1842: We clearly cannot use the canonical model in a practical way.  It  can

1843: be shown that it has uncountably many worlds.  Each of its worlds is

1844: characterized by an infinite set of formulas, so cannot be described

1845: easily.   Moreover, in general, both $\K_i^c(w)$

1846: and $W^c - \K_i^c(w)$ are infinite, so we cannot compute whether $L_i

1847: \phi$ or $N_i \phi$ holds at a given world.  Thus, our interest in the

1848: canonical model is mainly to understand whether it gives reasonable

1849: semantics to the $N_i$ operator.

1850: 

1851: %joe7: changed next line, to provide glue with previous paragraph

1852: %We now want to argue that,

1853: We start by arguing that,

1854: %joe2: added

1855: for an appropriate notion of ``possibility'' and ``conceivability'',

1856: this semantics satisfies the first two of

1857: Levesque's properties.

1858: %joe2: cut; notice that this only talks about the second property anyway

1859: \deleted{

1860: That is, we want to show that under an

1861: appropriate notion of ``conceivable state'',

1862: the set of conceivable states

1863: for agent $i$ is indeed the same at all worlds.  Notice that we say

1864: ``conceivable state'' here rather than ``conceivable world''.}

1865: %\end{delete}

1866: %gerhard2: rewriting to shorten

1867: What then is a conceivable world?

1868: Intuitively, it is an objective state of

1869: affairs from agent $i$'s point of view, which does not include $i$'s

1870: beliefs. In the single-agent case, this is simply a truth assignment.

1871: In the multi-agent case, things are more complicated, since beliefs

1872: of other agents are also part of $i$'s objective world.

1873: %gerhard2: cut

1874: %In the

1875: %single-agent case, a world

1876: %is simply a truth assignment; the set of conceivable worlds consists

1877: %of all truth assignments.  In the multi-agent case, we can no longer

1878: %identify a world with a truth assignment.  A world $w$ in a model $M$ is

1879: %characterized by a truth assignment together with the set of possible

1880: %worlds $\K_i^{M}(w)$.  It is not easy to give a nice

1881: %model-independent characterization of all the conceivable worlds.

1882: %Thus, we instead associate with each world

1883: %a notion of ``agent $i$'s state'' in that world in such a way that there

1884: %is a fixed set of conceivable states for agent $i$, independent of the

1885: %model.

1886: %Intuitively, a conceivable state of agent $i$ is a state of

1887: %affairs

1888: %that does not include $i$'s beliefs. In other words, it is an {\em

1889: %objective\/}

1890: %world from $i$'s point of view.

1891: %One way of characterizing $is

1892: %by the $i$-objective formulas that are true at that world.

1893: One way of characterizing a state of affairs from $i$'s point of view is

1894: by the set of $i$-objective formulas that are true at a particular world.

1895: For

1896: technical reasons, in this section we restrict even further to the

1897: $i$-objective {\em basic\/} formulas---%

1898: %joe4: added, since cut earlier

1899: that is, those formulas that do not mention any of the modal operators

1900: $N_j$, $j = 1, \ldots, n$---%

1901: that are true.

1902: %joe2: cut; we haven't talked about maximal sets.

1903: %The motivation for

1904: %this is in the same  spirit as Levesque's motivation for restricting to

1905: %maximal sets:

1906: If we assume that the basic formulas determine all the

1907: other formulas,

1908: %joe4:

1909: which can be shown to be true in the single-agent case, and under this

1910: semantics for the multi-agent case,

1911: then it is arguably reasonable to restrict to basic formulas.

1912: %joe4

1913: However,

1914: as we

1915: shall see in Section~\ref{tree-approach}, it is not clear that this

1916: restriction is appropriate,

1917: %joe2

1918: %For now, we take the $i$-objective basic

1919: %formulas true at a world to characterize that world from $i$'s point of

1920: %view.

1921: although we make it for now.

1922: 

1923: %gerhard6: made this into a dfn. Used underline (\newl) for better

1924: %visibility

1925: \dfn

1926: Given a situation $(M,w)$, let \newl{$\obji(M,w)$} consist of all the

1927: $i$-objective basic formulas that are true at $(M,w)$.

1928: %joe7: put in material from next definition too

1929: let \newl{$\Obji(M,w)$} = $\{\obji(M,w') \;|\; w'

1930: \in \K_i^M(w)\}$, and let

1931: \newl{$\subji(M,w)$} =

1932: $\{\mbox{basic}\ L_i\alpha\;|\; (M,w)\md L_i\alpha\} \union

1933:               \{\mbox{basic}\ \lnot L_i\alpha\;|\; (M,w)\nmd

1934: L_i\alpha\}$.

1935: \edfn

1936: We take $\obji(M,w)$

1937: to be $i$'s state at $(M,w)$.  Notice that $\obji(M,w)$ is a maximal

1938: consistent set of $i$-objective basic formulas.  For ease of exposition,

1939: we say \newl{$i$-set} from now on rather than ``maximal

1940: set of $i$-objective basic formulas''.  Thus,

1941: the set of conceivable states for agent $i$ is the set of all

1942: $i$-sets.

1943: Notice that the set of conceivable states is

1944: independent of the model.  It is easy to show that this is a

1945: generalization of the

1946: single-agent case, since in the single-agent case the $i$-objective

1947: basic formulas

1948: are just the propositional formulas, and

1949: an $i$-set

1950: can be identified with a truth assignment.

1951: 

1952: %joe7: moved this up from below too and added second sentence

1953: $\Obji(M,w)$ is the set of $i$-sets that agent

1954: $i$ considers possible in situation $(M,w)$;

1955: $\subji(M,w)$ characterizes $i$'s basic beliefs in $(M,w)$.  Notice that

1956: if $\alpha$ is an $i$-objective basic formula, then

1957: $L_i \alpha \in \subji(M,w)$ iff $\alpha$ is in every $i$-set in

1958: $\Obji(M,w)$.

1959: %joe5: cut (since definition reinstated below)

1960: %joe2: moved up from below (since I cut material below for abstract.

1961: %Given a situation $(M,w)$, define $\Obji(M,w) = \{\obji(M,w') \;|\; w'

1962: %\in \K_i^M(w)\}$.  Thus, $\Obji(M,w)$ is the set of $i$-sets that agent

1963: %$i$ considers possible in situation $(M,w)$.

1964: 

1965: %joe2:

1966: %With this definition of conceivable state for agent $i$, we can

1967: %re-examine the properties of the canonical model.

1968: With these definitions, we can

1969: show that the first two of Levesque's properties hold in the canonical

1970: model.

1971: The first property

1972: says that at all worlds $w'$ considered in evaluating a formula of the

1973: form $N_i \phi$ at a world $w$, the set of possible states---that

1974: is, the set $\{\obji(M^c,w'') \;|\; w''

1975: %joe2: this is a typo, right?

1976: %\in

1977: \notin

1978: \K_i^c(w')\}$---is the same

1979: for all $w' \in \K_i^c(w)$.

1980: This is easy to see, since the

1981: only worlds $w'$ we consider are those such that $\K_i^c(w') = \K_i^c(w)$.

1982: The second property says that the union of the set of states associated

1983: with

1984: the worlds used in computing $L_i \phi$ at $w$ and the set of states

1985: associated with the worlds

1986: used in computing $N_i \phi$ at $w$ should consist of all conceivable

1987: states. To show this, we must show that for every world $w$ in the

1988: canonical model, the set $\{\obji(M^c,w') \;|\; w' \approx_i w\}$

1989: consists of all $i$-sets.

1990: %joe2: unnecessary for abstract

1991: 

1992: %joe7:

1993: %To prove this, we need some preliminary results and definitions.

1994: To prove this, we need two preliminary lemmas.

1995: %which will also be useful in the next section.

1996: 

1997: %joe7: combined this definition with previous one

1998: %\dfn

1999: %Given a situation $(M,w)$, define \newl{$\Obji(M,w)$} = $\{\obji(M,w')

2000: %\;|\; w'

2001: %\in \K_i^M(w)\}$.  Thus, $\Obji(M,w)$ is the set of $i$-sets that agent

2002: %$i$ considers possible in situation $(M,w)$.  Define

2003: %\newl{$\subji(M,w)$} =

2004: %$\{\mbox{basic}\ L_i\alpha\;|\; (M,w)\md L_i\alpha\} \union

2005: %              \{\mbox{basic}\ \lnot L_i\alpha\;|\; (M,w)\nmd

2006: %L_i\alpha\}$. Thus, $\subji(M,w)$ characterizes $i$'s basic beliefs.

2007: %\edfn

2008: 

2009: \lem

2010: \label{$i$-equivalence-same-as-same-basic-beliefs}

2011: Let $w$ and $w'$ be worlds in $M^c$. Then $w\approx_i w'$ iff

2012: %gerhard5: added ``, that is,''

2013: %agent $i$ has the same basic beliefs at $w$ and $w'$.

2014: agent $i$ has the same basic beliefs at $w$ and $w'$, that is,

2015: $\subji(M^c,w) = \subji(M^c,w')$.

2016: \elem

2017: 

2018: \prf

2019: The ``only if'' direction is immediate because $w$ and $w'$ are assumed

2020: to have the same $\K_i$-accessible worlds.

2021: To prove the ``if'' direction,

2022: suppose that $\subji(M^c,w) = \subji(M^c,w')$ but

2023:  $w\not\approx_i w'$. Without loss of generality, there is a world $w^*

2024: \in  \K_i^c(w) - \K_i^c(w')$.

2025: By the definition of the canonical model,

2026: there must be a basic formula $L_i\alpha\in w'$ such that

2027: $\alpha\not\in w^*$. By assumption,

2028: $L_i\alpha\in w$, contradicting the assumption that $w^* \in

2029: \K_i^c(w)$. \eprf

2030: 

2031: %joe1: added this lemma; it's not completely trivial

2032: %gerhard7: added ``basic'' to i-objective

2033: \lem\label{consistency}  Suppose $\Gamma$ consists only of $i$-objective basic

2034: formulas, $\Sigma$ consists only of $i$-subjective basic formulas, and

2035: $\Gamma$ and $\Sigma$ are both $\Wax$-consistent.  Then $\Gamma \union

2036: \Sigma$ is $\Wax$-consistent. \elem

2037: 

2038: \prf

2039: This follows immediately from part (c) of Proposition~\ref{construction}

2040: below.  \eprf

2041: 

2042: 

2043: %Suppose not.  Since $\Gamma$

2044: %is consistent, there is a model $M = (W,\pi,\K_1, \ldots,

2045: %\K_n)$ and a world $w$ such that

2046: %$(M,w) \sat \Gamma$;%

2047: %\footnote{Throughout this paper we consistently identify a set of

2048: %formulas with its conjunction.  Thus, we write $(M,w) \sat \Gamma$ if

2049: %$(M,w)$ satisfies each formula in $\Gamma$, and if $\Delta$ is a finite

2050: %set of formulas, we write $\Delta \rimp \alpha$ as an abbreviation for

2051: %$(\land_{\delta \in \Delta} \delta) \rimp \alpha$.}

2052: %similarly there is a model $M' = (W',\pi', \K_1',

2053: %\ldots, \K_n')$ and a world $w'$ such that $(M',w') \sat \Sigma$.  We

2054: %can assume without loss of generality that $W \inter W' = \emptyset$

2055: %and that there is no edge in $M'$ leading to $w'$ (\ie for all $j = 1,

2056: %\ldots, n$ and all worlds $w'' \in W'$, we have

2057: %$(w'',w') \notin \K_j$).  (A formal construction satisfying these

2058: %properties appears in the proof of Proposition~\ref{construction}.)

2059: %  Let $M'' = (W'', \pi'', \K_1'',

2060: %\ldots, \K_n'')$ be the ``union'' of $M$ and $M'$, except that we

2061: %replace the successors of $w'$ in $W'$ by the successors of $w$; that

2062: %is,

2063: %$W'' = W \union W'$, $\pi''|_W = \pi$, $\pi''|_{W'} = \pi'$, $\K_j'' =

2064: %\K_j \union \K_j'$ for $j \ne i$, and $\K_i'' = \K_i \union \K_i' \union

2065: %\{(w',w'') : (w,w'') \in \K_i\} - \{(w',w''): w'' \in W''\}$.   It is now

2066: %easy to check that $(M'',w') \sat \Sigma \union \Gamma$.  This shows

2067: %that $\Sigma \union \Gamma$ is consistent. \eprf

2068: 

2069: %joe1: added glue

2070: We can now prove that the set of conceivable states for agent $i$ is the

2071: same at all worlds of the canonical model.

2072: This follows from

2073: %joe3: to save space

2074: %joe5: put back

2075: the following result.

2076: \thm

2077: \label{all-possibilities-covered}

2078: Let $w\in W^c$. Then for every

2079: %joe1: aren't abbreviations wonderful ...

2080: %maximal consistent set $\Gamma$ of $i$-objective basic formulas

2081: $i$-set $\Gamma$

2082: there is exactly one world

2083: $w^*$ such that $\obji(M^c,w^*) = \Gamma$ and $w\approx_i w^*$.

2084: \ethm

2085: 

2086: \prf

2087: %Let $\Sigma = \{{\rm basic}\ L_i\alpha\;|\; (M^c,w)\md L_i\alpha\}

2088: %\union

2089: %              \{{\rm basic}\ \lnot L_i\alpha\;|\; (M^c,w)\nmd

2090: %L_i\alpha\}$.

2091: Let $\Sigma = \subji(M^c,w)$.

2092: Since $\Gamma$ consists of $i$-objective basic formulas only,

2093: $\Sigma$ consists of $i$-subjective formulas, and $\Gamma$ and

2094: $\Sigma$ are both $\Wax$-consistent, by

2095: Lemma~\ref{consistency}, $\Gamma \union \Sigma$ is $\Wax$-consistent.

2096: Let $w^*$

2097: be a maximal consistent set that contains $\Gamma\union\Sigma$. Since

2098: $w$ and $w^*$ agree on $\Sigma$, $w\approx_i w^*$

2099: by Lemma~\ref{$i$-equivalence-same-as-same-basic-beliefs}. The uniqueness of $w^*$

2100: follows by a simple induction argument.

2101: \eprf

2102: 

2103: 

2104: %joe2: cut for abstract

2105: %Thus, by focusing on the canonical model, we guarantee that the

2106: %semantics has the second key property that we observed in the

2107: %single-agent case.  As we shall see, just as in the single-agent case,

2108: %it is this property that guarantees the analogue of {\bf A5}.

2109: 

2110: %joe1: this paragraph new; later material is moved back from the next

2111: %section

2112: What about the third property?  This says that every subset of

2113: $i$-sets arises as the set of $i$-sets associated

2114: with the worlds that $i$ considers possible in some situation; that is,

2115: for every set $S$ of $i$-sets, there should be some

2116: situation $(M^c,w)$ such that $S = \Obji(M^c,w)$.  As

2117: %\{\obji(M^c,w') \;|\; w' \in \K_i^c(w)\}$.

2118: we now show, this property does {\em not\/} hold in the canonical model.

2119: We do this by showing that the set of $i$-sets associated with

2120: the worlds considered possible in any situation in the canonical model

2121: all have a particular property we call {\em limit closure}.%

2122: \footnote{This turns out to be closely related to the limit closure

2123: property discussed in \cite{FGHV92}; a detailed comparison would

2124: take us too far afield here though.}

2125: \dfn

2126: \label{limit-closure}

2127: %joe1: rewrote all this material

2128: %Let $M = (W,\pi, \K_1, \ldots, \K_n)$ be a model with $w\in W$ and let

2129: %$S$

2130: %be a maximal consistent set of basic formulas. If for every finite

2131: %subset $S'$ of

2132: %$S$ there is a $w'\in\K_i^M(w)$ such that $(M,w')\md S'$, then there is

2133: %a $w^*\in \K_i^M(w)$ such that $(M,w^*)\md S$.

2134: We say that an $i$-set $\Gamma$ is a {\em limit\/} of a set $S$ of

2135: $i$-sets if, for every finite subset $\Delta$ of $\Gamma$, there is a

2136: set $\Gamma' \in S$ such that $\Delta \subset \Gamma'$.  A set $S$ of

2137: $i$-sets is \newl{limit closed\/} if every limit of $S$ is in $S$.

2138: \edfn

2139: %

2140: %While certainly not every model is limit-closed, it is not hard to see

2141: %that $M^c$ is.

2142: %joe1: the statement and proof of the lemma are new

2143: \lem\label{lc}

2144: For every world $w$ in $M^c$, the set $\Obji(M^c,w)$

2145: is limit closed.

2146: \elem

2147: 

2148: \prf

2149: %joe1: redid proof to match new theorem

2150: Let $w$ be a world in the canonical model and let

2151: $\Gamma$ be an $i$-set which is a limit

2152: of $\Obji(M^c,w)$.  We want to show that $\Gamma \in \Obji(M^c,w)$.  Let

2153: $\Sigma =

2154: \{\mbox{basic } \beta \;|\; L_i \beta \in w\}$.  We claim that $\Gamma

2155: \union \Sigma$ is $\Wax$-consistent.  For suppose not.  Then there must

2156: be a finite subset $\Delta \subseteq \Gamma$ such that $\Delta \union

2157: \Sigma$ is inconsistent.  Since $\Gamma$ is a limit of $\Obji(M^c,w)$,

2158: there

2159: must be some world $w'$ in $\Obji(M^c,w)$ such that $(M^c,w') \sat

2160: \Delta$. By

2161: construction of the canonical model, since $w' \in \K_i^c(w)$, we must

2162: have that $(M^c,w') \sat \Sigma$.  Thus $\Delta \union \Sigma$ is

2163: consistent, contradicting our assumption.

2164: 

2165: 

2166: Since $\Gamma \union \Sigma$

2167: is consistent, there is a world $w^*$ in the canonical model such that

2168: $(M^c,w^*) \sat \Gamma \union \Sigma$.  Clearly $\Gamma =

2169: \obji(M^c,w^*)$.  Moreover, by construction, we must have $w^* \in

2170: \K_i^c(w)$.  Thus, $\Gamma \in \Obji(M^c,w)$, as desired.

2171: \eprf

2172: 

2173: 

2174: Since there are clearly sets of $i$-sets that are not limit closed,

2175: it follows that this semantics does not satisfy the third property.

2176: One consequence of this

2177: %joe2:

2178: %as we now show, is that $\neg O_i \neg O_j p$

2179: %is valid under this semantics.

2180: is a result already proved in \cite{Lakemeyer93},

2181: %joe5:

2182: which we reprove

2183: here, using an approach that will be useful for later results.

2184: \pro

2185: \label{not-O-$i$-not-O-j-p}

2186: %joe2: added ref

2187: {\rm \cite{Lakemeyer93}}

2188: %joe5

2189: %Let $p$ be a primitive proposition. Then $\mdcm \lnot O_i\lnot O_j p$.

2190: If $p \in \Phi$ and $i \ne j$, then $\mdcm \lnot O_i\lnot O_j p$.

2191: \epro

2192: %

2193: 

2194: \prf

2195: %joe7: added intuition

2196: We proceed by contradiction.  Our goal is to show that if

2197: $(M^c,w) \sat O_i \neg O_j p$, then the set $\Obji(M^c,w)$

2198: must contain a set that includes $O_j p$, for otherwise it would not be

2199: limit closed.  It follows that there is some world $v \in \K_i^c(w)$

2200: such that $(M^c,v) \sat O_j p$, contradicting the assumption that

2201: $(M^c,w) \sat L_i \neg O_j p$.

2202: 

2203: We first need a definition and a lemma.  We say that a

2204: basic formula $\psi$ is {\em (K45)-independent\/} of

2205: a basic formula $\phi$ if neither $\vdash_{\sWax} \phi \rimp \psi$ nor

2206: $\vdash_{\sWax} \phi \rimp \neg \psi$ hold.

2207: 

2208: \lem\label{indep} If $n \ge 2$ (\ie there are at least two agents) and

2209: $\phi_1, \ldots, \phi_m$ are consistent basic

2210: $i$-objective formulas, then

2211: there exists a basic $i$-objective formula $\psi$ of the form $L_j\psi'$

2212: which is independent of each of $\phi_1, \ldots, \phi_m$.

2213: \elem

2214: 

2215: %gerhard6: added ``basic''

2216: \prf Define the {\em depth\/} of a basic formula $\phi$, denoted

2217: $d(\phi)$, inductively:

2218: \begin{itemize}

2219: \item $d(p) = 0$ for a primitive proposition $p$,

2220: \item $d(\phi \land \psi) = \max(d(\phi), d(\psi))$,

2221: \item $d(\neg \phi) = d(\phi)$,

2222: \item $d(L_i \phi) = 1 + d(\phi)$.

2223: \end{itemize}

2224: Suppose that $\phi_1, \ldots, \phi_m$ are $i$-objective formulas such

2225: that $\max(d(\phi_1(, \ldots, d(\phi_k)) = K$.  Let $p$ be an arbitrary

2226: primitive proposition, and suppose $j \ne i$.  (Such a $j$ exists, since

2227: we are assuming $n \ge 2$.)  Let $\psi$ be the formula $(L_j

2228: L_i)^{K+1} p$, where by $(L_j L_i)^{K+1}$ we mean $K+1$ occurrences of

2229: $L_j L_i$.  Standard model theoretic arguments show that $\psi$ is

2230: independent of $\phi_1, \ldots, \phi_m$.  Very briefly:

2231: By results

2232: of \cite{HM2}, we know that $\phi_i$ is satisfiable in a treelike

2233: structure of depth at most $d(\phi_i)$, for $i = 1, \ldots, m$.  It is

2234: easy to see that this can

2235: be extended to two structures, one of which satisfies $\psi$, and the

2236: other of which satisfies $\neg \psi$.  Hence, $\psi$ is independent of

2237: $\phi_i$.\eprf

2238: 

2239: Continuing with the proof of Proposition~\ref{not-O-$i$-not-O-j-p},

2240: suppose by way of contradiction that

2241: $(M^c,w) \sat O_i \neg O_j p$.

2242: Let $\overline{w}$ be a world such that $(M^c,\overline{w})\md O_j p$

2243: and let

2244: %joe5: typo, right?

2245: %$\Gamma = \obji(M^c,w)$.

2246: $\Gamma = \obji(M^c,\overline{w})$.

2247: We claim that $\Gamma$ is a limit of

2248: $\Obji(M^c,w)$.

2249: %joe5:

2250: %For consider any finite subset $\Delta$ of $\Gamma$.

2251: To see this, consider any finite subset $\Delta$ of $\Gamma$.

2252: %joe5: simplified proof; dropped dependence on $\Phi$ being infinite

2253: Let $\psi$ be an $i$-objective basic formula of the form $L_j

2254: \psi'$ which is independent both of the

2255: conjunction of the formulas in $\Delta$ and of $p$.  The existence of

2256: such a formula follows from Lemma~\ref{indep}.

2257: %(Again, we are using the fact that our language has an infinite number

2258: %of primitive propositions.)

2259: %Then

2260: %$\Delta \union

2261: %\{ L_j q\}$ is clearly $\Wax$-consistent and consists of $i$-objective

2262: %formulas.

2263: Let $\Sigma = \subji(M^c,w)$.

2264: %$$\Sigma = \{{\rm basic}\ L_i\alpha\;|\; (M^c,w)\md L_i\alpha\} \union

2265: %\{{\rm basic}\ \lnot L_i\alpha\;|\; (M^c,w)\md \lnot L_i\alpha\}.$$

2266: %Clearly $\Sigma$ is $\Wax$-consistent and consists of $i$-subjective

2267: %formulas.

2268: By Lemma~\ref{consistency},

2269: $\Sigma \union \Delta \union \{L_j \psi'\}$ is consistent.  Thus,

2270: there is some world $w' \in W^c$

2271: such that $(M^c,w')\sat \Sigma \union \Delta \union \{L_j

2272: \psi'\}$.    By Lemma~\ref{consistency} again, there is some

2273: world $w''$ satisfying $p \land \neg L_j \psi'$ such that $w'' \approx_i

2274: w'$.

2275: Since $(M^c,w') \sat L_j \psi'$, we cannot have $w'' \in \K_j^c(w')$.  It

2276: follows that $(M^c,w') \sat \neg N_j \neg p$, and hence $(M^c,w') \sat

2277: \neg O_j p$.  Moreover, since $w'$ and $w$ agree on all $i$-subjective

2278: formulas, the canonical model construction guarantees that $w' \approx_i

2279: w$.

2280: %joe7: this is not quite right

2281: %Since $(M^c,w) \sat O_i \neg O_j p$, it must be the case that

2282: %for all $u$, we have $u \in \K_i^c(w)$ iff $(M^c,u) \sat \neg O_j p$.

2283: %In particular, this means that

2284: Since $(M^c,w) \sat O_i \neg O_j p$ , $(M^c,w') \sat \neg O_j p$, and

2285: $w' \approx_i w$, we must have that

2286: $w' \in \K_i^c(w)$.  Thus, $\obji(M^c,w')

2287: \in \Obji(M^c,w)$.  Moreover, by construction,  $\Delta

2288: %joe5: another typo, right?

2289: %\subseteq \obji(M^c,w)$.

2290: \subseteq \obji(M^c,w')$.

2291: Since $\Delta$ was chosen arbitrarily, it

2292: follows that $\Gamma$ is a limit of $\Obji(M^c,w)$.  By Lemma~\ref{lc},

2293: $\Gamma \in

2294: \Obji(M^c,w)$.  Thus, there is some world $v \in \K_i^c(w)$ such that

2295: $\obji(M^c,v) = \Gamma$.  It is a simple

2296: property of the canonical-model approach that two worlds that agree on

2297: all basic beliefs of an agent also agree on what the agent only believes.

2298: Hence, since $\overline{w}$ and $v$ agree on $j$'s basic beliefs, it

2299: follows that

2300: $(M^c,v)\md O_j p$, contradicting the assumption that $(\Mc,w) \md

2301: O_i\lnot O_j p$.

2302: \eprf

2303: 

2304: It may seem unreasonable that $\neg O_i \neg O_j p$ should be valid in

2305: the canonical-model approach.  Why should it be impossible for $i$ to

2306: know only that $j$ does not only know $p$?  After all, $j$ can

2307: (truthfully) tell $i$ that it is not the case that all he ($j$) knows is

2308: $p$.  We return to this issue in Sections~\ref{tree-approach}

2309: and~\ref{synthesis}.  For now, we focus on a proof theory for this

2310: semantics.

2311: 

2312: %------------------------------------------------------------------------------

2313: \subsection{A Proof Theory}\label{prooftheory}

2314: %------------------------------------------------------------------------------

2315: %

2316: We now consider an axiomatization for the language.

2317: The following axiomatization is exactly like Levesque's except that

2318: axiom {\bf A5} now requires

2319: %joe4

2320: %satisfiability in K45$_n$

2321: $\Wax$-consistency

2322: instead of merely

2323: propositional

2324: %joe4

2325: %logic.

2326: consistency.

2327: %joe1:

2328: For ease of exposition, we use the same names for the axioms as we did

2329: in the single-agent case with a subscript $n$ to emphasize that we

2330: are looking at the multi-agent version.

2331: \eject

2332: \begin{description}

2333: \item [Axioms:]\ \\[2ex]

2334: \begin{tabular}{ll}

2335: %joe1: added subscript n here

2336:   {\bf A1$_n$}. & Axioms of propositional logic.\\

2337:   {\bf A2$_n$}.

2338:   & $L_i(\alpha \rimp \beta) \rimp (L_i\alpha \rimp L_i\beta)$.\\

2339:   {\bf A3$_n$}.

2340:   & $N_i(\alpha \rimp \beta) \rimp (N_i\alpha \rimp N_i\beta)$.\\

2341:   {\bf A4$_n$}. & $\sigma \rimp L_i\sigma\land N_i\sigma$

2342:               if $\sigma$ is an $i$-subjective formula.\\

2343:   {\bf A5$_n$}. & $N_i\alpha \rimp \lnot L_i\alpha$

2344:              if  $\neg \alpha$ is a $\Wax$-%

2345: %joe4:

2346: %satisfiable

2347: consistent

2348: $i$-objective basic formula.

2349: %joe1: unnecessary

2350: %  {\bf A6} & $O_i\alpha \dimp (L_i\alpha\land N_i\lnot\alpha)$ & for

2351: %all $\alpha$

2352: \end{tabular}

2353: \item [Inference Rules:]\ \\[2ex]

2354: \begin{tabular}{lll}

2355:  {\bf MP$_n$.} & From $\alpha$ and $\alpha\rimp\beta$ infer $\beta$.\\

2356:  {\bf Nec$_n$.}

2357:  & From $\alpha$ infer $ L_i\alpha$ and $ N_i\alpha$.\\[1ex]

2358: \end{tabular}

2359: \end{description}

2360: %

2361: %joe1: moved this back from next page

2362: Notice that {\bf A5$_n$} assumes that $\alpha$ ranges only over {\em

2363: basic\/} $i$-objective formulas.

2364: %joe1: changed "falsifiability" to "satisfiability" a few times

2365: We need this restriction in order to appeal to satisfiability in the

2366: existing

2367: logic $\Wax$.\footnote{Note that this peculiar axiom schema is

2368: recursive

2369: since satisfiability in propositional \KFFn\ is decidable~\cite{HM2}.}

2370: %joe1: added

2371: To get a more general version of {\bf A5$_n$}, that applies to arbitrary

2372: formulas, we will need to appeal to consistency within the logic that the axioms

2373: are meant to characterize.  We return to this issue in Section~\ref{synthesis}.

2374: %gerhard4: cut since now redundant

2375: %For the proof theory, which we call AX, we consider the exact analogue of

2376: %Levesque's axiomatization, now using subscripted modal operators, and replacing

2377: %{\bf A5} by

2378: %

2379: %\begin{tabular}{lll}

2380: %  {\bf A5$_n$}. & $N_i\alpha \rimp \lnot L_i\alpha$ &

2381: %             if  $\neg \alpha$ is a $\Wax$-%

2382: %joe4:

2383: %satisfiable

2384: %consistent

2385: %$i$-objective basic formula.

2386: %\end{tabular}

2387: %

2388: It is not hard to show that these axioms are sound.

2389: %Gerhard3 added provability wrt AX

2390: %gerhard5: cut since changed back again

2391: %We write $\vdash_{{\rm AX}} \alpha$ for {\em $\alpha$ is provable in AX}.

2392: 

2393: \thm

2394: %joe1: for consistency ...

2395: %Soundness\\

2396: \label{soundness} {\rm \cite{Lakemeyer93}}

2397: For all $\alpha$ in $\onln$, if $\vdash\!\alpha$  then $\mdcm\alpha$.

2398: \ethm

2399: 

2400: \prf The proof proceeds by the usual induction on the length of a derivation.

2401: %gerhard4: simplified, only do case for A5_n

2402: %

2403: %For the base case,

2404: %we need to prove that all the axioms are sound. The soundness of {\bf A1$_n$}--{\bf

2405: %A4$_n$} follows immediately from the fact that the {\bf $L_i$} and {\bf

2406: %$N_i$} are \KFFn-operators.

2407: Here we show only the soundness of {\bf A5$_n$}.

2408: %\begin{itemize}

2409: %\item []

2410: %joe1: simplified

2411: %Let $w$ be a world such that $w\md N_i\alpha$, where

2412: Suppose $\alpha$ is a

2413: basic $i$-objective formula

2414: %%joe1

2415: %falsifiable in K45$_n$.

2416: such that $\neg \alpha$ is $\Wax$-consistent.

2417: Thus, there is an $i$-set containing $\neg \alpha$.  By

2418: Theorem~\ref{all-possibilities-covered}, it follows that for each world

2419: $w \in W^c$,

2420: there is a world $w' \approx_i w$ such that $(M^c,w') \sat \neg \alpha$.

2421: If $w' \in \K_i^c(w)$, it follows that $(M^c,w) \sat \neg L_i \alpha$.

2422: If $w' \notin \K_i^c(w)$, then $(M^c,w) \sat \neg N_i \alpha$.

2423: Thus, $(M^c,w) \sat \neg L_i \alpha \lor \neg N_i \alpha$; equivalently,

2424: $(M^c,w) \sat N_i \alpha \rimp \neg L_i \alpha$.  It follows that

2425: $\sat N_i \alpha \rimp \neg L_i \alpha$.

2426: %From Lemma We need to show that $w\md \lnot

2427: %L_i\alpha$.  Let $\Sigma = \{{\rm basic}\ L_i\beta\;|\; w\md L_i\beta\} \union

2428: %\{{\rm basic}\ \lnot L_i\beta\;|\; w\md\lnot L_i\beta\}$.  Since

2429: %$\neg \alpha$ is $\Wax$-satisfiable

2430: %by assumption, and since $\alpha$ is $i$-objective,

2431: %%joe1: I wonder if it's worth making this a separate lemma

2432: %as shown in the proof of Theorem~\ref{all-possibilities-covered},

2433: %$\{\lnot\alpha\} \union \Sigma$ is consistent. Therefore, there is a

2434: %world

2435: %$w^*$ in the canonical model such that $w^*\md\lnot\alpha$ and

2436: %$w^*\md\sigma$ for every $\sigma\in\Sigma$.  Also, by

2437: %Lemma~\ref{$i$-equivalence-same-as-same-basic-beliefs}, $w\approx w^*$.  Since

2438: %$w\md N_i\alpha$, we obtain $(w,w^*)\in \K_i$. Thus $w\md\lnot

2439: %L_i\alpha$.

2440: %\end{itemize}

2441: %The inference rules are obviously sound for $M^c$. Then,

2442: %assuming soundness holds for theorems with proofs of length $k$, the

2443: %soundness of $\vdash \alpha$, where $\alpha$ has a proof of length $k+1$,

2444: %follows immediately.

2445: \eprf

2446: 

2447: 

2448: %joe1: Did some rewriting here.  Next few sentences new

2449: We show in Section~\ref{tree-approach} that this axiomatization is

2450: incomplete.  In fact,

2451: %joe2: cut for now

2452: %as we show in Theorem~\ref{incompleteness},

2453: the

2454: formula $\neg O_i \neg O_j p$ is not provable.

2455: %although, as we saw in the previous section, it is valid.

2456: Intuitively, part of the problem

2457: here is that

2458: {\bf A5$_n$} is restricted to basic formulas.

2459: For completeness, we would need an analogue of {\bf A5$_n$} for arbitrary

2460: formulas.

2461: \deleted{

2462: Of course, if we could reduce

2463: arbitrary formulas of the form $N_i\beta$ or $L_i\beta$ to

2464: equivalent formulas $N_i\beta^*$ and $L_i\beta^*$, where $\beta^*$

2465: is a basic formula, then we could apply {\bf A5$_n$} directly.

2466: Such a reduction cannot be done

2467: in general. For example, $L_i N_j p$ and $N_i L_j N_i p$ are not

2468: reducible for distinct $i$ and $j$.

2469: However,

2470: if we rule out such cases, the

2471: proof theory is indeed complete for the restricted language, which we call

2472: $\onlnminus$.

2473: }

2474: However, we obtain completeness for a restricted language, which we call

2475: $\onlnminus$.

2476: %gerhard6: added for motivation

2477: Roughly, the restriction amounts to limiting what

2478: an agent can only know. In particular, only knowing can only be

2479: applied to basic

2480: %joe7

2481: %sentences.

2482: formulas.

2483: %

2484: \dfn

2485: %joe1: simplified (now that O is an abbreviation)

2486: %The Language $\onlnminus$\\

2487: %$\alpha$ is a formula of $\onlnminus$ iff $\alpha$ is a formula of

2488: %$\onln$ and,

2489: %joe1: now unnecessary

2490: %after replacing every occurrence of $ O_i\beta$ within $\alpha$ by its

2491: %definition $L_i\beta\land N_i\lnot\beta$,

2492: $\onlnminus$ consists of all formulas $\alpha$ in $\onln$ such that, in

2493: $\alpha$, no $N_j$ may occur within the

2494: scope of an $N_i$ or $L_i$ for $i\ne j$.

2495: \edfn

2496: %

2497: For example, $ N_i L_i\lnot N_i p$ and $ N_i( L_j p\lor N_i\lnot p)$ are

2498: in $\onlnminus$, and $ N_i N_j p$ and $ N_i L_j N_i p$ are not, for

2499: distinct $i$ and $j$.

2500: Note that formulas such as

2501: %gerhard7: fixed typos \O_i

2502: $O_i\lnot O_j p$ cannot be expressed in \onlnminus.

2503: 

2504: 

2505: To prove  completeness for the sublanguage $\onlnminus$,

2506: we need

2507: %joe7

2508: %a preliminary lemma, which describes a normal form for formulas.

2509: four preliminary lemmas.  The first describes a normal form for

2510: formulas.  Having such a normal form greatly simplifies the completeness

2511: proof.

2512: 

2513: 

2514: \lem\label{normalform} Every formula $\alpha$ in $\onln$ is

2515: provably equivalent to a disjunction of formulas of the following form:

2516: $$\begin{array}{l}

2517: \sigma \land L_1 \phi_{10} \land \neg L_1 \phi_{11}  \land

2518: \ldots \land \neg L_1 \phi_{1m_1} \land \ldots \land L_n \phi_{n0} \land

2519: \neg L_n \phi_{n1} \land \ldots \land \neg L_n \phi_{nm_n} \land\\

2520: N_1 \psi_{10} \land \neg N_1 \psi_{11} \land \ldots

2521: \land \neg N_1 \psi_{1k_1} \land \ldots \land N_n \psi_{n0} \land

2522: \neg N_n \psi_{n1} \land \ldots \land \neg N_n \psi_{nk_n},\end{array}$$

2523: where $\sigma$ is a propositional formula and

2524: $\phi_{ij}$ and $\psi_{ij}$

2525: are all $i$-objective formulas.  Moreover, if $\alpha$ in $\onlnminus$,

2526: we can assume that $\phi_{ij}$ and $\psi_{ij}$ are $i$-objective basic

2527: formulas.

2528: %Furthermore, if the modal operator $N_j$

2529: %does not appear in $\phi$, then it does not appear in the disjunction.

2530: \elem

2531: \prf We proceed by induction on the structure of $\phi$.  The only

2532: nontrivial cases are if $\phi$ is of the form $L_i \phi'$ or $N_i

2533: \phi'$.  If $\phi$ is of the form $L_i \phi'$, then, since $\phi \in

2534: \onlnminus$, $N_j$ does not appear in $\phi'$ for $j \ne i$.  We use the

2535: inductive hypothesis to get $\phi'$ into the normal form described in

2536: the lemma.  Notice that $N_j$ does not appear in the normal form for $j

2537: \ne i$.  We now use the the following equivalences to get $L_i \phi'$

2538: into the normal form:

2539: \begin{itemize}

2540: \item $L_i (\psi \land \psi') \dimp (L_i \psi \land L_i \psi')$

2541: \item $L_i (\psi \lor L_i \psi') \dimp (L_i \psi \lor L_i \psi')$

2542: \item $L_i (\psi \lor \neg L_i \psi') \dimp (L_i \psi \lor \neg L_i

2543: \psi')$

2544: \item $L_i L_i \psi \dimp L_i \psi$

2545: %gerhard4: JOE, STRICTLY SPEAKING, DON'T WE NEED TO

2546: %REQUIRE THAT $\LNOT L_I(P \LAND \LNOT P)$ FOR THE EQ. TO HOLD

2547: %IN OTHER WORDS, THE CASE OF AN INCONSISTENT BELIEVER NEEDS TO

2548: %BE CONSIDERED SEPARATELY, RIGHT?

2549: %joe5: yes, you're right.  Fixed.

2550: %\item $L_i \neg L_i \psi \dimp \neg L_i \psi$

2551: \item $(\neg L_i \false \land L_i \neg L_i \psi) \dimp \neg L_i \psi$

2552: \item $L_i N_i \psi \dimp N_i \psi$

2553: \item $L_i \neg N_i \psi \dimp \neg N_i \psi$.

2554: \end{itemize}

2555: The first five of these equivalences are standard $\Wax$ properties;

2556: the last two are instances of axiom {\bf A4$_n$}.  Similar arguments

2557: work in the case that $\phi$ is of the form

2558: $N_i \phi'$.  We leave the straightforward details to the reader. \eprf

2559: 

2560: %joe7: added

2561: The next two lemmas give us some basic facts about the satisfiability

2562: and validity of formulas in $\OLNm$.

2563: 

2564: \lem\label{construction1} If $S_j$ is a set of consistent $j$-sets,

2565: $j = 1, \ldots, n$, and

2566: $\sigma$ is a consistent propositional formula, then there is a

2567: $\Wax$ situation $(M,w)$ such that $(M,w) \sat \sigma$ and $\Objj(M,w) =

2568: S_j$. \elem

2569: 

2570: \prf This follows immediately

2571: from part (b) of Proposition~\ref{construction} below. \eprf

2572: 

2573: \lem\label{LN} If $\phi$ and $\psi$ are $i$-objective basic formulas

2574: such that

2575: $L_i \phi \land N_i \psi$ is consistent, then $\phi \lor \psi$ is valid.

2576: \elem

2577: 

2578: \prf Suppose that $\neg \phi \land \neg \psi$ is consistent.  Then,

2579: %joe5: I wonder how many times we've missed this ...

2580: %by Axiom {\bf A4$_n$},

2581: by Axiom {\bf A5$_n$},

2582: $ N_i (\phi \lor \psi) \rimp \neg L_i (\phi \lor

2583: \psi)$ is provable.  It follows that $N_i \psi \rimp \neg L_i \phi$ is

2584: provable, contradicting the consistency of $L_i \phi \land N_i \psi$.

2585: \eprf

2586: 

2587: %joe7

2588: The last lemma gives us a sharper condition on when $w' \notin

2589: \K_i^c(w)$.  This condition will prove useful in the completeness proof.

2590: 

2591: \lem\label{objOK} If $w, w'$ are worlds in the canonical model such

2592: that $w \approx_i w'$ and

2593: $w' \notin \K_i^c(w)$, then there is an $i$-objective

2594: basic formula $\phi$ such that $L_i \phi \in w$ and $\phi \notin w'$. \elem

2595: 

2596: \prf By the construction of the canonical model, we know that if

2597: $w' \notin \K_i^c(w)$, then there is some basic formula $\phi$

2598: such that $L_i \phi \in w$ and $\phi \notin w'$.  From

2599: Lemma~\ref{normalform},

2600: it follows that we can assume without loss of generality that

2601: $\phi$ is in the normal form described by that lemma.  Let $A$

2602: consist of all subformulas of $\phi$ that are of the form $L_i \psi$

2603: and do not appear in the scope of any other modal operator.

2604: Let $\phi_A$ be $\band_{\psi \in A \inter w} \psi \land \band_{\psi \in A

2605: - w} \neg \psi$.  It is easy to see that $\phi_A \in w$ (since each of

2606: its conjuncts is).  Since $w \approx_i w'$, it follows that

2607: $\phi_A \in w'$.  Let $\phi'$ be the result of replacing each

2608: subformula $L_i \psi$ of $\phi$ that is in $A$ by either $\true$ or

2609: $\false$, depending on whether $L_i \psi \in w$.  By construction,

2610: $\phi'$ is $i$-objective.

2611: It is easy to

2612: see that $\phi_A \rimp (\phi \dimp \phi')$ is provable.  It follows

2613: %joe5

2614: %that $\phi' \in w'$.  It also follows that $L_i \phi_A \rimp

2615: that $\phi' \notin w'$.  It also follows that $L_i \phi_A \rimp

2616: (L_i \phi \dimp L_i \phi')$ is provable.  Since $\phi_A$ is an

2617: $i$-subjective formula, $\phi_A \rimp L_i \phi_A$ is provable.  Hence,

2618: $L_i \phi_A \in w$.  Since $L_i\phi \in w$, it follows that $L_i \phi'

2619: \in w$.  This gives us the desired result.  \eprf

2620: 

2621: %joe5: I cut the following lemma (and all subsequent lemmas that

2622: %depend on their being an infinite number of primitive propositions.

2623: %I think the replacements are both simpler are bring out more clearly

2624: %what's going on.

2625: \commentout{

2626: \lem\label{needit} Suppose $\alpha = \phi \land N_1 \psi_1 \land \ldots

2627: \land N_n \psi_n$ is a consistent formula, where $\phi$ is a basic

2628: formula and $\psi_j$ is a $j$-objective basic formula.  Let

2629: $q_1, \ldots, q_n$ be

2630: primitive propositions that do not appear in $\alpha$.  Then there is a

2631: world $w^*$ in the canonical model such that  $(M^c,w^*) \sat \alpha

2632: \land L_1(\neg \psi_1

2633: \lor q_1) \land \ldots \land L_n(\neg \psi_n \lor q_n)$.  \elem

2634: 

2635: \prf By Lemma~\ref{normalform}, we can assume without loss of generality

2636: that $\phi$ is of the form

2637: $\sigma \land L_1 \phi_{10} \land \neg L_1 \phi_{11}

2638: \ldots \neg L_1 \phi_{1m_1} \land \ldots \land L_n \phi_{n0} \land

2639: \neg L_n \phi_{n1} \land \ldots \land \neg L_n \phi_{nm_n}$.

2640: We claim that if $m_i > 0$ (so that there are some conjuncts in $\phi$

2641: of the form $\neg L_i \phi_{ij}$),

2642: then

2643: $\phi_{i0} \land \neg \phi_{ij} \land (\neg \psi_i \lor q_i)$ is

2644: consistent, for each $j > 0$.

2645: For if not, we must have

2646: that $\vdash_{\sWax} (\phi_{i0} \land \neg \phi_{ij}) \rimp (\psi_i \land

2647: \neg q_i)$.

2648: But a proof of $(\phi_{i0} \land \neg \phi_{ij}) \rimp

2649: (\psi_i \land \neg q_i)$ can be converted to a proof of $(\phi_{i0}

2650: \land \neg \phi_{ij}) \rimp \false$

2651: by replacing all

2652: occurrences of $q_i$ by $\true$.  (Here we are using the fact that

2653: $q_i$ does not appear in $\alpha$.)  But it then follows that

2654: $\phi_{i0} \rimp \phi_{ij}$ is provable, as is $L_i\phi_{i0} \rimp

2655: L_i\phi_{ij}$, contradicting the consistency of $\alpha$.

2656: 

2657: Let $S_i$ consist of all $i$-sets containing $\phi_{i0} \land

2658: (\neg \psi_i

2659: \lor q_i)$.  By Lemma~\ref{construction1}, there is a $\Wax$ structure

2660: $(M,w)$ such that $\Obji(M,w) = S_i$, $i = 1, \ldots, n$, and $(M,w)

2661: \sat \sigma$.

2662: Thus, there must be a world $w^*$ in the canonical model such that

2663: $w^* = \{\mbox{basic } \phi' \;|\; (M,w) \sat \phi'\}$.  We claim that

2664: $(M^c,w^*) \sat \alpha \land L_1(\neg \psi_1 \lor q_1) \land \ldots \land

2665: L_n(\neg \psi_n \lor q_n)$.  To see this, first we show that

2666: $(M,w) \sat \phi \land L_1(\neg \psi_1 \lor q_1) \land \ldots \land

2667: L_n(\neg \psi_n \lor q_n)$.  By construction, $(M,w) \sat \sigma$.

2668: Furthermore,

2669: by definition, each world $w' \in \K_i^M(w)$ satisfies $\phi_{i0}

2670: \land (\neg \psi_i \lor q_i)$,

2671: so we have $(M,w) \sat L_i \phi_{i0} \land L_i(\neg \psi_i \lor q_i)$.

2672: As we have seen, for each conjunct $\neg L_i \phi_{ij}$

2673: in $\phi$, we have that $\neg \phi_{i0} \land \neg \phi_{ij} \land

2674: (\neg \psi_i \lor q_i)$ is consistent.  Hence, there is a set in

2675: $\Obji(M,w)$ containing $\neg \phi_{ij}$.  It follows that $(M,w) \sat

2676: \neg L_i \phi_{ij}$.  Thus, we have shown that $(M,w) \sat \phi \land

2677: L_1(\neg \psi_1 \lor q_1) \land \ldots \land L_n(\neg \psi_n

2678:  \lor q_n)$.  Since

2679: $(M,w)$ and $(M^c,w^*)$ agree on basic formulas, it follows that

2680: $(M^c,w^*) \sat \phi \land L_1(\neg \psi_1 \lor q_1) \land \ldots \land

2681: L_n(\neg \psi_n \lor q_n)$.

2682: 

2683: Thus, it remains to show that $(M^c,w^*) \sat

2684: N_1 \psi_1 \land \ldots \land N_n \psi_n$.  To this end, suppose that

2685: $w' \approx_i w^*$ and $w' \notin \K_i^c(w^*)$.  By Lemma~\ref{objOK},

2686: there must be

2687: some $i$-objective basic formula $\phi'$

2688: such that $L_i \phi' \in w^*$

2689: and $\neg \phi' \in w'$.  Since $L_i \phi' \in w^*$, it follows that

2690: $\vdash_{\sWax} \phi_{i0} \land (\neg \psi_i \lor q_i) \rimp

2691: \phi'$, for otherwise there would be a world in $S_i$ satisfying $\neg

2692: \phi'$, and it would not be the case that $(M^c,w^*) \sat L_i \phi'$.

2693: Since we can replace $q_i$ by $\true$ in the proof of $\phi_{i0} \land

2694: (\neg \psi_i \lor q_i) \rimp \phi'$, it follows that in fact

2695: $\vdash_{\sWax}

2696: \phi_{i0} \rimp \phi'$.  We claim that $\vdash_{\sWax} \neg \phi' \rimp

2697: \psi_i$.  For if not, $\neg \phi' \land \neg \psi_i$ is consistent, and

2698: hence

2699: so is $\neg \phi_{i0} \land \neg \psi_i$ (since $\vdash_{\sWax} \neg

2700: \phi_i \rimp \neg \phi_{i0}$).  But since $\alpha$ is consistent,

2701: so is $L_i \phi_{i0} \land N_i \psi_i$.  From Lemma~\ref{LN}, it follows

2702: that $\vdash_{\sWax} \phi_{i0} \lor \psi_i$.  This is a contradiction.

2703: Hence, we must have that $\vdash_{\sWax} \neg \phi' \rimp \psi_i$, as

2704: desired.  This means that $(M^c,w') \sat \psi_i$.  It follows that

2705: $(M^c,w^*) \sat N_i \psi_i$.  This completes the proof. \eprf}

2706: 

2707: %joe7:

2708: We are finally ready to prove the completeness result.

2709: 

2710: \thm %Completeness Result\\

2711: \label{completeness} {\rm \cite{Lakemeyer93}}

2712: For all $\alpha\in\onlnminus$, if $\mdcm\alpha$ then $\vdash\!\alpha$.

2713: \ethm

2714: \prf

2715: As usual, it suffices to show that if the formula $\alpha \in \onlnminus$

2716: is consistent, then it is satisfiable in the canonical model.

2717: %joe5: rewrote proof

2718: \commentout{

2719: Using

2720: Lemma~\ref{normalform}, it suffices to assume that $\alpha$ is of the

2721: form $\phi \land

2722: N_1 \psi_{10} \land \neg N_1 \psi_{11} \land \ldots

2723: \land \neg N_1 \psi_{1k_1} \land \ldots \land N_n \psi_{n0} \land

2724: \neg N_n \psi_{n1} \land \ldots \land \neg N_n \psi_{nk_n}$,

2725: where $\phi$ is a

2726: basic formula and $\psi_{ij}$ is $i$-objective.

2727: Let $\alpha'$ be

2728: $\phi \land N_1 \psi_{10} \land \ldots \land N_n \psi_{n0}$.

2729: By Lemma~\ref{needit}, there is world $w^*$ in the canonical

2730: model such that $(M^c,w^*) \sat \alpha' \land L_1(\neg \psi_{10} \lor

2731: q_1) \land \ldots \land L_n(\neg \psi_{n0} \lor q_n)$.  Thus,

2732: it suffices to show that $(M^c,w^*) \sat \neg N_i\psi_{ij}$ for each

2733: conjunct $\neg N_i \psi_{ij}$ in $\alpha$.

2734: 

2735: Consider any such conjunct.

2736: We must have that $\neg \psi_{ij} \land \psi_{i0}$ is

2737: consistent (for otherwise, using {\bf Nec$_n$}, $N_i \psi_{i0} \rimp N_i

2738: \psi_{ij}$ would be provable, so $\alpha$ would be inconsistent).

2739: Since $q_i$ does not appear in $\psi_{i0}$ or $\psi_{ij}$,

2740: it is easy to see that

2741: $\neg \psi_{ij} \land \psi_{i0}\land \neg q_i$ is consistent.  Let

2742: $\Sigma$ consist of all

2743: the $i$-subjective basic formulas that are true at $w^*$.  By

2744: Lemma~\ref{consistency},

2745: $\Sigma \union \{\neg \psi_{ij} \land \psi_{i0} \land \neg q_i\}$ is

2746: consistent. Thus, there

2747: is some world $w'$ such that $(M^c,w') \sat \Sigma \union \{\neg

2748: \psi_{ij} \land \psi_{i0} \land \neg q_i\}$.

2749: %joe5: changed w -> w* throughout rest of paragraph

2750: %Since $w$ and $w'$ agree on all $i$-subjective basic

2751: Since $w^*$ and $w'$ agree on all $i$-subjective basic

2752: formulas, we must have that $w^* \approx_i w'$.  Since $L_i (\neg

2753: \psi_{i0} \lor q_i)$

2754: %\in w$ and $psi_{i0} \land q_i \notin w'$, it cannot be the case

2755: $\in w^*$ and $\psi_{i0} \land \neg q_i \notin w'$, it cannot be the case

2756: that $w' \in \K_i^c(w^*)$.  Finally, by construction, $(M^c,w') \sat \neg

2757: \psi_{ij}$.  Thus, it follows that $(M^c,w^*) \sat \neg N_i \psi_{ij}$.

2758: This shows that $(M^c,w^*) \sat \alpha$, so $\alpha$ is satisfiable in the

2759: canonical model, as desired. \eprf}

2760: %joe5: new proof

2761: Without loss of generality, we can assume that $\alpha$ is in the normal

2762: form described in Lemma~\ref{normalform}:

2763: $$\begin{array}{l}

2764: \sigma \land L_1 \phi_{10} \land \neg L_1 \phi_{11}  \land

2765: \ldots \land \neg L_1 \phi_{1m_1} \land \ldots \land L_n \phi_{n0} \land

2766: \neg L_n \phi_{n1} \land \ldots \land \neg L_n \phi_{nm_n} \land\\

2767: N_1 \psi_{10} \land \neg N_1 \psi_{11} \land \ldots

2768: \land \neg N_1 \psi_{1k_1} \land \ldots \land N_n \psi_{n0} \land

2769: \neg N_n \psi_{n1} \land \ldots \land \neg N_n \psi_{nk_n}.\end{array}$$

2770: Moreover, since $\alpha \in

2771: \onlnminus$, we can assume that $\phi_{ij}$ and $\psi_{ij}$ are

2772: $i$-objective basic formulas.  Let $A_i$ consist of all the consistent

2773: formulas of the form $\phi_{i0} \land \psi_{i0} \land \neg \phi_{ij}$

2774: or $\phi_{i0} \land \psi_{i0} \land \neg \psi_{ij}$, $j \ge 1$.

2775: Let $\xi_i$ be a formula that is independent of all the formulas in

2776: $A_i$; such a formula exists by Lemma~\ref{indep}.  Let $S_i$ consist of

2777: all $i$-sets containing $\phi_{i0} \land (\neg \psi_{i0} \lor

2778: (\psi_{i0} \land \xi_i))$.

2779: By Lemma~\ref{construction1}, there is a $\Wax$ structure

2780: $(M,w)$ such that $\Obji(M,w) = S_i$, $i = 1, \ldots, n$, and $(M,w)

2781: \sat \sigma$.

2782: Thus, there must be a world $w^*$ in the canonical model such that

2783: $w^* = \{\mbox{basic } \phi' \;|\; (M,w) \sat \phi'\}$.  We claim that

2784: $(M^c,w^*) \sat \alpha$.

2785: 

2786: To see this, let $\alpha'$ be the formula

2787: $\sigma \land L_1 \phi_{10} \land \neg L_1 \phi_{11}  \land

2788: \ldots \land \neg L_1 \phi_{1m_1} \land \ldots \land L_n \phi_{n0} \land

2789: \neg L_n \phi_{n1} \land \ldots \land \neg L_n \phi_{nm_n}$.  We first

2790: show that

2791: $(M,w) \sat \alpha'$.

2792: By construction, we have that $(M,w) \sat \sigma$.

2793: Furthermore,

2794: by definition, each world $w' \in \K_i^M(w)$ satisfies $\phi_{i0}$,

2795: so we have that $(M,w) \sat L_i \phi_{i0}$.

2796: Since $L_i \phi_{i0} \land \neg L_i \phi_{ij}$ is consistent for each $j

2797: \ge 1$, it must be the case that $\phi_{i0} \land \neg \phi_{ij}$ is

2798: consistent.  Thus, one of $\phi_{i0} \land \neg \psi_{i0} \land \neg

2799: \phi_{ij}$ or $\phi_{i0} \land \psi_{i0} \land \neg \phi_{ij}$ is

2800: consistent.  If the latter is consistent, then by the choice of $\xi$,

2801: $\phi_{i0} \land \psi_{i0} \land \xi_i \land \neg \phi_{ij}$ must be

2802: consistent as well.  Since $S_i$ consists of all $i$-sets containing

2803: $\phi_{i0} \land (\neg \psi_{i0} \lor

2804: (\psi_{i0} \land \xi_i))$,

2805: it follows that there must be an

2806: $i$-set in $S_i$ containing $\neg \phi_{ij}$.

2807: It follows that $(M,w) \sat \neg L_i \phi_{ij}$, for $j \ge 1$.

2808: Thus, we have shown that $(M,w) \sat \alpha'$.

2809: Since

2810: $(M,w)$ and $(M^c,w^*)$ agree on basic formulas, it follows that

2811: $(M^c,w^*) \sat \alpha'$.

2812: 

2813: Next, we show that $(M^c,w^*) \sat

2814: N_1 \psi_{10} \land \ldots \land N_n \psi_{n0}$.  To this end, suppose

2815: that

2816: $w' \approx_i w^*$ and $w' \notin \K_i^c(w^*)$.  By Lemma~\ref{objOK},

2817: there must be

2818: some $i$-objective basic formula $\phi'$

2819: such that $L_i \phi' \in w^*$

2820: and $\neg \phi' \in w'$.  Since $L_i \phi' \in w^*$, it follows that

2821: $(M,w) \sat L_i \phi'$, and hence $\phi'$ is in every $i$-set in $S_i$.

2822: It follows that $\obji(w') \notin S_i$.  Now, one of the following

2823: four formulas must be in $\obji(w')$: (1) $\phi_{i0} \land \psi_{i0}$,

2824: (2) $\phi_{i0} \land \neg \psi_{i0}$,

2825: (3) $\neg \phi_{i0} \land \psi_{i0}$, (4)  $\neg \phi_{i0} \land

2826: \neg \psi_{i0}$.  Since $L_i \phi_{i0} \land N_i \psi_{i0}$ is

2827: consistent, it cannot be (4), by Lemma~\ref{LN}.  It cannot be (2), for

2828: otherwise $w'$ would be in $S_i$.  Thus, it must be (1) or (3), so

2829: $\psi_{i0} \in \obji(w')$.  Since this is true for all $w'$ such

2830: that $w' \approx_i w^*$ and $w' \notin \K_i^c(w^*)$, it

2831: follows that $(M^c,w^*) \sat N_i \psi_{i0}$, for $i = 1, \ldots, n$.

2832: 

2833: Finally, we must show that $(M^*,w^*) \sat \neg N_1 \psi_{ij}$, for $i =

2834: 1, \ldots, n$ and $j = 1, \ldots, k_i$.  Clearly $\psi_{i0} \land \neg

2835: \psi_{ij}$ is consistent, for otherwise $N_i \psi_{i0} \land \neg N_i

2836: \psi_{ij}$ would be inconsistent.  Thus, at least one of

2837: (1) $\psi_{i0} \land \neg \psi_{ij} \land \neg \phi_{i0}$

2838: or (2) $\psi_{i0} \land \neg \psi_{ij} \land \phi_{i0}$ is consistent.

2839: In case (2), by choice of $\xi_i$, the formula $\psi_{i0} \land \neg

2840: \psi_{ij} \land \phi_{i0} \land \neg \xi_i$ is consistent.  Let $\beta$

2841: be $\psi_{i0} \land \neg \psi_{ij} \land \neg \phi_{i0}$ if it is

2842: consistent, and $\psi_{i0} \land \neg

2843: \psi_{ij} \land \phi_{i0} \land \neg \xi_i$ otherwise.  By construction,

2844: $\beta$ is consistent.

2845:  By Lemma~\ref{consistency}, there is a situation

2846: $(M',v)$ such that $\subji(M',v) = \subji(M^*,w^*)$ and $(M',v)

2847: \sat \beta$.  There is a world $w''$ in the canonical model which

2848: agrees with $(M',v)$ on the basic formulas.  By construction, we have

2849: $w'' \approx_i w^*$.  Moreover, since $(M^c,w) \sat L_i(\phi_{i0} \land

2850: (\neg \psi_{i0} \lor (\psi_{i0} \land \xi)))$, it follows that

2851: $(M^c,w^*)

2852: \sat L_i \neg \beta$.  Since $(M^c,w') \sat \beta$, we have that

2853: $w' \notin \K_i^c(w^*)$.  Moreover, since $(M^c,w') \sat \neg

2854: \psi_{ij}$, it follows that $(M^c,w^*) \sat \neg N_i \psi_{ij}$, as

2855: desired.  This completes the proof. \eprf

2856: 

2857: 

2858: %joe1: added

2859: %gerhard4: deleted since completeness proof added for overlapping semantics

2860: %We remark that, when specialized to the single-agent case, the proof

2861: %technique gives a simpler proof of the completeness of Levesque's

2862: %axioms than that given in \cite{Lev5}.

2863: 

2864: 

2865: %joe1: cut; said it above

2866: %\begin{theorem} Incompleteness Result\\

2867: %\label{incompleteness}

2868: %There is some $\alpha\in\onl$ such that $\md\alpha$ yet

2869: %$\not\vdash\!\alpha$. \end{theorem}

2870: %The proof of this theorem is deferred to Section~\label{new-semantics}.

2871: %joe1: material that was here on the limit closure has been moved back

2872: 

2873: %gerhard4: Cut since now redundant

2874: %\thm %Completeness Result\\

2875: %\label{completeness} {\rm \cite{Lakemeyer93}}

2876: %For all $\alpha\in\onlnminus$,

2877: %joe3:

2878: %if $\mdcm\alpha$ then $\vdash\!\alpha$.

2879: %$\mdcm\alpha$ iff $\vdash\!\alpha$.

2880: %\ethm

2881: 

2882: %------------------------------------------------------------------------------

2883: %joe2: cut for abstract; some of this moved to the b

2884: %section

2885: 

2886: \subsection{Discussion}

2887: %------------------------------------------------------------------------------

2888: %joe1: lots of rewriting and additions from here on in.  Very little is

2889: %marked.

2890: As we have shown,

2891: the canonical-model semantics for $N_i$ has some attractive features,

2892: in particular when restricted to the language $\onlnminus$.  It is for

2893: this sublanguage that we have

2894: a nice proof-theoretic characterization.

2895: %gerhard5: cut since all this moved to the end

2896: %; moreover, the connections between

2897: %only knowing and the

2898: %multi-agent generalization for Moore's notion of a stable expansion were

2899: %all made in $\onlnminus$ (since we considered only formulas of the form

2900: %$O_i \alpha$ where $\alpha$ is basic).

2901: %

2902: There is some evidence, however,

2903: that

2904: the semantics may not have the behavior we desire when we move beyond

2905: $\onlnminus$.  For one thing,

2906: the formula $\neg O_i \neg O_j p$ is valid in the canonical model:~it

2907: is impossible that all $i$ knows is that it is not the case that all $j$

2908: knows is $p$.  While it is certainly consistent for $\neg O_i \neg O_j

2909: p$ to hold, it seems reasonable to have a semantics that allows $O_i

2910: \neg O_j p$

2911: to be hold as well.  As we have seen, the validity of $\neg O_i \neg O_j

2912: %gerhard6: rephrased

2913: %p$ is intimately connected with the fact that the canonical-model

2914: p$ follows from the fact that the canonical-model

2915: semantics does not have the third property of Levesque's semantics in

2916: the single-agent case: not all subsets of conceivable states are

2917: possible.  In the next section, we discuss a different

2918: approach to giving

2919: semantics to only knowing---essentially that taken in \cite{Hal11}---%

2920: that has all three of Levesque's properties,

2921: %gerhard6: added

2922: at least as long as we continue to represent an agent's objective

2923: state of affairs using basic formulas only.

2924: The approach agrees with the canonical-model approach on formulas in $\onlnminus$,

2925: but makes $O_i \neg O_j p$ satisfiable.  Unfortunately, as we shall

2926: see, it too suffers from problems.

2927: 

2928: %joe1: changed it from "tree approach" to $i$-set approach, since I

2929: %don't want the overhead of describing trees.

2930: %------------------------------------------------------------------------------

2931: \section{The $i$-Set Approach}\label{tree-approach}

2932: %------------------------------------------------------------------------------

2933: %joe5: cut; more or less said this in the previous paragraph

2934: %As we have seen, the canonical-model semantics has some attractive

2935: %features, particularly when restricted to the language $\onlnminus$.

2936: %On the other hand, it has what may be considered undesirable

2937: %features, such as making $\neg O_i \neg O_j p$ valid.

2938: %In this section, we consider a second approach to giving semantics

2939: %to $N_i$, developed in \cite{Hal11}.  As we shall see, it too has its

2940: %good points and bad points.

2941: 

2942: In the $i$-set approach, we maintain the intuition that

2943: the set of conceivable states for each agent $i$ can be

2944: identified with  the set of $i$-sets.  We no longer restrict attention

2945: to the canonical model though; we consider all Kripke structures.

2946: 

2947: %Given a situation $(M,w)$, define $\Obji(M,w) = \{\obji(M,w') \;|\; w'

2948: %\in \K_i^M(w)\}$.  Thus, $\Obji(M,w)$ is the set of $i$-sets that agent

2949: %$i$ considers possible in situation $(M,w)$.

2950: We define a new semantics

2951: $\sat'$ as follows:  all the clauses of $\sat'$ are identical to the

2952: corresponding clauses for $\sat$, except that for $N_i$.  In this case,

2953: we have

2954: $$\begin{array}{l}

2955: %joe2: typos

2956: %(M,w) \sat N_i \phi \mbox{ iff } (M',w') \sat \phi \mbox{ for all

2957: (M,w) \sat' N_i \phi \mbox{ iff } (M',w') \sat' \phi \mbox{ for all

2958: situations $(M',w')$ such that}\\

2959: \ \ \ \ \mbox{$\Obji(M,w) = \Obji(M',w')$ and

2960: $\obji(M',w') \notin \Obji(M,w)$.}\end{array}$$

2961: Notice that $\sat$ and $\sat'$ agree for basic formulas; in general, as

2962: we shall see, they differ.  We remark that this definition is equivalent

2963: to the one given

2964: in \cite{Hal11}, except that there, rather than $i$-sets, {\em

2965: $i$-objective

2966: trees\/} were considered.  We did not want to go through the overhead

2967: of introducing $i$-objective trees here, since it follows from results

2968: in \cite{Hal11,Hal13}

2969: that $i$-sets are equivalent to $i$-objective trees: every $i$-set

2970: uniquely determines an $i$-objective tree and vice versa.

2971: %joe5: cut; redundant

2972: %Thus, the two definitions are essentially equivalent.

2973: 

2974: %joe7: added paragraph

2975: How well does this approach fare in terms of computing the truth of a

2976: formula at a given world.  Since we now allow arbitrary

2977: structures,

2978: not just the canonical model, it seems that for computational reasons,

2979: it seems we ought to focus on finite structures.  However, when it comes

2980: to formulas of the form $N_i \alpha$, where $\alpha$ is $i$-objective,

2981: satisfiable formula, it can be shown that $(M,w) \sat' \neg N_i \alpha$.

2982: There are simply too few sets in $\Obji(M,w)$ if $M$ is finite to

2983: have $\neg \alpha$ hold in all ``impossible'' situations.  This means

2984: that to really model interesting situations with only knowing, we must

2985: use infinite models, and we are back to the problems discussed in the

2986: case of the canonical model.  Thus, again we focus on whether this

2987: approach gives reasonable semantics to the $N_i$ operator.

2988: 

2989: 

2990: Notice that to decide if $N_i

2991: \phi$ holds in $(M,w)$, we consider all

2992: situations that agree with $(M,w)$ on the set of possible states, hence

2993: this semantics satisfies the first of the three properties we

2994: isolated

2995: in the single-agent case.  It is also clear that the $i$-sets considered

2996: in evaluating the truth of $N_i \phi$ are precisely those not considered

2997: in evaluating the truth of $L_i \phi$; hence we satisfy the second

2998: property.  Finally, as we now show, for every set $S$ of $i$-sets,

2999: there is a situation $(M,w)$ such that $\Obji(M,w) = S$.

3000: %joe2

3001: %

3002: In fact,

3003: we prove an even stronger result.

3004: %gerhard6: made this into a dfn for better visibility

3005: \dfn

3006: Let \newl{$\objsi(M,w)$} consist of all $i$-objective formulas (not necessarily

3007: just $i$-objective basic formulas) true at $(M,w)$ (with respect to

3008: $\sat'$) and let \newl{$\Objsi(M,w)$} =

3009: $\{\objsi(M,w') \;|\; w' \in \K_i^M(w)\}$.

3010: \edfn

3011: 

3012: \pro\label{construction}

3013: Let $\Gamma$ be a satisfiable set of $i$-objective formulas, let $S_i$

3014: be a set of maximal satisfiable sets of $i$-objective

3015: formulas, $i = 1, \ldots, n$, let $\Sigma$ be a satisfiable set of

3016: %gerhard6: added ``satisfiable''

3017: $i$-subjective formulas, and let $\sigma$ be a satisfiable propositional formula.

3018: Then

3019: \begin{enumerate}

3020: \item[(a)] there exists a situation $(M_1,w_1)$ such that $\Gamma

3021: \subseteq \objsi(M_1,w_1)$ and $S_i = \Objsi(M_1,w_1)$.

3022: \item[(b)] there exists a situation $(M_2,w_2)$ such that $(M_2,w_2)

3023: \sat \sigma$ and $\Objsj(M_2,w_2) = S_j$, $j = 1, \ldots, n$.

3024: \item[(c)] there exists a situation $(M_3,w_3)$ such that $(M_3,w_3)

3025: \sat \Gamma \land \Sigma$.

3026: \end{enumerate}

3027: \epro

3028: 

3029: \prf For part (a), we first show that, given an arbitrary situation

3030: $(M,w)$, we can construct a situation $(M^*,w^*)$ such that

3031: $\objsi(M^*,w^*) = \objsi(M,w)$ and there are no worlds $i$-accessible

3032: from $w^*$.  The idea is to have $M^*$ be the result of adding $w^*$

3033: to the worlds in $M$, where $w^*$ is just like $w$

3034: except that it has no $i$-accessible worlds and $w^*$ is not accessible

3035: from any world.

3036: More formally, if $M = (W,\pi,\K_1, \ldots,\K_n)$, we take $M^* =

3037: (W^*,\pi^*,\K_1^*,\ldots, \K_n^*)$, where $W^* = W \union \{w^*\}$,

3038: $\pi^*(w')

3039: = \pi(w')$ for $w' \in W$, $\pi^*(w^*) = \pi(w)$, $\K_j^* = \K_j \union

3040: \{(w^*,w') \;|\; w' \in \K_j(w)\}$ for $j \ne i$,

3041: and $\K_i^* = \K_i$.  It is easy to see that $\K_j^*$ is Euclidean and

3042: transitive.  By construction, there are no worlds $i$-accessible from

3043: $w^*$ and $(w',w^*) \notin \K_j^*$ for all $w'$ and all $j$.

3044: Moreover, if $\psi$ is an $i$-objective formula,

3045: we have $(M^*,w^*) \sat' \psi$ iff $(M,w) \sat' \psi$, since for $j \ne

3046: i$, we have $\K_j(w^*) = \K_j(w)$.  In particular, this means that

3047: $\objsi(M^*,w^*) = \objsi(M,w)$.

3048: 

3049: For each $\Delta \in S' =

3050: S_i \union \{\Gamma\}$, there is a situation

3051: $(M^\Delta,w^\Delta) \sat' \Delta$, where $M^\Delta = (W^\Delta,

3052: \pi^\Delta, \K_1^\Delta, \ldots, \K_n^\Delta)$. By the argument above, we

3053: can assume without loss of generality that there are no worlds

3054: $i$-accessible from $w^\Delta$ and $w^\Delta$ is not accessible from

3055: any world.

3056: We define $M_1 = (W,\pi,\K_1, \ldots,

3057: \K_n)$ by taking $W$ to be the union of all the worlds in $W^\Delta$,

3058: $\Delta \in S'$.  (We can assume without

3059: loss of generality that these are disjoint sets of worlds.)

3060: We define $\pi$ so that $\pi|_{W^\Delta} = \pi^\Delta$.  We define

3061: $\K_j = \union_{\Delta \in S'} \K_j^\Delta$ for $j \ne i$, and

3062: $\K_i$ to be the least transitive, Euclidean set containing

3063: $\union_{\Delta \in S'} \K_i^\Delta \union \{(w^\Gamma,

3064: w^\Delta) \;|\; \Delta \in S\}$.  It is easy to check that

3065: $\objsi(M_1,w^\Delta) = \objsi(M^\Delta,w^\Delta)$ (although this

3066: depends on the fact that $w_\Delta$ is not $j$-accessible

3067: from any world for $j \ne i$).  Thus, $\Objsi(M_1,w^\Gamma) = S_i$

3068: and $\objsi(M_1,w^\Gamma) \supseteq \Gamma$.  Thus, we can take

3069: $w_1 = w^\Gamma$, completing the proof of part (a).

3070: 

3071: To summarize the construction of part (a), we start with an arbitrary

3072: situation $(M,w)$ satisfying $\Gamma$, convert it to a

3073: situation satisfying $L_i \false \land \Gamma$, essentially by

3074: modifying the $i$-accessibility relation at $w$ so that there are no

3075: worlds $i$-accessible from $w$ and $w$ is not accessible from any world,

3076: and then again modifying the

3077: $i$-accessibility relation at $w$ so that we get a structure $(M_1,w_1)$

3078: such that $\Objsi(M_i,w_i) = S_i$.  Note that in doing this

3079: construction, we did not change the propositional formulas true at $w$,

3080: nor did we change the worlds that were $j$-accessible from $w$ for

3081: $j \ne i$.  Thus, starting with a situation that satisfies a

3082: propositional formula $\sigma$, we can repeat this construction for each

3083: $i$ in turn, for $i = 1, \ldots, n$.  The resulting situation is

3084: $(M_2,w_2)$, and it clearly has the desired properties.

3085: %joe7: added for Referee 2's benefit

3086: This proves part (b).

3087: 

3088: For part (c), suppose $(M',w') \sat \Sigma$; let $\Objsi(M',w') =

3089: S_i$.  By part (a), there is a situation $(M_3,w_3)$ such that

3090: $\Objsi(M_3,w_3) = S_i$ and $(M_3,w_3) \sat \Gamma$.  Since the

3091: set of subjective formulas true at a situation $(M,w)$ is completely

3092: determined by $\Objsi(M,w)$, and $\Objsi(M',w') = \Objsi(M_3,w_3)$,

3093: it follows that $(M_3,w_3) \sat \Sigma$ as well.  \eprf

3094: 

3095: %joe2: added to replace deleted

3096: %joe5: cut; follows from previous result

3097: %\pro For each set $S$ of $i$-sets, there is a situation $(M,w)$

3098: %such that $\Obji(M,w) = S$. \epro

3099: 

3100: How does this semantics compare to the canonical model semantics?

3101: First of all, it is easy to see that the axioms are sound.

3102: We write $\sat' \phi$ if $(M,w) \sat' \phi$ for every situation $(M,w)$.

3103: Then we have the following result.

3104: \thm {\rm \cite{Hal11}}

3105: For all $\alpha \in \onln$, if $\vdash \alpha$ then $\sat' \alpha$.

3106: \ethm

3107: 

3108: 

3109: \prf As usual, the proof is by induction on the length of a

3110: derivation.  All that needs to be done is to show that all the axioms

3111: are sound.  Again, this is straightforward.  The proof in the case of

3112: {\bf A5$_n$} proceeds just as that in the proof of

3113: Theorem~\ref{soundness}, using the fact that this semantics satisfies

3114: Levesque's second property. \eprf

3115: 

3116: Moreover, we again get completeness for the sublanguage $\onlnminus$.

3117: 

3118: 

3119: \thm {\rm \cite{Hal11}}

3120: For all $\alpha \in \onlnminus$,

3121: %joe3:

3122: %if $\vdash \alpha$ then $\sat'

3123: $\vdash \alpha$ iff $\sat'

3124: \alpha$. \ethm

3125: 

3126: 

3127: \prf As usual, it suffices to show that if $\alpha$ is consistent

3128: with the axioms, then $\alpha$ is satisfiable under the $\sat'$

3129: semantics.  From Theorem~\ref{completeness}, we know that

3130: $\alpha$ is satisfiable in the canonical model under the $\sat$

3131: semantics.   Thus, it suffices to show that for all formulas $\alpha

3132: \in \onlnminus$, we have $(M^c,w) \sat \alpha$ iff $(M^c,w) \sat'

3133: \alpha$.

3134: %Observe that this result is trivially true if $\alpha$ is a

3135: %basic formula, since $\sat$ and $\sat'$ agree on basic formulas.

3136: By Lemma~\ref{normalform}, it suffices to consider formulas

3137: $\alpha$ in normal form.  We proceed by induction on the structure of

3138: formulas.  The only nontrivial case obtains if $\alpha$ is of the form $N_i

3139: \alpha'$.  Since $\alpha$ is in normal form, we can assume that

3140: $\alpha'$ is basic.  Suppose $(M^c,w) \sat' N_i \alpha'$.  To show that

3141: $(M^c,w) \sat N_i \alpha'$, we must show that if $w' \approx_i w$ and

3142: $w' \notin \K_i^c(w)$, then $(M^c,w') \sat \alpha$.  By definition,

3143: if $w'

3144: \approx_i w$, then $\Obji(M^c,w') = \Obji(M^c,w)$.  Moreover, we must

3145: have $\obji(M^c,w') \notin \Obji(M^c,w)$, for otherwise we would have

3146: $w' \in \K_i^c(w)$.  Hence, we must have $(M^c,w') \sat' \alpha'$.  By

3147: the induction hypothesis, we have $(M^c,w') \sat \alpha'$.  Thus,

3148: $(M^c,w) \sat N_i \alpha'$, as desired.

3149: 

3150: For the converse, suppose that

3151: $(M^c,w) \sat N_i \alpha'$.  We want to show that $(M^c,w) \sat' N_i

3152: \alpha'$.  Suppose that $(M',w')$ is such that $\Obji(M',w') =

3153: \Obji(M^c,w)$ and $\obji(M',w') \notin \Obji(M^c,w)$.

3154: %joe5: added

3155: We must show that $(M',w') \sat' \alpha$.

3156: It is easy to

3157: see that for every

3158: situation $(M,w)$ and basic formula $\phi$, we have that $(M,w) \sat L_i

3159: \phi$ iff $(M,w) \sat' L_i \phi$ iff $\phi$ is in every set in

3160: $\Obji(M,w)$.  Thus, it follows that $\subji(M',w') = \subji(M^c,w)$.

3161: There must be a world $w''$ in $M^c$ such that $(M^c,w'')$ agrees

3162: with $(M',w')$ on all basic formulas according to the $\sat$ semantics.

3163: Since $\subji(M^c,w'') = \subji(M^c,w)$, it follows from

3164: Lemma~\ref{$i$-equivalence-same-as-same-basic-beliefs} that $w \approx_i

3165: w''$.  Since $\obji(M',w') \notin \Obji(M^c,w)$ and $\obji(M',w') =

3166: \obji(M^c,w'')$, it follows that $w'' \notin \K_i^c(w)$.  Since $(M^c,w)

3167: \sat N_i \alpha'$, we must have that $(M^c,w'') \sat \alpha'$.  And

3168: since $(M^c,w'')$ and $(M',w')$ agree on basic formulas, it follows that

3169: $(M',w') \sat \alpha'$.  Finally, since $\sat$ and $\sat'$ agree for

3170: basic formulas, we have $(M',w') \sat' \alpha'$.

3171: This completes the proof that $(M,w) \sat N_i \alpha'$. \eprf

3172: 

3173: %joe5: cut this here; it seems funny to reference something that's

3174: %going to be discussed in Section 6.2; this material used to appear

3175: %earlier.

3176: %This result shows that $\sat'$ shares many of the nice features of

3177: %$\sat$.

3178: %In particular, since they agree on $\onlnminus$, it follows

3179: %that

3180: %the connection between only knowing and stable expansions established

3181: %in Section~\ref{stable-sets} holds with respect to $\sat'$ as well

3182: %Unfortunately, our axiomatization

3183: Although our axiomatization is complete for $\onlnminus$, as we now

3184: show, it is not complete for the full language,

3185: for neither $\sat$ nor $\sat'$.

3186: %joe2: added for abstract

3187: Since the axiomatization is sound for both $\sat$ and $\sat'$, to prove

3188: incompleteness, it suffices to provide a formula which is satisfiable

3189: with respect to $\sat'$ and not $\sat$, and another formula

3190: which is satisfiable  with respect to $\sat$ and not $\sat'$.

3191: %joe5: we're about to show it

3192: %As is shown in \cite{Hal11}, $\neg O_i \neg O_j p$ is satisfiable

3193: As is shown in Proposition~\ref{incomplete1},

3194: $O_i \neg O_j p$ is satisfiable

3195: with respect to $\sat'$ and (by Proposition~\ref{not-O-$i$-not-O-j-p})

3196: not with respect to $\sat$.  On the other hand, it is easy to see

3197: that $L_j \false \land N_j \neg O_i \neg O_j p$ is satisfiable

3198: with respect to $\sat$ (in fact, it is equivalent to $L_j \false$);

3199: %joe5:

3200: %as we show in the full paper,

3201: as shown in Proposition~\ref{incomplete2},

3202: it is not satisfiable with respect

3203: to $\sat'$.

3204: %joe2:

3205: 

3206: %joe5: cut; redundant

3207: %We show this with two preliminary

3208: %results.  The first shows that $O_i \neg O_j p$ is satisfiable under the

3209: %$\sat'$ semantics, even if it is not satisfiable under the $\sat$

3210: %semantics.  The second provides a formula which is satisfiable under the

3211: %$\sat$ semantics but not the $\sat'$ semantics.

3212: 

3213: \pro\label{incomplete1} $O_i \neg O_j p$ is

3214: satisfiable under the $\sat'$ semantics. \epro

3215: 

3216: \prf

3217: Let $S = \{\objsi(M,w) \;|\; (M,w) \sat' \neg O_j p\}$.

3218: By Proposition~\ref{construction}, there is a situation

3219: $(M^*,w^*)$ such that $\Objsi(M^*,w^*) = S$.

3220: We claim that $(M^*,w^*) \sat' O_i \neg O_j p$.  Clearly

3221: $(M^*,w^*) \sat' L_i \neg O_j p$, since $\neg O_j p$ is true at all

3222: worlds $i$-accessible from $w^*$.  To see that $(M^*,w^*) \sat' N_i O_j

3223: p$, suppose that $\Obji(M,w) = \Obji(M^*,w^*)$ and $\obji(M,w)

3224: \notin \Obji(M^*,w^*)$.  We want to show that $(M,w) \sat' O_j p$.

3225: Suppose that $(M,w) \sat' \neg O_j p$.

3226: By definition, $\objsi(M,w) \in S$, so there is some world

3227: $w' \in \K_i^{M^*}(w^*)$ such that $\objsi(M^*,w') =

3228: \objsi(M,w)$.  In particular, this means that $\obji(M^*,w') =

3229: \obji(M,w)$.  But this contradicts the assumption that

3230: $\obji(M,w) \notin \Obji(M^*,w^*)$.  Thus, $(M,w) \sat O_j p$ as

3231: desired, and $(M^*,w^*) \sat O_i \neg O_j p$. \eprf

3232: 

3233: 

3234: \pro\label{incomplete2}  There is a formula $\beta$ such that $\sat'

3235: \beta$ but $\neg \beta$ is satisfiable under the $\sat$ semantics.

3236: \epro

3237: 

3238: \prf

3239: We first show that if $\phi$ is an $i$-objective

3240: formula that is satisfiable under the $\sat'$ semantics, then $\sat' L_i

3241: \false \rimp \neg N_i \neg \phi$.  For suppose that $\phi$ is

3242: satisfiable in a situation $(M,w)$.  By Proposition~\ref{construction},

3243: there is a situation $(M^*,w^*)$ such that $\objsi(M^*,w^*) =

3244: \objsi(M,w)$ and $\Objsi(M^*,w^*) = \emptyset$.  This means that

3245: $(M^*,w^*) \sat' \phi \land L_i \false$.

3246: Now let $(M',w')$ be any situation

3247: satisfying $L_i \false$.  Then $\Obji(M',w') = \Obji(M^*,w^*) =

3248: \emptyset$, and $\obji(M^*,w^*) \notin \Obji(M',w')$.  It follows that

3249: $(M',w') \sat' \neg N_i \neg \phi$.  Thus, we have shown that

3250: %joe5: want to be careful about \sat vs. \sat'

3251: %$L_i \false \rimp \neg N_i \neg \phi$ is valid.

3252: $\sat' L_i \false \rimp \neg N_i \neg \phi$.

3253: Since, as we showed

3254: in Proposition~\ref{incomplete1}, the formula $O_j \neg O_i p$ is

3255: satisfiable, this means that

3256: %joe5:

3257: %$L_i \false \rimp \neg N_i \neg O_j \neg

3258: %O_i p$ is valid with respect to $\sat'$.

3259: $\sat' L_i \false \rimp \neg N_i \neg O_j \neg O_i p$.

3260: On the other hand, since

3261: $O_j \neg O_i p$ is not satisfiable with respect to $\sat$, as we showed

3262: in Proposition~\ref{not-O-$i$-not-O-j-p},

3263: neither is $\neg N_i \neg O_j \neg O_i p$, and hence $L_i \false \rimp

3264: \neg N_i \neg O_j \neg O_i p$ is not valid under the $\sat$ semantics.

3265: Indeed, $L_i \false \land N_i \neg O_j \neg O_i p$ is equivalent to $L_i

3266: \false$

3267: %joe5: added

3268: under the $\sat$ semantics.

3269: \eprf

3270: 

3271: 

3272: We can now show that our axiom system is incomplete for the full

3273: language with respect to both the $\sat$ and $\sat'$ semantics.

3274: 

3275: \thm\label{incompleteness} There exist formulas $\alpha$ and $\beta$

3276: in $\onln$ such that $\not\vdash \alpha$ and $\sat \alpha$,

3277: and $\not\vdash \beta$ and $\sat' \beta$.

3278: \ethm

3279: %joe2:

3280: 

3281: 

3282: 

3283: \prf By Propositions~\ref{not-O-$i$-not-O-j-p}

3284: and~\ref{incomplete1}, we have that $\sat \neg O_j

3285: \neg O_i p$, but

3286: $\not \sat' \neg O_j \neg O_i p$.  Since $\vdash$ is sound with respect

3287: to $\sat'$, we cannot have $\vdash \neg O_j \neg O_i p$ (for otherwise

3288: we would have $\sat' \neg O_j \neg O_i p$).  Thus, we can take $\alpha$

3289: to be $\neg O_j \neg O_i p$.  A similar argument shows we can take

3290: $\beta$ to be $L_i \false \rimp \neg N_i \neg O_j O_i p$.

3291: \eprf

3292: 

3293: 

3294: The fact that neither $\sat$ nor $\sat'$ is complete with respect to the

3295: axiomatization described

3296: %joe2

3297: %in Section~\ref{prooftheory}

3298: earlier

3299: is not necessarily

3300: bad.  We may be able to find a natural complete axiomatization.

3301: However, as we suggested above, the fact that $\neg O_j \neg O_i p$ is

3302: valid under the $\sat$ semantics suggests that this semantics does not

3303: quite satisfy our intuitions with regards to only-knowing for formulas

3304: in $\onln - \onlnminus$.  As we now show,

3305: %joe4:

3306: %the

3307: $\sat'$ also has its

3308: problems.

3309: We might hope that if $\phi$ is a satisfiable $i$-objective

3310: formula, then $N_i \phi \rimp \neg L_i \phi$ would be valid under the

3311: $\sat'$ semantics.  Unfortunately, it is not.

3312: %joe7: called this a proposition

3313: %\lem\label{problems} The formula

3314: \pro\label{problems} The formula

3315: $N_i \neg O_j p \land L_i \neg O_j p$ is satisfiable under the

3316: $\sat'$ semantics.  \epro

3317: 

3318: \prf

3319: First we show that for any situation $(M,w)$

3320: that satisfies $O_j p$,  there exists another situation

3321: $(M',w')$ such that $(M,w)$ and $(M',w')$ agree on all basic

3322: formulas, but $(M',w') \sat' \neg O_j

3323: p$.  We can construct $(M',w')$ as follows: Choose a particular

3324: set $\Gamma \in \Objj(M,w)$.  It easily follows from

3325: Proposition~\ref{construction} that there is a situation $(M',w')$

3326: such that $\Objj(M',w') = \Objj(M,w) - \{\Gamma\}$ and

3327: $\objj(M',w') = \objj(M,w)$.

3328: We now show that for any

3329: basic formula $\phi$, we have $(M,w) \sat' \phi$ iff $(M',w') \sat'

3330: \phi$.  If $\phi$ is a $j$-objective formula, this is immediate from

3331: the construction.  Thus, it suffices to deal with the case that

3332: $\phi$ is of the form $L_j \phi'$.  By Lemma~\ref{normalform}, we can

3333: assume without loss of generality that $\phi'$ is $j$-objective.

3334: Suppose that $\phi' $ is a consistent $j$-objective formula.

3335: In this case, it is almost immediate from

3336: the definitions that if

3337: $(M,w) \sat' L_j \phi'$ then $(M',w') \sat' L_j \phi'$.

3338: For the converse,

3339: suppose that $(M,w) \sat' \neg L_j \phi'$.  Then there is some world

3340: $w'' \in \K_j^M(w)$ such that $(M,w'') \sat \neg \phi'$.  Since $(M,w)

3341: \sat' L_j p$, we have that $(M,w'') \sat' p \land \neg \phi'$.

3342: %joe5: rewrote to get rid of new proposition

3343: %Suppose $q$ is some primitive proposition other than $p$ that

3344: %does not appear in $\phi'$.

3345: Let $\psi$ be a $j$-objective basic formula that is independent of $p

3346: \land \neg \phi'$.   Let $\phi''$ be $\phi' \land p \land \neg

3347: \psi$ if $\psi \in \Gamma$, and $\phi' \land p \land \psi$ otherwise.

3348: Since $\psi$ is independent of $p \land \neg \phi'$, it follows that

3349: $\phi''$ is consistent.  Let $\Delta$ be any $j$-set

3350: containing $\phi''$.  It must be the case that $\Delta

3351: \in \Objj(M,w)$, for if not, let $(M^*,w^*)$ be a situation such that

3352: $\Objj(M^*,w^*) = \Objj(M,w)$ and $\objj(M^*,w^*) = \Delta$ (such a

3353: situation exists by Proposition~\ref{construction}).  Then

3354: $(M^*,w^*) \sat p$, contradicting the assumption that $(M,w) \sat N_j

3355: \neg p$.  By construction, $\Delta \ne \Gamma$.  Thus, there is some

3356: world $v \in \K_j^{M'}(w')$ such that $\objj(M',v) = \Delta$.

3357: It follows that $(M',v) \sat' \neg \phi'$, so

3358: %joe5: typos(?)

3359: %$(M,w') \sat \neg L_j

3360: $(M',w') \sat' \neg L_j

3361: \phi'$. Thus, $(M',w')$ agrees

3362: with $(M,w)$ on all basic formulas.  However,

3363: since $\Gamma \notin \Objj(M,w)$, it follows that $(M',w') \sat

3364: \neg N_j \neg p$, and hence that $(M',w') \sat \neg O_j p$.

3365: 

3366: %joe5: more typos

3367: %Let $S = \{\objsj(M,w) \;|\; (M,w) \sat \neg O_j p\}$.  By

3368: Let $S = \{\objsi(M,w) \;|\; (M,w) \sat' \neg O_j p\}$.  By

3369: Proposition~\ref{construction},

3370: there is a situation $(M^*,w^*)$ such that $\Objsi(M^*,w^*) = S$.

3371: Clearly  $(M^*,w^*)

3372: \sat' L_i \neg O_j p$.  We now show that $(M^*,w^*) \sat' N_i \neg O_j

3373: p$ as well.  For suppose that $(M,w)$ is a

3374: situation such that $\Obji(M,w) = \Obji(M^*,w^*)$ and

3375: $\obji(M,w) \notin \Obji(M^*,w^*)$.  Moreover, suppose, by way of

3376: contradiction, that $(M,w) \sat' O_j p$.  By the arguments above,

3377: it follows that there is a situation $(M',w')$ such that

3378: $(M',w') \sat' \neg O_j p$ and $(M,w)$ and $(M',w')$ agree on all basic

3379: formulas.   By construction,

3380: %joe5: added

3381: $\objsi(M',w') \in S = \Objsi(M^*,w^*)$, so

3382: $\obji(M',w') \in \Obji(M^*,w^*)$.  Since

3383: $\obji(M,w) = \obji(M',w')$,

3384: we must also have $\obji(M,w) \in \Obji(M^*,w^*)$, contradicting the

3385: choice of $(M,w)$.  Thus, $(M,w) \sat \neg O_j p$, as desired, and so

3386: $(M^*,w^*) \sat L_i \neg O_j p \land N_i \neg O_j p$. \eprf

3387: 

3388: %gerhard6: added subsection

3389: \subsection{Discussion}

3390: Proposition~\ref{problems} shows that

3391: %joe5:

3392: %although the semantics has the three

3393: although the $i$-set semantics has the three

3394: properties we claimed were appropriate, $N_i$ and $L_i$ still do

3395: not always interact in what seems to be the appropriate way.

3396: Intuitively, the problem here is

3397: that there is more to $i$'s view of a world than just the $i$-objective

3398: basic formulas that are true there.  We should really identify

3399: $i$'s view of a situation $(M,w)$ with

3400: %joe2:

3401: %$\objsi(M,w)$, not $\obji(M,w)$.

3402: the set of {\em all\/} $i$-objective formulas that are true there.

3403: In the canonical-model approach,

3404: the $i$-objective basic formulas that are true at a world

3405: %joe4: added

3406: can be shown to

3407: determine

3408: all the $i$-objective formulas that are true at that world.

3409: %joe2:

3410: %--that is, $\obji(M^c,w)$ determines $\objsi(M^c,w)$

3411: %joe3:

3412: %but

3413: This is not true at all

3414: situations under the $i$-set approach.

3415: %joe2

3416: 

3417: Indeed, it is no longer true

3418: that the $i$-set approach has the second of the

3419: three properties once we take $i$'s

3420: view of $(M,w)$ to be $\objsi(M,w)$.  For consider

3421: the situation $(M^*,w^*)$ constructed in the proof of

3422: Proposition~\ref{problems}.

3423: As the proof of that lemma shows, $\{\objsi(M^*,w) \;|\; w \in

3424: \K_i^{M^*}(w^*)\} \union \{\objsi(M',w') \;|\; \obji(M',w') \notin

3425: \Obji(M^*,w^*)\}$ does not include all maximal sets of $i$-objective

3426: formulas.  In particular, it does not include those maximal sets

3427: that satisfy $O_j p$.

3428: 

3429: %gerhard6: added

3430: To summarize: while the i-set approach arguably has enough worlds,

3431: it suffers from the fact that the full complement of worlds

3432: is not always taken into account for $L_i$ and $N_i$, as the

3433: above example shows. While the canonical model approach

3434: does not run into this problem, it suffers from a perhaps more basic

3435: deficiency: there just are not enough worlds to begin with. For example,

3436: there is no world where $O_i O_j p$ is true.

3437: 

3438: %gerhard6: changed

3439: %We consider a different approach in the

3440: %next section that attempts to address this problem.

3441: We consider a different approach in the

3442: next section that attempts to deal with both problems.

3443: %------------------------------------------------------------------------------

3444: \section{What Properties Should Only Knowing Have?}\label{synthesis}

3445: %------------------------------------------------------------------------------

3446: Up to now, we have provided two semantics for only knowing.  While both have

3447: properties we view as desirable, they also have properties that seem somewhat

3448: undesirable.  This leads to an obvious question: What properties should only

3449: knowing have?  Roughly speaking, we would like to have the multi-agent version

3450: of Levesque's axioms, and no more. Of course, the problem here is axiom {\bf

3451: A5$_n$}.  It is not so clear what the multi-agent version of that should be.

3452: The problem is one of circularity: We would like to be able to say that $N_i

3453: \phi \rimp \neg L_i \phi$ should hold for any

3454: %joe4:

3455: %satisfiable

3456: consistent

3457: $i$-objective formula.  The problem is that in order to say what

3458: the

3459: %joe4

3460: %satisfiable

3461: consistent

3462: formulas are, we need to define the axiom system.

3463: In particular, we have to make precise what this axiom should be.

3464: 

3465: To deal with this problem, we extend the language so that we can

3466: explicitly talk about satisfiability and validity in the language.

3467: We add a modal operator $\Vall$ to the language. The formula $\Val{\phi}$

3468: should be read ``$\phi$ is valid''.  Of course, its dual $\Con{\phi}$,

3469: defined as $\neg \Val{\neg \phi}$, should be read ``$\phi$ is

3470: satisfiable''.  With this operator in the language, we can

3471: replace {\bf A5$_n$} with

3472: \begin{itemize}

3473: \item[{\bf A5$'_n$}.]

3474: $\Con{\neg \alpha} \rimp (N_i\alpha \rimp \neg L_i \alpha)$

3475: %joe4: added

3476: if $\alpha$ is $i$-objective.

3477: \end{itemize}

3478: 

3479: In addition, we have the following rules for reasoning about

3480: validity and satisfiability:

3481: 

3482: \begin{description}

3483: \item[{\bf V1}.] $(\Val{\phi} \land \Val{\phi \rimp \psi}) \rimp

3484: \Val{\psi}$.

3485: %\item[{\bf V2.}] $\Val{\phi} \rimp \phi$.

3486: %\item[{\bf V3.}] $\Val{\phi} \rimp \Val{\Val{\phi}}$.

3487: %\item[{\bf V4.}] $\Cons{\phi} \rimp \Val{\Cons{\phi}}$.

3488: %\item[{\bf V5.}] $\Val{\phi} \rimp (L_i \phi \land N_i \phi)$

3489: \item[{\bf V2}.]

3490: $\Con{\phi}$, if $\phi$ is a satisfiable propositional formula.%

3491: \footnote{We

3492: can replace this by the simpler $\Con{p_1' \land \ldots \land p_k'}$,

3493: where $p_i'$ is a literal---either a primitive proposition or its

3494: negation---and $p_1' \land \ldots \land p_k'$ is

3495: consistent.}

3496: \item[{\bf V3}.]

3497: $(\Con{\alpha \land \beta_1} \land \ldots \land

3498: \Con{\alpha \land \beta_k} \land

3499: \Con{\gamma \land \delta_1} \land \ldots \land

3500: \Con{\gamma \land \delta_m} \land

3501: \Val{\alpha \lor \gamma})  \rimp$\\

3502: $\Con{L_i \alpha \land \neg L_i \neg \beta_1

3503: \land \ldots \land \neg L_i \neg \beta_k \land N_i \gamma \land

3504: \neg N_i \neg \delta_1 \land \ldots \land \neg N_i \neg \delta_m}$,\\

3505: if $\alpha, \beta_1, \ldots, \beta_k,

3506: \gamma, \delta_1, \ldots, \delta_m$ are $i$-objective

3507: formulas.

3508: \item[{\bf V4}.]

3509: $(\Con{\alpha} \land \Con{\beta}) \rimp \Con{\alpha \land \beta}$

3510: if $\alpha$ is $i$-objective and $\beta$ is $i$-subjective.

3511: \item[{\bf Nec$_V$}.] From $\phi$ infer $\Val{\phi}$.

3512: \end{description}

3513: %Axioms {\bf V1}--{\bf V4} and the rule {\bf Nec$_V$} say that $\Vall$

3514: Axiom {\bf V1} and the rule {\bf Nec$_V$} make $\Vall$ what is

3515: called a

3516: {\em normal\/} modal operator.  In fact,

3517: %joe4

3518: %as we shall see, it satisfies

3519: it can be shown to satisfy

3520: all the axioms of S5.

3521: %{\bf V5} is a restatement of

3522: %{\bf Nec$_n$} (and, in the presence of {\bf Nec$_V$}, clearly renders

3523: %{\bf Nec$_n$} unnecessary).

3524: The interesting clauses are clearly

3525: {\bf V2}--{\bf V4}, which capture the intuitive properties of

3526: validity and satisfiability.

3527: %joe2

3528: 

3529: If we restrict to basic formulas,

3530: then {\bf V3} simplifies to

3531: $(\Con{\alpha \land \beta_1} \land \ldots \land

3532: \Con{\alpha \land \beta_k}) \rimp

3533: \Con{L_i \alpha \land \neg L_i \neg \beta_1

3534: \land \ldots \land \neg L_i \neg \beta_k}$ (we can take $\gamma,

3535: \delta_1, \ldots, \delta_m$ to be

3536: $\true$ to get this).

3537: The soundness of this

3538: axiom (interpreting $\Conn$ as satisfiability) follows using much

3539: the same arguments as those in the proof of Proposition~\ref{construction}.

3540: The soundness of {\bf V4} if we restrict to basic formulas follows

3541: from Lemma~\ref{consistency}.  More interestingly, it follows from

3542: the completeness proof given below that these axioms completely

3543: characterize satisfiability in $\Wax$; together with the $\Wax$ axioms,

3544: they provide a sound and complete language for the language augmented

3545: with the $\Vall$ operator.

3546: 

3547: Let AX$'$ consist of the axioms for $\onl$ given

3548: %joe2

3549: %in Section~\ref{prooftheory}

3550: earlier

3551: together with {\bf V1}--{\bf V4} and

3552: {\bf Nec$_V$},

3553: except that {\bf A5$_n$} is replaced by {\bf A5$_n'$}.

3554: %Gerhard3: added provability wrt AX'

3555: %gerhard4: changed it back again

3556: %Provability in AX$'$ is denoted by $\provesAxP$.

3557: AX$'$ is the

3558: axiom system that provides what we claim is the desired

3559: generalization of Levesque's axioms to the multi-agent case.

3560: In particular, {\bf A5$_n'$} is the appropriate generalization

3561: of {\bf A5}.  The question is, of course, whether there is a

3562: semantics for which this is a complete axiomatization.  We now

3563: provide one, in the spirit of the canonical-model construction

3564: of Section~\ref{canonical-model},

3565: %joe2:

3566: except that, in the spirit of the extended situations of

3567: Section~\ref{review}, we do not attempt to make the set of worlds

3568: used for evaluating $L_i$ and $N_i$ disjoint.

3569: %gerhard4: cut

3570: %\footnote{In the full paper, we present a variant of the

3571: %canonical model construction that does make them disjoint.}

3572: 

3573: \begin{sloppypar}

3574: Let $\onlp$ be the extension of $\onln$ to include the modal

3575: operator $\Vall$.  For the remainder of this section, when we say

3576: ``consistent'', we mean consistent with the axiom system

3577: AX$'$.

3578: We define the \newl{extended canonical model}, denoted

3579: $M^e = (W^e, \pi^e, \K_1^e, \ldots, \K_n^e,\N_1^e,\ldots,\N_n^e)$,

3580: as follows:

3581: \end{sloppypar}

3582: 

3583: %gerhard4: replaced by overlapping semantics

3584: %\begin{itemize}

3585: %\item $W^e$ consist of pairs $(\Gamma,x)$, where $\Gamma$ is a

3586: %maximal consistent sets of formulas in $\onln$, and $x$ is either $L$ or

3587: %$N$

3588: %\item for all primitive propositions

3589: %$p$ and  $w = (\Gamma,x)$, we have $\pi^e(w)(p) =$ {\bf true},

3590: %  iff $p\in \Gamma$.

3591: %  \item $((\Gamma,x),(\Gamma',x'))

3592: %  \in \K_i^e$ iff (a) $\Gamma/L_i \subseteq \Gamma'$ and $x' = L$

3593: %or (b) $\Gamma/L_i \subseteq \Gamma'$ and $\Gamma/N_i - \Gamma' \ne

3594: %\emptyset$.

3595: %\end{itemize}

3596: %The definition of $\K_i^e$ requires some explanation.  Intuitively,

3597: %if $\Gamma/L_i \subseteq \Gamma'$, then it is consistent for a world

3598: %satisfying $\Gamma'$ to be $i$-accessible from a world satisfying

3599: %$\Gamma$.  The standard canonical model construction takes the

3600: %$i$-accessibility relation to be maximal, in the sense that every

3601: %world which can consistently be $i$-accessible is $i$-accessible.

3602: %The situation is a little more complicated once we have a modal

3603: %operator for impossibility.  If $\Gamma/N_i \subseteq \Gamma'$,

3604: %then it is consistent for a world satisfying

3605: %$\Gamma'$ {\em not\/}

3606: %to be $i$-accessible from a world satisfying $\Gamma$.

3607: %In $\onln$, the modal operators $L_i$ and $N_i$ play symmetric roles.

3608: %This suggests that when constructing a canonical model for $\onln$,

3609: %we should take both the $L_i$ and $N_i$ relations to be maximal.

3610: %Unfortunately, this is impossible if $N_i$ is to be the complement

3611: %of $L_i$.  The problem is particularly acute

3612: %if we have both $\Gamma/L_i \subseteq \Gamma'$ and $\Gamma/N_i

3613: %\subseteq \Gamma'$.  Roughly speaking, in this case, we can consistently

3614: %make $\Gamma'$ both $i$-accessible and not $i$-accessible from $\Gamma$.

3615: %Which should we choose?  We avoid the problem by having two copies

3616: %of $\Gamma'$: $(\Gamma',L)$ and $(\Gamma',N)$.  We then make $(\Gamma',L)$

3617: %the $i$-accessible copy and $(\Gamma',N)$ the inaccessible copy.

3618: %Thus, if $\Gamma/L_i \subseteq \Gamma'$, then we have $((\Gamma,x),

3619: %(\Gamma',L)) \in \K_i^e$ and, as long as it is not the case that

3620: %$\Gamma/N_i \subseteq \Gamma'$, we also have $((\Gamma,x), (\Gamma',N))

3621: %\in \K_i^e$.

3622: 

3623: 

3624: %joe2:

3625: %[PLUG IN NEW SEMANTICS WITH OVERLAPPING L$_i$ and N$_i$.]

3626: \begin{itemize}

3627: \item $W^e$ consists of the

3628: %gerhard5: should be \onlp, right?

3629: maximal consistent sets of formulas in $\onlp$.

3630: \item For all primitive propositions

3631: $p$ and  $w \in W^e$, we have $\pi^e(w)(p) = \true$

3632:   iff $p\in w$.

3633: \item $(w,w') \in   \K_i^e$ iff $w/L_i \subseteq w'$.

3634: \item $(w,w') \in \N_i^e$ iff $w/N_i \subseteq w'$.

3635: \end{itemize}

3636: 

3637: %joe2: rewrote

3638: In this canonical model, the semantics for $L_i$ and $N_i$ is defined

3639: in terms of the $\K_i^e$ and $\N_i^e$ relations, respectively:

3640: $$

3641: \begin{array}{l}

3642: \mbox{$(M^e,w) \sat L_i \alpha$ \ \ if \ \ $(M^e,w') \sat \alpha$ for

3643: all $w'$ such that $(w,w') \in \K_i^e$.}\\

3644: \mbox{$(M^e,w) \sat N_i \alpha$ \ \

3645: if \ \  $(M^e,w') \sat \alpha$ for all $w'$

3646: such that $(w,w') \in \N_i^e$.}\end{array}

3647: $$

3648: We define the $\Vall$ operator so that it corresponds to validity

3649: in the extended canonical model:

3650: $$\mbox{$(M^e,w) \sat \Val{\alpha}$ if $(M^e,w') \sat \alpha$ for all

3651: worlds $w'$ in $M^e$.}$$

3652: %joe2:

3653: 

3654: %gerhard6: $\Gamma$ should be ``max. cons. set''

3655: %We now want to show that every formula in $\Gamma$ is satisfied at a

3656: %world in the

3657: We now want to show that every formula in a maximal consistent

3658: set is satisfied at a

3659: world in the

3660: extended canonical model. To do this, we need

3661: one preliminary result, showing

3662: that $\Vall$ and $\Conn$ really correspond to

3663: provability and consistency in this framework.

3664: \pro\label{valok}

3665: For every formula $\phi \in \onln$, if $\phi$ is provable then

3666: so is $\Val{\phi}$, while if $\phi$ is not provable, then

3667: $\neg \Val{\phi}$ is provable.

3668: \epro

3669: 

3670: 

3671: \prf By {\bf Nec$_V$}, it is clear that if $\phi$ is provable, so is

3672: $\Val{\phi}$.  Thus, it remains

3673: to show that if $\phi$ is not provable, then $\neg \Val{\phi}$ is.

3674: Using {\bf V1}, it is easy to see that $\neg \Val{\phi}$ is provably

3675: equivalent to $\Con{\neg \phi}$, so it suffices to show that if

3676: $\phi$ is not provable---\ie if $\neg \phi$ is consistent---then

3677: $\Con{\neg \phi}$ is provable.  We prove by induction on $\phi$

3678: that if $\phi$ is consistent, then $\Con{\phi}$ is provable.

3679: 

3680: If $\phi$

3681: %gerhard5: should be V2 instead of V6

3682: %is propositional, the result is immediate from {\bf V6}.  For the

3683: is propositional, the result is immediate from {\bf V2}.  For the

3684: general case,

3685: we first use Lemma~\ref{normalform} to restrict attention to formulas

3686: in the canonical form specified by the lemma.  Using standard modal

3687: reasoning ({\bf V1} and {\bf Nec$_V$}) it is easy to show that

3688: $\vdash \Con{\phi \lor \psi} \dimp (\Con{\phi} \lor \Con{\psi})$.

3689: Thus, it suffices to restrict attention to a conjunction in the form

3690: specified by the lemma.  It is easy to see that if the conjunction

3691: is consistent, then each conjunct must be consistent.  Using

3692: {\bf V4}, it is easy to see that we can restrict attention to

3693: $i$-subjective formulas.  By applying Lemma~\ref{normalform}, we can

3694: assume without loss of generality that we are dealing with a

3695: consistent formula $\phi$ of the form

3696: $L_i \alpha \land \neg L_i \neg \beta_1

3697: \land \ldots \land \neg L_i \neg \beta_k \land N_i \gamma \land

3698: \neg N_i \neg \delta_1 \land \ldots \land \neg N_i \neg \delta_m$,

3699: where $\alpha, \beta_1, \ldots, \beta_k, \gamma, \delta_1, \ldots,

3700: \delta_m$ are all $i$-objective.  We can also assume that

3701: each of $\alpha \land \beta_i$, $i = 1, \ldots, k$ and

3702: $\gamma \land \delta_j$, $j = 1, \ldots, m$ are consistent, for

3703: otherwise we could easily show that $\phi$ is not consistent.

3704: Finally, we can show that $\alpha \lor \gamma$ must be provable,

3705: for if not, by applying {\bf A5$'_n$}, we can again show that

3706: $\phi$ is not consistent.  We now apply the induction hypothesis

3707: to prove the result.  \eprf

3708: 

3709: 

3710: \cor\label{noval} Each formula in $\onlp$ is provably equivalent to a

3711: formula in $\onln$.

3712: \ecor

3713: 

3714: \prf We proceed by induction on the structure of formulas.  The only

3715: nontrivial case is for formulas of the form $\Val{\phi}$.  By the

3716: induction hypothesis, $\phi$ is provably equivalent to a formula

3717: $\phi' \in \onln$.  By straightforward modal reasoning using {\bf V1}

3718: and {\bf Nec$_V$}, we can show that $\Val{\phi}$ is provably

3719: equivalent to $\Val{\phi'}$.  By Proposition~\ref{valok}, $\Val{\phi'}$

3720: is provably equivalent to either $\true$ or $\false$, depending

3721: on whether $\phi'$ is provable. \eprf

3722: 

3723: %joe2: end of my big delete

3724: 

3725: %We can now prove the analogue of Theorem~\ref{canonicalmodel}.

3726: Using standard modal logic techniques, we can now prove the following

3727: result.

3728: \thm\label{complete3}

3729: $M^e$ is a $\Wax$ structure

3730: %%joe2: added

3731: (that is, $\K_i^e$ and $\N_i^e$ are Euclidean and transitive).

3732: %gerhard4: Deleted, since a) not quite true in this form and b) not needed.

3733: %Moreover, $\K_i^e \union \N_i^e = W^e$, for $i=1, \ldots, n$,

3734: %and for each

3735: Moreover, for each world $w\in W^e$, we have

3736: $(M^e,w) \sat \alpha$ iff $\alpha

3737: \in w$.

3738: \ethm

3739: 

3740: \prf

3741: We leave it to the reader to check that the definition of $\K_i^e$

3742: guarantees that $M^e$ is a $\Wax$ structure.  Given

3743: Corollary~\ref{noval}, which allows us to restrict attention

3744: to $\alpha \in \onln$, the proof that

3745: %gerhard5: wrong notation

3746: %$(M^e,(\Gamma,x)) \sat \alpha$ iff $\alpha \in \Gamma$

3747: $(M^e,w) \sat \alpha$ iff $\alpha \in w$

3748: is completely straight forward and

3749: follows the same lines as the usual proofs dealing with

3750: canonical models (see, for example, \cite{Chellas,HM2}).

3751: \eprf

3752: 

3753: %gerhard4: redone since now using overlapping semantics

3754: % in act, things now turn out to be trivial given the previous corollary.

3755: \deleted{

3756: \prf We leave it to the reader to check that the definition of $\K_i^e$

3757: guarantees that $M^e$ is a $\Wax$ structure.  We now

3758: prove that $(M^e,(\Gamma,x)) \sat \alpha$ iff $\alpha \in \Gamma$.

3759: By Corollary~\ref{noval}, it suffices to restrict attention to

3760: $\alpha \in \onln$.  We proceed by induction on structure.  All the

3761: cases follow the same lines as the standard proofs dealing with

3762: canonical models (see, for example, \cite{Chellas,HM2}), except that

3763: for formulas of the form $N_i \phi$.  We deal with this case

3764: as follows.

3765: 

3766: First suppose $N_i \phi \in \Gamma$.  It clearly suffices to deal with

3767: formulas in the canonical form described in Lemma~\ref{normalform}, so

3768: we can assume without loss of generality that $\phi$ is $i$-objective.

3769: Let $w = (\Gamma,x)$, and

3770: suppose that $w' = (\Gamma',x') \approx_i w$ and $w' \notin \K_i^e(w)$.

3771: There are two cases to consider.  First suppose

3772: that for some $i$-objective $\phi' \in \onln$,

3773: we have $L_i \phi' \in \Gamma$ and $\neg

3774: \phi' \in \Gamma'$.  Since $N_i \phi \land L_i \phi' \in \Gamma$,

3775: it follows from {\bf A5$_n$} that $\Val{\phi \lor \phi'}$.  From

3776: Proposition~\ref{valok}, it follows that $\phi \lor \phi'$, or

3777: equivalently, $\neg \phi' \rimp \phi$, is provable.  Since $\neg \phi'

3778: \in \Gamma'$, it follows that $\phi \in \Gamma'$ and, by the induction

3779: assumption, that $(M^e,(\Gamma',x')) \sat \phi$.

3780: If the first case does not apply, the definition of $\K_i^e$

3781: guarantees that it must be the case that $x'

3782: = N$ and $\Gamma/N_i \subseteq \Gamma'$.  But this means that $\phi' \in

3783: \Gamma'$, and again by the inductive hypothesis we have that

3784: $(M^e,(\Gamma',x')) \sat \phi$.

3785: 

3786: Now suppose that $\neg N_i \phi' \in \Gamma$.  We claim that $\Gamma/N_i

3787: \union \{\neg \phi'\}$ must be consistent, for if not,

3788: there must be a finite subset $\Delta$ of

3789: $\Gamma/N_i$ such that $\Delta \rimp \phi'$ is provable, and standard

3790: modal logic arguments show that $N_i \phi'$ must be in $\Gamma$,

3791: contradicting the consistency of $\Gamma$.  It follows that there is

3792: some maximal consistent set $\Gamma'$ containing $\Gamma/N_i \union

3793: \{\neg \phi\}$.  Let $w' = (\Gamma',N)$.  By the inductive hypothesis,

3794: we have $(M^e,w') \sat \neg \phi'$.   Notice that if $\psi$ is an

3795: $i$-subjective formula

3796: in $\Gamma$, then by {\bf A4$_n$}, $N_i \psi \in \Gamma$, so $\psi \in

3797: \Gamma/N_i$.  Thus, $\Gamma$ and $\Gamma'$ agree on all $i$-subjective

3798: formulas, so $w \approx_i w'$.  Moreover, since $\Gamma/N_i \subseteq

3799: \Gamma'$, the definition of $\K_i^e$ guarantees that $w' \notin

3800: \K_i^e(w)$.  Thus, $(M^e,w) \sat \neg N_i \phi'$, as desired.  \eprf

3801: } %%% END DELETED \prf ... \eprf

3802: 

3803: %joe5: added

3804: %Suppose we define $\sat^e \alpha$ iff

3805: We say that $\alpha$ is \newl{e-valid}, denoted $\sat^e \alpha$, if

3806: $M^e \sat \alpha$, that is, if

3807: $(M^e,w) \sat

3808: \alpha$ for all worlds $w \in W^e$.  The following result is immediate

3809: from Theorem~\ref{complete3}.

3810: \cor $\sat^e \alpha$ iff $AX' \vdash \alpha$.  \ecor

3811: Thus, AX$'$ is a sound and complete axiomatization of $\onlp$ with

3812: respect to the $\sat^e$ semantics.

3813: 

3814: %gerhard6: added new axioms

3815: While AX$'$ is sufficient for our purposes, it comes at the expense

3816: of having to explicitly axiomatize validity as part of the logic

3817: itself.

3818: %joe7: added sentence (I think it's a a feature.)

3819: While we view the ability to axiomatize validity and

3820: satisfiability within the logic as a feature in our approach, it is

3821: reasonable to ask whether it is really necessary.

3822:  One of the anonymous referees suggested to us the following

3823: interesting variant,

3824: %joe7

3825: %which avoids this complication, though

3826: which may avoid this complication, although

3827: at the expense of an infinite

3828: number of axiom schemas.

3829: 

3830: %gerhard7: cut ``starting with''

3831: %First we define an infinite sequence of languages starting with

3832: First we define an infinite sequence of languages

3833: %gerhard7: replace k \ge 0 by k = 0,1,2,...

3834: \onlnk\ for $k = 0,1,2\ldots$:

3835: 

3836: \begin{itemize}

3837: \item \onlnzero = \onlnminus

3838: \item \onlnkplusone = $\{\alpha\;|\;$\parbox[t]{4.5in}{$\alpha$ is

3839: a Boolean combination of formulas of \onlnk\ together with\\

3840: formulas of the form $L_i\alpha$ or $N_i\alpha$ for $\alpha\in\onlnk$$\}$}

3841: \end{itemize}

3842: 

3843: Roughly, each language adds another level of nestings of only knowing

3844: with varying agent indices. For example, \onlnkplusone\ contains the formula

3845: %gerhard7: fixed indices to start at 0

3846: $O_{i_0}O_{i_1}\ldots O_{i_{k+1}} p$, where $i_j \ne i_{j+1}$, something

3847: that cannot be expressed in \onlnk.

3848: 

3849: Let \AXnew\ consist of the the axioms {\bf A1$_n$}--{\bf A4$_n$}

3850: as before together with the following set of axioms

3851: \begin{quote}

3852: \Afivenewkplusone. $N_i\alpha \rimp \lnot \L_i\alpha$, where

3853: $\alpha$ is an i-objective \onlnk\ formula which is consistent

3854: \wrt {\bf A1$_n$}--{\bf A4$_n$},\Afivenewone, \Afivenewtwo,$\ldots$ \Afivenewk.

3855: \end{quote}

3856: 

3857: It is not hard to show that the axioms are sound with respect

3858: to the semantics. Whether they are also complete remains an open

3859: problem.

3860: 

3861: %gerhard6: rephrased since glue needed

3862: %How does this semantics compare to our earlier two?

3863: Apart from the question of axiomatization, how does the $\sat^e$ semantics

3864: compare to our earlier two?  Clearly, they differ.  It is easy to see that the

3865: formula $O_i \neg O_j p$, which was not satisfiable under $\mdcm$, is

3866: satisfiable under $\sat^e$.  In addition, the formula $N_i \neg O_j p \land L_i

3867: \neg O_j p$, which is satisfiable under $\sat'$, is not satisfiable under

3868: $\sat^e$.  In both cases, it seems that the behavior of $\sat^e$ is more

3869: appropriate.  On the other hand, all three semantics agree in the case where our

3870: intuitions are strongest, $\onlnminus$.  Since the axiom system AX characterizes

3871: how our earlier two semantics deal with $\onlnminus$,

3872: %joe2:

3873: %it suffices to prove:

3874: this is shown by the following result.

3875: 

3876: \thm If $\phi \in \onlnminus$, then $AX \vdash \phi$ iff

3877: $AX' \vdash \phi$.  \ethm

3878: 

3879: 

3880: \prf It is easy to see that each axiom of AX is sound in AX$'$.  It

3881: follows that $\mbox{AX} \vdash \phi$ implies

3882: AX$' \vdash \phi$.  For the converse, it suffices to show that if

3883: $\phi \in \onlnminus$ is consistent with AX, then it is also

3884: consistent with AX$'$, \ie that $\Con{\phi}$ holds.

3885: We show this by induction

3886: on the structure of $\phi$, much in the same way we proved

3887: Proposition~\ref{valok}.  We can assume without loss of generality

3888: that $\phi$ is a conjunction in the normal form described

3889: Lemma~\ref{normalform}.  It is easy to see that if we can deal with the

3890: case that $\phi$ is an $i$-subjective formula, then we can deal with

3891: arbitrary $\phi$ by repeated applications of {\bf V4} followed

3892: by an application of {\bf V2}.  Thus, suppose that $\phi $ is an

3893: $i$-subjective formula which is consistent with AX.  We can assume that

3894: $\phi$ is of the form

3895: $L_i \alpha \land \neg L_i \neg \beta_1

3896: \land \ldots \land \neg L_i \neg \beta_k \land N_i \gamma \land

3897: \neg N_i \neg \delta_1 \land \ldots \land \neg N_i \neg \delta_m$.

3898: We must have  that $\alpha \land \beta_j$ is consistent for

3899: $j = 1, \ldots, k$, and that $\gamma \land \delta_l$ is AX-consistent

3900: for

3901: $l = 1, \ldots , m$, for otherwise $\phi$ would not be AX-consistent.

3902: Similarly, by Lemma~\ref{LN}, we must have that $\alpha \lor \gamma$ is

3903: $\Wax$-provable, otherwise $\phi$ would not be AX-consistent.  We can

3904: now apply {\bf V3} and the inductive hypothesis to show that $\alpha$ is

3905: AX$'$-consistent. \eprf

3906: 

3907: Thus, we maintain all the benefits of the earlier semantics with this

3908: approach.  Moreover,

3909: %joe7: added next three lines

3910: while it is just as intractable to compute whether $(M^e,w) \sat \alpha$

3911: for a particular world $w$ in the extended canonical model as it was in

3912: all our other approaches, we can show that

3913: the validity problem for this

3914: logic is no harder than that for $\Wax$ alone.  It is PSPACE-complete.

3915: 

3916: \thm The problem of deciding if $AX' \vdash \phi$ is PSPACE-complete.

3917: \ethm

3918: 

3919: 

3920: \prf PSPACE hardness follows from the PSPACE hardness of $\Wax$

3921: \cite{HM2}.\footnote{The result in \cite{HM2} is proved only for $\Dax$,

3922: but the same proof applies to $\Wax$.}  We sketch the proof of the upper

3923: bound.  First of all, observe that it suffices to deal with the case

3924: that $\phi$ is in $\onln$, since we can then apply the arguments of

3925: Corollary~\ref{noval} to remove all occurrences of $\Vall$ from inside

3926: out.  We consider the dual problem of consistency.  Thus, we want to

3927: check if $\Con{\alpha}$ holds.

3928: The first step is to convert

3929: $\alpha$ to the normal form of Lemma~\ref{normalform}.  Observe that

3930: $\alpha$ is consistent iff at least one of the disjuncts is consistent.

3931: Although the conversion to normal form may result in exponentially many

3932: disjuncts, each one is no longer than $\alpha$.  Thus, we deal with them

3933: one by one, without ever writing down the full disjunction.  It suffices

3934: to show that we can decide if each disjunct is consistent in polynomial

3935: space, since we can then erase all the work and start over for the next

3936: disjunct (with a little space necessary for bookkeeping).  We now

3937: proceed much as in the proof of Proposition~\ref{valok}.  By applying

3938: {\bf V4} repeatedly and then {\bf V2} (as in the previous theorem), it suffices to

3939: deal with $i$-subjective formulas.  We then apply {\bf V3} to get simpler

3940: formulas, and repeat the procedure.

3941: %joe: [[GERHARD, IS THIS ENOUGH DETAIL?]]

3942: %gerhard4: yep, seems pretty obvious what's happening here.

3943: %joe5: added

3944: We remark that this gives another PSPACE decision procedure for $\Wax$,

3945: quite different from that presented in \cite{HM2}. \eprf

3946: 

3947: 

3948: To what extent do the three properties we have been focusing on hold under the

3949: $\sat^e$ semantics?  Suppose we take the conceivable states from $i$'s point of

3950: view to be the maximal consistent sets of $i$-objective formulas with respect to

3951: AX$'$, or equivalently, the set of $i$-objective formulas true at some world in

3952: $M^e$.  Let \newl{$\objei(M^e,w)$} consist of all the $i$-objective formulas

3953: true at world $w$ in the extended canonical model (under the $\sat^e$

3954: semantics) and let \newl{$\Objei(M^e,w)$} = $\{\objei(M^e,w') \;|\; w' \in

3955: \K_i^e(w)\}$.  It is easy to see that the first two properties we isolated hold

3956: under this interpretation of conceivable state.  However, it is quite possible

3957: that the ``possible states'' at a world $(M^c,w)$, that is, $\Objei(M^c,w)$, and

3958: the ``impossible states'', that is, $\{\objei(M^c,w') \;|\; w' \approx_i w, w

3959: \notin \K_i^e(w)\}$ are not disjoint.

3960: %joe3: this seems to be an historical remnant

3961: %This is because it is possible to have a world

3962: %$(\Gamma,L) \in \K_i^e(w)$ such that $(\Gamma,N) \notin \K_i^e(w)$.

3963: %On the other hand, if we take a conceivable state to

3964: %have the form $(\Delta,x)$, where $\Delta$ is a maximal consistent

3965: %set of $i$-objective formulas and $x$ is either $L$ or $N$, then

3966: %the possible states and the impossible states at any situation are

3967: %always disjoint, and their union always consists of all conceivable

3968: %states.

3969: 

3970: Interestingly, this semantics does not satisfy the third

3971: property we isolated.  Not all subsets of conceivable states

3972: arise as the set of possible states at some situation $(M^e,w)$.

3973: %joe2:

3974: A proof analogous to that of Lemma~\ref{lc} shows that $\Objei(M,w)$

3975: is always limit closed.

3976: %gerhard6: edited and expanded

3977: %Although we do get limit closure, roughly speaking,

3978: %we avoid problems by having in a precise sense ``enough'' possibilities.

3979: In the canonical model approach, limit closure prevents an agent from

3980: considering certain desirable sets of states. Now this is no longer

3981: the case, despite limit closure. Roughly speaking,

3982: we avoid problems by having in a precise sense ``enough'' possibilities.

3983: More precisely, given any consistent $i$-objective

3984: formula $\alpha$, it is possible for agent $i$ to only

3985: %joe7: typo

3986: %it

3987: know $\alpha$

3988: by virtue of considering all maximal sets of $i$-objective

3989: formulas which contain $\alpha$.

3990: Thus, as we

3991: %joe7

3992: %already hinted at in the beginning,

3993: suggested earlier,

3994: the third property

3995: we isolated in the beginning turns out to be somewhat too strong---%

3996: it is sufficient but not necessary once we allow for enough possibilities.

3997: %joe2

3998: %Although we do not go into details here,

3999: %we remark that it is the device of annotating

4000: %the conceivable states by $N$ and $L$ that allows us to avoid the

4001: %problems associated with not having all sets of

4002: %conceivable states arise.

4003: %Gerhard3 should it not be ``do have'' instead of ``do not have''

4004: %Although we do not have limit closure, roughly speaking,

4005: 

4006: %-----------------------------------------------------------------------------

4007: \section{Multi-Agent Nonmonotonic Reasoning}\label{apps}

4008: %-----------------------------------------------------------------------------

4009: %gerhard4: generalized to OLNn with the new semantics

4010: %not every change marked from now on since too many

4011: In this section, we demonstrate that the logic developed in

4012: Section~\ref{synthesis} captures multi-agent

4013: autoepistemic reasoning in a reasonable way.

4014: %joe5: expanded

4015: %We begin with example derivations of

4016: We do this in two ways.  First we show by example that

4017: the logic can be used to derive some reasonable

4018: nonmonotonic inferences in a multi-agent context.

4019: %joe5:

4020: %Furthermore, we show that that

4021: We then show that the logic can be used to extend

4022: the definitions of stable sets and stable expansions

4023: originally developed for single agent autoepistemic logic

4024: %have natural counterparts in our framework.

4025: to the multi-agent setting.

4026: 

4027: %-----------------------------------------------------------------------------

4028: \subsection{Formal Derivations of Nonmonotonic Inferences}

4029: %-----------------------------------------------------------------------------

4030: \label{nonmon}

4031: %joe5: some glue

4032: In this section, we provide two examples of how the logic can be used

4033: for nonmonotonic reasoning.

4034: %gerhard4: now use full logic

4035: %While our axiomatization is complete only for a subset of the language, it

4036: %is nevertheless strong enough to model interesting

4037: %cases of multi-agent nonmonotonic reasoning. Here are two examples:

4038: 

4039: \xam

4040: Let $p$ be agent $i$'s secret and suppose $i$ makes the following

4041: assumption: unless I know that $j$ knows my secret assume that $j$ does

4042: not know it. We can prove that if this assumption is all $i$

4043: believes then he indeed believes that $j$ does not know his secret.

4044: Formally, we can show

4045: $$\vdash  O_i(\lnot L_i L_j p \rimp \lnot  L_j p)

4046:              \rimp  L_i\lnot L_j p.%

4047: \footnote{Note that if we replace $ L_j p$ by

4048: $p$ we obtain regular single-agent autoepistemic reasoning.}$$

4049: A formal derivation of this theorem can be obtained as follows. Let

4050: \mbox{$\alpha = \lnot L_i L_j p \rimp \lnot  L_j p$.} The justifications

4051: in the following derivation indicate which axioms or previous

4052: derivations have been used to derive the current line. PL

4053: or K45$_n$ indicate that reasoning in either standard propositional logic

4054: or K45$_n$, which are subsumed by AX$'$, is used without further analysis.

4055: 

4056: %

4057: \begin{tabular}{lll}

4058: %joe1: I cut A6; the axioms were also misnumbered, and some \N's should

4059: %have been N

4060: %1 & $ O_i\alpha \rimp  L_i\alpha$ & {\bf A7};{\em PL}\\

4061: %2 & $ O_i\alpha \rimp \N_i\lnot\alpha$ & {\bf A7};{\em PL}\\

4062: %3 & $( L_i\alpha \land \lnot L_i L_j p) \rimp  L_i\lnot L_j p$ &

4063: %\mbox{K45$_n$} \\

4064: %4 & $\N_i\lnot\alpha \rimp (\N_i\lnot L_i L_j p \land \N_i L_j p)$ &

4065: %\mbox{K45$_n$}\\

4066: %5 & $\N_i L_j p \rimp \lnot  L_i L_j p$ & {\bf A6}\\

4067: 1. & $ O_i\alpha \rimp  L_i\alpha$ & PL\\

4068: 2. & $ O_i\alpha \rimp N_i\lnot\alpha$ & PL\\

4069: 3. & $( L_i\alpha \land \lnot L_i L_j p) \rimp  L_i\lnot L_j p$ &

4070: \mbox{K45$_n$} \\

4071: 4. & $N_i\lnot\alpha \rimp (N_i\lnot L_i L_j p \land N_i L_j p)$ &

4072: \mbox{K45$_n$}\\

4073: %joe5: simplified a bit

4074: %5. & $\Con{\true\land p}$ & {\bf V2}\\

4075: %6. & $\Con{\true\land p} \rimp \Con{L_j \true\land \lnot L_j p}$ & {\bf V3}\\

4076: %7. & $\Con{L_j \true\land \lnot L_j p}$ & PL\\

4077: 5. & $\Con{p}$ & {\bf V2}\\

4078: 6. & $\Con{p} \rimp \Con{\lnot L_j p}$ & {\bf V3}\\

4079: %7. & $\Con{L_j \true\land \lnot L_j p}$ & PL\\

4080: 7. & $\Con{\lnot L_j p}$ & {\bf V1}, PL\\

4081: 8. & $\Con{\lnot L_j p} \rimp (N_i L_j p \rimp \lnot  L_i L_j p)$ & {\bf A5$'_n$}\\

4082: 9. & $N_i L_j p \rimp \lnot  L_i L_j p$ & {\em PL}\\

4083: %joe5: the reference numbers seem incorrect here

4084: %11. & $ O_i\alpha \rimp \lnot L_i L_j p$ & 2; 4; 5; PL\\

4085: %12. & $ O_i\alpha \rimp  L_i\lnot L_j p$ & 1; 3; 6; PL\\

4086: 10. & $ O_i\alpha \rimp \lnot L_i L_j p$ & 2; 4; 9; PL\\

4087: 11. & $ O_i\alpha \rimp  L_i\lnot L_j p$ & 1; 3; 10; PL\\

4088: \end{tabular}

4089: \ \\[2ex]

4090: %

4091: To see that $i$'s beliefs may evolve nonmonotonically given that $i$ knows

4092: only

4093: $\alpha$, assume that $i$ finds out that $j$ has found out about the secret.

4094: Then $i$'s belief that $j$ does not believe the secret will be retracted.

4095: %joe1:

4096: In fact, $i$ will believe that $j$ does believe the secret.

4097: Formally, we can show

4098: %joe1: simplified

4099: %$\vdash  O_i( L_j p\land\lnot L_i L_j p \rimp \lnot  L_j p)

4100: %             \rimp (\lnot L_i\lnot L_j p\land L_i L_j p)$.

4101: $$\vdash  O_i( L_j p\land \alpha)              \rimp L_i L_j p.$$

4102: Notice that the logic itself is a regular monotonic logic; the

4103: nonmonotonicity of agent $i$'s beliefs is hidden within the

4104: $ O_i$-operator.

4105: 

4106: %gerhard4: Change L_j p to O_j p to obtain an example for ONLn

4107: %          and not just Onln^-

4108: %joe5:

4109: %The above example formula is actually an instance of $\onlnminus$.

4110: All the formulas that appear in the proof above are in $\onlnminus$.

4111: Thus, we could have used the somewhat simpler proof theory of

4112: Section~\ref{prooftheory}. To obtain an example where we need

4113: the full power of AX$'$, simply replace $L_j p$ by $O_j p$, that

4114: is $i$ now uses the default that unless he knows that $j$ only knows

4115: $p$, then he assumes that $j$ does not only know $p$. In other words,

4116: $i$ (prudently) makes rather cautious assumptions about $i$'s epistemic state

4117: and assumes that $i$ usually knows more than just $p$. The proof

4118: is very similar to the one above.

4119: The only difference is that we now have to establish

4120: that $\Con{\lnot O_j p}$ is provable, which is straightforward.

4121: \exam

4122: %

4123: \xam

4124: \label{proof-of-$i$-knows-that-j-knows-that-Tweety-flies}

4125: Now let $p$ stand for

4126: %joe5: thought I would Canadianize the punctuation; I couldn't resist

4127: %adding the footnote.

4128: %the old ``Tweety flies.''

4129: ``Tweety flies''.%

4130: \footnote{Regular readers of papers on nonmonotonic logic will no doubt

4131: be gratified to see Tweety's reappearance.}

4132: %joe1: I switched the role of $i$ and $j$, to make it look like previous

4133: %example.  Also, I don't think this is quite right

4134: %We want to show that if $i$ knows that all $j$ knows about Tweety is

4135: %that

4136: %he is a bird then $i$ knows that $j$ believes is that Tweety flies.\\

4137: We want to show that if $j$ knows that all $i$ knows about Tweety is that

4138: by default it flies,

4139: then $j$ knows that $i$ believes that Tweety flies.

4140: %joe1: added

4141: As before, we capture the fact that all $i$ believes is that, by

4142: default, Tweety flies, by saying

4143: that all $i$ believes is that, unless $i$ believes that Tweety does not

4144: fly, then Tweety flies.   Thus, we want to show

4145: $$\vdash L_j O_i (\neg L_i \neg p \rimp p) \rimp L_j L_i p.$$

4146: We proceed as follows:

4147: 

4148: \begin{tabular}{lll}

4149: 1. & $O_i(\lnot L_i\lnot p \rimp p) \rimp  L_i p$ & as above, with

4150: $L_j p$ replaced by $\neg p$\\

4151: 2. & $L_j (O_i(\lnot L_i\lnot p \rimp p) \rimp L_i p)$ & 1; {\bf Nec$_n$}

4152: \\

4153: 3. & $L_j O_i(\lnot L_i\lnot p \rimp p) \rimp  L_j L_i p$ & 2;

4154: \mbox{K45$_n$}

4155: \end{tabular}

4156: \ \\[2ex]

4157: %

4158: In a sense, $i$ is able to reason about $j$'s ability

4159: to reason nonmonotonically essentially by simulating $j$'s reasoning pattern.

4160: \exam

4161: %

4162: A situation where $i$ knows that {\em all\/} $j$

4163: knows is $\alpha$ seems hardly attainable in practice, since

4164: an agent usually has at best incomplete information about another agent's

4165: beliefs. It would seem much more

4166: reasonable if we could say that $i$ knows that $\alpha$ is all $j$ knows about

4167: {\em some relevant subject}, say Tweety. This issue is dealt

4168: with in~\cite{Lakemeyer93b}, where the canonical-model approach is extended

4169: to allow statements of the kind that all agent $i$ knows about $x$ is $y$.

4170: It is shown that the forms of nonmonotonic reasoning just described,

4171: when restricted to $\onlnminus$,

4172: go through just as well with the weaker notion of only knowing about.

4173: %

4174: 

4175: %-----------------------------------------------------------------------------

4176: \subsection{$i$-Stable Sets and $i$-Stable Expansions}

4177: %-----------------------------------------------------------------------------

4178: \label{stable-sets}

4179: Single-agent autoepistemic logic was

4180: %joe1: added ref

4181: %originally developed using the concepts of

4182: %joe5: wrong ref!

4183: %developed by Moore \citeyear{Mo} using the concepts of

4184: developed by Moore \citeyear{Moore85} using the concepts of

4185: {\em stable sets} and {\em stable expansions}.

4186: %joe1: added

4187: Levesque proved that there is a close relationship between stable sets

4188: and only-knowing in the single-agent case.  Here we prove an analogous

4189: relationship for the multi-agent case.  We first need to define a

4190: multi-agent analogue of stable sets.

4191: %gerhard4: now do the whole language

4192: %For ease of exposition, we confine

4193: %ourselves to {\em basic\/} formulas only.

4194: 

4195: %joe1:

4196: In the single-agent case, it is well known that a stable set is a

4197: complete set of formulas that agent $i$ could know in some situation;

4198: that is, a set $S$ is stable if and only if there is a situation $(W,w)$

4199: such that $S = \{\alpha\;|\;(W,w) \sat L \alpha\}$.  This is the intuition

4200: that we want to extend to the multi-agent setting, where the underlying language

4201: is now $\onln$. First we define logical consequence in the extended canonical

4202: model

4203: %joe5:

4204: %which we call \econsequence,

4205: in the usual way:

4206: %joe5: added sentence and modified definition

4207: If $\Gamma$ is a set of formulas, we write $M^e \sat \Gamma$ if $M^e

4208: \sat \gamma'$ for each formula $\gamma' \in \Gamma$.

4209: %for any set of formulas $\Gamma$,

4210: %, for all $\gamma'\in\Gamma$, if

4211: %$(M^e,w)\sat\gamma'$ for all $w\in W^e$, then $(M^e,w)\sat\gamma$.

4212: We say that $\gamma$ is an {\em \econsequence\/} of $\Gamma$, and

4213: write $\Gamma\conse\gamma$, exactly if

4214: $M^e\sat\Gamma$ implies $M^e \sat \gamma$.

4215: \dfn

4216: %$i$-Stable Sets\\

4217: Let $\Gamma$ be a set of formulas in $\onln$.

4218: $\Gamma$ is called {\em $i$-stable\/} iff

4219: \begin{enumerate}

4220:   \item[(a)] if $\Gamma\conse\gamma$ then $\gamma\in\Gamma$,

4221:   \item[(b)] if $\alpha\in\Gamma$ then $ L_i\alpha\in\Gamma$,

4222:   \item[(c)]

4223:   if $\alpha\not\in\Gamma$ then $\lnot L_i\alpha\in\Gamma$. \bbox

4224: \end{enumerate}

4225: \end{definition}

4226: 

4227: Note that the only difference between $i$-stable sets and the original

4228: definition

4229: of stable sets is in condition (a), which requires $i$-stable sets to be

4230: closed under \econsequence\

4231: instead of tautological consequence

4232: %joe1; added

4233: (\ie logical consequence in propositional logic)

4234: as in the single-agent case.

4235: %joe1; expanded

4236: Using \econsequence\ rather than tautological consequence makes no

4237: difference in the single-agent case; in the multi-agent case it does.

4238: Intuitively, we want to allow the agents to use \econsequence\  here to

4239: capture the intuition that it is common knowledge that all agents

4240: %other agents are, like themselves, perfect reasoners in K45$_n$.

4241: are perfect reasoners under the extended canonical model semantics.

4242: %joe1: moved back from below

4243: For example, if agent $i$ believes $\lnot L_j p$

4244: for a different agent $j$, then we want him to also believe

4245: %gerhard4: replace L_j by N_j

4246: $N_j\lnot L_j p$.  To do this, we need to close off under \econsequence.

4247: \deleted{

4248: It is also interesting to note that Halpern and Moses~\cite{HalpernMoses84}

4249: proposed a very similar definition of stability in the n-agent case.

4250: The difference is that they require stable sets to be consistent and

4251: to contain all valid formulas of the logic {\em KT5$_n$}, also called {\em S5$_n$}.

4252: } %%% END DELETED

4253: 

4254: %joe1: You had never defined $i$-epistemic state

4255: %The next theorem proves that $i$-stable sets and $i$-epistemic states

4256: %are

4257: %equivalent notions. In other words, the definition of $i$-stability

4258: %falls out naturally given the semantics of the logic.

4259: The next theorem shows that $i$-stable sets do indeed satisfy the

4260: intuitive requirement.  We define an \newl{$i$-epistemic\/} state to be

4261: a set $\Gamma$ of $\onln$-formulas such that for some situation

4262: $(M^e,w)$ in the extended canonical model,

4263: $\Gamma = \{\alpha\in\onln\;|\; (M^e,w) \sat L_i \alpha\}$;

4264: in this case, we say that $\Gamma$ is the $i$-epistemic situation

4265: corresponding to $(M^e,w)$.

4266: For a set of $\onln$-formulas $\Gamma$, let $\Gammabar = \{\gamma\;|$

4267: $\gamma\in\onln$ and $\gamma\not\in\Gamma\}$,

4268: $ L_i\Gamma = \{ L_i\gamma\;|\; \gamma\in\Gamma\}$, and

4269: $\lnot L_i\Gammabar = \{\lnot L_i\gamma\;|\;

4270: %joe5: typo?

4271: %gerhard5: no, since \Gammabar is the set of wffs not in \Gamma

4272: \gamma\in\Gammabar\}$.

4273: %\gamma\notin\Gammabar\}$.

4274: 

4275: %

4276: \thm

4277: Let $\Gamma$ be a set of $\onln$-formulas. $\Gamma$ is $i$-stable iff

4278: $\Gamma$ is an $i$-epistemic state.

4279: \ethm

4280: \prf It is straightforward to show that every $i$-epistemic state is

4281: $i$-stable. To show the converse, let $\Gamma$ be $i$-stable. We need to

4282: show that

4283: it is also an $i$-epistemic state. Certainly $ L_i\Gamma$ is consistent.

4284: If $\Gamma$ contains all $\onln$-formulas, that is, if agent $i$ is

4285: inconsistent,

4286: %joe1: slight rewriting

4287: %then $\Gamma$ is also an $i$-epistemic state

4288: %(choose any world without any $\K_i^c$-accessible worlds).

4289: %Otherwise, let $\Gamma$ be a proper subset of

4290: then let $(M^e,w)$ be a situation where $\K_i^e(w) = \emptyset$; such a

4291: situation clearly exists. Then $\Gamma$ is the

4292: $i$-epistemic situation corresponding to $(M^e,w)$.

4293: If $\Gamma$ is a proper subset of

4294: the $\onln$-formulas,

4295: %joe1: rewrote proof

4296: %Then $ L_i\Gamma$ does not contain $(p\land\lnot p)$ for

4297: %an arbitrary  atom $p$ and $ L_i\Gamma\union \{\lnot L_i(p\land\lnot

4298: %p)\}$ is consistent.

4299: then $\Gamma$ must be consistent. (If $\Gamma$ were inconsistent, by the

4300: first property of stable sets, $\Gamma$ would contain all formulas.)

4301: In particular, this means that $p \land \neg p \notin \Gamma$ for a

4302: primitive proposition $p$.

4303: The second property of stable sets guarantees that $L_i \Gamma \subseteq

4304: \Gamma$, while the third guarantees that $\neg L_i (p \land \neg p) \in

4305: \Gamma$.  Since $\Gamma$ is consistent, so is $L_i \Gamma \union \{ \neg

4306: L_i (p \land \neg p)\}$.

4307: %joe5:

4308: %Thus, there is a $w^*\in W^e$

4309: %(maximal consistent set with respect to AX$'$) containing

4310: $W^e$ consists of all the maximal consistent sets (with respect to

4311: AX$'$); thus, there must be some $w^* \in W^e$ that contains

4312: $ L_i\Gamma\union \{\lnot L_i(p\land\lnot p)\}$.

4313: %joe5: rewrote rest of proof

4314: %We now show that $w^*$ contains

4315: %$\lnot L_i\Gammabar$. Let $\lnot L_i\alpha\in\lnot L_i\Gammabar$.

4316: %Since $\alpha \notin \Gamma$, by the second property of stable sets,

4317: %$\neg L_i \alpha \in \Gamma$, and thus $L_i \neg L_i \alpha

4318: %\in L_i\Gamma \subseteq w^*$.  Since

4319: %$ L_i\lnot L_i\alpha\land\lnot L_i(p\land\lnot p) \rimp \lnot

4320: %L_i\alpha$ is provable in AX$'$, we must have $\lnot L_i\alpha \in

4321: %w^*$.

4322: %Finally,

4323: %since $w^*$ contains both $ L_i\Gamma$ and $\lnot L_i\Gammabar$,

4324: %it is easy to see that $\Gamma$ must be the $i$-epistemic state

4325: %corresponding to $(M^e,w^*)$.

4326: We claim that $\Gamma$ is the $i$-epistemic state corresponding to

4327: $(M^e,w^*)$.  Thus, we must show that $\phi \in \Gamma$ iff $(M^e, w^*)

4328: \sat L_i \phi$.

4329: To see this, first suppose that $\phi \in \Gamma$.  Thus, $L_i \phi \in

4330: L_i \Gamma$.  By construction, $w^*$ contains $L_i \Gamma$.  By

4331: Theorem~\ref{complete3}, we have that $(M^e,w^*) \sat L_i \phi$.

4332: On the other hand, if $\phi \notin \Gamma$, then, since $\Gamma$ is

4333: $i$-stable, we have that $\neg L_i \phi \in \Gamma$.  By the previous

4334: argument, it follows that $(M^e,w^*) \sat L_i \neg L_i \phi$.

4335: {F}rom ${\bf A4}_n$, it follows that $(M^e,w^*) \sat \neg L_i \phi$, and

4336: hence $(M^e,w^*) \not\sat L_i \phi$.   This proves the claim.

4337: \eprf

4338: 

4339: %joe1: added some glue here

4340: Moore \citeyear{Moore85}

4341: defined the notion of a {\em stable expansion\/} of a

4342: set $A$ of formulas in the single-agent case.  Intuitively, a

4343: stable expansion of $A$ is a stable set containing $A$ all of whose

4344: formulas can be justified, given $A$ and the formulas believed in that

4345: stable set.  Further discussion and justification of the

4346: notion of stable expansion can be found in \cite{Hal13,Moore85}.

4347: Rather than

4348: discussing this here, we go directly to our multi-agent generalization

4349: of Moore's notion.

4350: 

4351: \dfn

4352: %$i$-Stable Expansion\\

4353: Let $A$ be a set of $\onln$-formulas.

4354: $\Gamma$ is called an \newl{$i$-stable expansion\/} of $A$ iff

4355: $\Gamma = \{ \gamma\in\onln \;|\;

4356: A\union L_i\Gamma \union\lnot L_i\Gammabar\conse\gamma\}$.

4357: \edfn

4358: %

4359: %joe1: added

4360: It is easy to see that an $i$-stable expansion is an $i$-stable set.  The

4361: definition of $i$-stable expansions looks exactly like Moore's definition

4362: of stable expansions except that we again use \econsequence\ instead of

4363: tautological consequence.  As in the case of stable sets, this is necessary

4364: to capture the fact that it is common knowledge that all agents can do

4365: reasoning under the extended canonical model semantics.

4366: %joe1: moved this material back to the discussion of stable

4367: %logical consequence in propositional logic.  Using the stronger \KFFn\

4368: %is

4369: %%necessary in the multi-agent case, since an agent knows that other

4370: %necessary here for the same

4371: %agents are

4372: %also perfectly introspective. For example, if agent $i$ believes $\lnot L_j p$

4373: %for a different agent $j$ then he also believes $ L_j\lnot L_j p$.

4374: 

4375: %joe5: it doesn't follow immediately

4376: %The following theorem demonstrates that the $i$-stable expansions

4377: We now generalize a result of Levesque's \citeyear{Lev5} (who

4378: proved it for the single-agent case), showing that the $i$-stable

4379: expansions

4380: of a formula $\alpha$ correspond precisely to the different

4381: %gerhard5: something was missing here

4382: situations where $i$ only knows $\alpha$.

4383: We first need a lemma.

4384: %joe1: added

4385: %it is a generalization of Levesque's \citeyear{Lev5} result for the

4386: %single-agent case.

4387: 

4388: %joe5: moved this lemma into the theorem.

4389: %\begin{lemma}

4390: %\label{N-vs-L-lemma}

4391: %Let $\phi$ and $\psi$ be i-objective formulas. If $N_i\lnot\phi\land

4392: %\L_i\psi$ is consistent, then $\conse\phi\rimp\psi$.

4393: %\end{lemma}

4394: %\prf

4395: %Let  $N_i\lnot\phi\land \L_i\psi$ be consistent and

4396: %assume, to the contrary, that $\lnot(\phi\rimp \psi)$ is also

4397: %consistent. Since $\vdash N_i\lnot\phi \rimp N_i(\phi\rimp\psi)$,

4398: %$\vdash N_i(\phi\rimp\psi) \rimp \lnot L_i(\phi\rimp\psi)$ (by axiom

4399: %{\bf A5'} and the fact that $\Con{\lnot(\phi\rimp \psi)}$ is provable),

4400: %and $\vdash \lnot L_i(\phi\rimp\psi)\rimp L_i\psi$,

4401: %we obtain $\vdash N_i\lnot\phi\rimp \lnot L_i\psi$, a contradiction.

4402: %\eprf

4403: \lem

4404: \label{e-states-decide-all-i-subj-form}

4405: Let $(M^e,w)$ be a situation with

4406: \[\Sigma = \{L_i\gamma \;|\;

4407: (M^e,w)\md L_i\gamma\}

4408: \union \{\lnot L_i\gamma \;|\; (M^e,w)\md \lnot L_i\gamma\}.

4409: \]

4410: For any $\alpha$,

4411: %joe5: rewrote statement of lemma

4412: %let $\alpha^*$ be $\alpha$ with

4413: %every occurrence of $L_i\gamma$ ($N_i\gamma$) replaced by \true\

4414: %if $\Sigma\conse L_i\gamma$ ($\Sigma\conse N_i\gamma$) and \false\

4415: %otherwise. Then $\Sigma \union \{\alpha\} \conse \alpha^*$.

4416: there is an $i$-objective formula $\alpha^*$ such that

4417: \begin{enumerate}

4418: \item[(a)] $\Sigma \conse \alpha\dimp \alpha^*$,

4419: %gerhard5: L_i and N_i instead of L and N

4420: \item[(b)] $(M^e,w) \sat (L_i \alpha \dimp L_i\alpha^*) \land (N_i \alpha

4421: \dimp N_i\alpha^*)$.

4422: \end{enumerate}

4423: \elem

4424: \prf

4425: %%gerhard4: JOE, ANY MORE DETAIL NECESSARY?

4426: %joe5: a little more detail (and actually corrected some details)

4427: Given a formula $\phi$, we say that a subformula

4428: $L_i \psi$ of $\phi$ occurs at {\em top level\/} if it is not in the

4429: scope of any modal operators.

4430: Let $\alpha^*$ be the result of replacing each top-level subformula of

4431: $\alpha$ of the form $L_i \gamma$ (\respc $N_i \gamma$) by $\true$

4432: if $\Sigma\conse L_i\gamma$

4433: (\respc $\Sigma\conse N_i\gamma$) and by $\false$

4434: otherwise.  Clearly $\alpha^*$ is $i$-objective.  Moreover, a trivial

4435: argument by induction on the structure of $\alpha$ shows that

4436: $\Sigma \sat \alpha \dimp \alpha^*$: If $\alpha$ is a primitive

4437: proposition then $\alpha^* = \alpha$; if $\alpha$ is of the form

4438: $\alpha_1 \land \alpha_2$ or $\neg \alpha'$, then the result follows

4439: easily by the induction hypothesis; if $\alpha$ is of the form $L_j

4440: \beta$ for $j \ne i$, then $\alpha = \alpha^*$, since $\alpha$ has no

4441: top-level subformulas of the form $L_i \phi$; finally, if $\alpha$ is

4442: of the form $L_i \beta$, then $\alpha^*$ is either $\true$ or $\false$,

4443: depending on whether $L_i \beta$ is in $\Sigma$.  Since either $L_i

4444: \beta$ or $\neg L_i \beta$ must be in $\Sigma$, the result is immediate

4445: in this case too.  Part (b) follows immediately from part (a), since if

4446: $w' \approx_i w$, we must have $(M^e,w') \sat \Sigma$, so $(M^e,w')

4447: \sat \alpha \dimp \alpha^*$. \eprf

4448: 

4449: %%The result follows easily from the fact that $\Sigma$ decides every

4450: %%i-subjective formula. In particular, since $L_i$ and $N_i$ are

4451: %%fully and mutually introspective, we have that for every formula

4452: %%$\gamma$, either $\Sigma\conse L_i\gamma$ or $\Sigma\conse \lnot

4453: %%L_i\gamma$

4454: %%and either $\Sigma\conse N_i\gamma$ or $\Sigma\conse \lnot N_i\gamma$.

4455: %%\eprf

4456: %%

4457: %%\begin{corollary}

4458: %%\label{Only-knowing-i-objec-form}

4459: %%If $(M^e,w)\md O_i\alpha$, then $(M^e,w) \md O_i\alpha^*$.

4460: %%\end{corollary}

4461: %%\prf

4462: %%Let $w'\in \K_i^e(w)$. Then $(M^e,w')\md  \Sigma \union \{\alpha\}$.

4463: %%Hence,

4464: %%by the lemma, $(M^e,w')\md \alpha^*$. Similarly, if $w'\in \N_i^e(w)$,

4465: %%then $(M^e,w')\md \lnot\alpha^*$.

4466: %%\eprf

4467: 

4468: \thm %Relating Only-Knowing and $i$-Stable Expansions\\

4469: \label{O-vs-stable-expansions}

4470: %gerhard4: major rewrite, also statement of the thm needs stronger assumption

4471: Let $w$ be a world in the extended canonical model and let

4472: $\Gamma$ be the $i$-epistemic state corresponding to $(M^e,w)$.

4473: Then, for every $\onln$-formula $\alpha$, we have that

4474: $(M^e,w)\md O_i\alpha$ iff

4475:       (a) $\Gamma$ is an $i$-stable expansion of $\{\alpha\}$ and

4476: (b) $\K_i^e(w)$

4477:          and $\N_i^e(w)$ are disjoint.

4478: \ethm

4479: \prf

4480: Let $\Sigma = L_i \Gamma \union \neg L_i \Gammabar$. To prove the ``only if''

4481: direction, suppose $(M^e,w)\md O_i\alpha$. The disjointness of $\K_i^e(w)$ and

4482: $\N_i^e(w)$ follows immediately from the fact that $(M^e,w)\md L_i\alpha\land

4483: N_i\lnot\alpha$.  To prove that $\Gamma$ is an $i$-stable expansion of

4484: $\{\alpha\}$, it suffices to show that for all $\onln$-formulas $\beta$, we have

4485: $(M^e,w)\md L_i\beta\ {\rm iff}\ \{\alpha\}\union\Sigma \conse \beta$.

4486: %joe1: lots of minor rewriting in this proof

4487: %Let $w'$ be any world such that $w\K_i^c w'$.

4488: %and $w' \in \K_i^e(w)$.

4489: 

4490: First suppose that $\{\alpha\}\union\Sigma \conse \beta$.

4491: Since $(M^e,w)\md \{O_i\alpha\} \union \Sigma$, and every formula in $\Sigma$ is

4492: of the form $L_i \gamma$ or $\neg L_i \gamma$, it easily follows that $(M^e,w)

4493: \md L_i \alpha$ and  $(M^e,w)\md L_i \Sigma$.  Hence, $(M^e,w') \md \alpha$

4494: and $(M^e,w') \md \Sigma$

4495: %gerhard5: added to make clear which w' are meant

4496: for every $w'\in \K_i^e(w)$.

4497: It follows that $(M^e,w')\md\beta$ and, therefore, $(M^e,w)\md L_i\beta$.

4498: 

4499: For the converse,

4500: suppose that $(M^e,w)\md L_i\beta$.  We want to show that

4501: $\{\alpha\} \union \Sigma \conse \beta$.

4502: %joe5: added

4503: By Lemma~\ref{e-states-decide-all-i-subj-form}, we can assume without

4504: loss of generality that $\beta$ is $i$-objective.  (For if not, we can

4505: replace $\beta$ by an $i$-objective $\beta^*$ such that $\Sigma \conse

4506: \beta \dimp \beta^*$ and $(M^e,w) \sat L_i \beta \dimp L_i \beta^*$,

4507: prove the result for $\beta^*$, and conclude that it holds for $\beta$

4508: as well.)  To show that $\{\alpha\} \union \Sigma \conse \beta$, we must

4509: show that for all worlds $w'$ such that

4510: $(M^e,w')\md \{\alpha\}\union\Sigma$, we have $(M^e,w') \sat \beta$.

4511: %It suffices to show that

4512: %$w'\in\K_i^e(w)$, that is, $w/L_i\subseteq w'$.

4513: %joe5: I don't think this argument is quite right, but my argument above

4514: %lets you reduce to $i$-objective.

4515: %By Lemma~\ref{normalform}, every

4516: %$\onln$-formula is provably equivalent to one where, for each

4517: %subformula

4518: %of the form $L_i\phi$, the formula $\phi$ is $i$-objective.  Hence it

4519: %suffices to consider only $i$-objective formulas.

4520: %joe5: more rewriting

4521: %Suppose $(M^e,w)\md L_i\gamma$, where

4522: %$\gamma$ is $i$-objective. Since

4523: %$(M^e,w)\md O_i\alpha$, by Corollary~\ref{Only-knowing-i-objec-form},

4524: %$(M^e,w)\md O_i\alpha^*$, where $\alpha^*$ is as defined in

4525: %Lemma~\ref{e-states-decide-all-i-subj-form}. In particular, $\alpha^*$

4526: %is $i$-objective.

4527: By Lemma~\ref{e-states-decide-all-i-subj-form}, there is an

4528: %gerhard5: should be M^e instead of M^*

4529: %$i$-objective formula $\alpha^*$ such that $(M^*,w) \sat O\alpha \dimp

4530: %O\alpha^*$ and $\Sigma \conse \alpha \dimp \alpha^*$.  Thus, $(M^*,w)

4531: $i$-objective formula $\alpha^*$ such that $(M^e,w) \sat O\alpha \dimp

4532: O\alpha^*$ and $\Sigma \conse \alpha \dimp \alpha^*$.  Thus, $(M^e,w)

4533: \sat N_i \alpha^* \land L_i \beta$.  By the arguments of Lemma~\ref{LN}

4534: (which apply without change to the extended canonical model semantics),

4535: it must be the case that $\conse \alpha^* \rimp \beta$.  Since $\Sigma

4536: \conse \alpha \dimp \alpha^*$, it follows that $\{\alpha\} \union \Sigma

4537: \conse \beta$.

4538: %

4539: %Hence, by Lemma~\ref{N-vs-L-lemma}, $\conse \alpha^*\rimp

4540: %\gamma$. Also, $\{\alpha\}\union\Sigma \conse \alpha^*$ by

4541: %Lemma~\ref{e-states-decide-all-i-subj-form}.

4542: Since $(M^e,w')\md

4543: \{\alpha\}\union\Sigma$ by assumption, we have that $(M^e,w')\md\beta$,

4544: as desired.

4545: %Thus, we have

4546: %shown that $w'\in \K_i^e(w)$ and, therefore, $(M^e,w')\md\beta$.

4547: 

4548: To prove the ``if'' direction of the theorem, suppose that

4549: $\K_i^e(w)$ and $\N_i^e(w)$ are disjoint and that for all

4550: $\onln$-formulas $\beta$, we have $(M^e,w)\md L_i\beta\ {\rm iff}\

4551: \{\alpha\}\union\Sigma \conse \beta$. We need to show that $(M^e,w)\md

4552: O_i\alpha$, that is, $(M^e,w)\md L_i\alpha\land N_i\lnot\alpha$.

4553: 

4554: Since $\{\alpha\}\union\Sigma \conse \alpha$, the fact that

4555: $(M^e,w)\md L_i\alpha$ follows immediately.

4556: To prove that $(M^e,w)\md N_i\lnot\alpha$, let $w'\in\N_i^e(w)$ and

4557: assume, to the contrary,

4558: that $(M^e,w')\md \alpha$. Since $w'\in\N_i^e(w)$, it follows that

4559: $\Sigma\subseteq w'$. Hence $w/L_i \subseteq w'$, from

4560: which $w'\in \K_i^e(w)$ follows, contradicting the assumption that

4561: $\K_i^e(w)$ and $\N_i^e(w)$ are disjoint.

4562: \eprf

4563: 

4564: %

4565: %\cor

4566: %Basic $i$-objective formulas have a unique $i$-stable expansion.

4567: %\ecor

4568: %\prf Follows directly from

4569: %Theorem~\ref{basic-$i$-objectives-are-determinate}~and~\ref{O-vs-stable-expansions}.

4570: %\eprf

4571: 

4572: 

4573: %------------------------------------------------------------------------------

4574: \section{Conclusion}\label{discussion}

4575: %------------------------------------------------------------------------------

4576: We have provided three semantics for multi-agent only-knowing.

4577: All agree on the subset $\onlnminus$, but they differ on formulas

4578: involving nested $N_i$'s.  Although

4579: %joe3: to save space

4580: %we have presented arguments

4581: a case can be made

4582: that

4583: the $\sat^e$ semantics comes closest to capturing our intuitions

4584: for ``knowing at most'', our intuitions beyond $\onlnminus$ are not

4585: well grounded.  It would certainly help to have more compelling

4586: semantics

4587: %joe2:

4588: %for $\sat^e$.

4589: corresponding to AX$'$.

4590: 

4591: On the other hand, it can be argued that semantics does not play

4592: quite as crucial a role when dealing with knowing at most as in

4593: other cases.  The reason is that the structures we must deal with,

4594: in general, have uncountably many worlds.  For example, whichever

4595: of the three semantics we use, there must be uncountably many

4596: worlds $i$-accessible from a situation $(M,w)$ satisfying

4597: $O_i p$, at least one for every $i$-set that includes $p$.

4598: To the extent that we are interested in proof theory, the

4599: proof theory associated with $\sat^e$, characterized by

4600: the axiom system AX$'$, seems quite natural.  The fact

4601: that the validity problem is no harder in this setting

4602: than that for $\Wax$ adds further support to its usefulness.

4603: %gerhard2: cut

4604: %gerhard4: put in again

4605: Of course, as we suggested above, rather than only knowing,

4606: it seems more appropriate to reason about only knowing about a certain

4607: topic.  Lakemeyer \citeyear{Lakemeyer93b} provides a semantics

4608: for only knowing about, using the canonical-model approach.

4609: It would be interesting to see if this can also be done using

4610: the other approaches we have explored here.

4611: %------------------------------------------------------------------------------

4612: 

4613: %\bibliographystyle{chicago}

4614: \bibliographystyle{plain}

4615: \bibliography{z}

4616: \end{document}

4617: 

4618: 

4619: