Cut Elimination in Sequent Calculi with Implicit Contraction, with a Conjecture on the Origin of Gentzen's Altitude Line Construction

Sequent calculi are given in which contexts represent finite sets of formulas. Standard cut elimination will not work if the principal formula of a logical rule is already found in a premiss, i.e., if there is an implicit contraction on it. A procedure is given in which cut with the original cut formula is first permuted up, followed by cuts on its immediate subformulas. It is next adapted to sequent calculi with multisets and explicit contraction, by which Gentzen's mix rule trick is avoided, a procedure strikingly similar to the peculiar "altitude line" construction that Gentzen used in his second proof of the consistency of arithmetic in 1938. The conjecture is close at hand that this is indeed the way Gentzen originally proved cut elimination in 1933.