rej@cornell.UUCP (Ralph Johnson) (02/11/84)
From: rej (Ralph Johnson) To: net-ai Subject: Undecideability BEGIN QUOTE Fermat's Last Theorem, Goldbach's conjecture, the Four Color Theorem (or Conjecture) and others of that type which can be disproved by a single counterexample can not be undecidable propositions in mathematics. Suppose Fermat's Last Theorem were undecidable. Then there cannot be a counterexample (four positive integers x,y,z > 0 and n > 2) such that x**n + y**n = z**n. Consequently Fermat's Last Theorem is true. Thus the assumption of undecidability of this individual statement implies that the statement is true. The assumption that Fermat's Last Theorem is undecidable and false is a contradiction. The assumption that Fermat's Last Theorem is decidable does not contradict either the falsehood or the truth of the Theorem. Paul Vitanyi END QUOTE Suppose that it were undecidable that a program never halts. Then there cannot be a counterexample (an execution trace in which the program halts). Consequently the program does not halt. Thus, the assumption of undecid- ability of this individual statement implies that the statement is true. All computer scientists should know that, in fact, the halting problem is undecidable. What is wrong, then, with the plausible sounding argument outlined above? The problem is that undecidabilty does not question whether something is TRUE or FALSE, only provable or disprovable. Since provability is always in reference to a particular proof system, something that is undecidable in one system may be decidable in another. As a matter of fact, if we can prove (in system S1) that theorem T is undecidable in system S2, then T is decidable in system S1. That is why the so called undecidable theorems are so interesting; nobody knows whether they are undecidable. If they knew for sure (by inventing a new proof system, and using it to show that the theorem is undecidable in the old proof system) then they would know whether or not the theorem was true. (Note that I am assuming that proof systems are "true", a dubious idea.) Classically, any mathematical statement is either true or false. Constructive mathematicians prefer to think about proved or disproved instead, and many mathematical statements are neither. Decideability is thus more a part of constructive mathematics than classical math. As a side note, the Four Color Theorem has been proved, thus it is not undecidable. However, the first proof was computer generated (over a thousand pages, I believe). The problem was broken down into a thousand or so cases, and each case was mechanically proved. Naturally, nobody read the proof. Later, a shorter proof was found, using ideas derived from the first. The shortest proof is still quite long, but the problem is generally supposed to be solved. Ralph Johnson