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?](https://math.codidact.com/posts/295470))
---
[^1]: An example of which is the way we prove the theory of dense linear orders complete.
[^2]: Roughly speaking, sentences with only $\exists$-quantifiers, none of which may be negated.
[^3]: 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 `(...)*(..)*`, …
clemens
·
2026-05-08T04:16:40Z (4 months ago)