Here's a question that I've long thought to be a puzzle in the history of logic. Perhaps I've been wrong about this, but there doesn't seem to be any reason for Gerhard Gentzen's sequent calculus to make use of sequences of formulae.
Let me try to clarify what I mean here. A sequent, for Gentzen, is a special inference expression connecting a (possibly empty) sequence of antecedent formulae with at least one consequent formula. The system for intuitionistic logic requires just one consequent formula, while the classical system allows a sequence in the consequent. The sequent calculus is then a way of defining classical or intuitionistic logic as a scheme of inferences among sequent expressions rather than the formulae within. Baez and Stay (2009) nicely explain that Gentzen used sequents so he could develop a logical calculus that has the subformula property, which has in turn led to so many useful developments. But that only requires sequent expressions connecting sets of formulae, not sequences of formulae.
I feel there remains the question, why did Gentzen insist that the antecedent and consequent of a sequent be a sequence of formulae? He immediately had to compensate for this by invoking the structural rules, special rules that eliminate the sensitivity of his systems to the sequence structure. He did this, of course, because classical and intuitionistic logic aren't sensitive to the structure of formulae occurring in a sequence. In fact, later authors relying on Gentzen to present classical or intuitionistic logic have frequently just gone ahead and redefined sequents as special expressions connecting sets of formulae, thus doing away with the structural rules. Logicians more recently have played extensively with the logics that result from not using one or more of the structural rules---these are the substructural logics, which are used in type-logical grammar, among other applications. But Gentzen didn't suggest doing away with any structural rules, so far as I know. So then, why did he insist that formulae came in sequences, only to turn around and insert provisions that eliminated this sensitivity? We certainly have to thank him for his odd bit of foresight, given how much fruitful research has been done using substructural logics in recent times.