¬¬(((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.