Conservative extenstion, identifying objects of different type In a comment here, Terence Tao says:

in practice we often “abuse notation” by identifying objects of one type with another, e.g. identifying the natural number 3 with the integer +3, the rational 3/1, and the real 3.0; this is technically a violation of the usual laws of typed first-order logic, but can be justified by passing to a suitable conservative extension of the original mathematical theory

How can one construct this conservative extension in which one identifies these objects of different type? Can one formalize Tao's idea?
 A: Here's an example of how to do this to go from $\mathbb{N}$ to $\mathbb{Z}$ — or, more accurately, from a theory of the natural numbers to a theory of the integers (the concept of "conservative extension," which you referred to, is a syntactic notion referring to sentences and theories, not a semantic notion referring to models). This is based on the construction of integers as equivalence classes of ordered pairs of natural numbers.
Start with the first-order theory of Peano arithmetic.  There are various slightly different ways of defining it (all equivalent), but let's construe PA as a theory in the language $\mathscr{L}$ containing constant symbols for $0$ and $1,$ a two-place relation symbol $\ge,$ and two two-place function symbols $+$ and $\cdot.$
For any formula $\varphi$ in our language, define $\varphi^*$ by induction on formulas as follows:


*

*If $\varphi$ is atomic, then $\varphi^*$ is $\varphi.$

*If $\varphi$ is $\,\lnot \psi,\,$ $\varphi_1\lor\varphi_2,$ or $\,\varphi_1\land\varphi_2,$ then $\varphi^*$ is $\lnot (\psi^*),\,$ $\varphi_1^*\lor\varphi_2^*,$ or $\,\varphi_1^*\land\varphi_2^*,$ respectively.

*If $\varphi$ is $\exists x\,\psi,$ then $\varphi^*$ is $\exists x\,(x\ge 0 \land \psi^*).$

*If $\varphi$ is $\forall x\,\psi,$ then $\varphi^*$ is $\forall x\,(x\ge 0 \rightarrow \psi^*).$
Consider the following theory $T$ in the language $\mathscr{L};$ $\,T$ is intended to be a theory of the integers. $T$ contains the following axioms:


*

*$\,\varphi^*$ for every $\varphi$ that is an axiom of PA.

*$(\forall x)(\forall y)(x\ge 0 \,\land\, y\ge 0 \rightarrow (\exists z)(x=y+z).$
(Existence of all integers—really just needed for $y\gt x.)$

*$(\forall x)(\exists y)(\exists z)(y \ge 0 \,\land\, z\ge 0 \,\land\, x+z=y).\;$
(Every integer can be written as the difference of two natural numbers.)

*$(\forall x_1)(\forall y_1)(\forall z_1)(\forall x_2)(\forall y_2)(\forall z_2)\big((x_1+z_1=y_1 \,\land\, x_2+z_2=y_2)\rightarrow(x_1=x_2\iff y_1+z_2=y_2+z_1)\big).\;$
(Equality of integers.)

*$(\forall x_1)(\forall y_1)(\forall z_1)(\forall x_2)(\forall y_2)(\forall z_2)\big((x_1+z_1=y_1 \,\land\, x_2+z_2=y_2)\rightarrow(x_1 \ge x_2\iff y_1+z_2 \ge y_2+z_1)\big).\;$
(Comparison of integers.)

*$(\forall x_1)(\forall y_1)(\forall z_1)(\forall x_2)(\forall y_2)(\forall z_2)\big((x_1+z_1=y_1 \,\land\, x_2+z_2=y_2)\rightarrow (x_1+x_2)+(z_1+z_2)=y_1+y_2\big).\;$ 
(Addition of integers.)

*$(\forall x_1)(\forall y_1)(\forall z_1)(\forall x_2)(\forall y_2)(\forall z_2)\big((x_1+z_1=y_1 \,\land\, x_2+z_2=y_2)\rightarrow (x_1\cdot x_2)+(y_1\cdot z_2 + y_2\cdot z_1)=y_1\cdot y_2 + z_1\cdot z_2\big).\;$
(Multiplication of integers.)
(In 4-7 above, you can restrict $y_1, y_2, z_1,$ and $z_2$ to be greater than or equal to $0$ if you prefer, in the interest of conceptual parsimony, but it makes the sentences physically longer, so I didn't write them that way.)
The integers with the standard operations form a model of $T.$
If $M$ is any model of $T,$ then the submodel of $M$ consisting of all $x$ such that $\,M\models (x\ge 0)\;$ is a model of PA.
Moreover, if $N$ is any model of PA, then you can construct a model $M$ of $T$ whose members are equivalence classes of ordered pairs from $N,$ in the usual way.  $N$ is then isomorphic to the appropriate submodel of $M,$ just as one would expect.
These two operations (extending a model of PA to a model of $T,$ and going from a model of $T$ to a submodel satisfying PA) are inverses of one another.
Finally, $T$ is a conservative extension of PA in the sense that all of this can be proven syntactically: For any sentence $\varphi$ in the language $\mathscr{L,}$ $\,\text{PA}\vdash\varphi$ iff $T\vdash \phi^*$ (and $\phi^*$ here is the sentence which means precisely that $\varphi$ is true when all its variables are restricted to values $\ge 0.)$
You can do the same sort of construction to go from the integers to the rational numbers.
However, the real numbers are more complicated; it can be done, but you need to include in your formal theory sets of rational numbers (for use as Dedekind cuts or Cauchy sequences), so it's more complicated.  (Moreover, I'm not sure that Peano arithmetic is really the best starting point for the reals, unless you're interested in knowing which parts of analysis can actually be done "in" PA, rather than in, say, ZFC or even second-order arithmetic.)
