Formal definition of the function $Sin$

Question

Which is the formal definition of the function $Sin$, starting from axioms of real numbers ?

I never found it in any book.

Not its Taylor serie, that is based upon the intuitive definition of $Sin$; I want the formal definition of $Sin$ without confusing drawings of circles, angles and straight lines.

Answer 1

The $\sin$ function is usually defined using "confusing drawings of circles, angles and straight lines." It is usually from this that you derive its Taylor series, which is another possible candidate for the definition. I don't believe there are any other ways of defining it and I don't see any connection to the "axioms of real numbers."

Answer 2

Maybe I found an answer in this web page:

http://math2.org/math/algebra/functions/trig/sin-cos-definition.htm

Answer 3

One formal definition is via complex analysis, as used, e.g., by metamath (df-sin): $$ \sin z=\frac{e^{iz}-e^{-iz}}{2i}. $$

This, in turn, rests on the definition of $\exp$ (df-ef): $$ \exp z=\sum_{k=0}^\infty\frac{z^k}{k!}. $$

For more details see the definition of sum (df-sum) which, in the case of infinite sums, is defined in terms of limits (df-clim).

Answer 4

If you wish, you can define $\sin$ by solution of differential equation $$\ddot x + x = 0,\enspace x(0)=0,\dot x(0)=1,$$ and $\cos$ in the same manner.

Answer 5

All the definitions go in circles, in that from one you can always get to the other. Some people who are very big into foundations (e.g. Bourbaki) have specific preferences for what should be the "formal" definition.

To avoid a power series definition, we can first define the complex exponential function $\mathrm{cexp}(x)$ as the unique $2\pi$-periodic positively-oriented continuous group homomorphism $(\mathbb{R},+) \rightarrow (U, \cdot)$, where $(U, \cdot)$ is the complex multiplicative circle group (where $\pi$ can be defined by an integral). Then $\sin(x)$ and $\cos(x)$ are the imaginary and real parts of that function.