Some evidence for a bold conjecture

Sara has formulated a conjecture or two about the difference between the D and E rulesets. Sara proposed the example to Chris, who proposed looking for a counterexample with the formula

¬¬(((A → B) → C) → (((B → A) → C) → C))

This formula was put forward by Chris as a potential counterexample owing to the way that he thinks of Sara's conjecture: for Chris, Sara is claiming that one can get away without contraction in an intuitionistic sequent calculus. But we know the latter not to be the case, hence one should look at at intuitionistically valid formulas for which every sequent deduction involves contraction. Whence the formula above. It turns out that this is not yet a counterexample to Sara's claim. Here is one strategy discovered interactively for that formula (with the help of some brand new functionality of the dialogical logic software that I've been working on, which will be released soon): In this example, see various cases where the E rule is violated:

• in the left branch at move 15;
• in the middle branch also at move 15;
• in the right branch at move 9.

Each branch contains a violation of E, and there is in fact only one violation in each branch. Sara's conjecture still holds because if we were to chop off each branch the first time a violation of the E rule occurs, we obtain an E-strategy. This doesn't prove Sara's conjecture, of course, but in light of the purported significance of this formula (Chris thought it would turn out to be a counterexample) and its complexity (there are eight connectives appearing in it), this is certainly a satisfying piece of evidence in favor of the conjecture.