# What is the interpretation of Presburger Arithmetic in WS1S?

It’s my understanding that Julius Büchi showed that $$WS1S$$, the weak monadic second-order theory of one successor is decidable by a finite-state automaton, and that this implies that Presburger arithmetic, the first-order theory of successor and addition, is also decidable by a finite-state automaton.

But my question is, why does the first statement imply the second? What is the definition/interpretation of Presburger arithmetic in $$WS1S$$?

In order to be able to express $$+$$ in WS1S, you can encode a natural number in terms of its expansion in base 2. So the set $$X$$ encodes $$\sum_{i \in X} 2^i$$. To check if two encodings of numbers $$A,B$$ sum to $$E$$, you need a third set $$C$$ describing the set of carry digits, and using boolean logic specify the correct interrelationships between whether $$i \in A, i \in B, i \in C, i \in E, succ(i) \in C$$ for all $$i$$.
This boolean relationship is just elementary-school arithmetic in base 2: if at least two of $$i \in A, B, C$$ then $$succ(i) \in C$$, and if an odd number of $$i \in A, B, C$$ then $$i \in E$$.
You can define $$\leq$$ in terms of $$+$$ of natural numbers.
Note that you can define $$\leq$$ for unencoded natural numbers directly in terms of predecessor-closed sets. A set $$X$$ is predecessor-closed if $$S(x) \in X \implies x \in X$$. Then $$x \leq y$$ if every predecessor-closed set containing $$y$$ also contains $$x$$, but this doesn't help answer your question since $$+$$ for unencoded natural numbers cannot be expressed in WS1S.