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?
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.