Independence of being an integer 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? 
 A: 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.
