Теорема о нормальной форме для классической логики 2 порядка с аксиомой выбора

Доказывается теорема об устранимости сечения для логики 2 порядка с аксиомой выбора типа $(0,1)$ и $(1,1)$. В первом случае применяется схема Пеппингхауза, во втором используется исчисление с эпсилон-символом по предикатам.
Библиография: 5 названий.