EMIS ELibM Electronic Journals Publications de l'Institut Mathématique, Nouvelle Série
Vol. 82(96), pp. 37–53 (2007)

Previous Article

Next Article

Contents of this Issue

Other Issues

ELibM Journals

ELibM Home


Pick a mirror



Mirjana Borisavljevic

Saobracajni fakultet, Vojvode Stepe 305, 11000 Beograd, Serbia

Abstract: In a system of sequents for intuitionistic predicate logic a theorem, which corresponds to Prawitz's Normal Form Theorem for natural deduction, are proved. In sequent derivations a special kind of cuts, maximum cuts, are defined. Maximum cuts from sequent derivations are connected with maximum segments from natural deduction derivations, i.e., sequent derivations without maximum cuts correspond to normal derivations in natural deduction. By that connection the theorem for the system of sequents (which correspond to Normal Form Theorem for natural deduction) will have the following form: for each sequent derivation whose end sequent is $\Gamma\vdash A$ there is a sequent derivation without maximum cuts whose end sequent is $\Gamma\vdash A$.

Keywords: cut-elimination theorem; normalization theorem

Classification (MSC2000): 03F05

Full text of the article: (for faster download, first choose a mirror)

Electronic fulltext finalized on: 20 Feb 2008. This page was last modified: 26 Feb 2008.

© 2008 Mathematical Institute of the Serbian Academy of Science and Arts
© 2008 ELibM and FIZ Karlsruhe / Zentralblatt MATH for the EMIS Electronic Edition