We introduce a new symbol $\lambda$ to denote class-abstractions, and we add the following rule:
if $\phi$ is a formula that use $``\mu"$, and in which the symbol $\sf y$ doesn't occur; then: $\lambda \phi \text { is a term}$.
$\mu$ is a contant symbol.
We stipulate that every $\lambda$-term is not quantified upon, so $``\forall \lambda \phi,\exists \lambda \phi"$ are not parts of formulas of our language. However, they can seep into the quantifiers indirectly if we have them equal to some non-$\lambda$-term, so if we have $\exists x: \lambda \phi=x$ then this $\lambda$-term would be quantified upon implicitly within $\forall s, \exists s$
The expression $\phi^{\sf y}$ means the formula obtained from a formula $\phi$ where $\lambda \phi$ is a term, by merely replacing all occurrences of the symbol $\mu$ by the symbol ${\sf y}$.
The idea of having that particular kind of notation occurred to me after reading this positing, however the notation here is not exactly what's written there. The signature of this logic is still first order + equality and membership symbols + a primitive function symbol $\lambda \phi$ whose arity is the number of free variables in $\phi$, for each formula $\phi$ with the above stated qualification.
Axioms:
Extensionality: $ \forall \vec{w} : \forall {\sf y} (\phi^{\sf y} \leftrightarrow \psi^{\sf y}) \iff\lambda \phi = \lambda \psi $
Comprehension: $\forall \vec{w}: \forall {\sf y} ({\sf y} \in \lambda \phi \iff \phi^{\sf y})$
$\sf Define:$ $set\,\lambda \phi \iff \exists s: s =\lambda \phi$
ٌRepresentation: $ \forall a: a= \lambda (\mu \in a)$
Membership: $ \forall \vec{w} : (\lambda \phi \in \lambda \psi) \to set \, \lambda \phi$
Separation: $ \forall \vec{w} \forall a: set\,\lambda (\mu \in a \land \phi)$
Replacement: $ \forall \vec{w} \forall a: set \,\lambda (\exists x \in a \forall z (\psi(x,z) \leftrightarrow z=\mu))$
We write the rest of axioms of ZF in $\lambda$-terms as:
Pairing: $\forall a \forall b: set \, \lambda (\mu = a \lor \mu = b)$
Union: $\forall a: set \, \lambda (\exists x \in a: \mu \in x)$
Power: $\forall a: set \, \lambda (\mu \subseteq a)$
Infinity: $set \, \lambda (\mu \text{ is a finite ordinal})$
Foundation: $\forall \vec{w} : \exists x \in \lambda \phi \to \exists x \in \lambda \phi \, \forall y \in \lambda \phi \, (y \not \in x)$
To express global choice we need to add a primitive binary relation symbol $\in^* $, denoting "is chosen from", then axiomatize:
$\forall x: \forall y \in^* x \, (y \in x) \land [x \neq \emptyset \to \exists! y: y \in^* x] $
So for any set $A$, the set of all chosen elements from elements of $A$ is $\lambda (\exists x \in A : \mu \in^* x)$.
Also we can have this actually for any class $\lambda \phi$, so we have $\lambda (\exists x \in \lambda \phi : \mu \in^* x)$ being the choice class of any class $\lambda \phi$
I'm introducing this notation, but at the same time I have a question about the above system. I wonder if it is equi-consistent with NBG? The idea here is that all classes (i.e., $\lambda$-terms) that are not sets won't be quantified upon, simply the language here is restricting them from being so. So I think that this restriction would inherently render class comprehension equivalent to that of NBG.
However, generally speaking the language of NBG seems to be stronger than this one. The reason is because it does have class variables that are quantified upon!
I think that NBG theorems about proper classes are not expressible here. Also this system might not be finitely axiomatizable? Hence my question:
Can NBG be interpreted in this system?
Is there a problem in the notation used in this system?
