То есть, по сути, утверждение об однозначности арифметики второго порядка истинно, но не доказуемо?
Хм. Я понимаю, что практически это и сказал, но всё-таки это не совсем то, что я хотел сказать.

Вся тонкость в том, что считать легитимным доказательством. С формальной точки зрения, если принять за аксиому, что "драконы существуют", то это сразу станет "доказуемым фактом". Однако ж такое доказательство не очень убедительно...
С арифметикой второго порядка ситуация примерно такая: То, что у неё единственная модель, следует практически из её же собственной аксиоматики (аксиома индукции примерно это и утверждает). В этом смысле однозначность определения натуральных чисел конечно доказана. Вот только это доказательство (как и доказательство существования драконов) не является конструктивным. Т.е. вполне может оказаться так, что для некоторого конкретного объекта невозможно будет ни доказать, ни опровергнуть, что он является натуральным числом.