4
$\begingroup$

It is well-known that validity in Peano Arithmetic is undecidable. It is less well-known that validity is already undecidable in True Arithmetic (the theory of the standard model of Peano Arithmetic).

But what about the quantifier-free fragments of Peano Arithmetic and True Arithmetic? My hunch is that they must be undecidable too. Where would I be looking for a discussion of these questions?

$\endgroup$
4
  • 3
    $\begingroup$ Are you asking about validity of quantifier-free sentences or quantifier-free formulas? Quantifier-free sentences don't involve any variables, so deciding their truth in the standard model or their provability in PA is easy. A quantifier-free formula, on the other hand, is valid iff its universal closure is. So the negative solution of Hilbert's 10th problem implies that there's no decision procedure even for negated equations. $\endgroup$ Commented Jun 5, 2016 at 21:48
  • $\begingroup$ @AndreasBlass I'm asking about quantifier-free formulas. I had forgotten about the universal closure thing. That settles it. Thanks. If you want to make your comment an answer, I can accept it. $\endgroup$ Commented Jun 5, 2016 at 21:50
  • $\begingroup$ can we please rename "true arithmetic" into "zfc arithmetic" $\endgroup$
    – mercio
    Commented May 21, 2018 at 13:12
  • $\begingroup$ @mercio I don't mind, but "true arithmetic" is a widely used name, pace the eponymous Wikipedia article. $\endgroup$ Commented May 21, 2018 at 16:18

1 Answer 1

4
$\begingroup$

There is no decision algorithm for validity in the standard model of negated equations between polynomials. The reason is that such a procedure would decide truth of universally quantified negated equations, and that amounts to the complementary problem of deciding existentially quantified equations. That would be an algorithmic solution to Hilbert's 10th problem, which is known to be impossible by the Davis-Putnam-Robinson-Matijasevich theorem.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .