soft question - Theorems with unexpected conclusions

My favorite example of this phenomenon is Goodstein's Theorem.

Take any positive number a₂, such as the number 73, and write it in complete base 2, which means write it as a sum of powers of 2, but write the exponents also in this way.

• a₂ = 73 = 64 + 8 + 1 = 2²²⁺² + 2²⁺¹ + 1.

Now, obtain a₃ by replacing all 2's with 3's, and subtracting 1. So in this case,

• a₃ = 3³³⁺³ + 3³⁺¹ + 1 - 1 = 3³³⁺³ + 3³⁺¹.

Similarly, write this in complete base 3, replace 3's with 4's, and substract one, to get

• a₄ = 4⁴⁴⁺⁴ + 4⁴⁺¹ - 1 = 4⁴⁴⁺⁴ + 3 4⁴ + 3 4³ + 3 4² + 4 + 3.

And so on. The surprising conclusion is that:

Goodstein's Theorem. For any initial positive integer a₂, there is n > 2 for which a_n = 0.

That is, although it seems that the sequence is always growing larger, eventually it hits zero. So our initial impression that this process should proceed to ever larger numbers is simply not correct. The proof of Goodstein's theorem uses transfinite ordinals to measure the complexity of the numbers that arise, and proves that this complexity is strictly descending with each step. Thus, it must hit zero, and the only way this happens is if the number itself is zero. One can see that we had to split up the complexity of the number somewhat in moving from a₃ to a₄, although even in this case the number did get larger. Eventually, the proof goes, the complexity drops low enough that the base exceeds the number, and from this point on, one is just subtracting one endlessly.

This conclusion is very surprising. But this theorem actually packs a one-two punch! Because not only is the theorem itself surprising, but then thee is the following surprise follow-up theorem:

Theorem. Goodstein's theorem is not provable in the usual Peano Axioms PA of arithmetic.

That is, the statement of Goodstein's theorem is independent of PA. It was a statement about finite numbers that is provable in ZFC, but not in PA.