Если же нет - то, скорее всего, вы, как и я, как и многие раньше и позже, придумали или проверили доказательство этого утверждения в ZF. Можно было взять вместо ZF другую теорию и доказать, что существует бесконечная последовательность Гудштейна.
Существуют модели арифметики Пеано, в которых имеются неограниченно продолжаемые последовательности Гудстейна, то есть, в этих моделях теорема Гудстейна неверна. Где-то мне попадалась статья, в которой такие модели строились.
С арифметикой, на самом деле, то же самое - могут быть какие-то "слишком большие" числа, которые кодируют какие-то странные вещи
Недоказуемость часто связана с какой-нибудь "слишком быстро растущей" функцией. Например, длина последовательности Гудстейна растёт "слишком быстро", поэтому средства арифметики Пеано оказываются недостаточными для того, чтобы доказать, что эта последовательность всегда заканчивается нулём.
Сообщение сверху скорее неудачно отражает следующий вопрос о напрашивающемся различии между как-бы двумя классами аксиоматически/формально недоказуемых предложений. С одной стороны, это класс оригинальных Гёделевых предложений "я недоказуемо", арифметических теорем Рамсея (результат Пэриса - Харрингтона,
https://ru.wikipedia.org/wiki/%D0%A2%D0 ... 0%BD%D0%B0 ) и Гудстейна, диофантова примера неполноты вслед за Матиясевичем (
https://ru.wikipedia.org/wiki/%D0%A2%D0 ... 0%BC%D0%B0 ) и других подобных, видимо "истинных/доказанных" на экспертном, хоть и неформальном, уровне предложений.
У Вас тут какая-то каша.
Прежде всего, в арифметике Пеано невозможно сформулировать утверждение "я недоказуемо" или "арифметика Пеано непротиворечива" (это невозможно ни в какой формальной теории). Всякие утверждения о доказуемости или недоказуемости формул формальной теории принадлежат метатеории, поэтому речь идёт о некоем хитром метаутверждении, которое, будучи определённым образом закодировано, превращается в некоторое арифметическое утверждение, которое, в свою очередь, недоказуемо в арифметике Пеано (деталей я не знаю). Если не знать заранее, что и как закодировано, то мы будем иметь дело просто с некоторой арифметической формулой. Поскольку эта формула недоказуема и неопровержима, то мы можем добавить в список аксиом либо саму эту формулу, либо её отрицание. Однако при этом мы получаем другую формальную теорию, в которой эта формула теряет свой закодированный смысл.
То же относится и к другим указанным Вами примерам. Например, диофантово уравнение, не имеющее решений в одной модели арифметики, может иметь решение в другой. Другое дело, что, возможно, мы никогда это решение найти не сможем (нестандартные модели арифметики неконструктивны).
С другой стороны, накопилось уже множество предложений (аксиома выбора, гипотеза континуума, аксиома детерминации и другие подобные, преимущественно в теории множеств), которые не только недоказуемы (аксиоматически/формально или не), но и неразрешимы в смысле логической непротиворечивости/совместимости их отрицаний/альтернатив с остальными аксиомами (даже древняя проблема параллельных попадает сюда).
В этом отношении "второй" класс ничем не отличается от "первого".
Не был уверен, но естественно ожидать, что такие недоказуемые в арифметике теоремы как Рамсея, Гудстейна и другие (
https://ru.wikipedia.org/wiki/%D0%A2%D0 ... 0%BA%D0%B8 ) можно будет доказать в некоторой подходящим образом аксиоматизированной теории множеств
Упомянутые Вами теоремы доказуемы в ZF. Поэтому ничего изобретать не надо.