The role of regexps/finite automata in quantifier elimination for Presburger arithmetic
I've read that Presburger arithmetic (arithmetic with only addition, hence not subject to Gödel's incompleteness theorem) can be proven complete through quantifier elimination.[1] I've also read that this is done by making a correspondence between sentences in Presburger arithmetic and finite automata.
Intuitively speaking, it's very clear that $\Sigma^0_1$-sentences[2] will correspond to finite automata/regular expressions[3]. But I don't quite see how this works for more complicated expressions, e.g. those with nested $\exists$ and $\forall$ quantifiers.
Thus, is the $\Sigma^1_0$-sentence/finite automation correspondence I made on the right track, or is the Presburger-arithmetic-sentence/finite-automaton correspondence more complicated than I'm currently thinking?
(Related: Why are regular languages closed under intersection and complementation?)
-
An example of which is the way we prove the theory of dense linear orders complete. ↩︎
-
Roughly speaking, sentences with only $\exists$-quantifiers, none of which may be negated. ↩︎
-
E.g. $\exists m(m+m+m=n)$ means that $n$ matches the regexp
(...)*, $\exists m_1 \exists m_2(m_1+m_1+m_1+m_2+m_2=n)$ means that $n$ matches the regexp(...)*(..)*, … ↩︎
1 answer
The following users marked this post as Works for me:
| User | Comment | Date |
|---|---|---|
| clemens |
Thread: Works for me This answer not only deals succinctly and clearly with the quantifier elimination question but also makes a very interesting and helpful effort to ... |
May 8, 2026 at 19:18 |
As far as I'm aware, quantifier elimination in Presburger arithmetic and the translation to finite state automata are unrelated.
Given a formula $\varphi(x)$ in Presburger arithmetic, we can translate it to an automaton / regular expression $A$ on the characters $0$ and $1$ that reads in $x$ in binary and accepts iff $\varphi$ is true of $x$.
In order to get more variables involved, so, for instance, we can deal with formulas with more quantifiers, we need a way of feeding in multiple words, in this case multiple numbers in binary, into an automaton.
If we tried to feed them in sequentially, we'd want something like an automaton that can read in words on the alphabet $\{0,1,+,=\}$ like "101+11=1000" and tell us if they're true. The problem is that by the time we hit the plus sign, the automaton needs to have the entire first summand in memory, and we can't fit arbitrarily large summands in finite memory.
So what we'll do is we'll pad our numbers to be the same length and feed them in simultaneously. For instance, the sum above becomes
$$\begin{pmatrix}0\\0\\1\end{pmatrix}\begin{pmatrix}1\\0\\0\end{pmatrix}\begin{pmatrix}0\\1\\0\end{pmatrix}\begin{pmatrix}1\\1\\0\end{pmatrix}$$The first row is our first addend, the second row is our second addend, and the third row is our sum. We feed this into our automaton as a word of $3$-vectors on $\{0,1\}$. (There are only $8$ of them, so it's still a finite alphabet.)
You can create an automaton / regular expression that accepts only correct addition facts when entered in this way. It's a little bit easier to construct this automaton if you decide to read in the input from right to left, but ultimately it doesn't matter which convention you decide on.
This automaton corresponds to the formula $\varphi(x,y,z) \equiv x+y=z$ in Presburger arithmetic.
So the translation is: given a formula $\varphi$ in Presubrger arithmetic with free variables $x_1,\ldots,x_n$, there is an automaton / regular language on the alphabet $\{0,1\}^n$ that accepts a tuple of numbers read in simultaneously iff $\varphi$ holds of that tuple of numbers.
And the translation is almost exact: given an automaton that reads in a tuple of numbers fed in in binary simultaneously, there's a formula in Büchi arithmetic (https://en.wikipedia.org/wiki/Büchi_arithmetic) that's equivalent to it. Büchi arithmetic is Presburger arithmetic with an added function $V_2(x)$ which returns the largest power of $2$ dividing $x$. If you want to read more, you're likely to find more information looking into why Büchi arithmetic is equivalent to finite automata.
You might be able to use this to get quantifier elimination in Presburger arithmetic, but the technique I know of is explained in Christoph Haase's "A Survival Guide to Presburger Arithmetic" https://www.cs.ox.ac.uk/people/christoph.haase/home/publication/haa-18/haa-18.pdf which essentially boils down to this:
To get quantifier elimination in Presburger arithmetic, you need to add inequalities and the ability to assert that two terms are equivalent modulo various natural numbers.
Any formula in this augmented Presburger arithmetic of the form $\exists y: \varphi(x_1,\ldots,x_n;y)$ asserts a bunch of inequalities and modular congruences for $ky$ for some constant $k$. Replace $ky$ with $z$, so we're asserting an extra modular congruence that $z$ is congruent to $0$ mod $k$.
By the Chinese remainder theorem, we're just searching for a $z$ with particular congruences modulo some big modulus $M$. To do this, we only need to search the $M$ entries on the left or right ends of the ranges given by the inequalities.
For instance, if we want to eliminate the quantifier from $$\exists z: (3a+4b \leq z \leq 5a+2b+10) \wedge (z \equiv 12a+2b+7 (\text{mod} 5)),$$ we just need to check to see if one of: $3a+4b, 3a+4b+1, 3a+4b+2, 3a+4b+3,$ or $3a+4b+4$ works for $z$. i.e. we can convert this $\exists z: \varphi(a,b;z)$ to $$\varphi(a,b;3a+4b) \vee \cdots \vee \varphi(a,b;3a+4b+4).$$
0 comment threads