# 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!

-
@Ben: cs.nyu.edu/pipermail/fom/2012-November/016758.html Randall has a privately circulated manuscript, that he's been editing. He'll most likely send you the latest version if you email him about it. – Andrés Caicedo Dec 28 '12 at 0:24
The second paragraph of the question, beginning "More precisely," isn't exactly what you meant, because it can be satisfied by defining $L$ to be $V$, the whole universe. Your definability requirement is satisfied because you allow parameters from $L$; any set $s$ (in $V$) has a trivial stratified definition with a parameter from $V$, namely $s$ itself: $s=\{x:x\in s\}$. The essence of "genuine" $L$ (as opposed to my phony $L$ defined as $V$) is that the parameters in the definition of $s$ must come "before" $s$, in some (presumably ordinal-indexed) hierarchy. – Andreas Blass Dec 28 '12 at 0:43
Some thoughts on how to approach this or how to make the question more specific. I suspect that there is no "iterative conception" or "predicative view" that makes perfect sense for NF, so $L$ might not be the right idea. However, I think it makes sense to ask whether NF has a some kind of a "prime model." Perhaps there is some extension NF+? such that the (parameter-free) definable elements of a model also model NF+?... – François G. Dorais Dec 28 '12 at 1:21
@Nick: This is addressed in Randall's announcement. If Randall's argument is correct, ZF proves the consistency of NF. In fact, NF is equiconsistent with Mac Lane set theory, which is strictly weaker than Zermelo's set theory, which is strictly weaker than ZF. – Andrés Caicedo Dec 28 '12 at 5:20
@Nick: The idea of eliminating definable parameters in favor of their definitions is not mine. I'm pretty sure it existed before I was born, but I don't know who first used it. My best guess is Tarski, but that's only a guess. I think you can safely refer to it as "well known" in your proof. – Andreas Blass Dec 30 '12 at 1:56

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.