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)$?



Is this set theory used by Gandy first-order with signature $(\in, \lambda)$?
A signature of first order [logic](https://en.wikipedia.org/wiki/Signature_(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)$


