GL-Based Calculi for PCL and Its Deontic Cousin

We introduce a natural sequent calculus for preferential conditional logic PCL via embeddings into provability logic GL, achieving optimal complexity and enabling countermodel extraction. Extending the method to PCL with reflexivity and absoluteness – corresponding to Åqvist’s deontic system F with cautious monotony – we employ hypersequents to capture the S5 modality; the resulting calculus subsumes the known calculi for the weaker systems E and F within Åqvist family