Is the Presburger arithmetic decision problem known to be outside of BQP or BPP? Presburger arithmetic is well-known to be decidable but intractable, requiring doubly exponential time even with nondeterminism (Fischer and Rabin, 1974).  I am wondering if it is also known whether the Presburger arithmetic decision problem remains intractable with quantum computation or even just randomized computation, and specifically whether it falls outside of BQP or BPP.  It would be profoundly humbling if such a seemingly weak mathematical theory, which doesn't even allow multiplication, gives rise to provably intractable problems.
Let $~{\mathrm{PRESARITH}}$ denote the decision problem of the truth of statements in Presburger Arithmetic. As you note, [Fischer+Rabin&nbsp;1974] (PS manuscript) show that the nondeterministic time complexity of $\mathrm{PRESARITH}$ is at least $2^{2^{\Omega(n)}}$. In particular, $\mathrm{PRESARITH} \notin \mathsf{NEXP}$.
However, we have the containments
$$ \mathsf{
BPP \;\subseteq\; BQP \;\subseteq\; PP \;\subseteq\; PSPACE \;\subseteq\; EXP \;\subseteq\; NEXP
}
$$

Thus, it directly follows that $\mathrm{PRESARITH} \notin \mathsf{BQP}$, and in particular it is not in $\mathsf{BPP}$ either.