publication . Preprint . 1999

On Permuting Cut with Contraction

Borisavljevic, Mirjana; Dosen, Kosta; Petric, Zoran;
Open Access English
  • Published: 10 Nov 1999
Abstract
The 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. It is also shown that in the absence of implication, pushing cut above contraction doesn't pose problems for directly eliminating cut.
Subjects
free text keywords: Mathematics - Logic, 03F05 (Primary) 03B20, 03F07 (Secondary)
Download from

Borisavljevi´c, M. [1997] A cut-elimination proof in intuitionistic predicate logic. Annals of Pure and Applied Logic 99 105-136.

Carbone, A. [1997] Interpolants, cut elimination and flow graphs for the propositional calculus. Annals of Pure and Applied Logic 83 249-299.

Curry, H. B. [1963] Foundations of Mathematical Logic, McGraw Hill.

Doˇsen, K., and Petri´c, Z. [1999] Cartesian isomorphisms are symmetric monoidal: A justification of linear logic. The Journal of Symbolic Logic 64 227-242.

Dyckhoff, R., and Pinto, L. [1997] Permutability of proofs in intuitionistic sequent calculi. University of St Andrews Research Report CS/97/7 (expanded version of a paper in Theoretical Computer Science 212, 1999, 141-155). [OpenAIRE]

Gentzen, G. [1935] Untersuchungen u¨ber das logische Schließen. Mathematische Zeitschrift 39 176-210, 405-431 (English translation in [Gentzen 1969]).

Gentzen, G. [1938] Neue Fassung des Wiederspuchsfreiheitsbeweises fu¨r die reine Zahlentheorie. Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften, N.S. 4 19-44 (English translation in [Gentzen 1969]).

Gentzen, G. [1969] The Collected Papers of Gerhard Gentzen, Szabo, M.E. (ed.), North-Holland.

Girard, J.-Y., Scedrov, A., and Scott, P. J. [1992] Bounded linear logic: A modular approach to polynomial-time computability. Theoretical Computer Science 97 1-66.

Kleene, S.C. [1952] Permutability of inferences in Gentzen's calculi LK and LJ. In: Kleene, S.C. Two Papers on the Predicate Calculus, American Mathematical Society 1-26.

Lambek, J. [1958] The mathematics of sentence structure. The American Mathematical Monthly 65 154-170 (reprinted in: Buszkowski, W. et al. (eds) Categorial Grammar, Benjamins, 1988, 153-172). [OpenAIRE]

Minc, G.E. [1996] Normal forms for sequent derivations. In: Odifreddi, P. (ed.) Kreiseliana: About and Around Georg Kreisel, Peters 469-492.

Szabo, M.E. [1978] Algebra of Proofs, North-Holland.

Zucker, J. [1974] The correspondence between cut-elimination and normalization. Annals of Mathematical Logic 7 1-112. [OpenAIRE]

Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue