Is $ \pi $ definable in $(\Bbb R,0,1,+,×, <,\exp) $?

1.2k Views Asked by At

Is there a first-order formula $\phi(x) $ with exactly one free variable $ x $ in the language of ordered fields together with the unary function symbol $ \exp $ such that in the standard interpretation of this language in $\Bbb R $ (where $ \exp $ is interpreted as the exponential function $ x \mapsto e^x $), $\phi (x) $ holds iff $ x=\pi $?

EDIT: As Levon pointed out, a negative answer to this problem would imply that $π$ and $e$ (and $e^e$, $(2e)^{3e^2}$, and so on) are algebraically independent over $\Bbb Q$, which is an unsolved problem. So, if you think that a definition of $\pi$ is impossible, I would be pleased if you could show something like, that it is possible to reduce $\phi$ to a formula which contains no terms involving bound variables inside exponential functions, which would reduce the problem more or less to a question on algebraical independece. However because there are such intricate connections between exponential and trigonometric functions, I don't think that $\pi$ should be undefinable.

2

There are 2 best solutions below

0
On BEST ANSWER

Todd Trimble provided the answer to this question on MO:

Assuming Shanuel's conjecture, this treatise about exponential rings proves that (see Theorem 2.5.1) the exponential ring generated by $\pi$ looks just as the exponential ring generated by nearly every other real number, which implies that there is no defining relation of $\pi$ over $\Bbb R_{\exp}$.

5
On

Using that $\int_{-\infty}^\infty e^{-x^2} = \sqrt{\pi}$

$$ \phi(x) := (\forall_y \psi(y) \implies y^2 = x) $$

Where $$ \psi(y) := \forall_{\epsilon > 0} \exists_N \forall_{n > N} \forall_x s(n, x) \implies |x - y| < \epsilon $$ The formula $\psi(y)$ says that $y$ is a limit of $x_n$ such that $s(n, x_n)$ holds. Now, $s(n, x)$ says that $\int_{-n}^n e^{-t^2} = x$:

$$ s(k, x) = \forall_{\epsilon > 0} \exists_N \forall_{n > N} \forall_y p(n, k, y) \implies |x - y| < \epsilon $$

Now $p(n, k, y)$ says that $y$ is a value of k-th Riemann sum of integral $\int_{-n}^n e^{-t^2}$. I'll leave the details.