How is closure of equality possible for natural numbers on ZFC?

Question

I've recently been delving into axiomatic set theories for the first time, and I've been troubled by the construction of natural numbers with the Peano axioms under ZFC. What I don't understand is how equality can be closed under the natural numbers, when the natural numbers are just an arbitrary encoding.

In other words, if I take the encoding of natural numbers to be $0=\{\}, 1=\{0\}, 2=\{0,1\}, ...$, then why could I not define some other concepts on ZFC as well, say primary colors as $red=\{\{\},\{\}\}, green=\{\{\},\{\{\}\}\}, blue=\{\{\{\}\},\{\{\}\}\}$ in which case $2=\{\{\},\{\{\}\}\}=green$, but green is not a natural number which seems to violate closure on equality. (i.e. $\forall x,y :(x \in \mathbb{N}) \wedge (x=y) \Rightarrow y \in \mathbb{N}$)

Edit: Even though the question is answered, some people still seem to be wondering why this issue was troubling to me so I'll eplain for clarity. In practical use, colors and natural numbers are probably not concepts that would be mixed. However, perhaps a better example would have been $\mathbb N$ and functions $\mathbb N \to \mathbb N$. Now if natural numbers are encoded in the traditional way as listed above and functions encoded in the traditional way, as sets of tuples, then the set {} denotes both the natural number 0 and a function that maps nothing to nothing. Thus any proof using ZFC that used both the notion of natural numbers and functions over natural numbers would violate the peano axioms for natural numbers. Now if you can use a different encoding for either functions or natural numbers that are completely disjoint, then this is not a problem which as @Henning Makholm noted, is always possible. However, without that being always possible any proof under ZFC using both natural numbers and functions would be invalid and since that fact was not obvious to me, I found it troubling.

Answer 1

If you define "$\mathit{green}$" as an alternative name for the set you've already decided to represent the concept of $2$ with, then naturally "green" is a member of $\mathbb N$. This may be a bit confusing, but there's nothing technically wrong with it. It's mathemathics; you're allowed to define names to mean whatever you want.

More to the point, perhaps, if the reasoning you aim to formalize using ZFC depends on $\mathbb N$ and the set of primary colors being disjoint, then it is your responsibility to choose representatives for those concepts that are in fact disjoint.

However, it is more common in everyday mathematics to treat numbers and colors as entirely different kinds of things that never belong in the same set. If the arguments you want to formalize in ZFC follow that convention, then it is not a problem to use the same object to represents concepts of two different kinds. Again it will be up to you to make sure that when you're formalizing something about numbers you're not conflating them with colors and vice versa.

---

The underlying important point here is that axiomatic set theory (in general and ZFC in particular) is a tool that you can use to formalize everyday prose mathematical arguments if you so choose. And it's up to you how you use the tool.

It is quite common for students to get an impression that ZFC is supposed to be "what mathematics really is", and that everything else you've ever learned is just lazy approximations to the "true ZFC reality". This is not a useful viewpoint, and it's not actually shared by many set theorists. In particular, it doesn't tell you anything interesting about ordinary mathematics outside set theory, and doesn't tell you anything interesting about set theory itself either. It's best just to get rid of it as soon as you can.

Answer 2

$\{\{\},\{\{\}\}\}$ is a natural number, regardless of whether you call it "green" or "2". When you work from this foundation, you are defining arithmetic on this underlying set structure, not on the labels, like $1$, $2$ and $3$, which we use for them. It's almost as if you set variables red=1 and green=2 and said red+red=green - which is totally okay.

You might regard that set theory doesn't come built in with any kind of "type safety". Everything's just data, encoded as sets - and, simply inspecting this data doesn't tell you whether its meant to encode a number, a string, or a color.

Answer 3

Given your definitions, the statement that $green \not \in \Bbb N$ is false. Both $green$ and $\Bbb N$ are objects in ZFC that we have given names to. We need to expand the names to the formal objects to check the truth of the statement $green \not \in \Bbb N$. In a similar perverse manner, I could define $0=\{\}, 2=\{0\}, 1=\{0,2\}$ and using my definitions and the usual definition of ordinal addition $1+1=2$ is false.

As your activity indicates substantial computer interest, think about a word in memory. We can interpret it as an unsigned int, an int, a float, some characters, some pixels of a picture, or other ways. Similarly we can give various names to the same set. The only problem comes when we assume that different names refer to the same set. If the word is 32 bits, the bit pattern of $-1$ as a(twos complement) int is the same as the bit pattern of $2^{32}-1$ as an unsigned int.

Even in math, we allow multiple names for the same object. If I write $\forall x \forall y$ (something) it is not guaranteed that $ x \neq y$

The simple answer is that equality is not closed on the naturals. $0,1,2,green$ are names for sets. The names are not formally part of ZFC. I can give a name to any ZFC set I want, and I can give multiple names to the same set. When I write a proof in ZFC I often use abbreviations, like names for sets, that are not part of the formal language. I need to convince the readers that if the argument were expanded into formal ZFC it would hold, or my proof will be rejected. That convincing is not formal mathematics, it is informal. Someone may claim that "You call this $x$ and that $y$. If they are the same object, your proof fails." In the computer arena, this is an argument for strong typing-every variable should come with a prefix that says what type it is and the compiler should reject references that are not of the proper type. This would make the attacks you describe more difficult. I suspect we can prove that it is not sufficient, that the halting theorem says you can get around this.