Constructible models of New Foundations? 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!
 A: My impression is that a reconstruction of L in NF is not very
satisfactory.  One version of L's construction, following Jensen, is to take the
rudimentary set functions and iterate them under composition and unions along 
the (von Neumann) ordinals.  However not all the rudimentary functions can be given a stratified definition.  Thomas Forster remedies this and defines a list of strat.rud. functions and mimicks the Jensen process using these to build a strat.rud. closed model S.  However choice fails in S, but more significantly, S has a canonical wellorder (that of construction) but initial segments of the graph of this well order are only unstratified, and thus are not in S. In short the model S cannot "construct itself" in the way that "V=L" is shown to hold in L. Worse still, there is no total order even of $V_\omega$ (let alone a wellorder) in S.
The problem seems to be that one can iterate the strat.rud functions along wellorderings, but there is no way in general to compare the results: one does not have in general a Mostowski-Shepherdson Collapsing Lemma in NF to "transitivize and compare" the differing hierarchies so produced, because there is insufficient induction. (The latter problem would seem to raise its head whatever version of L's construction one used.)
Forster's article is in Contemporary Mathematics, vol 36, 2004. You may want to check out his webpage, which lists publications of himself and his research group. Dang's thesis to be found there (I think) looks to be relevant.  
A: You can't do it for NF, but there is a good notion of constructible model of the theory CUS of Church, that has a universal set.   But that's really just a trick of the light, since the big sets of CUS are magicked into existence by a coding trick.  None of that is in print, so there is nothing i can cite.  Sorry!
