# Are statements of arithmetic without logical negation or existential quantifiers decidable?

Consider the set of statements of arithmetic, such that:

• the statement contains no existential quantifiers, only universal quantifiers;

• the statement contains only logical and and not logical or; and

• the statement contains no logical negations.

For exact details of the language, see here.

Is there a formal system that can decide the truth of all such statements, or does the incompleteness theorem guarantee that some will always be undecidable?

• Well, the first thing to note is you can reduce the formula to a conjunction of universally quantified atomic formulas which we can attempt to decide separately. So the question is whether we can determine if one (multi-variate) polynomial with integer coefficients is or is not pointwise greater than another polynomial when viewed as functions of integers. – Derek Elkins Apr 3 '18 at 5:34
• @DerekElkins thanks, that's helpful. Of course that then boils down to whether we can decide whether a single multivariate polynomial is greater than zero for all integer values of its variables. That sounds like it should be decidable, but I don't know straight away. – Nathaniel Apr 3 '18 at 5:46
• "The incompleteness theorem" isn't the claim that a logic is incomplete. It is much stronger than that. "The incompleteness theorem" still applies to complete logics. – DanielV Apr 3 '18 at 7:15
• @DanielV in the comments we are discussing what would happen if you removed negation. For equality, what's wrong with a<b+1 & b<a+1? – Nathaniel Apr 3 '18 at 7:43

It looks like you're working in $\mathbb{Z}$ and your language consists of: variables, numerals such as 1, plus, times, minus, $\wedge$, $\forall$, and $>$. If this is correct, then your problem is undecidable, because we can inject the known-to-be-undecidable problem:
Does the the multivariable polynomial $p$ have integer roots?
by squaring the polynomial and asking whether $\forall \vec x \;( p(\vec x) ^2 > 0).$