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.

1 Answer

$\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).

This shows you why your question reduces to finding a decision procedure for Presburger arithmetic. This has a known double-exponential lower bound, you can find a proof in Rabin and Fischer's paper "Super-Exponential Complexity of Presburger Arithmetic". This bound also holds for nondeterminstic algorithms.