 Zermelo’s original form of the Axiom of Choice, AC1, can be expressed as a scheme of sentences within a suitably strengthened version of \(L\). Accordingly we now suppose \(L\) to contain in addition predicate variables \(X\), \(Y\), \(Z\), … and second-order function variables \(F\), \(G\), \(H\), …. Here a second-order function variable \(F\) may be applied to a predicate variable \(X\) to yield an individual term \(FX\).   The scheme of sentences