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

NORMAL FORM THEOREM FOR SYSTEMS OF SEQUENTSMirjana BorisavljevicSaobracajni fakultet, Vojvode Stepe 305, 11000 Beograd, SerbiaAbstract: 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: cutelimination 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
