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.

  • 4
    $\begingroup$ One can define $2x=\pi$ as the least positive real such that $\sin x=0$. Given the intimate relation with $\exp$ and the trigonometric functions, can you work something out? $\endgroup$
    – Pedro
    Jun 9, 2013 at 22:58
  • 5
    $\begingroup$ A negative answer would imply $\pi$ and $e$ are algebraically independent over $\mathbb Q$. $\endgroup$ Jun 10, 2013 at 0:49
  • 1
    $\begingroup$ Since $\int_{-\infty}^{\infty} e^{-x^2} = \sqrt{\pi}$, we could express $\pi$ as a square of the value of this integral. I think we can express this in first order language. $\endgroup$
    – xyzzyz
    Jun 10, 2013 at 0:52
  • 4
    $\begingroup$ Carl's comment implies that Peter's approach can't work. $\;$ $\endgroup$
    – user57159
    Jun 10, 2013 at 1:45
  • 3
    $\begingroup$ Partial answer. Leave out exp, answer is "no". There are models of $(\Bbb R,0,1,+, \times, \lt)$ (that is, real-closed fields) that do not contain $\pi$. An easily described one is the set of all algebraic real numbers. $\endgroup$
    – GEdgar
    Jun 12, 2013 at 17:12

2 Answers 2


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}$.


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.

  • 10
    $\begingroup$ How do you define the Riemann sum in this structure (which cannot even define or quantify over $\mathbb{N}$)? $\endgroup$ Jun 10, 2013 at 1:07
  • $\begingroup$ @Carl : $\:$ How do you know that this structure cannot define $\mathbb{N}$? $\;\;\;$ $\endgroup$
    – user57159
    Jun 10, 2013 at 1:24
  • 7
    $\begingroup$ @Ricky Demer: Alex Wilkie proved in 1999 that the structure $\mathbb{R}_{\text{exp}}$ is o-minimal. en.wikipedia.org/wiki/O-minimal_theory $\endgroup$ Jun 10, 2013 at 1:34
  • 1
    $\begingroup$ (Note: I have upvoted this, not because I agree but because -3 seemed harsh for a well-meant (and flawed) attempt.) $\endgroup$
    – Myself
    Jun 12, 2013 at 17:02
  • 3
    $\begingroup$ One would then similarly use $\int_{-\infty}^\infty dx/(1+x^2)$ to define $\pi$ without using $\exp$ at all, which is impossible. $\endgroup$
    – GEdgar
    Jul 14, 2013 at 18:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.