If it takes infinite steps to prove a statement, is that a valid proof? In Cantor's diagonal argument, it takes (countable) infinite steps to construct a number that is different from any numbers in a countable infinite sequence, so in fact the proof takes infinite steps too. Is that a valid proof?
 A: First, let's deal with your confusion about Cantor's theorem. Here I find that proving the general case makes it much clearer that there's nothing special about numbers being used.
Let $X$ be a set, let $\mathscr{P}(X)$ be the set of subsets of $X$, and let $f : X \to \mathscr{P} (X)$ be a map. We define a subset
$$C_f = \{ x \in X : x \notin f (x) \}$$
and we observe that $C_f \ne f (y)$ for any $y$ in $X$. Indeed, suppose $C_f = f (y)$. Then, $y \in C_f$ if and only if $y \notin C_f$ – a contradiction. So $C_f \ne f (y)$. We conclude $f : X \to \mathscr{P} (X)$ is not surjective.
I think it is fairly obvious here that we have a finite proof, even though $X$ may be an infinite set. With this in mind, it's easier to see why the proof of the uncountability of the real numbers is a finite one: we don't have to construct the counterexample stage-by-stage in any sense at all – we just define it in one fell swoop like we did with $C_f$. 

Here is a real example of an infinite "proof" that turns out to be invalid. Suppose first-order Peano Arithmetic (PA) is consistent. Then, each of the following statements can be formally proven in PA:


*

*$0$ does not code the proof of an inconsistency in PA.

*$1$ does not code the proof of an inconsistency in PA.

*$2$ does not code the proof of an inconsistency in PA.

*etc.


It is tempting to now claim that PA proves


*

*For all $n$, $n$ does not code the proof of an inconsistency in PA.


but this is in fact false – because it would contradict Gödel's second incompleteness theorem. Essentially this is because the entities $n$ that PA considers to be natural numbers are potentially non-standard; for example, by the compactness theorem for first order logic we can construct an uncountable model of PA, which for obvious reasons must contain non-standard numbers. Thus, we are forced to conclude that the infinitary inference rule


*

*From $\phi (0), \phi (1), \phi (2), \ldots$, deduce $\forall n . \phi (n)$.


is inadmissible for PA.
A: Take the Cantorian diagonal argument that, given a countable sequence of infinite binary strings, there must be a string not in the sequence. To get the argument to fly you don't need to actually construct the anti-diagonal string in the sense of print out all the digits (that would indeed be an infinite task)! You just need to be able to specify the string -- as is familiar, it is the one whose $n$-th digit is 1 if the $n$-digit of the $n$-th string in the countable sequence is 0, and is 0 otherwise. And just from that (finite!) specification, it follows that this specified infinite string is distinct from all the strings on the original list. You don't have to actually, per impossibile, construct (in the sense of write down all of) the string to see that!
It's the same, of course, with the Cantorian argument for e.g. the uncountability of the reals between 0 and 1.
A: Since you have a computability bent, here is another version of Cantor's theorem:
Let $T$ be a Turing machine that prints a sequence of outputs. Each of the outputs of $T$ is the specification of a Turing machine that prints a sequence of numbers.
Cantor's argument says there exists a Turing machine $S$ that prints a sequence of numbers that is not printed by any of the outputs of $T$: specifically the Turing machine:


*

*For every natural number $n$:

*

*Simulate $T$ to obtain it's $n$-th output.

*If $T$ has halted prematurely:

*

*Output 0

*Halt.


*Let $M$ be the $n$-th output of $T$.

*Simulate $M$ to obtain it's $n$-th output.

*If $M$ has halted:

*

*Output 0.


*Else

*

*Let $x$ be the $n$-th output of $M$.

*Output $x+1$




Furthermore, it's not hard to see there exists a Turing machine that can, given the specification of any $T$ satisfying the hypothesis, will output the specification of the corresponding Turing machine $S$.
A: In the usual logic employed in mathematics and in most related systems, a proof has to have only finitely many steps. This means that on the level of the formal, uninterpreted language, a proof has to have only finitely many steps.
But one can use a language in which all proofs are finite to make arguments abut infinitary theories, such as set theory. And the usual language of logic is expressive enough to make infinitary statements in a finite statement. The intuitive conjunction of the infinitely many statements "$1<2$", "$2<3$", "$3<4$", and so on is the same thing as "$\forall n: n<n+1$", which consists of a total of $8$ symbols and is provable in finitely many steps from the axioms of Peano arithmetic.
It is easy to create a finite theory that has only infinite models. For example, it is very easy to axiomatize the theory of strict partial orders without maximal elements with three axioms: 


*

*$\forall x:\neg(x>x)$ 

*$\forall x,y,z:(x<y)\wedge (y<z)\implies (x<z)$

*$\forall x\exists y:x<y$. 


By a standard argument, every finite strict partial order has a maximal element, so this theory describes only infinite strict partial orders.
In set theory, we only use finite proofs and have a countable language. This gives rise to the so called Skolem paradox that a theory dealing with uncountable sets can have a model of countable cardinality. But inside the theory, we can deal with many sizes of infinite and make operations that would correspond to infinitely many operations in a weaker language. And it is the formal language in which set theory is formulated in which all proofs are of finite length.
A: As long as the nature of the steps is formulaic, I see no problem with it. The proof of equal cardinality of Dedekind-infinite sets is similar. To prove that two sets have the same cardinality, you define a bijection that will transform each element of the one set to a unique element of the other, with no "holes", no duplicates and no ambiguities (one element transforming into either of two elements). If such a bijection exists, then one can say that by applying the bijection to each of the (infinite) elements of the source set, a unique element of the destination set is created, and thus the sets have the same number of elements (even though that number is infinite).
