По-моему, можно обойтись без нуля и пятью аксиомами:
Ну, если извратиться, то без нуля можно обойтись.
Кроме этого, я бы ввёл именующее понятие: "

- натуральное число" и аксиомы области определения и значений понятий

,

,

:
Что бы это значило? "Именующее понятие" содержится в названии теории, ибо это - "теория натуральных чисел". Стало быть, любой терм этой теории определяет "натуральное число". Никакие дополнительные аксиомы для этого не просто не нужны, а невозможны, ибо в синтаксисе логики первого порядка словосочетание "натуральное число" не предусмотрено.
Меня устраивает и эта система и система аксиом Пеано
Хочу заметить, что, в отличие от арифметики Пеано, эта теория, хотя она и доказывает или опровергает "любые равенства без переменных", тем не менее имеет кучу моделей, не являющихся расширением множества стандартных натуральных чисел.
Ничего подобного. Такая аксиома неочевидна, и полученная система аксиом может быть противоречивой.
Арифметика Пеано тоже "может быть противоречивой". Что же касается очевидности аксиомы, то это - вопрос вкуса. Я, например, полагаю, что длительные безуспешные поиски нечётного совершенного числа - это достаточно убедительное свидетельство его несуществования. Точно так же, как длительные безуспешные поиски противоречия в арифметике Пеано - это достаточно убедительное свидетельство её непротиворечивости. Я не вижу чем одно хуже другого.
В любом случае, я просто
формально следовал Вашему определению: Нашёл теорию, доказывающую утверждение о несуществовании числа, и из её непротиворечивости вывожу истинность данного утверждения о несуществовании.
Другое дело если доказать это утверждение в ZFC или какой-либо другой теории с очевидными аксиомами.
Нет, это "не другое дело". Для меня, например, аксиомы ZFC куда менее "очевидны", чем аксиомы Пеано. А аксиомы бесконечности или выбора, например, кажутся мне менее "очевидными", чем даже аксиома о несуществовании нечётного совершенного числа: Последнее, по крайней мере, пытались найти (и безуспешно), а бесконечное множество даже выписать поэлементно никто всерьёз не пытался.
Гёдель не утверждал, что

истинно или недоказуемо в арифметике Пеано. Он утверждал это при условии, что арифметика Пеано непротиворечива
Он утверждал, что из непротиворечивости арифметики следует и истинность, и недоказуемость

.
А это теорема арифметики Пеано, точнее это утверждение мета-теории можно выразить доказуемым в арифметике Пеано утверждением.
Нет, это не теорема арифметики и это нельзя выразить доказуемым в ней утверждением. Это синтаксически корректное предложение в языке арифметики, и всё.
Почему нельзя сказать, что утверждение о несуществовании решения диофантового уравнения истинно, если существует модель минимальной арифметики, в которой оно истинно?
Потому что как только Вы определите что такое "минимальная арифметика", Вы определите конкретную аксиоматику, к которой и будет привязано Ваше понятие "истинности".