Abstract
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 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 variant of might-free CK, which we call ConstCK□→, and an intuitionistic variant of CK, called IntCK. Building on the proof systems defined for CK and for intuitionistic modal logics, in this paper w e introduce a nested calculus for IntCK and a sequent calculus for ConstCK□→. Based on the sequent calculus, we define ConstCK, a conservative extension of Weiss’ logic ConstCK□→ with the might operator. We introduce a class of models and an axiomatisation for ConstCK, and extend these result to some extensions of ConstCK.