As I understand it, Gödel and Rosser proved constructively that for any consistent, effectively generated system within which basic arithmetic can be carried out, an infinite amount of statements which can be proven neither true nor false within the system can be generated. The proof involves encoding the systems own axioms ad rules of deduction using properties of numbers. The resulting statement has the form $\neg \exists n:F(n)$ for some primitive recursive F. The crux of the proof is that this statement can be interpreted to state its own undecidability. Such a statement is commonly called a Gödel sentence.
My question is if there are any statements in some formal system which are Gödel sentences which mathematicians were interested in before it was known the statement was a Gödel sentence.
Statements that are undecidable in Peano arithmetic, but can be stated in it and are provable in something larger such as ZF or second-order arithmetic, include $\varepsilon_0$ induction, Goodstein's theorem and the Paris–Harrington theorem. I'm not sure, though, if they can be formatted as Gödel sentences. See also @DanielWainfleet's comment.