Some other people have already shown theorems not provable in Peano arithmetic. For any "formal system" S; consider the assertion C(S) : "S is free of paradox". Proofs can be coded by finite sequences of symbols and the correctness of a proof can be checked by a Turing like machine. If S is strong enough to develop elementary arithmetic C(S) can be formalized in S. A paradox is a contradiction in the theory: i.e. the ability to proof a theorem and its contrary (and in this case we can show that the system can proof everything). Sure that if you consider a formal system S; you "believe" that S is free of paradox; so you believe that C(S) is true but it can be shown that C(S) is non provable in S (by Goedel). Of course since you have no proof you cannot be sure that C(S) is true. This has the consequence that if you want a formal system S in which you can develop all of mathematics; you cannot have a "convincing" proof P that S is consistent (because P would be reproducible in S; in contradiction with Goedel). The usual system that mathematician take to develop mathematics is ZFC (Zermelo Fraenkel set theory with the axiom of choice). Mathematicians "believe" it is consistent but it is exaggerate that they "know" it is consistent. The consistency of ZFC can be proved in stronger systems; say ZFC*; but it does not really help because if you consider ZFC* then you would be interested in the consistency of ZFC*; not ZFC alone and the problem appears again.You know, in all my discussions about Godel's theorem, I've never seen an example of a statement which is well formed and true, but not provable by that system. That would certainly help. I guess the trouble is as soon as you find one, it is immediately added as one of the axioms of a larger system. But that only argues for the definition of axioms to be such that each axiom is so fundamental it cannot be proven by the others. But's that's inherently obvious.