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?