The problem is, is that the Godel sentence is proven in Godel's theorem that it cannot be formally derived in the axiomatic system without making the axiomatic system inconsistent. The interpretation that I've seen of formally derived is that this means that G cannot be proven in the axiomatic system. That is, to prove a theorem is to formally derive this theorem. It says nothing, to me, on whether a mathematical truth can be non-formally derived (or intuitively derived) in a Ramanujan style of mathematics (who largely avoided proofs in his work). Are you sure that Penrose is referring to derived truths versus formally derived truths? It might be possible, I guess, that all mathematical truths are not even derivable from their axioms, but I know of no restriction in Godel's incompleteness theorems that prevent all true theorems from being non-formally derived from their axioms. One possibility is Goldbach's conjecture in number theory (every even interger greater than two is a sum of two primes). We can derive this conjecture from number theory, but we cannot formally derive it (i.e., prove it). The possibility exists that there is a Godelian restriction of proof of Goldbach's conjecture. Perhaps there are many Goldbach conjectures that are true and also undiscoverable, even as conjectures, but I don't know any Godelian restriction in at least discovering the conjecture by 'deriving' them. What do you think?

• I agree - yanniru - September 24, 2003 - 20:58 UTC