Do you think that $\mathbb Z \subset \mathbb R$? On one hand this inclusion is quite handy. We like to write things like:
$$
\sqrt{n} \quad \text{for $n\in \mathbb Z$}
$$
which requires the number $n$ to be a real number (where $\sqrt\cdot$ is defined). On the other hand it is difficult to obtain such an inclusion when comes to definition. One would like to be able to define whole numbers without the need to define real numbers. This becomes more tricky when one notices that there are other inclusions which one would like to satisfy. For example I would like $1$ to be a polynomial with whole coefficients, or maybe a polynomial with complex coefficients, or maybe a real function of one variable... 


I would say that it is not possible to satisfy all these inclusions. So maybe we must not insist on saying that $\mathbb Z \subset \mathbb R$ in the first place. Are there alternatives?


One possibility I see is that of having many different sets isomorphic to $\mathbb Z$. We should use the name $\mathbb Z$ for integers as we use $V$ for vector spaces. We should say: let $\mathbb Z$ be any set of integers. Or: let $\mathbb R$ be a set of reals and let$\mathbb Z$ be the set of real integers $\mathbb Z \subset \mathbb R$. And so on...


Another possibility I see (but I'm not sure if it can be really founded) is that of redefining the meaning of equality $=$ and distinguish between equality and identity. We could try to take an "object-oriented" approach where equality could be defined like any other operation. So one could define $1 = 1/1$ i.e. the integer $1$ is the same as the rational $1/1$ and one should define the sum of integers and rational by converting the integer to a rational and then performing the sum between rationals. This also modifies the concept of 'set' since the set $\{1, 1/1 \}$ is equal to $\{1/1\}$ and hence has a single element. This is, more or less, how types work in computer languages. Can this approach be made rigorous?



Are integers real?
We do in fact have many different sets isomophic to $\mathbb{Z}$. The correct definition of $\mathbb{Z}$ is a set with some operations on it that satisfy some axioms. This is easier to see with $\mathbb{N}$, which is a set with a 0, a "plus one" operations, that satisfies mathematical induction. There is only one such set up to oeration-preserving isomorphism.


$\mathbb{R}$ can be axiomatized similarly, as a complete Archimedean ordered field (see the synthetic approach section [at Wikipedia](http://en.wikipedia.org/wiki/Axiomatic_theory_of_real_numbers)). Again there is only one such set up to operation-preserving isomorphism. You can identify in that set a copy of $\mathbb{Z}$, so you can treat $\mathbb{Z}$ as a subset. But this is a matter of notation. If you had a compelling reason to make it disjoint, you could require that, instead.


We say "the integers" or "the reals" because there is only one, up to isomorphism. Any theorem you prove about $\mathbb{Z}$ or $\mathbb{R}$ that doesn't use the internal representation will transfer to any isomorphic copy, so we don't need to know which one.


There is a whole mathematical notion of types that actually underpins languages with more-complicated type systems, such as ML or Haskell. You can think of $\mathbb{Z}$ and $\mathbb{R}$ as a type in a type system. Some typing systems have a notion of "subtype", but let's suppose that you don't. Then $\mathbb{Z}$ and $\mathbb{R}$ are types, and there's a designated monomorphism $i$ from $\mathbb{Z}$ to $\mathbb{R}$. Then 2 + 3.5 is an overloaded operation that is syntactic sugar for $i(2) + 3.5$. I don't know if anyone has ever worked out a clear account of what mathematicians do from this point of view, but what they do is not very complicated.


If you do want to allow subtypes, there's a notion of order-sorted algebra that allows the kind of overloading you probably have in mind. I don't know of a canonical link, but introductions are easy to find.


