To some degree Chaitlin's equations [1] make the issue less abstract than that though.
"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.
There's no single f(x) for which finiteness of the solution set is independent from all axiom systems. (We can always just add an axiom saying f(x) has finitely many solutions.) Chaitin shows something different, an f(x,y) for which finiteness of solution set in x for a given y becomes independent from more and more axiom systems as y grows (because it encodes larger and larger instances of the halting problem). That doesn't disagree with my intuition at all, in fact it seems obvious.
Well given that it was considered a surprising and highly non-trivial result when it came out less than thirty years ago, I'll say that it's obvious only in the sense that all statements that have been proven are obvious after the fact.
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.
"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.
[1] https://www.cs.auckland.ac.nz/~chaitin/berlin.pdf