Supplement to Dynamic Epistemic Logic
Appendix J: Conditional Doxastic Logic
The language (???) of conditional doxastic logic is defined by the following grammar:
F::=p∣F∧F∣¬F∣BFaFp∈P,a∈AWe think of the formula BFaG as saying that agent a believes F after conditionalization (or static belief revision) by G. The satisfaction relation ⊨ between pointed plausibility models and formulas of (CDL) and the set [[F]]M of worlds in the plausibility model M at which formula F is true are defined by the following recursion.
- [[F]]M:={w∈W∣M,w⊨F}.
- M,w⊨p holds if and only if w∈V(p).
- M,w⊨F∧G holds if and only if M,w⊨F and M,w⊨G.
- M,w⊨¬F holds if and only if M,w⊭.
- 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.