Supplement to Dynamic Epistemic Logic

Appendix J: Conditional Doxastic Logic

The language \eqref{CDL} of conditional doxastic logic is defined by the following grammar:

\[\begin{gather*}\taglabel{CDL} F \ccoloneqq p \mid F\land F \mid \lnot F\mid B_a^FF \\ \small p\in\sP,\; a\in\sA \end{gather*}\]

We think of the formula \(B_a^FG\) as saying that agent a believes F after conditionalization (or static belief revision) by G. The satisfaction relation \(\models\) between pointed plausibility models and formulas of \eqref{CDL} and the set \(\sem{F}_M\) of worlds in the plausibility model M at which formula F is true are defined by the following recursion.

  • \(\sem{F}_M\coloneqq\{w\in W\mid M,w\models F\}\).
  • \(M,w\models p\) holds if and only if \(w\in V(p)\).
  • \(M,w\models F\land G\) holds if and only if \(M,w\models F\) and \(M,w\models G\).
  • \(M,w\models\lnot F\) holds if and only if \(M,w\not\models F\).
  • \(M,w\models B_a^GF\) holds if and only if \(\min_a(\sem{G}_M\cap\cc_a(w))\subseteq\sem{F}_M\).
    \(B_a^GF\) means that “F is true at the most plausible G-worlds consistent with a’s information”.

In the language \eqref{CDL}, the operator \(K_a\) for possession of information may be defined as follows:

\[ K_a F \text{ denotes } B_a^{\lnot F}\bot, \]

where \(\bot\) is the propositional constant for falsehood. We then have the following.

Theorem (Baltag and Smets 2008b). For each pointed plausibility model \((M,w)\), we have: \[ M,w\models B_a^{\lnot F}\bot \text{ iff } M,v\models F \text{ for each }v \text{ with } v\simeq_a w. \] So the \eqref{CDL}-abbreviation of \(K_aF\) as \(B_a^{\lnot F}\bot\) gives the same meaning in \eqref{CDL} for “possession of information” as we had in \((K\Box)\).

The validities of \eqref{CDL} are axiomatized as follows.

The axiomatic theory \(\CDL\) (Baltag, Renne, and Smets 2015).

  • Axiom schemes and rules for classical propositional logic
  • \(B_a^F(G_1\to G_2)\to (B_a^FG_1\to B_a^FG_2)\)
  • \(B_a^FF\)
  • \(B_a^F\bot\to B_a^{F\land G}\bot\)
  • \(\lnot B_a^F\lnot G\to( B_a^FH\to B_a^{F\land G}H)\)
  • \(B_a^{F\land G}H\to B_a^F(G\to H)\)
  • \(B_a^{F\land G}H\to B_a^{G\land F}H\)
  • \(B_a^FH\to B_a^G B_a^FH\)
  • \(\lnot B_a^FH\to B_a^G\lnot B_a^FH\)
  • \(B_a^F\bot\to\lnot F\)

\(\CDL\) Soundness and Completeness (Board 2004; Baltag and Smets 2008b; Baltag, Renne, and Smets 2015). \(\CDL\) is sound and complete with respect to the collection \(\sC_*\) of pointed plausibility models. That is, for each \eqref{CDL}-formula F, we have \(\CDL\vdash F\) if and only if \(\sC_*\models F\).

← beginning of main article

Copyright © 2016 by
Alexandru Baltag <>
Bryan Renne <>

Open access to the SEP is made possible by a world-wide funding initiative.
The Encyclopedia Now Needs Your Support
Please Read How You Can Help Keep the Encyclopedia Free