What is the origin of Büchi arithmetic? Wikipedia only says it is named in his honour.
"A Survival Guide to Presburger arithmetic" mentions in section 6.1 what was the motivation for the arithmetic.
Edit
From this paper:
A basic result about Büchi arithmetic is that a subset $X \subseteq \mathbb{N}^n$ is first-order definable over $\langle \mathbb{N}, +, V_p \rangle$ if and only if $X$ is p-automatic, that is, recognisable by an automaton under a base-p encoding of natural numbers. This result was first stated by Buchi in [they cite this paper].
Now the question is within this paper where is the result stated.
In Büchi's "Weak Second-Order Arithmetic and Finite Automata", Section 5, Theorem 4, Büchi states that the natural numbers with + and a predicate recognizing powers of 2 ($Pw_2$) is expressively equivalent to the Weak Monadic Second-Order Theory of 1 Successor.
However, the proof there is fundamentally wrong. Büchi claims that: $$E(x,y): Pw_2(x) \wedge \exists u, v: [(y=u+x+v) \wedge (u < v) \wedge [v = 0 \vee 2x \leq v]]$$ is an expression of "$x$ occurs in the representation of $y$ as a sum of powers of 2". But the requirement on $v$ (meant to represent the digits to the left of $x$) actually needs to be that it is divisible by $2x$.
Thanks to MauroALLEGRANZA's comment I was able to find "Logic and $p$-Recognizable Sets of Integers" (Bruyère, V., Hansel, G., Michaux, C., Villemaire, R., 1994 https://doi.org/doi:10.36045/bbms/1103408547) which elaborates on the history from there in section 4.4:
R. MacNaughton pointed out this mistake in his 1963 review of Büchi's paper (Journal of Symbolic Logic 28.01) and proposed an easy fix of replacing "is a power of 2" by $E(x,y)$ above.
Someone named M. Boffa suggested to V. Bruyère in a personal communication in 1985 to replace $E(x,y)$ with the $V_p$ predicates now in use, which he published in something called "Entiers et automates finis, Mémoire de fin d’études, Université de Mons (1985)". I don't know French and can't find the paper so any help with this bit would be appreciated.
C. Michaux and F. Point also prove the equivalence using $V_p$ in "Les ensembles $k$-reconnaissables sont définissables dans <$\mathbb{N},+,V_k$> C.R. Acad. Sci. Paris 303 (1986)." Which I also can't find.
Are these two papers aware of each other? V. Bruyère and C. Michaux collaborated in the 1994 paper.