Trouble is, there are completeness results. You can prove everthing that is true in all interpretations of first order logic. The statements that cannot be prov

Trouble is, there are completeness results. You can prove everthing that is true in all interpretations of first order logic. The statements that cannot be proven are unproveable because they are false in a non-standard interpretation of arithmetic. It is the existence of non-standard interpretations that is the big surprise, and the fact that statements are, in a sense, false that blocks proving them. The equation whose roots are the Godel numbers of the proofs that it have no solutions has non-standard solutions. That is why there is no proof that it has no solutions. But the non-standard solution is the Godel number of, err, well what exactly? The trouble with the extra, non-standard numbers is that you cannot reach them by counting, so the proof they number is only finite in the non-standard interpretation. You cannot write it out. It doesn't count because we require that proofs be finite, and by finite we mean finite in the ambient meta-theory, which takes the standard model of the natural numbers. It would be much better to sumarise Godel's theorem as showing that first order logic fails to tie down the nature of infinity. Do we care about non-standard arithmetic? If memory serves, there are proofs that non-standard arithmetic is not computable. I can see why Bernie Madoff might find that convenient, but the rest of us can regard the uselessness of non-standard arithmetic as mathematically proven. Godel's proof shows that first order logic is limited by the existence of mathematical monstrosities that we cannot use (because their arithmetic is not computable) and never encounter (because you cannot reach them by counting)