NORMAL FORM THEOREM FOR SYSTEMS OF SEQUENTS

Mirjana Borisavljevic

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)

• Compressed DVI file (32 kilobytes)
• Compressed PostScript file (180 kilobytes)
• PDF file (176 kilobytes)