If you believe that some model of computation can be expressed in arithmetics (this implies expressibility of the notion of correct proof), Godel's first theorem is more or less analyzis of "This statement cannot be proved". If it can be proved, it is false and there is a provable false statement; if it cannot be proved it is an unprovable true statement.

But most of the effort in proving Godel's theorem has to be spent on proving that you cannot go half way: if you have a big enogh theory to express basic arithmetical facts, you have to have ful... (read more)