I am reading Hofstadter's book GEB and am in a state of being blown away. My universe has just under gone a huge expansion... I now know why people spend their lives studying this stuff. It is staggering. On page 72, Hofstadter quotes a result: "There exist formal systems for which there is no typographical decision procedure." This follows from the result that "There exist recursively enumerable sets which are not recursive." This made me think of Penrose's Platonic mathematical world (The Road to Reality page 20). Lets for a moment assume that this mathematical world exists and that we discover things out of it instead of just inventing math. It would seem that the results quoted in GEB means that some of this Platonic world is inaccessible to us. Correct? Now I studied Canter last year and read a beautiful proof that demonstrated that the are an order of infinity more irrational numbers than rational numbers. The second question is: Are the formal systems for which there exist no typographical decision procedure orders of infinity "larger" (inexact word, but I'm not sure what to use) than the systems where a decision process exist? This seems to be intuitively what should be true but as Hofstadter says, you can't always trust your intuition in such things.