# Do we know the index of the minimal stage in the constructible universe which is a model of $ZFC$?

A stage in the Constructible Universe, $L_\alpha$, is defined as the union of all $D_\beta$, $\beta<\alpha$, such that $D_\beta$ is the collection of sets from the Von Neumann Universe which are definable, in a precise sense, from sets in $L_\beta$.

It is known that, if $ZFC$ has a well founded model, then there is a minimal $\lambda$ such that $L_\lambda$ is a model of $ZFC$.

### If not, do we have any results pointing to the identity of $\lambda$?

It seems that knowing $\lambda$ would almost immediately give a finitary consistency proof of $ZFC$, at least if $\lambda$ is computable, so I am guessing the answer to the first question is "no", as I have never heard of a finitary consistency proof being available. Nonetheless, I would like some confirmation of this suspicion, hopefully with reference to the literature if at all possible.

EDIT

The comments and answer have discussed what I mean by "know". I mean it in an absolute sense. For example, the proof theoretic strength of Peano arithmetic is $\epsilon_0$. This fact is true in an absolute sense. Maybe we can present an axiomatization of set theory that is consistent with Peano arithmetic having a greater proof theoretic strength, or not having one at all in the sense of proving all ordinals to be well founded. Even if we could do this that would not change the fact that the actual proof theoretic strength, in an absolute sense, is $\epsilon_0$.

I understand that to a pure formalist my question on $L_\lambda$ would seem ill defined. However, I hope I have described what I am asking enough for it to be clear what I am going for.

If I were asking for the proof theoretic strength of Peano arithmetic, I would be looking for $\epsilon_0$, not examples of what strengths are consistent with what first order theories.

Also, it has been pointed out that we could easily define $\lambda$ in an appropriate context. This is true. I am looking for a definition of $\lambda$ that is clear enough to be independent of any contextual axiomatization. For example, $\epsilon_0$ can be defined this way. The Church-Kleene ordinal can even be defined this way, if we accept that computability can be defined this way. I understand that what I am asking for is not exactly formal, but I think it is sufficiently clear.

• In what sense is it "known" that, if ZFC is consistent, then there is an ordinal $\lambda$ such that $L_\lambda$ is a model of ZFC? In the model $L_\lambda$ that you're asking about, isn't it true that ZFC is consistent but there is no such ordinal? – bof Nov 24 '16 at 5:55
• Building on @bof 's comment: Note that the consistency strength of any well-founded set model of $\operatorname{ZFC}$ is strictly larger (assuming its consistency) than the existence of a model of $\operatorname{ZFC}$. So, no... If $\operatorname{ZFC}$ is consistent, then it is consistent that there is no transitive set model at all. – Stefan Mesken Nov 24 '16 at 10:23
• I have added an edit to hopefully describe what I mean by "know" a little better. – Kyle Nov 24 '16 at 15:28

It depends what you mean by "knowing" $\lambda.$

First, you can obviously give a definition for it in set theory: "the least ordinal $\lambda$ such that $L_\lambda\models \mathrm{ZFC}\!"$ (it may or may not exist, of course, but if it does exist, then this is a definition for it).

However, this presumably isn't what you meant. It would be nice to be able to describe a well-ordering of order type $\lambda$ in some nice, simple combinatorial way. Unfortunately, that's probably not possible. In this regard, you asked if $\lambda$ was computable (assuming it exists), and it's certainly not.

