Untyped lambda calculus and set theory

There has been some work on building a "set theory" on top of the untyped \lambda-calculus, starting with Church's work in the 1930s.

Church's interpretation

Many interpretations of set theory in terms of \lambda-calculus, including Church's original interpretation proceed by defining

sets as functions
membership as application
class-formation as abstraction

Hence,

x \in y is interpreted by "y(x) is true" (whatever that means)
\{ x \mid P(x) \} is interpreted by \lambda x. P(x)

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

Grue's interpretation

In the early 1990s, Klaus Grue proposed map theory, which is a set theory built on top of the untyped \lambda-calculus.

The fundamental difference with previous work is that of interpreting x \in y as

\exists u.\ x = y(u)

References

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},
}