In this set of notes I want to sketch Gödel’s proof that is consistent with the other axioms of set theory. Gödel’s argument goes well beyond this result; his identification of the class of constructible sets eventually led to the development of inner model theory, one of the main areas of active research within set theory nowadays.
A good additional reference for the material in these notes is Constructibility by Keith Devlin.
The idea behind the constructible universe is to only allow those sets that one must necessarily include. In effect, we are trying to find the smallest possible transitive class model of set theory.
is defined as
where for limit, and where
The first question that comes to mind is whether this definition even makes sense. In order to formalize this, we need to begin by coding a bit of logic inside set theory. The recursive constructions that we did at the beginning of the term now prove useful.
I won’t provide full details, but I expect that what follows allows you to fill in the gaps without difficulties.We begin by coding formulas inside set theory. For this, we begin by coding variables. What I mean is, recall that our official list of variables is even though we usually write We need to assign a set to each variable in a way that whenever we want to talk about the variable, we can instead talk about the set. Then we will do the same for all the logical symbols, and use this to code formulas.
One simple way of coding variables is letting the ordered pair code the variable Clearly, there is a formula
that holds of iff codes a variable, namely, states that is an ordered pair, that its first coordinate is 0, and its second coordinate is a natural number.
(Later, we will code some symbols with natural numbers. It is in order to distinguish between these symbols and the variables, that we use rather than simply to code )
It will prove convenient to use constants, to represent sets. We have a constant for each set . We want to code each constant by a set. One way could be to simply let the set act as the constant Unfortunately, this would be ambiguous, as when we have coded a formula by a set , we wouldn’t know whether is coding or the constant , for example. There are other issues as well. For this reason, we choose to code the constant by the ordered pair As before, there is a formula
which holds of iff codes a constant for some
Now that we have coded variables and constants, we can code formulas. We will represent the logical symbols as follows:
and other symbols, are treated as abbreviations.
We begin by coding atomic formulas. Remember that these are formulas of the form or where are either constants or variables. We simply code them by a finite sequence and, in general, we will use finite sequences to represent formulas. The sequence coding where is either or would be where codes , codes , codes , etc. Formally, we see that there is a formula
That holds iff codes an atomic formula: says that is a function with domain that and, for
To code arbitrary formulas, remember that to each we can associate a parsing sequence consisting of the subformulas of listed in such a way that whenever a formula is listed, all its subformulas have been listed before, and that if appears in a parsing sequence, then it is indeed a formula. We can then define
by saying that there is a function with domain some natural number and such that and, for all we have that
or there is a such that
where is the formula coded by (which we can take simply to mean that is a sequence of length that and ), or there are such that
where are the formulas coded by (meaning, is a sequence of length 5, and ), or there is , and a variable such that
where is the formula coded by (meaning, is a sequence of length 3, and ). Any function witnessing we can call a parsing witness for We can then define a class function
that, whenever holds, assigns to the set of free variables of the formula coded by Remember that this means that is a formula of two free variables, that for every there is a unique such that holds, and that if , then is as stated and, as usual, we write rather than The definition of is by recursion, using a parsing witness for . More carefully, we define by recursion, so that if fails, then Otherwise,
- If codes then is if exactly one of is a variable, and that variable is or if and or otherwise.
- If codes and codes then I.e., if and is a formula, then
- If codes and code then
- If codes and codes then
In order to do this, we use a parsing witness for One checks that, no matter what parsing witness is used, is always computed the same way.
We can then define a formula describing satisfiability. This is a formula
which holds iff codes a formula in the language of set theory (i.e., is the only non-logical symbol in , and the free variables of are exactly as shown), is a tuple of elements of , and, letting be the formula resulting from substituting in each free occurrence of by we have
(We may also write or even the admittedly ambguous for )
This definition is by recursion on the complexity of of course. More precisely, the definition refers to a parsing witness for and implements the inductive clauses of Tarski’s definition of truth in models. As before, there ends up being no difference, no matter what parsing witness is used. I omit additional details, but it should be routine at this point to write down in detail both the formula and the formula
The point of all this is that, now that we have a single formula which captures the notion of satisfiability, then we can define by
Note that now that we have a formula describing it follows that “” is also expressible by a formula, i.e., is indeed a class. Clearly, then, if is a set, then so is as
and this is a set, by comprehension.
Remark 1 We have taken advantage in this section of the fact that in set theory, we can directly use functions. Gödel’s incompleteness theorem for Peano Arithmetic begins in very much the same form, by coding logic inside number theory. But Gödel has the additional problem that, in number theory, we do not have functions but only numbers, and so he first needs to device a way of coding finite sequences by numbers.
Once this is done, there is still the problem that there does not seem to be a reasonable way of coding arbitrary models by numbers, so instead Gödel works not with satisfiability but with provability. The possibility of using models directly is another advantage of working within set theory.
Remark 2 On the other hand, although we have a formula that we can use to code all statements of the form for a set and a formula, we do not have a formula that holds of iff codes a formula that is true in This is a somewhat subtle point related to both a theorem of Tarski usually called “undefinability of truth” and to Gödel’s incompleteness theorem.
Although I won’t prove this fact, informally, the issue is that expanding the definition of for a formula with alternations of quantifiers requires itself alternations, so there is no formula that (provably in ) works for all And this is, ultimately, because is a proper class rather than a set.
2. Basic properties of
In this section we present some basic properties of and of the constructible hierarchy that we will require in the proof that The basic facts listed in the theorem below, and the fact that is a model of .
- For all we have
- For all is transitive. Therefore, is transitive.
- For all If then On the other hand, if is infinite,
- Whenever then
- For all In particular, contains all the ordinals.
Proof: We begin by arguing simultaneously by induction that, for all is transitive and for all
This is clear from the definition if is and from the definition and induction, if is a limit ordinal. Suppose now the result for and argue for For this, note that (by induction) it suffices to show that and that is transitive.
Let Then since is transitive. But then
This proves that
Now, if then so and, therefore, This shows that is transitive.
Now we show that for all by induction. Again, this is immediate from the definitions if is 0 or a limit ordinal. At successor ordinals, we have
We argue by induction that if This immediately gives as well that Suppose, then, that (this clearly holds for ). Let Then say
a finite set, since itself is finite. But then
This shows that and we already have the other containment.
On the other hand, if for infinite, then
where the first equality follows from noting that each element of is determined by a formula in the language of set theory (and there are only countably many of them) and a finite tuple of elements of
At limit stages we have that
where the sum indicates the size of a (possibly infinite) disjoint union.
We still need to check that for infinite. This is a consequence of the next item, that if This is because, in particular, it follows that and then of course
To prove the result, we only need to argue that The rest follows by induction. But
By induction, we have and a further inductive argument (looking for the least counterexample) gives that, in fact, But then
That follows immediately, and this completes the proof.
Before we prove that we need a particular case of the reflection theorem:
Lemma 2 Suppose that is a formula. Then there are arbitrarily large ordinals such that
for all tuples
In the situation of the lemma, we say that is reflected down from to .
Proof: This can be established by an argument very similar to the one we used in the notes on the Löwenheim-Skølem theorem. Namely, for and each of its subformulas consider Skølem functions from Let be the set of these Skølem functions. Recall that if is closed under then for any we have that iff
Now, given any we describe an iterative procedure: Let be the closure of under Let be least such that In general, given consider its closure under and let be least such that Now note that if then
is closed under and therefore has the required property. Since was arbitrary, we are done.
We are now ready for the main result of this section:
Theorem 3 (Gödel)
Proof: Extensionality: This follows from transitivity of and extensionality in
Pairing: If then they belong to some Then
Union: If let be such that Then is definable in
Foundation: This follows from transitivity of and foundation in Given there is in a with Since is transitive,
Power set: Given we can let
Note that is a set, as it is the range of a function Let and
Then and i.e.,
Note there is no reason to suspect that is actually the true
Comprehension: Let let be a formula, and let be a tuple of elements of Write for the tuple of constants for in Let
We need to show that It is here that Lemma 2 is useful: Pick large enough so and for any
Replacement: Let be a formula and let be a tuple of sets in such that
Let We need to find a such that
since replacement for then follows by comprehension. Using replacement in , let the unique such that first appears in Then
and we are done.
Choice: Note that since is a model of the formalization of logic inside set theory can be carried out in It then makes sense to talk, for any of i.e., the set that in satisfies the definition of One can easily verify by induction the following two claims:
- For all
- For all
To prove that choice holds in begin by fixing some sufficiently definable enumeration of all (codes for) formulas without constant symbols (so the enumeration is in ). Given let:
- be the least such that
- be the least natural such that is definable over using and some parameters.
We now define with the properties that is a well-ordering of for all and the orders end-extend each other, i.e, and if and then The construction is carried out inside
Once this is done, we can then define a global well-ordering of all of by setting, for
iff either or else say, and
The definition of the orderings is carried out by recursion in and if is limit, Finally, given we define as follows: Given set
- Either or else
- but or
- and but the tuple of parameters in used to define by means of the formula precedes the corresponding tuple for in the lexicographic ordering of tuples induced by
It is straightforward to check that the orderings so defined are indeed well-orderings, and we are done.
Remark 3 One can organize the proof of Comprehension in somewhat more carefully, to avoid the appeal to the axiom of choice implicit in the use of Skølem functions in the proof of Lemma 2. Note that the argument above can then be formalized in since the proof that choice itself holds in does not use the axiom of choice in This establishes Gödel’s result that, if is consistent, then so is
3. The condensation lemma
In this section we sketch the fundamental condensation lemma, the last preliminary result needed in the proof of in The condensation lemma is in turn a consequence of the following basic result:
Lemma 4 (Mostowski collapsing lemma) If is a set and satisfies the axiom of extensionality, then there is a unique transitive set and a unique map that is an isomorphism between and Moreover, is the identity on any transitive subset of
Proof: Suppose that is as wanted. Then, for any with we have Also, if then there must be some such that and we have This means that
By induction on the rank of it follows that there is a unique map defined by recursion by means of the equation above. Letting be the range of it also follows that is unique.
By extensionality, it is routine to check that so defined is injective, and therefore a bijection between and In effect, suppose is of least rank such that there is some distinct from and such that
If there is some then, by definition of we have so (by definition of again) we must have with Since we have But then contradicts the minimality of the rank of A similar contradiction is obtained if
By definition of as the range of we have that is indeed transitive. It remains to verify that is an -isomorphism. By definition, for implies Suppose now that and Since is injective, it follows that and we are done.
That is the identity for any that is already transitive is now immediate.
is usually called the collapsing map, and is the collapse of
The condensation lemma extends the above when is an elementary substructure of an initial segment of by concluding that the transitive set it collapses to, is also an initial segment of
Theorem 5 (Condensation lemma) Suppose is a limit ordinal, and i.e., is an elementary substructure of Then there is a unique and a unique map such that is an isomorphism.
Proof: Begin by checking that To do this, argue by induction on that for all since every element of is definable. In particular, if there is nothing to prove. Now suppose
Note that satisfies the axiom of extensionality, and therefore so does The existence and uniqueness of now follows from Mostowski’s collapsing lemma. Let be the collapsing map.
We want to show that for some But this follows from checking that the construction of can be carried out inside with being the output. Hence, i.e.,
Then and one checks that for all It follows that Since each ordinal of is for some ordinal it is clear that
4. holds in
We conclude the course by showing:
Theorem 6 (Gödel)
Proof: We argue inside (or, if you wish, within the theory ). Let be a cardinal, and let be a subset of There is some such that and it suffices to show that the least such is strictly smaller than Because then and this set has size by Theorem 1.
To see this, let be large enough and a limit ordinal, so that Let be an elementary substructure of of size and such that Let be the transitive collapse of and let be the collapsing map. Note that as and is the identity on since is transitive and Since has size so does so has size Since we are done.
We have thus established that, if is consistent, then so is In particular, this shows that one cannot refute in On the other hand, in 1963, Paul Cohen devised a very powerful method, known as forcing that, in particular, can be used to show that if is consistent, then so are and This provides a concrete example of a natural mathematical statement (namely, ) verifying the incompleteness theorem for set theory.
Typeset using LaTeX2WP. Here is a printable version of this post.
[Edited Dec. 11]
Here I sketch two suggestions for how to avoid appealing to Choice in the proof of the reflection argument:
1. Prove choice in first. This require a bit of care, checking that (without appealing to replacement or comprehension) inside we can organize the proof I presented here. Once this is done, we can define in the Skølem functions we need for the reflection argument. This is fine but it is technically somewhat demanding.
Or we could do as follows, which is easier and feels like the natural approach:
2. Check that one can prove the reflection theorem without appealing to choice. Previously, given a structure and a formula we defined the Skølem function by saying that is the least such that holds in if there is some such and as a previously fixed element of otherwise. (Where “least” is with respect to a fixed well-ordering of ) In we can eliminate the use of choice by being somewhat less careful: Now let be the set of such that holds in where is least such that, if there is some such that then there is some such in The difference is that rather than picking a single witness we are now potentially picking a very large set of witnesses. Of course, if is closed under then if and then there is a such that With this definition, we can now proceed as before.
The (new) notion of being closed is the natural one: is closed under iff for any we have
[Comment by Dan moved from the other site. The formatting is unfortunately ruined, and I could not reconstruct the comment properly.]
Dear Dr. Caicedo,
I’m currently writing my B.Sc. thesis on the constructible universe, and I have a question regarding your proof of the condensation lemma. My question relates to why for all and larger than limit.
As far as I can see, you argue that it’s the case since we can carry out the construction of inside , and therefore get . However, this requires the recursion theorem to hold inside , so that we can argue that for all .
Devlin's constructibility book argues using that the map is uniformly inside for all limit larger than . But the lemma buildup is vast for his case, and if your argument works, then it would be a lot more comprehensible.
Thanks in advance.
Dan, you are right that the sketch I give (“But this follows from checking that the construction of can be carried out inside , with being the output”) leaves out the key issue of uniform definability which, however one presents it, needs careful checking of details similar to what Devlin has to do in his book. This was properly addressed during lecture back when I gave this course, but I never liked the notes I had on the topic, and ended up not posting them.
So there’s apparently no obvious shortcuts I see – I’ll get started on Devlin’s treatment. Thanks for the quick reply!