"We outline our construction of a single equation involving only addition, multiplication, and exponentiation of non-negative integer constants and variables with the following remarkable property. One of the variables is considered to be a parameter. Take the parameter to be 0, 1, 2, ... obtaining an infinite series of equations from the original one. Consider the question of whether each of the derived equations has finitely or infinitely many non-negative integer solutions. The original equation is constructed in such a manner that the answers to these questions about the derived equations are independent mathematical facts that cannot be compressed into any finite set of axioms."
So there are finite (though several hundred pages long) equations for which the finiteness of the solution set is independent of every finite axiomatization of arithmetic. So suddenly, even though the formula is enormous, the type of sentence is perfectly normal. Does f(x) have finitely many solutions, where f(x) is built from addition, multiplication and exponentiation.
Much more so than Gödel’s incompleteness this deeply violates my intuition about what type of statements should be decidable.
And yes, I worded that ambiguously. Let me rephrase, to see if I got it correct: Pick any finite axiomatization. Then there is a concrete f(x) that we can write down in about 200 pages, for which finiteness of the solution set is not decidable.
The fact that there are diphantine equations for which finiteness is undecidable is really surprising to start with to me.
~(Ex)Proof(x, ~0=0)
I.e., "There doesn't exist a proof of ~0=0."
Of course, representing the word "proof" using PA isn't trivial, and expanding that bulks things up a bit. But the sentence that's really long is the Godel sentence. "(G) There is no proof of G."
Also, the comment about size and diagonalization is interesting. The Gödel sentence from the first incompleteness theorem is made by diagonalizing, while the sentence from the second incompleteness theorem is just "Con(T)", so the sentence from the 2nd theorem is shorter and more natural if written out in full---making it even more disappointing that it's not provable. Indeed, if we put in more work we should be able to prove a more interesting theorem, but I never really thought about it before.
[1] http://mathoverflow.net/questions/66776/alternative-arithmet...
Let's say your beliefs about the integers can be summarized by some formal theory T. ("Every number has a successor", and so on, until your intuition runs out of things to say.) Now Godel jumps out of the bushes and says aha, your T doesn't include Con(T), so you aren't the math genius that you thought you were!
But let's stop for a moment and consider what it would take for T to include Con(T). First of all, compared to other sentences about integers that you believe, Con(T) is an absolutely huge sentence. It must contain an arithmetization of all of T (encoding the axioms, inference rules, etc. into integer arithmetic).
Second of all, if Con(T) is included in T while speaking about T, it might need to include an arithmetization of Con(T) itself! That uses a diagonal construction ("quine" in computer science terms), making the sentence even bigger. Now you're looking at some kind of hundred-kilobyte Diophantine equation, with no intuitive reason to believe it at all.
And third of all, it's easy to see that an inconsistent theory T would easily prove Con(T) (because it proves any sentence), so having Con(T) inside T doesn't even give you any positive evidence for trusting T. In fact, we're lucky to live in a world where Godel's theorems are true, and having Con(T) inside T is negative evidence instead of none at all!