From the last two posts we managed to prove both the existence and the uniqueness of the rationals, which could be done by explicit definitions using known facts about the natural numbers. However, we also showed that the property that distinguished the real numbers from the rationals, namely completeness, couldn’t be defined in first-order logic. This also means that we can’t proceed to prove the existence of the reals in a direct matter as the rationals, and we will do so by indirect means. More specifically, the proof will consist of the following steps, illustrated in figure 1 below:
- Start of with our “rationals”
- Define from another structure which satisfies completeness
- Construct , being dense in , which is isomorphic to
- Find an isomorphic copy of , which satisfies that
- This results in being dense in the complete
- is then our “reals”
Figure 1. Structure of the proof.
But before we state the theorem and get started on the actual proof, we need to get some definitions down:
Definition 1. Let and be linear orderings with . Then is said to be dense in if for every there is such that .
Definition 2. A linear ordering is said to have the supremum property if for every subset , if has an upper bound in , it has a supremum in as well.
The last definition is crucial for the proof and underlines the whole idea of it as well, the notion of Dedekind cuts:
Definition 3. Let be a linear ordering and let be a nonempty proper subset. Then is said to be a left-cut if it satisfies:
Said in words, is a nonempty proper subset of closed to the left and with no right endpoint. We can now state our theorem, which due to Dedekind:
Theorem (Dedekind). Let be a countable dense linear ordering without endpoints. Then there exist such that
- is a dense linear ordering without endpoints
- is dense in
- has the supremum property
Proof. Define and the ordering defined as . We want to prove that this defined fits the demand of the second part of the aforementioned “proof plan”, which is split up into the following three claims:
Claim 1. is a strict linear ordering.
Proof of claim. Irreflexivity and transitivity is trivial from the definition, so we show that the ordering is linear. Let and assume that ; we show . Since , we can pick . Let . Because is a linear ordering, either or . Suppose . Then because is closed to the left, . Suppose instead that . Then because is closed to the left, , contradiction; so . Since was arbitrary, ; being proper because .
Claim 2. has no endpoints.
Proof of claim. Let . Since is a left-cut, and ; so pick and . Define and , which are clearly left-cuts and satisfies . Since has no right endpoint, one can pick such that . Then , meaning ; so is not an endpoint. Since the choice of was arbitrary, has no endpoints.
Claim 3. has the supremum property.
Proof of claim. Suppose is a nonempty subset with an upper bound in . Define . We must show that (i.e. is a left-cut) and that . The following must be satisfied:
- is an upper bound in
- is the least such upper bound.
is clearly nonempty since is. For (2) let . Then is a left-cut and thus . Thus for every , , meaning . Moreover, , since for every there is such that , due to being in some left-cut. (3) and (4) follow analogously. (5) is seen by definition of union, since , meaning . Lastly we show (6), that is the least such. Let be an upper bound for . We must show that . Suppose it is not the case, meaning that by linearity of the ordering. Then we can pick some . Since , is in some left-cut . But then since , , contradiction.
By having found that satisfies completeness, we will now find a substructure , which satisfies . The reason for this is because we cannot be sure sure that . Define then for each the set , and lastly . Now construct the map , which is clearly seen to be an isomorphism by construction of .
Claim 4. is dense in .
Proof of claim. Suppose with , meaning by definition. Now pick . Since is a left-cut, it has no right endpoint, so we can pick such that . Now , making satisfy the condition.
This completes the third point on our proof agenda. As our last task, we would like to construct satisfying . Construct the map by if and for define . First of all, is clearly an injection due to . Also, , since else , contradicting Foundation.
Now, define as and for all , . Now is clearly seen to be the wanted isomorphism.