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

Question

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?

Answer 1

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

The undecidability of this problem is known as Matiyasevich's Theorem, among other names.