= Existential quantification
{title2=$\exists x\,\varphi$}
{wiki}
<Existential quantification> forms $\exists x\,\varphi(x,\mathbf y)$. In a <first-order structure>, it is true at an assignment to $\mathbf y$ when some domain element makes the instance true. In <natural deduction>, elimination uses a fresh variable for the hypothetical witness; that variable may not escape into the conclusion or the remaining undischarged assumptions.
Existence requires at least one witness, not exactly one. Over the <natural numbers> $\mathbb N=\{0,1,2,\ldots\}$, $\exists m\,(m>5)$ is true: $m=6$ works, as do $7,8,\ldots$. In <intuitionistic first-order logic>, a direct proof supplies a witness together with a proof of the corresponding instance; merely rejecting nonexistence is generally weaker.
Placing <existential quantification> before <universal quantification> requires a single witness that works throughout:
$$
\exists m\in\mathbb N\,\forall n\in\mathbb N\;(m>n).
$$
This <first-order sentence> is false. For any proposed $m$, choose $n=m$: the required inequality becomes $m>m$. For example, $m=3$ works for $n=0,1,2$ but fails at $n=3$. No finite list of successful checks establishes <universal quantification> over the <natural numbers>.
Back to article page
