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 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.
