Cut Elimination in a Gentzen-Style ϵ-Calculus Without Identity
✍ Scribed by Linda Wessels
- Publisher
- John Wiley and Sons
- Year
- 1977
- Tongue
- English
- Weight
- 725 KB
- Volume
- 23
- Category
- Article
- ISSN
- 0044-3050
No coin nor oath required. For personal study only.
✦ Synopsis
The elegance and simplicity with which sequent calculi can be used to establish important and profound theorems for formal systems is well known. But until recently little use has been made of the powerful GENTZEN approach to explore the properties of HILBERT'S &-calculus. The recent investigations by LEISENRING [4] and MAEHARA [5] in this direction have been hampered by the fact that neither of their systems admits of a Cut Elimination Theorem, a theorem which has in the past proved to be the key to much of the advandage gained in using a Gentzen-style system.2) I n this paper a sequent &-calculus which does admit of a Cut Elimination Theorem will be presented.
A proof of that theorem will be outlined. It will be shown that the consistency of the system follows trivially, as is to be expected. But more interestingly, we shall see that three '&-theorems ', i.e. theorems concerning the relations of derivations in the various subsystems of the ~-calculus, also follow almost trivially. The first two of these are HILBERT'S original first and second &-theorems. HILBERT and BERNAYS' generalization of the first &-theorem can also be proved with the aid of the Cut Elimination Theorem : a proof will be outlined.