Timeline for getting rid of existential quantifiers
Current License: CC BY-SA 3.0
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 22, 2012 at 8:20 | vote | accept | James Propp | ||
| Mar 6, 2012 at 23:24 | answer | added | Goldstern | timeline score: 2 | |
| Mar 6, 2012 at 22:14 | answer | added | Neil Strickland | timeline score: 1 | |
| Mar 6, 2012 at 21:50 | comment | added | Zhen Lin | To amplify Qiaochu's point, one should note that in many cases of interest, the inversion map of a group object is required to be a morphism in the same category: for example, topological groups, Lie groups, algebraic groups, etc. Though there are some cases where something odd happens with inverses, like partially-ordered groups... | |
| Mar 6, 2012 at 21:42 | answer | added | Goldstern | timeline score: 4 | |
| Mar 6, 2012 at 21:17 | answer | added | François G. Dorais | timeline score: 14 | |
| Mar 6, 2012 at 17:21 | history | edited | Amit Kumar Gupta |
edited tags
|
|
| Mar 6, 2012 at 12:28 | answer | added | Jirka Hanika | timeline score: 5 | |
| Mar 6, 2012 at 4:46 | comment | added | Qiaochu Yuan | In category theory the existential quantifier definition of inverses is problematic because not all categories have a good notion of element; one nice aspect of the definition in terms of the identity and inverse as primitives is that all of the axioms merely assert the equality of various compositions of morphisms so the axioms can be interpreted in any (monoidal) category. A relevant keyword here is "Lawvere theory," I guess. | |
| Mar 6, 2012 at 3:30 | comment | added | Gerhard Paseman | Another technique that might interest you is Skolemization. Look it up for the actual detail, but as I recall existentially qualified variables are replaced by function symbols with the function depending on some outer universally quantified variables. Gerhard "Ask Me About System Design" Paseman, 2012.03.05 | |
| Mar 6, 2012 at 2:48 | comment | added | Benjamin Steinberg | The formulation in terms of the identity and inverse as primitives is the standard viewpoint in universal algebra where one sticks to universal quantifiers. | |
| Mar 6, 2012 at 1:37 | comment | added | Gerald Edgar | Here is a small amount on quantifier elimination: en.wikipedia.org/wiki/Quantifier_elimination | |
| Mar 6, 2012 at 1:28 | history | asked | James Propp | CC BY-SA 3.0 |