A Gentzen- or Beth-type system, a practical decision procedure and a constructive completeness proof for the counterfactual logics VC and VCS

Source abstract

In [1] and [2] D. Lewis formulates his counterfactual logic VC as follows. The language contains the connectives ∧, ∨, ⊃, ¬ and the binary connective ≤. A ≤ B is read as “ A is at least as possible as B ”. The following connectives are defined in terms of ≤. A < B : = ¬( B ≤ A ) (it is more possible that A than that B ). ◊ A ≔ ¬(⊥ ≤ A ) (⊥ is the false formula; A is possible). □ A ≔ ⊥ ≤ ¬ A ( A is necessary). (if A were the case, then B would be the case). (if A were the case, then B might be the case). and are two counterfactual conditional operators. ( A B ) iff ¬( A ¬ B ). The following axiom system VC is presented by D. Lewis in [1] and [2]: V : (1) Truthfunctional classical propositional calculus.