What is "non-simple applied first-order functional calculus" (60's set theory)

Question

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?

Answer 1

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).