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?
Solution 1:
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.
Solution 2:
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.