A sequent calculus for preferential conditional logic based on neighbourhood semantics

The basic preferential conditional logic PCL, initially proposed by Burgess, finds an interest in the formalisation of both counterfactual and plausible reasoning, since it is at the same time more general than Lewis’ systems for counterfactuals and it contains as a fragment the KLM preferential logic P for default reasoning. This logic is characterised by Kripke models equipped with a ternary relational semantics that represents a comparative similarity/normality assessment between worlds, relativised to each world. It is first shown that its semantics can be equivalently specified in terms of neighbourhood models. On the basis of this alternative semantics, a new labelled calculus is given that makes use of both world and neighbourhood labels. It is shown that the calculus enjoys syntactic cut elimination and that, by adding suitable termination conditions, it provides a decision procedure.