The logic of conditional beliefs: Neighbourhood semantics and sequent calculus

The logic of Conditional Beliefs has been introduced by Board, Baltag and Smets to reason about knowledge and revisable beliefs in a multi-agent setting. It is shown how the semantics of this logic, defined in terms of plausibility models, can be equivalently formulated in terms of neighbourhood models, a multi-agent generalisation of Lewis' spheres models. On the basis of this new semantics, a labelled sequent calculus for the logic of Conditional Beliefs is developed. The calculus has strong proof-theoretic properties, in particular admissibility of contraction and cut, and it provides a direct decision procedure for the logic. Furthermore, its semantic completeness is used to obtain a constructive proof of the finite model property of the logic