Showing that Presburger arithmetic is decidable by deciding if $\mathbb N \models \varphi$, but does it give provability in the axioms?

Here Presburger arithemtic is given by a set of axioms over the signature with binary operation $+$ and two constants $0$ and $1$. Similarly in Presburgers original paper he gives the arithmetic in terms of an axiomatic system. With this decidability could be proven by quantifier eliminiation, reducing everything to equations or congruence relations, which for fixed numerals are provable iff they are true in $\mathbb N$.

Another approach I have seens shows that the structure $\mathbb N$ with $+$ and $0$ and $1$ is decidable, i.e. that the set $$\mbox{Th}(\mathbb N) = \{\varphi \mid \mathbb \models \varphi \}$$ is decidable, where the formulas have signature $+$ with $0$ and $1$. This approach constructs finite automata, see for example these lecture notes. These automata are a particular simple computational model, and most basic questions and constructions are decidable, which gives decidability for the above sentences, as to every formula an automaton could be constructed.

But isn't the second approach weaker than the first? I mean the first one implies that $\mbox{Th}(\mathbb N)$ is decidable, but in the second approach there is still the question for a meaningful axiomatic system in which we could construct proofs? Surely, we can take $\mbox{Th}(\mathbb N)$ itself as a decidable axiom system, and then every sentence proofs itself, but this seem a little bit artificial.

So am I right? Or does I overlook something, and the second approach also gives provability in the axiom systems referred to in the first paragraph?

• Can you please explain the differences between the two theories? I am confused, because in the link to the lecture notes you posted, it is claimed that Presburger arithmetic does not admit quantifier elimination, and he even gives an example of a sentence which has no quantifier-free formula, namely, $\exists y (x = y+y)$. Thank you. – Ekanshdeep Gupta Mar 9 at 7:26
• @EkanshdeepGupta According to the original paper formulas with quantifiers would be converted into congrunce equations/divisibility statements, your example would be $x \equiv 0 \pmod{2}$. So, the language must be enlarged to allow these statements. See, for example en.wikipedia.org/wiki/Presburger_arithmetic where it is written: "The decidability of Presburger arithmetic can be shown using quantifier elimination, supplemented by reasoning about arithmetical congruence". – StefanH Mar 9 at 23:44

• Regarding your last sentence, you mean that these sets are the boolean closure of the sets $\{ (n,n) : n \in \mathbb N \}$ and $\{ (n,m) \mid n \equiv m \pmod{k} \}$ for some fixed $k$ (those sets came from the basic relations to which everything is reduced by quantifier elimination)? – StefanH Apr 11 '18 at 19:06