I've been doing a bit of independent research on existential quantification, and I was wondering if anyone could tell me if I have the hang of it. Here's a statement regarding the intermediate value theorem of calculus:
If $f$ is a function of $x$ that is continuous on the interval $[a,b]$, then $$\exists\left( p\in [a,b]\right)\,\left( f(p)\in [f(a),f(b)]\right)$$ is true.
If it helps, I typed this as
If $f$ is a function of $x$ that is continuous on the interval $[a,b]$, then $$\exists\left( p\in [a,b]\right)\,\left( f(p)\in [f(a),f(b)]\right)$$ is true.
If you are having trouble with existential quantifiers, there are just four rules that govern its usage in a mathematical proof (with each quantifier explicitly restricted to a set):
From $\exists x\in A: P(x)$, we can infer that $y\in A$ and $P(y)$ where $y$ is a free variable not previously used in that proof. (Existential specification or instantiation.)
(EDIT) From $y\in A$ and $P(y)$, we can infer that $\exists y\in A: P(y)$, or that $\exists x\in A: P(x)$ where $x$ is not a bound variable in $P(y)$, and where $P(x)$ is formed replacing some or all occurrences of $y$ in $P(y)$ with $x$. (Existential generalization)
From $\exists x\in A: P(x)$, we can infer that $\neg \forall x\in A:\neg P(x)$. (Changing quantifier, $\exists \to \forall$)
From $\forall x\in A:P(x)$, we can infer that $\neg\exists x\in A: \neg P(x)$. (Changing quantifier, $\forall \to \exists$)
where $A$ is a set and $P$ is a unary predicate.
Note that: $$\exists x\in A: P(x) \equiv \exists x: [x\in A \land P(x)]$$ $$\forall x\in A: P(x) \equiv \forall x: [x\in A \implies P(x)]$$
Avoid the construct:
$$\exists x: [x\in A \implies P(x)]$$
Very strange things can happen otherwise! (See "Drinker's Paradox" at Wikipedia and at my blog.)