Is $π$ definable in $(\Bbb R,0,1,+,×,<,\exp)$? (This question is originally from Math.SE, where it didn't receive any answers.)
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 $?
(Since a negative answer to this problem would imply that $e$ and $\pi$ are algebraically independent, I cannot expect anyone to give a complete proof that it isn't possible. However, in the case that one suspects strongly that the answer to this question is negative, I would already be pleased if someone could give intuitive arguments why one shouldn't believe in the definability of $\pi$.
However because there are such intricate connections between exponential and trigonometric functions, I don't think that $\pi$ should be undefinable.)
 A: It seems to me that Schanuel's conjecture (which is a kind of article of faith in transcendental number theory, but of course very far from proven itself) ought to imply that $\pi$ is not definable in this structure. The linked Wikipedia article contains the assertion 


*

*Euler's identity states that $e^{\pi i} + 1 = 0$. If Schanuel's conjecture is true then this is, in some precise sense involving exponential rings, the only relation between $e$, $π$, and $i$ over the complex numbers. [2]


where reference [2] is unfortunately not something I have access to: 


*

*Terzo, Giuseppina (2008). "Some consequences of Schanuel's conjecture in exponential rings". Communications in Algebra 36 (3): 1171–1189. doi:10.1080/00927870701410694. 


(link), courtesy of Dominik in a comment below. 
See in particular theorem 2.5.1 on page 37, which gives a more precise answer to the OP (under the assumption of Schanuel's conjecture). The bottom line is that a claim that $\pi$ should be definable in this structure would amount to an assertion that SC is false (which would be a pretty big deal, if you know a little about the stature and importance of SC). 
Related of course is Wilkie's theorem, which says that any first-order unary formula $\phi(x_1)$ in the language of ordered rings with an exponential function is equivalent to 
$$\exists x_{2}\ldots\exists x_n \;\; f_1(x_1,\ldots,x_n,e^{x_1},\ldots,e^{x_n})=\cdots= f_r(x_1,\ldots,x_n,e^{x_1},\ldots,e^{x_n})=0$$ 
for some exponential polynomials $f_i$ with integer coefficients. So a putative definition of $\pi$ can't be that intricate in principle, at least not in terms of logical complexity. 
