proving cantors diagonalization proof The Cantor Diagonalization proof seems hard to grasp, and it ignites endless discussions regarding its validity. Also i have been reading similar threads here on stackexchange and im very sorry to keep beating this dead horse. Nevertheless i freely admit that i still do not understand the proof correctly. Also i'm not trying to disprove it.
I want to simplify the proof to its bare minimum, reducing all arbitrary choices, and be able to follow every step, so only cantors conclusion "feels" valid.  As "Anti-Cantor Cranks" never seem to vanish, this seems a reasonable quest. Im willing to completely rework the notation if anything seems unreadable, confusing or "non standard", etc.
As a starting point i want to convert an argument which was shown to me in an attempt to disprove cantors diagonal argument into a valid proof.


*

*Every real number has a decimal representation (Axiom of completeness)

*Also every decimal number has a corresponding binary representation (by construction).

*There is no largest integer 
Now Assume we represent the binary numbers smaller than one as a string
of symbols (0 and 1) with their usual meaning:
$$0.01001 = 2^{-2} + 2^{-5}$$
We can list (all?) integers in increasing order using the usual way to count in binary:
$$\begin{bmatrix}000 \dots 001\\000 \dots 010\\000 \dots 011\\000 \dots 100\\000 \dots 101\\ \dots \\\end{bmatrix}$$
We can also reverse these numbers, to count rationals<1: (where for example 1100 stands for $0.1100 = 2^{-1} + 2^{-2}$)
$$\begin{bmatrix}000 \dots 000 \dots \\100 \dots 000 \dots \\010 \dots 000 \dots \\110 \dots 000 \dots \\001 \dots 000 \dots \\ \dots \\\end{bmatrix}$$
Lets call this matrix $A$.
where we identify each element of the matrix $A[l][c]$ with a line $(l)$ and column $(c)$. 
 Hereby establishing a 1-to-1 mapping between integers $(l)$ and finitely representable rationals (thus no $1/10$) (Thanks Noah Schweber!). We start to count lines and columns beginning with 1. So $010.000$ will be line 3 ($A[3]$), with a "1" in column 2 ($A[3][2]=1$).
