A normal form theorem for second-order classical logic with an axiom of choice

A cut-elimination theorem for the second-order logic with an axiom of choice of type $0,1$ or $1,1$ is proved. In the first case the Päppinghaus scheme is applied; in the second the calculus with an epsilon-symbol for predicates is used.
Bibliography: 5 titles.