Earlier quoted context omitted.
> he resulting system is unsound (in the sense of Tarski) because it asserts the existence of natural numbers that have no "written form" (i.e. the existance of natural numbers that are larger than any term you can write to denote a natural number). Isn't that basically the definition of the natural numbers, ie. if you write down any natural number (say n) I can always construct a natural number that is larger than i…
This surprisingly doesn't mean repeatedly adding 1 will exhaust all natural numbers -- there are models for the natural numbers with elements that can't be reached this way! The ultrafilter construction gives one such model. You take the set of all sequences of natural numbers (n1, n2, n3, ...) then use an ultrafilter to decide which of these sequences are considered to be equal. The usual operations of natural numbe…
It's worth noting that this construction relies on the axiom of choice, so exists in ZFC but not ZF. Generally a lot of counter-intuitive constructions disappear when eliminating the axiom of choice (such as the Banach–Tarski paradox and non-continuous functions).