Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Unary counting quantifiers do not increase the expressive power of Presburger aritmetic: an alternative shorter proof

Christian Choffrut

Abstract

This work was presented in June 5-7, 2017 at the conference "Journées sur les Arithmétiques Faibles -- Weak Arithmetics Days" held in Saint-Pertersburg of which no proceeding was ever published. It was not a new result but showed that a different approach is possible. The paper presented at ICALP 2024 addresses, among other problems, the complexity issues which were ignored in my 2017 talk.

Unary counting quantifiers do not increase the expressive power of Presburger aritmetic: an alternative shorter proof

Abstract

This work was presented in June 5-7, 2017 at the conference "Journées sur les Arithmétiques Faibles -- Weak Arithmetics Days" held in Saint-Pertersburg of which no proceeding was ever published. It was not a new result but showed that a different approach is possible. The paper presented at ICALP 2024 addresses, among other problems, the complexity issues which were ignored in my 2017 talk.

Paper Structure

This paper contains 4 sections, 2 theorems, 28 equations.

Table of Contents

  1. Semilinear sets
  2. An example
  3. The proof
  4. The structure ${\mathcal{N}}$

Key Result

Theorem 1

Given a Presburger formula $\phi(x_{1}, \ldots, x_{n})$ with free variables $x_{1}, \ldots, x_{n}$, there exists a Presburger formula $\psi(x_{1}, x_{2}, \ldots, x_{n-1},y)$ equivalent to the formula $\exists^{=y}_{x_{n}} \phi(x_{1}, \ldots, x_{n})$

Theorems & Definitions (5)

  • Theorem 1
  • Definition 2
  • Theorem 3
  • Remark 1
  • Remark 2