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$?
 A: 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.
