Speedups for Presburger Arithmetic and Real Closed Fields

TL;DR

This paper compares different axiomatizations of Presburger arithmetic and real closed fields, demonstrating that those using full induction or least upper bound principles significantly speed up proof lengths, with at least double exponential improvements.

Contribution

It provides a comparison of axiomatizations based on proof lengths, highlighting the efficiency gains of certain schemas in Presburger arithmetic and real closed fields.

Findings

Full induction axiomatizations achieve at least double exponential speedup.

Axiomatizations avoiding unbounded quantifier formulas are less efficient.

Proof length improvements are significant in these theories.

Abstract

In the present paper, we consider Presburger arithmetic PrA and the theory of real closed fields RCF. Due to quantifier elimination in these theories, there are two kinds of natural ways to axiomatize them. Namely, on one hand, PrA can be axiomatized with the full schema of first-order induction, and RCF with the full schema of the first-order least upper bound principle. At the same time, there are natural axiomatizations of these theories that avoid the use of formulas of unbounded quantifier depth. In the present paper, we compare these two groups of axiomatizations from the perspective of proof lengths. We show that the first group of axiomatizations enjoys at least a double exponential speedup.