Interdefinability of two expansions of the Real Field - MathOverflow most recent 30 from http://mathoverflow.net2013-05-22T07:28:39Zhttp://mathoverflow.net/feeds/question/81353http://www.creativecommons.org/licenses/by-nc/2.5/rdfhttp://mathoverflow.net/questions/81353/interdefinability-of-two-expansions-of-the-real-fieldInterdefinability of two expansions of the Real FieldJames Freitag2011-11-19T16:41:29Z2011-11-19T17:02:13Z
<p>I was asked the following question two days ago, but I couldn't completely resolve it. </p>
<p>Here is the claim:
$\mathcal R = (\mathbb R,+,\cdot)$ is the real field.</p>
<p>Let $I$ be an open interval (perhaps unbounded) in $\mathbb R$ and let $f: I \rightarrow \mathbb R$ be $C^1$ and such that $f'$ has no zeros. Then the structures:</p>
<p>$$(\mathcal R, sin (f)) = (\mathcal R, cos (f))$$
are interdefinable. </p>
<p>Notes: Start with $(\mathcal R, sin (f))$:</p>
<p>1) We know that the absolute value of $cos(f)$ is definable, simply by the Pythagorean theorem.</p>
<p>2) The fact that the derivative of $f$ has no zeros, along with the fact that the derivative of $sin(f)$ is $cos(f) \cdot f'$ and is definable means that we can identify all of the places at which $cos(f)$ switches signs. That is the zeros of $cos(f) \cdot f'$ are the same as $cos(f)$. The fact that $f'$ does not vanish assures that $cos(f)$ actually switches signs at these points. </p>
<p>So, here is one approach: identify the sign of $cos(f)$ on some interval near zero. Now we must simply identify, in a first order way, the number of zeros of the function $cos(f)$ between the interval on which you are defining the value and the first interval. I don't see exactly how to do this. Do you? </p>
<p>Of course, perhaps someone has a better way to do this. </p>
http://mathoverflow.net/questions/81353/interdefinability-of-two-expansions-of-the-real-field/81358#81358Answer by Serge R. for Interdefinability of two expansions of the Real FieldSerge R.2011-11-19T17:02:13Z2011-11-19T17:02:13Z<p>I am not sure I see the difficulty. </p>
<p>Let's assume $f'>0$ on $I$. The function $s$ that sends $x$ to $\frac{f'(x)\cos(f(x))}{|f'(x)\cos(f(x))|}$ if $f'(x)\cos(f(x))\neq 0$ and to $0$ else is definable in the first structure and, as you noted, $\cos(f(x))=s(x)|cos(f(x))|$ is therefore also definable. </p>
<p>Or did I miss something ?</p>