2 ms·
> There are statements in Presburger arithmetic that take time doubly exponential (or worse) in the size of the statement to reach via any path of the formal sy
by aleph_minus_one 2y ago
> There are statements in Presburger arithmetic that take time doubly exponential (or worse) in the size of the statement to reach via any path of the formal system whatsoever.
This is a correct statement about the worst case runtime. What is interesting for practical applications is whether such statements are among those that you are practically interested in.
- Xcelerate 2y agoI would certainly think so. The statements mathematicians seem to be interested in tend to be at a "higher level" than simple but true statements like 2+3=5. And they necessarily have a short description in the formal language of ZFC, otherwise we couldn't write them down (e.g., Fermat's last theorem). If the truth of these higher level statements instantly unlocks many other truths, then it makes sense to think of them in the same way that knowing BB(5) allows one to instantly classify any Turing machine configuration on the computation graph of all n ≤ 5 state Turing machines (on empty tape input) as halting/non-halting.