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.
