Timeline for getting rid of existential quantifiers
Current License: CC BY-SA 3.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 22, 2012 at 8:20 | vote | accept | James Propp | ||
| Mar 9, 2012 at 19:43 | comment | added | Tegiri Nenashi | But there is more more than one choice for midpoint. One can argue that mediant is more natural than arithmetic average:-) | |
| Mar 7, 2012 at 14:56 | comment | added | Dave Marker | For orders like $({\mathbb Q},<)$ or $({\mathbb R},<)$ one could interpret the Skolem function in a natural way, say as midpoint, to preserve many of the nice model theoretic properties (decidability, o-minimality...). This becomes much less clear for algebraically closed fields where there are no canonical choices for Skolem functions. I believe there is a result, perhaps of Ash and Nerode, saying that there are no nice Skolemizations, but I don't recall if they were considering decidability or stability (or both). | |
| Mar 7, 2012 at 12:16 | comment | added | Emil Jeřábek | In particular, Skolemization is often unnatural when the existential quantifier does not have a unique or canonical witness. For instance, in the density axiom the quantifier can be witnessed by any element of the interval $(x,y)$ equally well, and it does not feel natural to arbitrarily pick one out. Also, when Skolem functions are not definable, their introduction can mess up properties of the theory: the theory of dense linear orders is complete and decidable, and it has elimination of quantifiers, which all fails for its Skolemized version. | |
| Mar 6, 2012 at 21:17 | history | answered | François G. Dorais | CC BY-SA 3.0 |