 Hilbert-Ackermann (1938) added to the proof system of second-order logic also two different schemas that they call Axioms of Choice. We are used to thinking of the Axiom of Choice as a set-theoretical principle. But second-order logic has the same situation with choice principles as set theory. It makes perfect sense in second-order logic to ask whether there is a well-order of the domain. The existence of such a well-order does in general not follow from the Comprehension Schema because the well-order may be---and is likely to be---undefinable. So the only way to get a well-order of, say, the real numbers, in second-order logic is to assume some form of second-order Axiom of Choice. The first choice principle is 