What is "non-simple applied first-order functional calculus" (60's set theory) Azriel Lévy says in his 1960 paper Axiom Schemata of Strong Infinity in Axiomatic Set Theory, that the $\sf{ZF}$ set theory is formalized with a finite number of axioms in "non-simple applied first-order functional calculus". While this obviously refers to what we today call second-order logic, I am curious what precisely does it mean. I have tried to google the phrase with zero results, Lévy's 1979 textbook doesn't say a word about it either.
What was the reference set theory text book in the late 50's or early 60's?
 A: The functional calculus of first-order is FOL.
For a mathematical logic textbook of early '60s, see:


*

*Alonzo Church, Introduction to Mathematical Logic (1956), page 281:



We shall speak of the pure functional calculus of first order with equality if the primitive symbols include all propositional and functional variables and no functional constants except $I$ [the binary functional letter $I(x,x)$ for equality]; an applied functional calculus of first order with equality if there are other functional constants in addition to $I$ [like $\in$ for set theory]; a simple applied functional calculus of first order with equality 
  if there are other functional constants in addition to $I$ and no functional 
  variables. 

For a set theory textbook, ref [2] in Levy's paper, see:


*

*Abraham Adolf Fraenkel & Yehoshua Bar-Hillel, Foundations of Set Theory (1958): see footnote 3, page 28, with refernce to Church.



The difference seems to be in the axiom of subset; instead of the now "standard" formulation where the condition "specifying" those $z \in x$ such that ... is expressed through an open statement $\varphi(z)$, with $z$ free, as in Fraenkel & Bar-Hillel, the condition is expressed by Levy through a functional variable $p(z)$.
In the first case, we have an axiom schema, while in the second we have a formula.
The functional variable is not quantified (this is why the underlying logic is not FOL), but the logic has a substitution rule (see Church, page 218).
