Yeah, I'm very familiar. The 'up to isomorphism' applies to dedekind cuts et al.
I'm pointing out that the nature of R is independent of its definition, and that any mathematical formal system you invent to construct R (up to isomorphism) is just a description. R exists independently on its own.
The constructions of R are useful, because you can show things about them that could be applicable to R.
However, the article gives a rhetorical question of whether you should be able to say 0 is in 3. No you should not, because while there are many constructions of the natural numbers, the universal property they all share (that there is a zero and a successor) does not permit any notion of inclusion. The construction of the naturals as sets would permit such notions, but these are not relevant to any discussion of the natural numbers.
Put in homotopy type theory terms, the natural numbers are the equivalence class of all representations of the natural numbers, and all propositions over the natural numbers are the equivalence classes of all propositions over all representations of the natural numbers.
Since one cannot draw an equivalence between '0 \in 3' and any proposition from another construction of the natural numbers (I believe), then the term '0 \in 3' is not a proposition over the natural numbers.
Put another way, I posit that there are constructions isomorphic to the natural numbers whose propositions cannot be mapped onto the space of all propositions over the construction of the natural numbers as sets. Whereas, all constructions of the natural numbers will permit a proof of the associativity of addition, or the infinity of primes. So these proofs are what should be accepted as 'proofs' over the natural numbers, but '0 \in 3' would not, because it's missing in many systems. '0 \in 3' could be used in the set representation to be the definition of less than, but it is not a statement that applies to all representations.
> I'm pointing out that the nature of R is independent of its definition, and that any mathematical formal system you invent to construct R (up to isomorphism) is just a description. R exists independently on its own.
Isn't that a bit metaphysical and open to interpretation? I would say R only meaningfully exists as defined. A mathematical "truth" is either an axiom or it has a proof?
(Not that I think that makes a difference for the original argument about 1)
I'm pointing out that the nature of R is independent of its definition, and that any mathematical formal system you invent to construct R (up to isomorphism) is just a description. R exists independently on its own.
The constructions of R are useful, because you can show things about them that could be applicable to R.
However, the article gives a rhetorical question of whether you should be able to say 0 is in 3. No you should not, because while there are many constructions of the natural numbers, the universal property they all share (that there is a zero and a successor) does not permit any notion of inclusion. The construction of the naturals as sets would permit such notions, but these are not relevant to any discussion of the natural numbers.
Put in homotopy type theory terms, the natural numbers are the equivalence class of all representations of the natural numbers, and all propositions over the natural numbers are the equivalence classes of all propositions over all representations of the natural numbers.
Since one cannot draw an equivalence between '0 \in 3' and any proposition from another construction of the natural numbers (I believe), then the term '0 \in 3' is not a proposition over the natural numbers.
Put another way, I posit that there are constructions isomorphic to the natural numbers whose propositions cannot be mapped onto the space of all propositions over the construction of the natural numbers as sets. Whereas, all constructions of the natural numbers will permit a proof of the associativity of addition, or the infinity of primes. So these proofs are what should be accepted as 'proofs' over the natural numbers, but '0 \in 3' would not, because it's missing in many systems. '0 \in 3' could be used in the set representation to be the definition of less than, but it is not a statement that applies to all representations.
Is that clearer?