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 don't really know what "run into Godel incompleteness" means. The most obvious problem if trying to write something like "an AI" as a proven-correct-program, is what does "correct" even mean? What statement is one trying to prove? But for many subprograms that would be no obstacle. And obviously these programs would be being written by other programs, all smarter than me... But to return to the world I understand... What did Godel prove? Really, his result was basically just Turing's theorem "there exist Turing machines for which it is undecidable whether they halt" all dressed up in math. I.e. you encode the machines as statements in number theory, etc and it transmutes to "there exist statements in number theory which are true, but for which there is no proof." (Historically it did not happen that way, but if it had it would have been simpler.) So what? There exist plenty of programs, which cannot be proven correct, even though they are. So what? If you wanted to fulfil my vision of writing an AI (and it writing better versions of itself, which in turn do so again...) with the programs coming with correctness proofs, then you would not use programs in that nasty class. You would only write programs in the nice subclass of programs that ARE provably correct. And for which you actually have a proof. And this is quite a wide class. Some examples to help illustrate how wide a class it is: By hooking up a counter to a (verified) proof-verifier, you would get a provably correct program that would output every mathematical theorem, with proof. Or would output every provably correct computer program. Or would find a proof or disproof of the Riemann hypothesis (if a proof or disproof exists) otherwise run forever. Another provably correct program exists, which emulates every neuron inside Brent Meeker. So, I mean, the subclass of provably-correct programs is quite a large one. It certainly is large enough to include programs that (if run on a fast enough computer) would pass a "Turing test." Penrose in ENM had nutty notions that since humans solve instances of undecidable problems, that "proves" their neurons work using quantum gravity, and "proves" human brains have super-Turing power and cannot be emulated by Turing machines and "proves" quantum gravity (whatever it is) is beyond understanding by a Turing machine. That all is complete garbage. Penrose simply did not understand the basics of computer science dating from the 1920s or 1930s and made a fool of himself. Because he was such a famous genius, nobody in the publishing house tried to stop him. If I'd tried the same thing (which I wouldn't have since I am not that incompetent) then my manuscript would hopefully have been savagely reviewed and rejected. If you want a little story about the dysfunctionality of science, and/or me: I actually did once write a paper demonstrating that the Navier Stokes equations would (if taken seriously as "laws of physics") enable a physical system to solve the general halting problem in 1 hour. Or certain other equally remarkable consequences. My paper was correct. It was, however, rejected, by a referee who, like Penrose, did not understand what undecidability even was. But like Penrose, he thought he understood it. I then got a computer scientist expert in the decidability area, who'd written a book on that topic and whose office was right down the hall from the editor of the journal, to write a letter saying "referee=idiot, Smith=correct" to that editor. But this failed; my paper was never accepted. The editor wrote to me saying my anonymous referee was a Truly Great Expert and could not be contradicted by any mere computer scientist down the hall from him. The Navier Stokes equations are, however, not the true laws of physics obeyed by real fluids, and that very much matters. Real fluids are made of atoms, for example. Indeed, one can write down truer laws than the NS equations, and prove they are simulable by a Turing machine, even though the NS equations are not.