実閉体の量化記号の除去の一番簡単な例は二次方程式の判別式。
∃x(x^2+ax+b=0) は a^2-4b≧0 と同値。

代数閉体の場合だと、簡単な場合が Sturm の定理で、
一般の場合が Tarski-Seidenberg の定理でいいのかな。