A Proof-Theoretic View of Basic Intuitionistic Conditional Logic

Intuitionistic conditional logic, studied by Weiss, Ciardelli and Liu, and Olkhovikov, aims at providing a constructive analysis of conditional reasoning. In this framework, the would and the might conditional operators are no longer interdefinable. The intuitionistic conditional logics considered in the literature are defined by setting Chellas' conditional logic CK, whose semantics is defined using selection functions, within the constructive and intuitionistic framework introduced for intuitionistic modal logics. This operation gives rise to a constructive and an intuitionistic variant of (might-free-) CK, which we call CCKbox and IntCK respectively. Building on the proof systems defined for CK and for intuitionistic modal logics, in this paper we introduce a nested calculus for IntCK and a sequent calculus for CCKbox. Based on the sequent calculus, we define CCK, a conservative extension of Weiss' logic CCKbox with the might operator. We introduce a class of models and an axiomatization for CCK, and extend these result to several extensions of CCK.