Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Speedups for Presburger Arithmetic and Real Closed Fields

Fedor Pakhomov, Julien Daoud

TL;DR

This paper compares two groups of axiomatizations of Presburger arithmetic PrA and the theory of real closed fields RCF and shows that the first group of axiomatizations enjoys at least a double exponential speedup.

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.

Speedups for Presburger Arithmetic and Real Closed Fields

TL;DR

This paper compares two groups of axiomatizations of Presburger arithmetic PrA and the theory of real closed fields RCF and shows that the first group of axiomatizations enjoys at least a double exponential speedup.

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.
Paper Structure (9 sections, 16 theorems, 24 equations)

This paper contains 9 sections, 16 theorems, 24 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Speedup in Presburger Arithmetic
  4. Definitions
  5. Theories
  6. Speedup
  7. Speedup over the Theory of Real Closed Fields
  8. Speedup
  9. Upper Bounds for Proofs in $\mathsf{PrA}_{\mathit{alt}}$

Key Result

Theorem 1

Let $\mathcal{L}$ be a first-order language, where $\neg$ and at least one of the three logical connectives $\rightarrow$, $\vee$, or $\wedge$ are present. Furthermore, $\mathcal{L}$ should contain the equality symbol and constants $0,1$. Let $\phi_0(\vec{a}, \vec{b} )$ and $\Phi (R,\vec{a}, \vec{b} have polynomial (in $n$) proofs in $\mathsf{QPC}$ from the axiom $0\ne 1$.

Theorems & Definitions (42)

  • Theorem 1: Solovay, see Pud98
  • Definition 1
  • Definition 2
  • Lemma 1: On bounded size definability of bounded multiplication
  • proof
  • Definition 3
  • Definition 4
  • Definition 5
  • Definition 6
  • Lemma 2
  • ...and 32 more