# Building a verifier for sentences involving addition over the natural numbers

Consider the model $(\mathbb{N},+)$; that is, the natural numbers equipped with the addition relation, PLUS($x$,$y$,$z$), where PLUS($x$,$y$,$z$) is true iff $x + y = z$. Let Th$(\mathbb{N},+)$ be the theory of this model; that is, the set of true sentences in the language of the model. For example, the sentence $\forall x \exists y [x + x = y]$ is a true sentence in this model. Let's assume for simplicity that all of these sentences are in prenex normal form.

I'm interested in coming up with either an (efficient) verifier for Th$(\mathbb{N},+)$ or a nondeterminstic algorithm that decides Th$(\mathbb{N},+)$. In the former case, I'm wondering what a certificate could be. If all of the quantifiers in the input statement are existential, this isn't a problem: a certificate would just be an assignment of all the variables. However, things are made difficult when the input has a universal quantifier, since it isn't obvious how we can check that something holds for all members of an infinite set.

$\left(\mathbb{N},+\right)$ is a model of Presburger arithmetic. Persburger arithmetic is a complete theory (see the answer here), so for any model $\mathcal M$ for Presburger arithmetic (lets denote this theory by $T$) and every first order formula $\varphi$ in the language of $T$ it holds that:
$\mathcal{M}\vDash \varphi \iff T \vdash \varphi$
To see why this follows for completeness, assume $M\vDash \varphi$, then obviously $T\not\vdash \neg\varphi$, thus by completeness $T\vdash\varphi$ (the $\Leftarrow$ implication is trivial).