Axioms for a Logic of Consequential Counterfactuals

The basis of the paper is a logic of analytical consequential implication, CI.0, which is known to be equivalent to the well-known modal system KT thanks to the definition A -> B = (df) A -> B boolean AND Xi (Alpha, Beta), Xi (Alpha, Beta) being a symbol for what is called here Equimodality Property: (square A equivalent to square B) perpendicular to (square A equivalent to square B) Lambda (lozenge A equivalent to lozenge N). Extending CI.0 (=KT) with axioms and rules for the so-called circumstantial operator symbolized by *, one obtains a system CI.0*Eq in whose language one can define an operator (sic) suitable to formalize context-dependent conditionals (so to counterfactual conditionals) via the definition (Def (sic)) A (sic) B = (df) *A (sic) B perpendicular to Xi (Alpha, Beta)(.). The central problem of the paper is to identify inside CI.0*Eq + Def (sic) a set of axioms yielding the fragment consisting of all and only theorems in which only truth-functional operators and the two operators -> and (sic) occur. This system, here called CI.0, is introduced in 3. In view of the intended purpose, it is introduced a complete and tableau-decidable system KTw, which is an extension of KT with axioms for the so-called quasi-variables w(A), w(B) horizontal ellipsis Three translation functions among the three languages used in the paper are then introduced. The first, Tr, maps every wff of form *A into wffs of form w(A) perpendicular to A and translates theorems of CI.0*Eq into theorems of KTw. The second, t degrees, translates theorems of CI.0 into theorems of CI.0*Eq by applying Def(sic). A third one, t, translates theorems of CI.0 >> into theorems of KTw. As a consequence, it follows that t degrees A = TrtA. In 4 it is proved that CI.0 >> is complete w.r.t. the class of CI.0-models of form < W, f, R,V > where f is a selection function and R an access relation. It is then proved (i) that CI.0 >> models may be converted into KTw-models; (ii) that the truth-value of a proposition in a world of a CI.0 >>-model is preserved in the same world of the derived KTw-model; (iii) that A is a CI.0 >>-thesis iff its translation tA is KTw-thesis. It follows that, if A is not a CI.0 >>-thesis, tA is not a KTw-thesis, so also that TrtA is not a CI.0*Eq-thesis. Since t degrees A = TrtA and t degrees A is a function built on Def(sic), this proves that every t degrees-translation of a CI.0 >>-wff that is a CI.0*Eq-theorem is a CI.0 >>-theorem. Since the converse proposition is proved in 2, their conjunction establishes the desired result. In the final section, it is proved that CI.0 >> is tableau-decidable, that (sic) is not a trivial operator and that (sic) enjoys the positive and negative properties required in 1 for context-dependent conditionals. Some final remarks suggest that studying the relations between CI.0 >> and systems of classical conditional logic may be a promising line of investigation.