Proof analysis for Lewis counterfactuals (Q2804473)

The authors of this paper together with others have developed a comprehensive study on labelled deduction systems, particularly those of Gentzen's sequential style, so as to cover many non-classical logics characterized by means of relational semantics. The logical aspects of counterfactuals, on the other hand, were studied by R. Stalnaker and D. Lewis mainly in 70's. NEWLINENEWLINEIn this paper, the logic VC of Lewis is formalized in a labelled sequential system. The semantical conditions considered by Lewis are represented in relational terms featuring certain ternary accessibility, and then give rise to logical inference rules in the labelled sequential system along the general approach mentioned above, where a sequent is constituted by labelled formulas (with variables for labels to represent possible worlds) as well as auxiliary atomic formulas (to represent the accessibility, namely, relationship between labels). For the sequent system thus introduced, the structural rules are shown to be admissible by a method established in general setting. In particular, the cut-elimination theorem is proved directly according to invertible principles of other rules. On the base of these observations, the authors show not only a direct proof of completeness, but a finite counter model construction as well according to the saturation of open branch on unprovable sequent, which therefore establishes decidability. Moreover, related literatures and further developments are also discussed in concluding remarks.