  There is just one left rule for conjunction (and dually just one  right rule for disjunction). The left implication rule has what are  called “shared contexts”: the assumptions and cases in  the conclusion, except for the formula with the connective, are  repeated identically in both premisses. Ketonen's idea was to define  a system of proof search: one starts from a given sequent to be  derived, chooses a formula in it, and writes the premisses of a rule  that can conclude the given sequent. By invertibility, the question  of derivability is replaced by one or two equivalent questions of  derivability on simpler sequents. The new rules are needed to ensure  uniquely defined premisses in such “root-first”  decomposition.