Hostname: page-component-6bf8c574d5-mggfc Total loading time: 0 Render date: 2025-02-21T04:35:13.026Z Has data issue: false hasContentIssue false

On permuting cut with contraction

Published online by Cambridge University Press:  01 April 2000

MIRJANA BORISAVLJEVIĆ
Affiliation:
Faculty of Transport and Traffic Engineering, University of Belgrade, Vojvode Stepe 305, 11000 Belgrade, Yugoslavia
KOSTA DOšEN
Affiliation:
IRIT, University of Toulouse III, 31062 Toulouse cedex, France, and Mathematical Institute, P.O. Box 367, 11001 Belgrade, Yugoslavia, Email: kosta@mi.sanu.ac.yu
ZORAN PETRIĆ
Affiliation:
Faculty of Mining and Geology, University of Belgrade, Djušina 7, 11000 Belgrade, Yugoslavia
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

This paper presents a cut-elimination procedure for intuitionistic propositional logic in which cut is eliminated directly, without introducing the multiple-cut rule mix, and in which pushing cut above contraction is one of the reduction steps. The presentation of this procedure is preceded by an analysis of Gentzen's mix-elimination procedure, made in the perspective of permuting cut with contraction. We also show that in the absence of implication, pushing cut above contraction does not pose problems for directly eliminating cut.

Type
Research Article
Copyright
© 2000 Cambridge University Press