Slaughtering Competition Problems with Quantifier Elimination
22 Dec 2021 - Tags: sage , featured
Anytime I see questions on mse that ask something “simple”, I feel a powerful urge to chime in with “a computer can do this for you!”. Obviously if you’re a researching mathematician you shouldn’t waste your time with something a computer can do for you, but when you’re still learning techniques (or, as is frequently the case on mse, solving homework problems), it’s not a particularly useful comment (so I usually abstain). The urge is particularly powerful when it comes to the contrived inequalities that show up in a lot of competition math, and today I saw a question that really made me want to say something about this! I still feel like it would be a bit inappropriate for mse, but thankfully I have a blog where I can talk about whatever I please :P So today, let’s see how to hit these problems with the proverbial nuke that is quantifier elimination!
I want this to be a fairly quick post, so I won’t go into too much detail. The gist is the following powerful theorem from model theory:
Tarski-Seidenberg Theorem If $\varphi$ is any formula of the form $p(\overline{x}) = 0$, for $p \in \mathbb{R}[\overline{x}]$
$p(\overline{x}) \lt 0$, for $p \in \mathbb{R}[\overline{x}]$
combinations of the above using $\lor$, $\land$, $\lnot$, $\to$
combinations of the above using $\exists$ and $\forall$ Then $\varphi$ is equivalent to a formula without quantifiers.
I’m legally required to give the following example:
The formula $\exists x . a x^2 + bx + c = 0$ (which has a quantifier) is equivalent to the formula $b^2 - 4ac \geq 0$
... continue reading