13 |
13 |
14 text \<open>The following document presents a proof that the Continuum is |
14 text \<open>The following document presents a proof that the Continuum is |
15 uncountable. It is formalised in the Isabelle/Isar theorem proving |
15 uncountable. It is formalised in the Isabelle/Isar theorem proving |
16 system. |
16 system. |
17 |
17 |
18 {\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In other |
18 {\em Theorem:} The Continuum \<open>\<real>\<close> is not denumerable. In other |
19 words, there does not exist a function @{text "f: \<nat> \<Rightarrow> \<real>"} such that f is |
19 words, there does not exist a function \<open>f: \<nat> \<Rightarrow> \<real>\<close> such that f is |
20 surjective. |
20 surjective. |
21 |
21 |
22 {\em Outline:} An elegant informal proof of this result uses Cantor's |
22 {\em Outline:} An elegant informal proof of this result uses Cantor's |
23 Diagonalisation argument. The proof presented here is not this |
23 Diagonalisation argument. The proof presented here is not this |
24 one. First we formalise some properties of closed intervals, then we |
24 one. First we formalise some properties of closed intervals, then we |
25 prove the Nested Interval Property. This property relies on the |
25 prove the Nested Interval Property. This property relies on the |
26 completeness of the Real numbers and is the foundation for our |
26 completeness of the Real numbers and is the foundation for our |
27 argument. Informally it states that an intersection of countable |
27 argument. Informally it states that an intersection of countable |
28 closed intervals (where each successive interval is a subset of the |
28 closed intervals (where each successive interval is a subset of the |
29 last) is non-empty. We then assume a surjective function @{text |
29 last) is non-empty. We then assume a surjective function \<open>f: \<nat> \<Rightarrow> \<real>\<close> exists and find a real x such that x is not in the range of f |
30 "f: \<nat> \<Rightarrow> \<real>"} exists and find a real x such that x is not in the range of f |
|
31 by generating a sequence of closed intervals then using the NIP.\<close> |
30 by generating a sequence of closed intervals then using the NIP.\<close> |
32 |
31 |
33 theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)" |
32 theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)" |
34 proof |
33 proof |
35 assume "\<exists>f::nat \<Rightarrow> real. surj f" |
34 assume "\<exists>f::nat \<Rightarrow> real. surj f" |