A NORMAL FORM THEOREM FOR SECOND-ORDER CLASSICAL LOGIC WITH AN AXIOM OF CHOICE
G. E. Mints · Mathematics of the USSR-Izvestiya · 1989
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 Pappinghaus scheme is applied; in the second the calculus with an epsilon-symbol for predicates is used. Bibliography: 5 titles.