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?