Fischer and Rabin proved a superexponential bound $2^{2^{cn}}$ for the worst-case length of a proof of a proposition of length $n$ in Presburger arithmetic.  The result is in

>Michael J. Fischer and Michael O. Rabin, Super-Exponential Complexity of Presburger Arithmetic, Proceedings of the SIAM-AMS Symposium in Applied Mathematics 7 (1974), pp.27–41.

Are there any explicit positive lower bounds for the constant $c>0$ in their estimate?

This was asked [on MSE](https://math.stackexchange.com/questions/4994818/explicit-bound-for-superexponential-estimate-for-presburger-arithmetic) without input.

The question is whether the Fischer-Rabin theorem could have philosophical consequences.  Gaifman claimed in 2012 that

>"if our resources restrict us to less than super-exponential computation, then some truths must remain unknown. ... the answers to some simple mathematical questions—for example, that some Diophantine equations have no solution—are beyond what we can know; and this is due to our epistemic limitations."

Gaifman appears to derive such a consequence from both incompleteness and Fischer-Rabin.  But apparently one could not derive such philosophical consequences without an explicit lower bound for the constant $c$. Indeed, statements of interest to human beings have a uniform upper bound on length, say 1000000. If the constant $c$ is small enough, the superexponential bound of the Fischer-Rabin estimate may not provide any practical limitation on the length of a proof of statements of interest to human beings.  Thus, concrete estimates on $c$ could have some bearing on the possibility of deriving philosophical consequences from the Fischer-Rabin result, as envisioned by Gaifman.