Аннотация:Впервые формальная процедура построения нормальных выводов в сформулированном Г. Генценом натуральном исчислении классической логики предикатов первого порядка была предложена Д. Правицем в [1, гл. III]. Позднее нормализационные теоремы для различных исчислений были сформулированы и доказаны Дж. П. Селдином в [2, с. 628 - 634], Г. Штолмарком в [3], Э. Циммерманном в [4, с. 570 - 574] и некоторыми другими исследователями.
Интерес к проблеме построения нормальных выводов в различных исчислениях обу-
словлен большим количеством возможностей для анализа выводов, предлагаемых проце-
дурой нормализации. Наиболее интересными среди указанных выше работ кажутся иссле-
дования Д. Правица и Г. Штолмарка – в силу того, что доказательства нормализационных
теорем, построенные другими авторами, так или иначе базируются на методе, предложен-
ном Правицем и впоследствии расширенным Штолмарком. Ядро этого метода составляет
ряд процедур, позволяющих строить нормальные выводы, прежде всего, в натуральном
исчислении классической логики высказываний.
В данной работе будет проведен сравнительный анализ способов доказательства нор-
мализационной теоремы, предложенных Д. Правицем и Г. Штолмарком. При этом анализ этой теоремы с точки зрения пропозиционального фрагмента натурального исчисления
классической логики первого порядка кажется достаточным для выявления ключевых
свойств данных способов, их отличительных особенностей и перспектив.