There has been some work on building a "set theory" on top of the untyped -calculus, starting with Church's work in the 1930s.
Many interpretations of set theory in terms of -calculus, including Church's original interpretation proceed by defining
Hence,
A system of this sort is presented in [Myhill and Flagg 1989].
Older systems of this sort are mentioned in [Feferman 1984].
Interestingly, in this interpretation it is easy to see that Russell's paradox arises from the Y combinator (by taking the fixed pointed of the function).
In the early 1990s, Klaus Grue proposed map theory, which is a set theory built on top of the untyped -calculus.
The fundamental difference with previous work is that of interpreting as
Myhill, John, and Bob Flagg. “A Type-Free System Extending (ZFC).” Annals of Pure and Applied Logic 43, no. 1 (1989): 79–97.
@article{myhill_1989,
title = {A type-free system extending ({ZFC})},
volume = {43},
pages = {79--97},
number = {1},
journaltitle = {Annals of Pure and Applied Logic},
author = {Myhill, John and Flagg, Bob},
date = {1989},
}
Feferman, Solomon. “Toward Useful Type-Free Theories. I.” Journal of Symbolic Logic 49, no. 1 (1984): 75–111. https://doi.org/10.2307/2274093.
@article{feferman_1984,
title = {Toward useful type-free theories. I},
volume = {49},
doi = {10.2307/2274093},
pages = {75--111},
number = {1},
journaltitle = {Journal of Symbolic Logic},
author = {Feferman, Solomon},
date = {1984},
}