A natural sequent calculus for Lewis logic of counterfactuals
Nicola Olivetti, Gian Luca Pozzato · Institutional Research Information System University of Turin (University of Turin) · 2015
The logic V is the basic logic of counterfactuals in the family of Lewis' systems.It is characterized by the whole class of so-called sphere models.We propose a new sequent calculus for this logic.Our calculus takes as primitive Lewis' connective of comparative plausibility : a formula A B intuitively means that A is at least as plausible as B, so that a conditional A ⇒ B can be defined as A is impossible or A ∧ ¬B is less plausible than A. As a difference with previous attempts, our calculus is standard in the sense that each connective is handled by a finite number of rules with a fixed and finite number of premises.Moreover our calculus is "internal", in the sense that each sequent can be directly translated into a formula of the language.The peculiarity of our calculus is that sequents contain a special kind of structures, called blocks, which encode a finite combination of .We show that the calculus is terminating, whence it provides a decision procedure for the logic V.