I'm referring to the conditional logic of C+ as described Graham Priest in "An introduction to non-classical logic" chapter 5, where the strict conditional is enhanced with ceteris paribus, and a multiplicity of accessibility relations are defined for various formulae.
The simple tableaux rule for the conditional operator ">" is that:
** GIVEN: ** A > C, i ** ie. "A > C" is the case at world i ** i r_A j ** ie. world i A-accesses j ** ** THEN I CAN ADD: ** A, j **ie. A is the case at world j** C, j **ie. C is the case at world j**
An example of an application of this rule involving a complex antecedent is:
** GIVEN: ** (A or B) > C 0 r_(A or B) 1 ** ie. world 0 (A or B)-accesses world 1 ** ** THEN I CAN ADD: ** (A or B), 1 C, 1
My question is whether I can apply the conditional using this rule in the case of a complex antecedent which is merely entailed by the formulae in the branch, rather than explicit. For example building on the example above:
** GIVEN: ** (A or B) > C 0 r_A 1 ** ie. world 0 A-accesses world 1 ** ** QUESTION: CAN I ADD THIS, since A -> (A or B)? and 0 (A or B)-accesses 1? ** (A or B), 1 C, 1