A Proof-Theoretic View of Basic Intuitionistic Conditional Logic (Extended Version)

TL;DR

This paper develops proof-theoretic frameworks for intuitionistic conditional logic, introducing nested and sequent calculi, and extends existing logics with new operators and models for constructive reasoning.

Contribution

It introduces a nested calculus for IntCK and a sequent calculus for CCKbox, extending Weiss' logic with new operators and providing axiomatizations and models.

Findings

Defined a class of models for CCK

Extended CCK with the might operator

Provided axiomatizations for CCK and its extensions

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 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.