Откуда следует, что у каждого натурального числа (кроме нуля) должен быть предшественник?
Опровергается методом бесконечного спуска.
А вот как опровергается, например, существование неотличимых чисел

?
Почему бы натуральному ряду не оказаться не вполне упорядоченным.
Например, возьмем пару "натуральных" рядов

и

, можно даже записать для каждого совершенно одинаковые аксиомы, но обозначить основания разными символами.
А теперь посмотрим, равны ли эти ряды, а заодно - одни и теже ли множества "натуральных" чисел определяют совершенно одинаковые аксиомы. Просто посмотрим, как эти ряды и соответствующие аксиомы, вообще, можно объединить.
Можно, например, записать

. Заметьте, в данном случае существуют и предшественники нуля и бесконечно большие натуральные числа, хотя ни одной аксиоме это не противоречит, т.к. основания разные. Это противоречит некоторым аксиомам стандартной теории множеств, но кто сказал, что натуральные числа, как они определены в данной теме, должны удовлетворять именно свойствам некоторых множеств ZF(C) ? Абсолютно не обязаны.
В общем, в свойствах, вообще, и чисел в частности, отношения, на мой взгляд, не такие "линейные" и "деревянные", как обычно пытаются представить, оттого и попытки решить в двузначной логике утверждения о некоторых свойствах натуральных чисел не удается. Даже такое простое свойство, как "следовать за…", которое в рассматриваемом случае формализовали символом

не такое уж и простое, как можно увидеть из предыдущего примера.
Так и свойство конечности, хоть и сложное и запутанное, но формализуется, не хуже, чем любое другое свойство или отношение, как, например, красный или больший. Вводится символ, как, например

или

и синтаксические правила его применения, вот и все дела.