Timeline for Tarski-Seidenberg for strict inequalities and bounded quantification
Current License: CC BY-SA 4.0
19 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 3 at 19:04 | comment | added | Dima Pasechnik | Naively, after elimination one ends up with a quantifier-free formula with only $>,<,=$ (finitely many systems of strict inequalities and equations joined by $\vee$) but because it's an open set, all the atoms with $=$ are redundant, and so one ends up with a "My Language" formula. That's basically done in Paul's answer, right? | |
| Sep 3 at 18:48 | comment | added | Dima Pasechnik | sorry, indeed, I should have been drawing graphs. :/ Do I get it right that one basically wants to have an algorithm to convert a usual formula of an open semialgebraic set (obtained by quantifier elimination over reals, e.g. as in Basu-Pollack-Roy) into a "My Language" formula? | |
| Sep 3 at 18:43 | history | edited | Dima Pasechnik | CC BY-SA 4.0 |
again the opposite
|
| Sep 3 at 17:48 | history | edited | Dima Pasechnik | CC BY-SA 4.0 |
correct signs
|
| Sep 3 at 17:34 | comment | added | Paul Taylor | Anyway, the relevance of this discussion to the Question is that elimination of the quantifiers is more complicated than one might expect. But I would still like to know the constructive semi-algebraic geometry algorithm for quantifier elimination for my bounded language of open subspaces. | |
| Sep 3 at 17:22 | comment | added | Paul Taylor | Multiplication and division with signed reals is infuriating. Drawing the graph of reciprocal seems to be the clearest way of getting it right. In fact @DimaPasechnik was correct first time: if $0\leq a\leq b$ then $\forall y:[a,b].x y\neq 1$ is $x a>1 \lor x b< 1$ and $\forall y:[-a,b].x y\neq 1$ is $-1<x a\land x b< 1$. | |
| Sep 3 at 17:16 | comment | added | Paul Taylor | @AndreasBlass. Universal quantification over a compact (sub)space preserves openness: Leopoldo Nachbin 1992 (Martin Escardo told me it was 1950). For existential quantification, overtness plays the role of compactness. | |
| Sep 3 at 16:39 | comment | added | Andreas Blass | I'm pretty sure that, with classical foundations (ZFC to be specific), the projection from a product space $X\times Y$ to a factor $X$ is a closed map provided the other factor $Y$ is compact. That is, existential quantification over a compact space preserves closedness. Scattering negations through that result, we get that universal quantification over a compact space preserves openness. (Unfortunately, I don't know what happens when the foundations are constructive.) | |
| Sep 3 at 16:19 | comment | added | Dima Pasechnik | @PaulTaylor - my objection still stands. One doesn't always get an open set after eliminating $y$ here. | |
| Sep 3 at 16:15 | history | edited | Dima Pasechnik | CC BY-SA 4.0 |
restored the original meaning
|
| Sep 3 at 15:54 | comment | added | Dima Pasechnik | bounds should be OK now. Apologies, I haven't been working in this area since 2010, feel very rusty. | |
| Sep 3 at 15:50 | history | edited | Dima Pasechnik | CC BY-SA 4.0 |
correct elimination result
|
| Sep 3 at 15:10 | comment | added | Dima Pasechnik | Yes, bounds on $x$ wrong, I can fix these. Or I can remove it, even though it explains why you need bounded ranges of elimination, IMHO. | |
| Sep 2 at 20:46 | comment | added | Dima Pasechnik | oops, right. I converted my answer into a comment. | |
| Sep 2 at 20:45 | history | edited | Dima Pasechnik | CC BY-SA 4.0 |
made the statement correct; Post Made Community Wiki
|
| Sep 2 at 20:26 | comment | added | Emil Jeřábek | Actually, you end up with $-1/10<x<1/10$. | |
| Sep 2 at 20:16 | comment | added | Dima Pasechnik | still, if you only allow, say, $-10\leq y\leq 10$, you end up with $x=0$, | |
| Sep 2 at 20:03 | comment | added | Paul Taylor | In my language, universal quantification is only allowed over compact subspaces, which in $\mathbb R$ may be encoded using just intervals. | |
| Sep 2 at 19:56 | history | answered | Dima Pasechnik | CC BY-SA 4.0 |