# Decidability of quantifier-free formulae in Peano- and True Arithmetic

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?

• 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. Commented Jun 5, 2016 at 21:48
• @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. Commented Jun 5, 2016 at 21:50
• can we please rename "true arithmetic" into "zfc arithmetic" Commented May 21, 2018 at 13:12
• @mercio I don't mind, but "true arithmetic" is a widely used name, pace the eponymous Wikipedia article. Commented May 21, 2018 at 16:18