I lack much of the theoretical background for QE (my background is primarily optimization and control), but have stumbled across it in the process of learning about hybrid automata & decidability. From what little reading I've done, it seems QE is typically only applicable to polynomials, the most ubiquitous example being the relationship between quadratics and the discriminant.
What prevents quantifier elimination from being possible over general functions (without simply approximating by a truncated power series or some kind of piecewise affine approximation)? What other functions forms if any, beyond polynomials, are we able to perform quantifier elimination on? Why / why not?
Suggestions on good jumping-off points into the literature would be greatly appreciated as well; beyond cylindrical algebraic decomposition I'm a bit lost, both on context / motivation and prerequisite theory to read up on.
EDIT: As suggested by Rodrigo de Azevedo in the comments below, MetiTarski is an interesting approach to QE for non-polynomial predicates. Most of their approach appears to be along the lines of sandwiching functions with conservative polynomial approximations (truncated Taylor series), from above and below.