Home| Home |
Metamath Proof Explorer |
| Contents of this page |
God made integers, all else is the work of man.
--Leopold Kronecker |
If we want to consider these as axioms independently of their
set-theoretical
construction, we introduce two classes
(set of complex numbers) and
(set of real numbers); three constants
(zero),
(one), and
(imaginary unit); two binary operations
(plus) and
(times); and one binary relation
(less than). We then assert that these objects have the properties
specified by the axioms below, which we add as an extension to ZFC set theory.
Note that subtraction
and division
are introduced later as definitions.
We later define
natural numbers, integers,
and rational
numbers as specific subsets of
,
leading to the nice relationships
.
Most analysis texts construct complex numbers as ordered pairs of
reals, leading to construction-dependent properties that satisfy these
axioms but are not usually stated as explicit axioms. Other texts will
simply state that is a "complete ordered subfield of ," leading to redundant axioms
when this phrase is completely expanded out. I have not seen a text
with the axioms in the explicit form given here, and an open problem is
whether any axiom on this list is redundant (can be derived from the
others). In particular, I wonder if axioms axrnegex and axrrecex can be derived from the others - does
anyone know?
Interestingly, 0 is redundant. We can introduce 0 as a defined term by considering axi2m1 to be its the definition and replacing 0 with the other side of the axi2m1 equality throughout the other axioms.
| Ref | Expression |
|---|---|
| axcnex |
   |
| axresscn |
 |
| ax0re |
|
| ax1re |
|
| axicn |
|
| axaddcl |
      |
| axaddrcl |
|
| axmulcl |
|
| axmulrcl |
|
| axaddcom |
 |
| axmulcom |
|
| axaddass |
 |
| axmulass |
|
| axdistr |
|
| ax1ne0 |
 |
| ax0id |
|
| ax1id |
|
| axnegex |
  |
| axrecex |
|
| axrnegex |
|
| axrrecex |
|
| axi2m1 |
|
| axlttri |
   |
| axlttrn |
|
| axltadd |
|
| axmulgt0 |
|
| axcnre |
|
| axsup |
 |
