Quantifier elimination for the reals with a predicate for the powers of two

TL;DR

This paper presents a syntactic method for quantifier elimination in the theory of reals with powers of two, providing a primitive recursive decision procedure with explicit complexity bounds.

Contribution

It introduces a syntactic approach to quantifier elimination that improves upon previous model-theoretic methods by offering primitive recursive complexity bounds.

Findings

Quantifier elimination can be performed in time $2^{O(n)}$ for a block of existential quantifiers.

The method is primitive recursive but not elementary.

Decidability of the theory is established with explicit complexity bounds.

Abstract

In 1985, van den Dries showed that the theory of the reals with a predicate for the integer powers of two admits quantifier elimination in an expanded language, and is hence decidable. He gave a model-theoretic argument, which provides no apparent bounds on the complexity of a decision procedure. We provide a syntactic argument that yields a procedure that is primitive recursive, although not elementary. In particular, we show that it is possible to eliminate a single block of existential quantifiers in time $2^0_{O(n)}$, where $n$ is the length of the input formula and $2_k^x$ denotes $k$-fold iterated exponentiation.