Speedups (i.e., differences in the lengths of shortest proofs of the same sentences) between various theories in the language of first-order arithmetic and richer languages is a relatively well-studied phenomenon. There are three typical orders of speedup that occur in natural examples: non-recursive speedups, at most polynomial speedups, and speedups of the order of the super-exponentiation function exp*(0)=1, exp*(x+1)=exp(exp*(x)).

In the present talk I will compare this situation to what happens over the language of Presburger arithmetic. We consider theories that are complete in the language of Presburger arithmetic and for them the usual quantifier elimination algorithm guarantees that any formula of the length n has a proof of the length ≤exp(exp(exp(P(n)))). This shows that speedups in this setting are at most triple-exponential. An important tool for proving non-polynomial speedups for first-order theories is Friedman-Pudlak finite version of Gödel's second-... more

In the present talk I will compare this situation to what happens over the language of Presburger arithmetic. We consider theories that are complete in the language of Presburger arithmetic and for them the usual quantifier elimination algorithm guarantees that any formula of the length n has a proof of the length ≤exp(exp(exp(P(n)))). This shows that speedups in this setting are at most triple-exponential. An important tool for proving non-polynomial speedups for first-order theories is Friedman-Pudlak finite version of Gödel's second-... more