A computable ordinal (more commonly known as a recursive ordinal) is the order type of a well-ordering of $\omega$ that happens to be a recursive set (a well-ordering of $\omega$ is a relation on $\omega,$ which is a subset of $\omega\times\omega,$ so it makes sense to ask if it's recursive). Every recursive set is in $L_\lambda,$ so every computable ordinal is in $L_\lambda,$ and, moreover, is a computable ordinal according to $L_\lambda.$ It follows that every computable ordinal is countable according to $L_\lambda.$ In other words, every computable ordinal is less than $\aleph_1^{\,L_\lambda},$ which is in turn less than $\lambda.$

In fact, $\lambda$ is much bigger than the least non-computable ordinal, which is called $\omega_1^{CK},$ the Church-Kleene $\omega_1.$ The argument above already yields that $\omega_1^{CK}\lt \aleph_1^{\,L_\lambda}\lt\lambda,$ but $\lambda$ is even larger than this suggests:

You can characterize $\omega_1^{CK}$ as the least ordinal $\eta$ such that $L_\eta$ satisfies Kripke-Platek set theory (KP), which is a very weakened version of ZF (without the power set axiom, and with separation and collection only for formulas with bounded quantifiers). Your ordinal $\lambda$ is much greater than $\omega_1^{CK}$ because ZF is much more powerful than KP. For example, $A=\{\alpha\lt\lambda\mid L_\alpha\models KP\}$ is an unbounded subset of $\lambda$ and has order type $\lambda;$ this set $A$ is a proper class according to $L_\lambda,$ and the ordinal $\omega_1^{CK}$ is the least member of $A.$

By the way, it's probably worth pointing out explicitly that $\lambda$ is countable if it exists, and that the existence of $\lambda$ is equivalent to the existence of a well-founded model of ZF.

Addendum 1: Here's why $\lambda$ is not a recursive ordinal, and, in fact, is greater than $\omega_1^{CK}:$

Assume $\lambda$ exists. If $\alpha$ is a recursive ordinal, then $\alpha$ is the order type of some recursive (hence arithmetic) well-ordering $W.$ It follows that there is a formula $\phi$ in the language of number theory such that, for all $m, n\lt\omega,$ we have that $mWn$ holds iff $N\models\phi(m,n),$ where $N$ is the model $\langle\omega;+,\cdot;\lt\rangle.$ The model $N$ belongs to $L_\lambda,$ and, for any specific numbers $m$ and $n,$ $N\models\phi(m,n)\iff L_\lambda\models\,"\!\!N\models\phi(m,n)\!".$ So the same definition that we've found defines $W$ in the real world defines, in $L_\lambda,$ the same set $W.$ It follows that $W\in L_\lambda.$

Since $W$ is a well-ordering in the real world, it must be a well-ordering in $L_\lambda$ (every non-empty subset in $L_\lambda$ has a least element, since every subset has a least element).

Now, $L_\lambda\models \text{ZFC},$ so, in $L_\lambda,$ every well-ordering is order-isomorphic to an ordinal. It follows that the order type of $W,$ which is $\alpha,$ belongs to $L_\lambda;$ in other words, $\alpha\lt\lambda.$

You can see that, for any recursive ordinal $\alpha,$ $L_\alpha\models\,"\!\alpha\text{ is a recursive ordinal."}$ (There are two ways of seeing this: (1) Use the fact that the recursive ordinals are the same as the arithmetic ordinals, and we've already seen that $\alpha$ can be defined by an arithmetic formula in $L_\lambda.$ Or (2) Observe that since $W$ above is recursive, we can actually find two formulas $\phi$ as above, one $\Sigma^0_1$ and the other $\Pi^0_1.$ Those same formulas work to define $W$ in $L_\lambda,$ so $W$ is recursive in $L_\lambda,$ and $\alpha$ is still its order type there.)

Moreover, it's actually true that any ordinal $\alpha$ is recursive iff it is recursive according to $L_\lambda.$ (The same argument as above works in reverse: being recursive is equivalent to being definable by certain types of formulas, and those formulas are absolute between $V$ and $L_\lambda.)$

ZF proves that $\omega_1^{CK}$ exists, and it follows from the above that $\omega_1^{CK}$ as computed in $L_\lambda$ is the same as the real $\omega_1^{CK}.$ Therefore $\omega_1^{CK}\lt\lambda.$

I am looking for a definition of $\lambda$ that is clear enough to be independent of any contextual axiomatization. For example, $\epsilon_0$ can be defined this way. The Church-Kleene ordinal can even be defined this way, if we accept that computability can be defined this way. I understand that what I am asking for is not exactly formal, but I think it is sufficiently clear.

Yes, $\varepsilon_0$ can be defined combinatorially like this. However, I would argue that that doesn't apply to $\omega_1^{CK}.$

The ordinal $\omega_1^{CK}$ is a very complicated ordinal; it's easy to lose sight of that fact since it's countable and we give it a short, easy-to-use name.

But there are increasingly complex recursive well-orderings that one can devise, and there is no computable notation for ordinals that includes all the recursive ordinals.

In fact, saying that $\omega_1^{CK}$ is the least non-recursive ordinal is essentially the same as saying that it is the least ordinal $\eta$ such that $L_\eta\models\mathrm{ KP}$ (both specifications are saying, more or less, that it's the least ordinal that you can't reach from underneath by a $\Sigma_1$ formula). This puts that definition on a par with the definition of $\lambda$ as the least ordinal such that $L_\lambda\models\mathrm{ ZFC}.$

If you want to define $\lambda$ in a way closer in spirit to the definition of $\omega_1^{CK}$ as the least non-recursive ordinal, I think you may be able to define it as the least ordinal without a name, where a name is defined inductively as either a symbol for the empty set or a term in the language of set theory with names as parameters, imitating the definition of $L.$ (It's going to be tricky to do this right, making sure that you go through high enough ordinals, and you'll probably run afoul of Tarski's truth theorem if you try to formalize it.) Of course, you can't prove in ZFC that this ordinal exists; $L_\lambda$ is a model of ZFC in which it doesn't exist.

• I have corrected my question based on your comment on well foundedness. – Kyle Nov 24 '16 at 15:37
• @Stefan -- You're right; for some reason, I had thought that OP has mentioned that $\lambda$ was countable, but apparently he didn't state that explicitly, and neither did I. But of course it's true, and when I say that $\lambda$ is much bigger than $\omega_1^{CK},$ it's within the context of countable ordinals -- just as one might say, for instance, that $\omega_1^{CK}$ is much larger than $\varepsilon_0.$ (I've added to my answer to spell out that $\lambda$ is countable if it exists.) – Mitchell Spector Nov 24 '16 at 17:08
• @Kyle I've modified the final paragraph of the answer to say that $\lambda$ exists iff there is a well-founded model of ZF, and that $\lambda$ is then countable. – Mitchell Spector Nov 24 '16 at 17:13
• @Kyle At the end of Addendum 2 in my answer, I've put a way of looking at $\lambda$ that might be something like what you're aiming for. – Mitchell Spector Nov 24 '16 at 18:21
• @Kyle The part about "names" that I quickly added a few minutes ago has problems -- the idea should be workable, but bounded quantifiers aren't sufficient and formalizing it would be problematic because of the undefinability of truth. (For example, it's correct that every member of $L_\lambda$ is definable in $L_\lambda,$ but you can't express that in the form "$L_\lambda\models$ some sentence of set theory.") – Mitchell Spector Nov 24 '16 at 18:48