The stipulation that term-reduced formulas will suffice still allows for constants to show up in S-formulas.
if anyone has the book "Mathematical Logic" by Ebbinghaus, Flum and Thomas, I'd like to check if the pf of thm 1.3 on pg 117 is correct. I don't think it is. In the pf of part (a)we're not told anything about possible S-formulas where constant symbols appear. The pf of equivalence would be completely non-trivial when we have to deal with such formulas. Can someone tell me why it is that this case isn't treated?