Writing infinitely long expressions in set theory

Question

Using just the three symbols {, }, and , we can write any hereditarily finite set as a finite sequence of those three symbols. However, I have thought of something recently. What if we allow infinitely long sequences of those symbols, indexed by ordinals? Then, we can write even more sets than just the hereditarily finite sets. For example, $\{\{\},\{\{\}\},\{\{\{\}\}\},...,\}$ is an infinitely long expression that represents the set containing the empty set, and the singleton of the empty set, and the singleton of that, etc. More formally, it is a sequence of length $\omega + 1$. My real question is, has anyone else talked about this topic in some book or paper or journal article? That is, has anyone else thought about infinitely long expressions that represent certain sets, and developed the theory quite a bit?

Answer 1

This is pretty closely related to infinitary logic, which is extremely well-studied. In particular, for each set $s$ we can give an $\mathcal{L}_{\infty,\omega}$-formula $\varphi_s$ which in $V$ (or indeed in any transitive set containing $s$) picks out $s$ uniquely: this is recursively defined by $$\varphi_s(x)\equiv\forall y(y\in x\leftrightarrow \bigvee_{t\in s}\varphi_t(y))$$ (note that by interpreting the empty disjunct as $\perp$ we don't need a special case for $s=\emptyset$ here). Moreover, the complexity of $\varphi_s$ is closely tied to the complexity of $s$ itself; see this old answer of mine for an example of how this can be used.