Two measures for proving Gentzen's Hauptsatz without mix

Archive for Mathematical Logic 42 (4):371-387 (2003)

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.
Keywords Legacy
Categories (categorize this paper)
DOI 10.1007/s00153-002-0155-x
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 44,293
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

No references found.

Add more references

Citations of this work BETA

A Connection Between Cut Elimination and Normalization.Mirjana Borisavljević - 2006 - Archive for Mathematical Logic 45 (2):113-148.

Add more citations

Similar books and articles


Added to PP index

Total views
11 ( #694,251 of 2,271,449 )

Recent downloads (6 months)
5 ( #265,242 of 2,271,449 )

How can I increase my downloads?


My notes

Sign in to use this feature