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