Abstract

I define the notion of normality for deductions in a Gentzen system for the classical case; I prove the normalization theorem for this notion and I build two direct maps between normal Gentzen deductions and natural deductions in *-normal form, i.e., natural deductions in normal form that also satisfy other conditions. I give the proof of the '*-normalization theorem', i.e. I give a procedure for transforming a normal deduction of →Nc into a unique deduction in *-normal form