Defunctionalizing Set Theory

First, note that Higher Order Logic has no real need for Set Theory, as you have the ability to quantify over predicates natively. This is not the case in First Order Logic, so a hack is needed to be able to restore this ability.

This is a lot like a Defunctionalization transformation; forming a set stores the "code" of a predicate, and the membership relation $\member:V\to V\to\Omega$ allows us to "decode" a set into a predicate again. Moreover, set builder notation even looks like Closure Allocation! This is analogous to the situation with application in the Untyped Lambda Calculus, but it returns a sort of quote-unquote Continuation $V\to\Omega$ instead of a function $D\to D$ like a Reflexive Object does.

This leads us to some interesting questions: can you somehow Delimit this continuation? Can you somehow reify the call stack as a datastructure (This seems almost related to how CDCL works)? What happens if you add value types ala Call-By-Push-Value?