A sequent- or tableau-style system for Lewis’s counterfactual logic VC

Abstract

In a 1983 paper, de Swart gave sequent based proof systems for two counterfactual logics: Stalnaker’s VCS and Lewis’s VC. In this paper I demonstrate that de Swart’s system for VC is incorrect by giving a counterexample. This counterexample does not affect de Swart’s system for VCS. Then I give a new sequent- or tableau-style proof system for VC together with soundness and completeness proofs. The system I give is closely modeled on de Swart’s. © 1992 by the University of Notre Dame. All rights reserved.