27
$\begingroup$

In this MO question, the OP asked for an example of a statement which was known not to be independent of ZFC, but for which the truth value was unknown. I immediately thought of a question I asked on math.SE: is $e^{e^{e^{79}}}$ an integer? This is apparently an open question, but I realized after some thought that I don't know how to prove it is decidable in ZFC.

If the number is not an integer, this can be proved in ZFC, because that fact could be expressed by an arithmetical sentence saying there is an integer $n$ such that the sum of a certain definable series is greater than $n$ and less than $n+1$. This sentence can be seen to be $\Sigma^0_1$ by standard techniques, and any true $\Sigma^0_1$ sentence is provable in ZFC.

But if the sum is an integer, it does not seem obvious that this must be provable in ZFC. In general, only $\Sigma^0_1$ statements have to be provable if they are true, and the claim that a certain definable series sums to an integer is $\Sigma^0_2$ rather than $\Sigma^0_1$.

Moreover, it's not hard to see that there are definitions of sequences $(a_n)$ in ZFC such that ZFC proves that $\sum a_n$ converges but ZFC doesn't prove this sum is an integer and ZFC doesn't prove it is not an integer. These sequences can be constructed using the incompleteness theorem in the usual way. In fact, we can make $0 \leq a_n \leq 2^{-n}$ for all $n$, so there is no issue with the rate of convergence.

But there must be something special about $e^{e^{e^{79}}}$ that means either ZFC can prove it's an integer, or can prove it's not an integer - right?

Improve this question
$\endgroup$
4
  • $\begingroup$ If it's not an integer, then ZFC can certainly prove that, just by approximating it closely enough. $\endgroup$
    – Chris Eagle
    Commented Sep 9, 2011 at 23:21
  • 5
    $\begingroup$ Even simpler than your sequences $(a_n)$, define $a$ to be 0 if $\mathrm{Con(ZFC)}$ and $\frac 12$ otherwise. Then $ZFC$ proves that there's a unique real satisfying the definition of $a$, but it can't prove whether it's an integer or not. But yeah, it feels like something about $e^{e^{e^{79}}}$ should be different. $\endgroup$
    – Amit Kumar Gupta
    Commented Sep 10, 2011 at 4:36
  • $\begingroup$ @Chris, I suppose that argument fails if we ask instead whether it's rational. $\endgroup$
    – Gerry Myerson
    Commented Sep 10, 2011 at 4:59
  • 1
    $\begingroup$ @Amit: That is my sequence $(a_n)$, essentially. $\endgroup$
    – Carl Mummert
    Commented Sep 10, 2011 at 11:44

1 Answer 1

Reset to default
18
$\begingroup$

Here is a conditional answer. It was shown by Macintyre and Wilkie that if (a weak variant of) Schanuel's Conjecture is true, then the first-order theory of the real exponential field $(\mathbb{R};0,1,+,\times,\exp)$ is decidable. In particular, the (very unwieldy) first-order sentence $$\bigvee_{n=A}^B \exp\exp\exp 79 = n,$$ where $A = 2^{2^{2^{79}}}$ and $B = 3^{3^{3^{79}}}$ is then decidable by finitary means. Of course, it is conceivable that Schanuel's Conjecture is false...

As pointed out by Dave Marker and George Lowther, Schanuel's Conjecture directly implies that $e^{e^{e^{79}}}$ is not an integer. Indeed, since $e^{79}$ is irrational, $79$ and $e^{79}$ are linearly independent over $\mathbb{Q}$, which means that $e^{79},e^{e^{79}}$ are algebraically independent over $\mathbb{Q}$. Since $79,e^{79},e^{e^{79}}$ are therefore linearly independent over $\mathbb{Q}$, it follows that $e^{79},e^{e^{79}},e^{e^{e^{79}}}$ are algebraically independent over $\mathbb{Q}$. In particular, $e^{e^{e^{79}}}$ is not an integer.

Improve this answer
$\endgroup$
7
  • $\begingroup$ I'm glad you pointed this out. The only trouble for the purposes of this question, of course, is that Schanuel's conjecture is open. But I have some hope that maybe there is an approach to my question along these lines that doesn't require the full strength of Schanuel's conjecture. For example, the sentence you wrote is quantifier-free, so (naively) we don't need the decidability of the entire theory. $\endgroup$
    – Carl Mummert
    Commented Sep 10, 2011 at 14:55
  • 8
    $\begingroup$ You don't need Macintyre-Wilkie, as Schanuel's Conjecture tells you immediately $\exp(\exp(\exp(79))))$ is not an integer. $\endgroup$
    – Dave Marker
    Commented Sep 10, 2011 at 15:01
  • 5
    $\begingroup$ According to Schanuel's conjecture, $79$, $e^{79}$, $e^{e^{79}}$, $e^{e^{e^{79}}}$ are algebraically independent over the rationals. So it implies that $e^{e^{e^{79}}}$ is not an integer. $\endgroup$
    – George Lowther
    Commented Sep 10, 2011 at 15:14
  • 1
    $\begingroup$ Ah! Never mind, I just figured out the bootstrapping trick... $\endgroup$
    – François G. Dorais
    Commented Sep 10, 2011 at 15:28
  • 1
    $\begingroup$ As I can't edit comments, I'll just add that obviously I should have said that $e^{79}$, $e^{e^{79}}$, $e^{e^{e^{79}}}$ are algebraically independent. Clearly I shouldn't have had 79 in there too. $\endgroup$
    – George Lowther
    Commented Sep 10, 2011 at 22:21

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .