Abstract.
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.
Similar content being viewed by others
Author information
Authors and Affiliations
Additional information
Received: 1 June 2001 / Published online: 5 November 2002
Mathematics Subject Classification (2000): 03F05
Key words or phrases: Systems of sequents – Cut-elimination theorem
Rights and permissions
About this article
Cite this article
Borisavljević, M. Two measures for proving Gentzen's Hauptsatz without mix. Arch. Math. Logic 42, 371–387 (2003). https://doi.org/10.1007/s00153-002-0155-x
Issue Date:
DOI: https://doi.org/10.1007/s00153-002-0155-x