Speedups for Presburger Arithmetic and Real Closed Fields
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , |
|---|---|
| Format: | Preprint |
| Publié: |
2026
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866918363319500800 |
|---|---|
| author | Pakhomov, Fedor Daoud, Julien |
| author_facet | Pakhomov, Fedor Daoud, Julien |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_00642 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Speedups for Presburger Arithmetic and Real Closed Fields Pakhomov, Fedor Daoud, Julien Logic 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. |
| title | Speedups for Presburger Arithmetic and Real Closed Fields |
| topic | Logic |
| url | https://arxiv.org/abs/2603.00642 |