Hi all! Is there anything like Gödel's constructible universe for New Foundations?

More precisely, I would like a process for taking a model $M$ of NF, and using it to build a model $L \subseteq M$ of NF with the property that every set in $L$ is defined by a (stratified) first-order formula with quantifiers ranging over $M$. (Edited; see the comments for a discussion of some issues surrounding this definition.)

Anything not exactly that, but along those lines, would also be of interest. I would also be interested in hearing about such results for non-well-founded set theories other than NF. Has this been done? Is it possible?

I'm wondering because I am trying to build this sort of constructible model for a naïve set theory that I am studying. I haven't figured out how to apply the methods used for models of ZF to models of naïve set theory. I'm guessing that similar issues might apply in working with NF, because both theories are primarily distinguished by their use of a powerful comprehension axiom.

Thank you!

15more comments