Decidability of equations in True Arithmetic

81 Views Asked by At

Is the validity of equations (with variables) in True Arithmetic decidable? In 1, Andreas Blass argues that validity of negated equations is undecidable by sketching a reduction of Hilbert's 10th problem. But what about pure equations (or, equivalently, universally quantified equations)?