Talk: Existential quantification
From open-encyclopedia.com - the free encyclopedia.
Someone may just want to find a simple description of existential quantifier. It may be a overkill to direct the reader to the article "existential quantification". -- User:Wshun
How do you learn about a symbol without knowing what it means? The existential quantifier (what you call the symbol) is not a mathematical concept; existential quantification is. This isn't MathWorld, thank goodness; we're not writing a dictionary, and we don't have a separate article on every variation in terminology.
OTOH, you've started material related to uniqueness quantification, so I'd better start that article!
-- Toby Bartels 02:52 25 Jul 2003 (UTC)
Feel free to redirect it to existential quantification, but please explain what an existential quantifier is in that article in a way that the explanation is easy to locate.
I did not start uniqueness quantification. You can read the history of this article. wshun 03:18 25 Jul 2003 (UTC)
You're right, I have Poor Yorick to thank for stimulating me into action.
Looking over the quantification articles just now, I think that they're too unwieldy, and in even worse ways than not being able to find these variant terms easily. I need to go to bed now and will be gone for a couple of days, but Sunday I plan to rearrange all of these articles to make everything easier to find. Then I'll want your opinion on how well I did! ^_^ In the meantime, I'm not moving anything anymore. -- Toby Bartels 03:55 25 Jul 2003 (UTC)
OK, done. Please look and give your opinion. -- Toby Bartels 21:09, 2 Aug 2003 (UTC)
Skolemization
Um, what's wrong with my definition of skolemization? —Ashley Y 11:24, 2004 Aug 20 (UTC)
- Skolemization is a method of reordering quantifiers to move existential quantifiers to the left, like this:
- <math>\forall{a}{\in}\mathbf{A}.\exists{b}{\in}\mathbf{B}.P(a,b)<math>
- is equivalent to
- <math>\exists{f}{\in}\mathbf{A}\rightarrow\mathbf{B}.\forall{a}{\in}\mathbf{A}.P(a,f(a))<math>
- Your understanding is correct, but
- A->B is not a standard notation for the set of functions from A->B
- It moves from first-order logic (where Skolemization is normaly used) to second order logic (quanitfication over functions)
- Normally, the existance of f is postulated implicitely as a concrete function, not a higher-order variable. In that case, a formula and its Skolemized form are not equivalent (because Interpretations and hence Models change), but equisatisfiable.
- --Stephan Schulz 09:45, 14 Oct 2004 (UTC)