In case you are wondering: Why do we use the purple class variables
instead of red set variables? In fact, we can equivalently state these
with red set variables only (which would be more in keeping with
textbook notation) then prove these class-variable versions from them.
You may want to do that if you want a nice conventional presentation of
these axioms for your classroom, book, etc. However, in our formalism
the advantage of a class variable is that we can directly substitute it
with another class expression such as the number "2" or the term
"
".
A set variable would require some logic manipulations to do
this, using theorems such as vtoclg (as used,
for example, to convert eirrv to
eirr).
So for convenience we use class variables outright. On the other
hand a class variable cannot be quantified with
and
,
so for some axioms the red set variables are unavoidable.
Even so, the "simpler" proof is still daunting when worked out in complete formal detail, involving some 39 lemmas. Therefore I will first give an informal description of the proof, then describe the key formal lemmas that lead to the final result, which is theorem ruc (or equivalently ruclem39).
The informal
argument We will start by claiming that
we can list all the reals, i.e. that there exists a function f
from (natural
numbers) onto
(the reals). We will then proceed to construct a real number that is
not in the list f(1), f(2), f(3),... , thereby
falsifying this claim.
Here is how we construct this number. We construct, in parallel, two auxiliary sequences g(1), g(2), g(3),... and h(1), h(2), h(3),... derived from f(1), f(2), f(3),...
We start off by assigning:
g(1) = f(1) + 1Given g(i) and h(i), we construct the next value g(i+1) and h(i+1) as follows:
h(1) = f(1) + 2
If g(i) < f(i+1) < h(i), then assignIn either case, f(i+1) will not fall between g(i+1) and h(i+1).g(i+1) = (2Otherwise, assign
h(i+1) = (f(i+1) + 2g(i+1) = (2
h(i+1) = (g(i) + 2
Now, using elementary algebra, you can check that g(1) < g(2) < g(3) < ... < h(3) < h(2) < h(1). In addition, for each i, the interval between g(i) and h(i) does not contain any of the numbers f(1), f(2), f(3), ..., f(i). This interval keeps getting smaller and smaller as i grows, avoiding all the f(i)'s up to that point. In effect we are constructing an interval of real numbers that are different from all f(i)'s. This is very much like the diagonal argument, but it is much better suited to a formal proof. Just as happens when we add more decimals in Cantor's proof, the sequence g(1), g(2), g(3),... gets closer and closer (converges to) to a real number that is not in the claimed complete listing.
As i goes to infinity, the interval shrinks down to almost nothing. What is left in this shrinking interval? Well, g(i) and h(i) will converge towards each other, from opposite directions, so the interval will shrink down either to a single point or to an empty interval. It is tempting to think that the interval will shrink down to exactly nothing, but in fact it will not be empty, and the formal proof shows this. Specifically, it will contain exactly one real number, which is the supremum (meaning "least upper bound") of all values g(i). How do we know this? Well, it results from one of the axioms for real numbers. This axiom, shown as axsup above, says that the supremum of any bounded-above set of real numbers is a real number. And the set of values g(i) is certainly bounded from above; in fact all of them are less than h(1) in particular.
Contrast this to the rational numbers, where the supremum axiom does not hold. That is why this proof fails for the rational numbers, as it should, since we can make a countable list of all rational numbers. To give you a concrete feel for why the supremum axiom fails for rationals, consider the infinite set of numbers 3, 3.1, 3.14, 3.141, 3.1415... Each of these numbers is a rational number. But the supremum is pi, which is not a rational number.
In Cantor's original diagonal proof, the supremum comes into play as follows. As you go diagonally down the list of decimal expansions of real numbers, mismatching the list digit by digit, at each point you will have a new rational number with one more digit (that is different from all numbers in the list up to that point). The supremum of this list of rational numbers is a real number (with an infinite number of digits after the decimal point) that is not on the list. The statement "all decimal expansions represent real numbers," which is often stated casually and taken for granted, is actually somewhat deep and needs the supremum axiom for its derivation.
The formal
proof
The formal proof consists of 39 lemmas, ruclem1 through ruclem39, and the final theorem ruc.
In the formal proof, the functions f, g, and h
above are called 
, 
,
and 
. A
function value such as f(1) is expressed 
. A
natural number index i is usually expressed as ; you can tell by
the hypothesis such as ruclem.a in ruclem26.
In the hypotheses for many of the lemmas, for example those for ruclem14, we let be any function such that 
, meaning can be any arbitrary mapping from into . We then derive additional
properties that must
have. In particular, we will conclude that no matter what the
function is, it
is impossible for it to map onto the set of all reals.
We also have to
construct the functions and ,
and doing this formally is rather involved. The purpose of the majority
of the lemmas, in fact, is simply to work out that the hypotheses of ruclem14 indeed result in functions and that have the
properties described in our informal argument section above.
What makes it complicated is the fact that and depend not only on but on each other as well. So, we
have to construct them in parallel, and we do this using a
"sequence builder" that you can see defined in df-seq. The sequence builder takes in the
functions and
defined in
hypotheses ruclem.1 and ruclem.2 of ruclem14, and uses them to construct a function
on whose
values are ordered pairs. The first member of each ordered pair
is the value of
and the second is the value of . By using ordered pairs, the sequence builder can
make use of the previous values of both and simultaneously for its internal recursive
construction.
The function , which provides the second argument or "input
sequence" for the sequence builder 
, is constructed from as follows. Its first value
(value at 1) is the ordered pair 
. This provides the
"seed" for the sequence builder, corresponding to the initial
assignment to g(1) and h(1) in the informal argument
section above. The subsequent values at 2, 3,... are just the values of , and these feed the
recursion part of the sequence builder to generate new ordered pairs for
the values of the sequence builder at 2, 3,....
The 
and 
functions in
hypothesis ruclem.2 of ruclem14 return
the
first and
second members, respectively, of an ordered pair.
The 
operation, defined by
df-if, can be thought of as a conditional
expression operator
analogous to those used by computer languages.
The expression 
can be read "if is true then return else return ."
Hypotheses ruclem.3 and ruclem.4 of ruclem14 extract the first and second
members from the ordered pair values of the sequence builder
finally giving us our desired auxiliary functions
,
and
Armed with this information, you should now compare the arithmetic expressions in the hypothesis ruclem.2 of ruclem14 to the ones in the informal argument section above. Hopefully you will see a resemblance, if only a very rough one, that will provide you with a clue should you want to study the formal proof in more depth. By the way, the assertion (conclusion) of ruclem14 shows the first value of the sequence builder. You can see that the ordered pair entries match g(1) and h(1) from the informal argument section above.
Let us now look at the key lemmas for the uncountability proof.
Lemma ruclem26 shows that has an ever-increasing set of
values, and ruclem27 shows that has an
ever-decreasing set of values. In spite of this, the twain shall never
meet, as shown by ruclem32. Lemma ruclem34 defines the supremum 
of the values of
(i.e. the supremum of its range) and shows that
the supremum is a real number. Lemma ruclem35 shows that the supremum is always sandwiched
between and
, whereas ruclem29 shows that this is not true for the
values of .
Lemma ruclem36 uses these last two facts to
show that the supremum is not equal to any value of and therefore not in the list of
real numbers provided by . This means, as shown by ruclem37, that cannot map onto the set of all reals.
We are now in a position to get rid of most of the hypotheses (since
their variables are no longer referenced in the assertion). In ruclem38 we eliminate all but one hypotheses of
ruclem37 by using instances of cleqid. In ruclem39
we get rid of the final hypothesis (using the
weak deduction theorem dedth, involving a quite different application of
the
operator) to result in "there is no function mapping onto the
reals," and finally ruc converts this to the
notation for a strict dominance relation.