ZFC and apples described using only fundamental axioms (complete expanded reasoning)

Question

Let's assume that I'm adding two numbers representing my count of objects I perceive (lets say a green and a blue apple that are consider to be of the same class) and I see them as a set of two apples and, with my mathematical background, I would be limited to this language:

1+1=2

1) Given that I base my observation and perception in accordance to assumed axioms of ZFC, how would I describe the above in a formally correct set of statements using accepted symbolic language? I.e. using the union symbol (∪)

2) The next thing I want to know is how I can expand the statement using a more generic symbolic language where I am forced also to replace ∪with its axiomatic definitions assuming that I understand logic and share the assumption that things can exist. I assume that this is possible as I understand the ZFC is built on axiomatic reasoning on top of some simple assumptions shared by most mammals (things can exist etc. etc.).

The reason I'm asking is that I find Set Theory appealing to begin to learn the language you guys use (i.e. mathematics).

NOTE

I'm looking for the complete chain of reasoning (including the axioms defining the union itself). For the difference in colours, I simply meant that I could identify each apple as being two different things in existence. The notion of them both being apples is because it would make sense that I would be able to expand 2 into a set representing both apples and then expand it into the complete rigorous axiomatic definition of the set using only formal logic and the assumption that two items actually exist as separate identifiable entities.

Answer 1

Let us formalize the following proposition.

Prop. Suppose $R$ and $G$ are disjoint singleton sets. Then $|R \cup G|=2$.

The first step is to get rid of all the function symbols:

Prop 0. Suppose $R$ and $G$ are disjoint singleton sets. Then if $\kappa$ is the cardinality of $R \cup G,$ then $\kappa=2$.

Prop 1. Suppose $R$ and $G$ are disjoint singleton sets, and suppose $U$ is an arbitrary set. Then if $\kappa$ is the cardinality of $U,$ and if $(x \in U)$ is equivalent to ($x \in R$ or $x \in G$), then $\kappa = 2$.

Surprisingly, we're not quite done with removing the function symbols; $2$ is a constant symbol (read: nullary function symbol), so lets get rid of it:

Prop 2. Suppose $R$ and $G$ are disjoint singleton sets, and suppose $U$ and $2$ denote arbitrary sets. Then if $2$ has the property that $x \in 2$ is equivalent to $x=0$ or $x=1$, and if $\kappa$ is the cardinality of $U,$ and if $(x \in U)$ is equivalent to ($x \in R$ or $x \in G$), then $\kappa = 2$.

Unfortunately, our unrolling has introduced $2$ more constants, namely $0$ and $1$! So we'd better unroll some more.

Prop 3. Suppose $R$ and $G$ are disjoint singleton sets, and suppose $U$ and $0,1$ and $2$ denote arbitrary sets. Then if $2$ has the property that $x \in 2$ is equivalent to $x=0$ or $x=1$, and if $1$ has the property that $x \in 1$ is equivalent to $x=0$, and if $0$ has property that $x \in 0$ is simply false, and if $\kappa$ is the cardinality of $U,$ and if $(x \in U)$ is equivalent to ($x \in R$ or $x \in G$), then $\kappa = 2$.

So now we've expressed everything in terms of relations, and we need to replace those relations with statements only mentioning $\in$ and $=$. Lets take a big step in that direction.

Prop 4. Suppose $R,G,U$ and $0,1$ and $2$ are arbitrary sets. Then if ($x \in R$ and $x \in G$) is vacuously false, and the cardinality of $R$ is $1$, and the cardinality of $G$ is also $1$, and if $2$ has the property that $x \in 2$ is equivalent to $x=0$ or $x=1$, and if $1$ has the property that $x \in 1$ is equivalent to $x=0$, and if $0$ has property that $x \in 0$ is simply false, and if $\kappa$ is the cardinality of $U,$ and if $(x \in U)$ is equivalent to ($x \in R$ or $x \in G$), then $\kappa = 2$.

We haven't quite got rid of all our relations, because phrases of the form "$\kappa$ is the cardinality of $X$" still abound. Formally, this means that $\kappa$ is the least ordinal such that there exists a surjection $S : \kappa \rightarrow X$. However, this takes a lot of time and space to formalize (trust me, I've been trying to do it for the past hour or so), so let us instead replace it with the statement "$\kappa$ is equipotent to $X$."

TFAE.

1. $\kappa$ is equipotent to $X$
2. There exists $S \subseteq \kappa \times X$ such that $S$ is a function and so too is its converse.
3. There exists $S$ such that firstly, if $s \in S$, then there exists $\alpha \in \kappa, x \in X$ such that $s = \{\{\alpha\},\{\alpha,\kappa\}\}$, secondly, we have that for all $\alpha \in \kappa$, there exists unique $x \in X$ such that $\{\{\alpha\},\{\alpha,x\}\} \in S,$ and thirdly, we have that for all $x \in X$, there exists unique $\alpha \in \kappa$ such that $\{\{\alpha\},\{\alpha,x\}\} \in S.$
4. An even longer statement obtained by replacing $\{\{\alpha\},\{\alpha,x\}\}$ with its definition.

Okay now "just" substitute statement (4) immediately above (the one that I don't have any energy left to write out properly) into Prop 4, replacing all statements of the form "the cardinality of $*$ is $*$" with the corresponding formalization. Now replace the enormous English sentence you get with its first-order logic formalization, and you're done.

Its just that easy!

Answer 2

Ok, let me be serious: Let's say you have a set $G$ of blue apples and a set $B$ of blue apples and an apple cannot be both green and blue. Then we know that there is not $x$ such that $x$ lies in both $G$ and $B$, i.e. $G \cap B$ is the empty set, denoted by $\emptyset$. We now consider $G\cup B$ that is the set of all elements which lie in $G$, $B$ or both. As we know, these sets have no elements in common, we know that the number of elements in $G \cup B$ is the number of elements in $G$ plus the number of elements in $B$. Therefore, we can write $|G\cup B| = |G| + |B|$, where $|.|$ denotes the number of elements of a given set.

The above can be stated more rigorously, which is key when dealing with sets in infinite sizes. (Just a side note: One can prove in ZFC, that there are indeed infinitely many different kinds of infinity and the study of them - the study of cardinal arithmetic that is - is absolutely beautiful, I think.)