Now for the simplification of G. It has been shown that whenever you
have a sufficiently powerful formal number theory, and a Godel-
numbering for it, there is a Diophantine equation which is equivalent to G.
The equivalence lies in the fact that this equation, when interpreted on a
metamathematical level, asserts of itself that it has no solutions. Turn it
around: if you found a solution to it, you could construct from it the
Godel number of a proof in the system that the equation has no solutions!
This is what the Tortoise did in the Prelude, using Fermat's equation as his
Diophantine equation. It is nice to know that when you do this, you can
retrieve the sound of Old Bach from the molecules in the air!
(^460) On Formally Undecidable Propositions