This way the first non zero digit in column n will be line $2^n-1$.
Meaning: $A[2^n -1][n]=1$.  $(4)$
The first line where we have n leading 1's (1111..1 ... 000) is A[2^n].
Meaning: for all $1\le i\le n : A[2^n][i]==1$    $(5)$
Which means that line $2^n$ contains the number $n$ in "unary" representation.
Thus we have no "longest" string of 1's.
Okay now lets apply cantors diagonal argument.(Which does not depend on the ordering of A?) We construct the number $d$ by inverting the nth digit in the nth line, placing it in digit n of $d$:
for all n: $d[n]:=1-A[n][n]$.
Since $A[n][n] =0$ for all $n$ (according to $(4)$)
$\implies d[n]=1$ for all n.
So the (well defined) number d(n) is the string 1111...  n one's.
The Matrix A n has for each given n a line consisting of n consecutive 1's: $A[2^n]$. (according to $(5)$).
There is no longest string of one's (according to $(3)$).
Now what is a valid conclusion? 
Is the line (all 1's) contained in A? Probably not, since it would correspond to counting up to the "largest representable  integer" $111\dots111\dots$ (thus contradicting  ( $(3)$ and $(2)$ )
Thank you Noah Schweber for the short axiomatic proof in your replies.
I think its better to reemphasize the crux of the Question:
Since for each n we have a corresponding line in $A$ with $A[2^n]=d(n)$, which is a 1-to-1 mapping between $d(n)$ and $A[2^n]$: Given this observation (and Noahs proof), how can we claim the following: 
Letting n go to infinity we get d=11111... all one's, but the corresponding Entry in A does not exist?
Thanks!
 A: Here's what's going on:
(For simplicity, I'm going to talk about infinite binary sequences rather than real numbers, since the former are slightly easier to handle (the annoyance of the latter being that binary expansions aren't unique: $0.01111111...=0.10000000...$)
You understand correctly the machine Cantor is using: given a "list" $L$ of infinite sequences of $0$s and $1$s (that is: a function $L$ from $\mathbb{N}$ to $\{$infinite binary sequences$\}$), Cantor constructs an inifinite sequence $d(L)$ not on that list.
It's the next step where I think the confusion happens. The existence of $d(L)$ is not, inherently, a contradiction! For instance, let's take the list $L$ you describe, of sequences gotten from "reversing" integers. These are exactly the sequences which have finitely many "$1$"s in them. By definition of $d(L)$, we know $d(L)$ isn't on the list $L$. But that's fine: we never assumed anything about this $L$ that makes this a problem! For instance, precisely because $d(L)$ contains infinitely many $1$s, we know it doesn't "come from an integer", so it shouldn't be on $L$ in the first place.
(Incidentally, you claim that every rational between $0$ and $1$ appears in this $L$ in an appropriate sense. That is false: only the dyadic rationals do so. ${1\over 3}$, for example, does not appear. But that doesn't really matter here.)

So how do you use Cantor's diagonal construction to prove that some set $B$ of infinite binary sequences is uncountable?


*

*First, let $L$ be an arbitrary list of some (maybe all) of the sequences in $B$. 


(Note: again, "list" means "map from $\mathbb{N}$ to $B$".)


*

*We want to find some infinite binary sequence $f$ which is in $B$, but is not on $L$.

*We know that $d(L)$ is not in $L$ . . .

*So we'll be done if we can prove that $d(L)$ is in $B$! Since then we'll have shown that no "list" of elements of $B$ contains every element of $B$.
But this third step is crucial. If we're trying to show that the set of all infinite binary sequences is uncountable, it's trivial, and so we often ignore it: $d(L)$ is an infinite binary sequence by definition! However, let's say you're trying to show that (say) the set of infinite binary sequences corresponding to rationals is uncountable. Then you'd need to prove that $d(L)$ is such a sequence - and here you'd get stuck.

You wanted a step-by-step, axioms-explicit proof. Here it is.
We will prove that - for every "list of infinite binary sequences" (that is, every map $L$ from $\mathbb{N}$ to $\{$infinite binary sequences$\}$), there is an infinite sequence not on the list (that is, an infinite binary sequence $f$ which is not in the range of $L$).
So let $L$ be such a map.
Let $d$ be the infinite binary sequence $$d(n)=1-L(n)(n).$$ We need an axiom to conclude that $d$ exists - something along the lines of "definable binary sequences exist." In ZFC this is handled by the Axiom (scheme) of Separation, but this is wild overkill.
Now for every $n$, we have $d(n)=1-L(n)(n)\not=L(n)(n)$, so $d\not=L(n)$. For this, all we need is that equality works the way it should: if $f=g$, then $f(n)=g(n)$ for all $n$. This is usually built directly into the logic, at a "pre-axiomatic" level, but can be taken as an axiom if you prefer. (Incidentally, the converse - that if $f(n)=g(n)$ for all $n$, then $f=g$ - is less trivial, and has a special name ("Axiom of Extensionality"), but isn't needed here.)
And now . . . we're done! We've shown that $d$ is an infinite binary sequence, and that $d\not=L(n)$ for any $n$; which was exactly what we set out to prove. So any theory which


*

*Can prove basic (really basic) facts about equality, and

*Can prove basic construction principles for sets,
proves that the set of infinite binary sequences is uncountable.
A: First, to dispel some misinterpretations:


*

*Cantor's point was not to prove anything about real numbers. It was
to prove that IF you accept the existence of infinite sets, like the
natural numbers, THEN some infinite sets are "bigger" than
others.

*The easiest way to prove it is with an example set.

*Diagonalization was not his first proof. The example he used in the first proof was, indeed, the real numbers. But the proof was not about real numbers, it was about sets in general.

*In that proof, he used assumed properties about the continuum of real numbers that other mathematicians objected to. The proof was not widely accepted.

*So he put forward a second proof - diagionalization - that specifically did not use real numbers in any way.

*It is not a proof by contradiction, although it is very similar. If what you contradict in a proof by contradiction is what you assumed, it looks an awful lot like circular reasoning. That's why, when diagonalization is presented as one, it sounds phony.


Diagonalization uses what I call "Cantor Strings." They are infinite-length combinations of only two different characters. Cantor used "m" and "w", which I find confusing when printed. You could use "0" and "1", but that is not the same thing as using binary numbers. ("010111111..." and "01100000..." are different strings, but 0.010111111... and 0.01100000... are the same number.)
What diagonalization proves is "If an infinite set of Cantor Strings C can be put into a 1:1 correspondence with the natural numbers N, then there is a Cantor String that is not in C."
But we know, from logic, that proving "If X, then Y" also proves "If not Y, then not X." This is called a contrapositive. So diagonalization also proves "If there is no Cantor String that is not in set C, then C cannot be put into a 1:1 correspondence with the natural numbers N."
