Two measures for proving Gentzen's Hauptsatz without mix

 This paper presents a cut-elimination procedure for classical and intuitionistic logic, in which cut is eliminated directly, without introducing the mix rule. The well-known problem of cut eliminations, when in the derivation the contractions of the cut-formulae are above the premisses of the cut, will be solved by new transformations of the derivation. Received: 1 June 2001 / Published online: 5 November 2002 Mathematics Subject Classification (2000): 03F05 Key words or phrases: Systems of sequents – Cut-elimination theorem