# 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 E. 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 E. 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.

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.

-

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!

-