Labeled Fitch-style natural deduction for basic intuitionistic conditional logic

Abstract

This article presents a labeled Fitch-style natural deduction system, $\mathcal F\mathbf{IntCK}$, for the basic propositional intuitionistic conditional logic $\mathbf{IntCK}$ introduced by G.K. Olkhovikov. The logic $\mathbf{IntCK}$ serves as a correct intuitionistic counterpart to Chellas' minimal conditional logic $\mathbf{CK}$, designed to accommodate Lewis' strong and weak counterfactual conditionals within a single framework. In order to do this, $\mathbf{IntCK}$ features two independent logical connectives, namely $\square\mspace{-7.25mu}\to$ and ◇→, and is interpreted over birelational Kripke semantics with specific confluence conditions linking the intuitionistic and conditional accessibility relations. The $\mathcal F\mathbf{IntCK}$ calculus employs labels, relational atoms, and the notion of labeled quasi-formulas to encode semantic notions and conditions, allowing the construction of derivations that reflect the truth and non-truth of formulas in possible worlds. The system is built upon a subordinate derivation framework, enabling an inductive definition of derivability (in~the~style of V.A.~Smirnov). The inference rules of $\mathcal F\mathbf{IntCK}$ are aligned with semantic principles: structural rules govern relational atoms, while logical rules determine the correct assertibility conditions for connectives, including the two counterfactual operators $\square\mspace{-7.25mu}\to$ and ◇→. Finally, the paper outlines the proof strategies for two metatheorems: weak completeness of $\mathcal F\mathbf{IntCK}$ with respect to the class of all birelational intuitionistic conditional frames and deductive equivalence of $\mathcal F\mathbf{IntCK}$ and $\mathbf{IntCK}$.