What's contraction good for?

We are looking for a deductive system for classical propositional logic in which in proof-search (i.e. bottom-up) no duplication ever happens. Contraction is duplication, as is additive context treatment.

If you're used to the sequent calculus, you'll think that we're out of our minds. We're not. By allowing deep inference we can split contraction into two rules, atomic contraction and medial, medial does not duplicate anything. Now how to get rid of atomic contraction? First, notice that we have the cocontraction rule, the dual of contraction, which is collapsing two equals in a conjunction into one when seen bottom up. Now, imagine a contraction of an atom in a proof (say in the sequent calculus). Look at the two copies. Trace their path up to the leaves of the proof. There, they disappear in an axiom, so for each of the two copies, there is a dual atom, the "killer". Trace the path of the two killers down to the conclusion of the contraction. So here we have one victim (the atom that's duplicated) and two killers (the dual atoms that will end up in an identity axiom with the copies). Now, rather than duplicating the victim, and letting each killer kill one copy, we can do the following: not duplicate the victim (remove the contraction) and collapse the two killers into one (by using cocontraction). One killer, one victim, we have a proof in which we have replaced an instance of contraction by cocontraction. Proceed with the remaining contraction instances, done.

The difficulty is in the fact that, in order to collapse the two killers into one, they have to be close together (in the same conjunction). But they could be anywhere. How to bring them together without breaking the proof? We don't know, and the counterexample I present now shows that, in the system we have, this is impossible.

Note that formulae that require the use of contraction in the sequent calculus in order to prove them, e.g. Peirce's law, often can be proved without contraction in KS U {ac^} (cocontraction). But not all of them:

Proposition.  System (KS \ {ac_}) U {ac^} is incomplete.

Proof.  Consider the valid formula
[  ( [a,b] , [-c,(a,b)] )  ,  (-a,-d)  ,  ( [(c,d),-b] , [c,d] )  ]  ,

which I will show to be not provable in the system.

Note that there are three conjunctions, left, middle and right. To simplify the case analysis, note that the formula is symmetric with respect to the comma in the middle conjunction.

Rules ai_ and ac^ don't apply.

Rule aw_ applies in 12 cases, because of symmetry it suffices to check 6, in every case there is a countermodel for the premise.

Medial applies in two cases, for symmetry we just check the one where it applies in the left conjunction. We have two subcases corresponding to two ways in which the medial is applied, in both cases there is a countermodel for the premise.

Switch applies 1) inside the left conjunction (inside the right conjunction is symmetric), 2) bringing together left and middle conjunction (bringing together right and middle is symmetric), 3) bringing together left and right conjunction, and 4) bringing two conjunctions into the third. All these cases have subcases corresponding to the ways in which the switch can be applied. It's tedious but easy to check that for all these cases, there is a countermodel for the premise.

qed.

So, this somehow answers the question in the title. Thanks to Alwen for asking me that question!

Now the next question of course is whether the rules can be changed somehow in order to prove this formula without contraction, and the final question is whether there is a duplication-free system.