Is this set theory used by Gandy first-order with signature $(\in, \lambda)$? In On the Axiom of Extensionality, Part II, The Journal of Symbolic Logic, Vol. 24, No. 4 (Dec., 1959),  https://doi.org/10.2307/2963897, pp. 287-300, R. O. Gandy shows that a class theory X containing NBG minus extensionality is not weaker than NBG; X includes a use of class-abstraction denoted with $\lambda$, so that $\lambda x(x=x)$ is a universal class.  Gandy does have identity. It is worth noticing that one can show (use A2 p. 289 and I29 p. 290) that  $x\in \lambda z\phi(z)\leftrightarrow \exists y(x\in y)\wedge\phi(x)$. Is X a first-order theory with signature $(\in, \lambda)$?
 A: A signature of first order logic is usually taken to be a list of extra-logical symbols that range over specific elements (for constants) or over specific subsets (for n+1 ary functions, predicates) of the universe of discourse. The class-abstraction symbol $\lambda$ here doesn't fit into any of those. I'm not sure if it can be considered among symbols of the underlying logic, but by then that kind of logic won't be called just first order, one may call it first order logic with class-abstractions, or something to that effect. That said, I think the signature of Gandy's theory if described in terms of first order logic then it would be very extensive (in agreement with comment by James Hanson), so if $ \{x_i: i \in \mathbb N \}$ is the set of all variable symbols in a langauge, and  $\{\phi_j(x_i): i,j \in \mathbb N \}$ is the set of all formulas in one free variable in the language then the signature would be something like: $(=,\in, \lambda x_i \phi_j(x_i): i,j \in \mathbb N)$, a countably infinite signature! Where each $\lambda x_i \phi_j(x_i)$ is a constant (zero place function) symbol, i.e. an argumentless (doesn't take an element of the universe of discourse as argument) expression that range over a single element of the universe of discourse. However, if $n$ many free variables other than $x_i$ are allowed to occur in $\phi_j(x_i)$, then the expression $\lambda x_i \phi_j(x_i)$ would become an $n$-ary function symbol. In nutshell X is a first order theory with signature $(=,\in, \lambda x_i \phi_j(x_i): i,j \in \mathbb N)$
