Normalization as a consequence of cut elimination


Pairs of systems, which consist of a system of sequents and a natural deduction systemfor some part of intuitionistic logic, are considered.For each of these pairs of systems the property that the normalization theoremis a consequence of the cut-elimination theorem is presented.