Proving decidability of $(\mathbb N, +)$ with Quantifier elimination and evaluating basic formulas The original proof of the decidability of Presburger arithmetic goes by Quantifier elimination, for example noting that
$$
 \exists x (\underbrace{x + \ldots + x}_{\alpha\mbox{ times}} + b = c )
$$
is equivalent with $b \equiv c \pmod{\alpha}$, and such a congruence statement is easily decidable. The proof reduces every formula to a boolean combination of such basic formulas.
Surely, by this reasoning I see that
$$
 \mbox{Th}(\mathbb N) := \{ \varphi \mid \mathbb N \models \varphi \}
$$
is a decidable theory, i.e. for every formula with summation I can decide if it holds or not when interpreted in the natural numbers.
But what Presburger actually is doing, is he gives a decidable set of axioms, considers the closure under deduction of these axioms. And uses the above arguments to conclude that set of all deducable formulas from the axioms is decidable.
But what I do not understand about this reasoning is that if I denote the set of  axioms by $\Delta$, then by soundness
$$
 \{ \varphi \mid \Delta \vdash \varphi \} 
 \subseteq \mbox{Th}(\mathbb N).
$$
But why should these sets be equal? To be more specific, given a formula $\varphi$, reduce it to a formula which is simply decidable over $\mathbb N$, then that it is fullfilled over $\mathbb N$ does not has to imply that $\Delta \vdash \varphi$ holds?
EDIT: A translation of Presburgers article could be obtained here. In the introduction of the translator it is said that

A disjunt consisting of an equation
  $$
 \exists x (\alpha x + a = b) \mapsto a \equiv_{\alpha} b
$$
  is really the definition of congruence. It appears to be cheating to eliminite a quantifier by forming a congruence, but it is computationally easy to determine if two numbers are congruent.

The problematic parts is "computationally easy to determine". Surely it is easy, but does it imply provability in the axiomatic system?
 A: What the quantifier elimination proves is that the axiomatic theory $\Delta$ is complete: For every sentence $\varphi$, eliminating the quantifiers eventually produces one of
$$ \Delta \vdash \varphi\leftrightarrow\bot \qquad\text{or}\qquad
\Delta \vdash \varphi\leftrightarrow\top $$
Now suppose $\varphi$ is in $\operatorname{Th}(\mathbb N,{+})$. Since we're assuming that all the axioms are true in $\mathbb N$ and the logic is sound, this means that $\Delta\vdash\varphi\leftrightarrow\bot$ cannot be the case. But then $\Delta\vdash\varphi\leftrightarrow\top$ must be true. And that is just a few steps away from $\Delta\vdash\varphi$.

Edit: After a discussion in the comments, the crucial step seems to be that every formula of the shape $\exists x(\alpha x+b=c)$, where $b$ and $c$ are numerals, is either provable or disprovable.
If the formula is true in $\mathbb N$, then of course it is provable -- just insert the numeral for the $x$ that works and evaluate it.
If the formula is false in $\mathbb N$, then we can still just wing it. Prove by induction that
$$\tag{*} \forall x(x =0 \lor x=1 \lor x=2 \lor \cdots \lor x=c \lor x>c)$$
Then prove
$$\forall x(x>c \to \alpha x + b \ne c) $$
(assuming that $\alpha\ne 0$)
and you can now do a case analysis on (*) to show that no $x$ makes $\alpha x + b = c$ true, by evaluating the left-hand side for each possible $x$ that's not known to be too large.
