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?

  • 2
    $\begingroup$ 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. $\endgroup$ – Derek Elkins Apr 3 '18 at 5:34
  • $\begingroup$ @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. $\endgroup$ – Nathaniel Apr 3 '18 at 5:46
  • $\begingroup$ "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. $\endgroup$ – DanielV Apr 3 '18 at 7:15
  • 2
    $\begingroup$ @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? $\endgroup$ – 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).$

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

  • $\begingroup$ A detailed exposition of this theorem (suitable for students) was presented in American Mathematical Monthly, circa 1972. $\endgroup$ – DanielWainfleet Apr 3 '18 at 7:34
  • $\begingroup$ Thank you, I believe this is the answer. (You are correct in your interpretation of the question.) $\endgroup$ – Nathaniel Apr 4 '18 at 9:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.