27

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?

Community
  • 1
Carl Mummert
  • 9,593
  • If it's not an integer, then ZFC can certainly prove that, just by approximating it closely enough. – Chris Eagle Sep 09 '11 at 23:21
  • 5
    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. – Amit Kumar Gupta Sep 10 '11 at 04:36
  • @Chris, I suppose that argument fails if we ask instead whether it's rational. – Gerry Myerson Sep 10 '11 at 04:59
  • 1
    @Amit: That is my sequence $(a_n)$, essentially. – Carl Mummert Sep 10 '11 at 11:44

1 Answers1

18

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.

François G. Dorais
  • 43,723
  • 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. – Carl Mummert Sep 10 '11 at 14:55
  • 8
    You don't need Macintyre-Wilkie, as Schanuel's Conjecture tells you immediately $\exp(\exp(\exp(79))))$ is not an integer. – Dave Marker Sep 10 '11 at 15:01
  • 5
    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. – George Lowther Sep 10 '11 at 15:14
  • @Dave: Ah, beaten to it. – George Lowther Sep 10 '11 at 15:18
  • Thanks for confirming my suspicion, Dave and George! What's the easy way to see (the intuitively obvious fact) that $79, e^{79}, e^{e^{79}}$ are linearly independent over $\mathbb{Q}$? – François G. Dorais Sep 10 '11 at 15:21
  • 1
    Ah! Never mind, I just figured out the bootstrapping trick... – François G. Dorais Sep 10 '11 at 15:28
  • 1
    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. – George Lowther Sep 10 '11 at 22:21