Penrose redux

In 2006, I posted my thoughts on Roger Penrose's argument that human thought must be noncomputable. Penrose's argument follows from the fact that Godel's incompleteness theorem states that there exist true statements in a consistent formal system (e.g. arithmetic with integers) that cannot be proved within that system. The proof basically boils down to showing statements like "this statement cannot be proved" are true but cannot be proved because if they could be proved then there would be an inconsistency with the system. Turing later showed that this was equivalent to saying that there are problems, known as undecidable or uncomputable problems, that a computer could not solve. From these theorems, Penrose draws the conclusion that since we can recognize unprovable statements are true then we must not be a computer.

My original argument refuting Penrose's claim was that we didn't really know what formal system we were using or whether or not it remained fixed so we couldn't know if we were recognizing true statements that we can't prove. However, I now have a simpler argument, which is simply that no human has ever solved an uncomputable problem and hence has not shown they are more than a computer. The fact that they know about uncomputability is not an example. A machine could also have the same knowledge since Godel's and Turing's proofs (as are all proofs) are computable. Another way of staying this is that any proof or thing that can be written down in a finite number of symbols could also be done by a computer.

An example is the fact that you can infer the existence of real numbers using only integers. Thus, even though real numbers are uncountable and thus uncomputable, we can prove lots of properties about then just using integers. The Dedekind cut can be used to prove the completeness of real numbers without resorting to the axiom of choice. Humans and computers can reason about real numbers and physical theories based on real numbers without actually ever having to deal directly with real numbers. To paraphrase, reasoning about uncomputable problems is not the same as solving uncomputable problems. So until a human being can reliably tell me whether or not any Diophantine equation (polynomial equation with integer coefficients) has a solution in integers (i.e. Hilbert's tenth problem) or always know if any program will ever halt (i.e. the halting problem), I'll continue to believe that a computer can do whatever we can do.