I would not recommend believing anything Roger Penrose ever said about computation and/or Godel. His entire book "Emperor's new mind" was insane garbage at the core. Penrose has at various times been brilliant but that book was not it. Here's a fact. A universal turing machine (UTM) is capable of running a program P which will prove that its design indeed represents a UTM. This proof will be valid no matter what input that UTM ever might have. Further, said program P can be proven to be correct, and a verification of said proof could be performed by P itself. (P would be a "verified general-purpose proof-verifier.") This proof will be valid no matter what input might later be given to program P. I suspect that programs of this "self proving" ilk might become important, or even essential, in the future. But right now, most programs are unproven barf, and large programs contain many bugs. And even if self-proving programs become commonplace, that will be no means be a cure-all.
On 5/18/2015 1:10 PM, Warren D Smith wrote:
I would not recommend believing anything Roger Penrose ever said about computation and/or Godel. His entire book "Emperor's new mind" was insane garbage at the core. Penrose has at various times been brilliant but that book was not it.
Here's a fact. A universal turing machine (UTM) is capable of running a program P which will prove that its design indeed represents a UTM. This proof will be valid no matter what input that UTM ever might have. Further, said program P can be proven to be correct, and a verification of said proof could be performed by P itself. (P would be a "verified general-purpose proof-verifier.") This proof will be valid no matter what input might later be given to program P.
So P only proves that the machine it runs on is a UTM and it also verifies that it is correct. But what about the AI program that you want to run on the UTM to operate your robot? If it can do mathematical induction it will run into Goedel's incompleteness. Right? Brent
I suspect that programs of this "self proving" ilk might become important, or even essential, in the future. But right now, most programs are unproven barf, and large programs contain many bugs. And even if self-proving programs become commonplace, that will be no means be a cure-all.
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com https://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun
participants (2)
-
meekerdb -
Warren D Smith