Consider the set of statements of arithmetic, such that:
the statement contains no existential quantifiers, only universal quantifiers;
the statement contains only logical
andand not logical
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?