[lisper]

More concretely: you can add an axiom to standard PA that says, "There exists a number that is the Godel number of a proof of G." The resulting system is consistent, and includes a new kind of number that is not a natural number (because you can prove that N is not a proof of G for any N that is a natural number). It's analogous to adding an axiom that says, "There exists a number whose successor is 0", which introduces a new kind of number that we call "negative numbers." Math is extended in familiar interesting directions like this all the time by adding axioms like "There exists a number whose square is 2" (which gives you irrational numbers) or "there exists a number such that the successor of its square is 0" (which gives you imaginary numbers).

[Y_Y]

You didn't say otherwise, but it's interesting to note that the irrationals is quite "big" in the sense that you can do a lot without them. Not only can you make a nice consistent extension of usual structures on N, Z, Q etc by just adding sqrt(2), you can even add all square roots, or all n-th roots, or the solutions to all polynomials without getting plenty of good irrationals. Sets between Q and R are often neglected, but there's a wealth of good maths in there.