Is there a set-based semantics for the untyped lambda calculus? Is there a set-based semantics for the untyped lambda calculus?

As an example, here's a simple set-based semantics for the simply typed lambda calculus (henceforth STLC). It is extremely naive and amounts to little more than an observation that a function from $A$ to $B$ can be represented as a set of pairs. This treatment here sweeps some details under the rug regarding management of free variables in the interest of brevity.
For every ground type $A, B, C \cdots$, we have a sets $A, B, C \cdots$. For each primitive constant and function, we send the symbol to its interpretation. For example if $f$ is a primitive function from $A$ to $B$, the interpretation of $f$ will be a subset of $A \times B$ that is left-total.
Let $\varphi$ be a well-formed formula with free variables $x_1, \cdots, x_n$ of type $A_1, \cdots, A_n$. Let the interpretation of $\varphi$ be a function that sends $v_1, \cdots, v_n$ to the interpretation of $\varphi(v_1, \cdots, v_n)$.
Let the interpretation of $\lambda x : A \mathop. \varphi$ be a function that sends each $a$ in $A$ to the interpretation of $\varphi(a)$.
Let the intepretation of $a(b)$ be the unique value $u$ such that $(b^*, u) \in a^*$ where $a^*$ is the interpretation of $a$ and $b^*$ is the interpretation of $b$.

Attempting to do the same trick for the untyped lambda calculus doesn't work because ZFC is well-founded.
For example, if $X$ is the interpretation of $(\lambda x : x(x))$, then $X(X)$ would have to equal to $X$.
 A: Let's say that you want to interpret λ-terms as elements of a set $U$. Instead of saying that an element of $U$ is literally a function $U \to U$ ­— which would not be well-founded as you mention — you could try to find a bijection $U \cong (U \to U)$. This still fails as it is because $U$ has strictly smaller cardinality than $(U \to U) = U^U$ as soon as $|U| \geq 2$ because of Cantor's theorem. However a variation of this approach can be made to work: consider an isomorphism between

*

*some set endowed with extra structure $U$,

*the collection of structure-preserving maps from $U$ to itself.

The idea is that a "structure-preserving" constraint might exclude enough maps to lower the cardinality of the "function space". A semantics of this kind was first proposed by Dana Scott in 1970 with $U$ being some kind of partially ordered set and the maps being monotone and Scott-continuous; nowadays this is called "domain theory".
(You can generalize "set with structure" by "object in a category" and "structure-preserving map" by "morphism" and then you get what is called a reflexive object in a cartesian closed category.)
