Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

I have to remove the existential quantifier from the following formula:

$$\exists i\left[\left(i \geq 0\right) \land \left(z-2i = 0\right) \land \left(y+i=x\right)\right]$$

First I make some simple transformations:

$$\exists i\left[\left(i \geq 0\right) \land \left(\frac{z}{2} =i\right) \land \left(x-y=i\right)\right]$$

We can get rid of $\exists i \geq 0$ because we can simply pick such an $i$

So we can move the existential quantifier inwards and arrive at:

$$\left(\frac{z}{2} \geq 0\right) \land \left(x-y \geq 0\right)$$

Is this a valid way to get rid of the existential quantifier?

share|cite|improve this question
I think there is a typo in your question. From $y+1=x$ you deduce $x-y=i$. Should it not start with $y+i=x$? – drhab Jan 29 '14 at 10:41
yeah thank you. i've edited my question – user1291235 Jan 29 '14 at 10:42
I don't know whether the 'way is valid' (I am not familiar with logic) but the conclusion is correct. You can make it look a bit more concise: $z\geq0\wedge x\geq y$ – drhab Jan 29 '14 at 10:45
What is "get rid of existencial quantificator" for you? And $z=2(x-y)$ is required. – Martín-Blas Pérez Pinilla Jan 29 '14 at 10:45
The statement that you arrive at does not imply the original one. You should come to: $2x-2y=z\geq 0$ – drhab Jan 29 '14 at 10:54
up vote 1 down vote accepted

In formal logic, the way to "get rid" of an existential quantifier is through the so-called $\exists$-elimination rule; see Natural Deduction.

If you have proved or assumed that $\exists x \phi(x)$, you can procede assuming $\phi(n)$, provided that $n$ is new, i.e.there are no other assumptions in your proof that use $n$ [this corerspond to the "intuitive" way of reasoning: I know that a number exists such that $\phi$; call it $n$].

Then, from assumption $\phi(n)$ you derive a statement $\psi$.

If $\psi$ does not use $n$, you can discharge (i.e."remove") the assumption $\phi(n)$ and you have obtained a proof of $\psi$ from $\exists x \phi(x)$, i.e.

$\exists x \phi(x) \vdash \psi$.

In your application, you have assumed $i$ such that $i \ge 0$; then you have derived the two inequalities $\psi_1$ and $\psi_2$ that do not include $i$ any more; so you can say that :

$\exists i ( i \ge 0) \vdash \psi_1 \land \psi_2$.

share|cite|improve this answer

$\exists i\left[i\geq0\wedge\frac{z}{2}=i\right]$ and $z\geq0$ are equivalent statements.

Secondly $\exists i\left[\frac{z}{2}=i\wedge x-y=i\right]$ and $2x-2y=z$ are equivalent.

This combined tells us that $\exists i\left[i\geq0\wedge\frac{z}{2}=i\wedge x-y=i\right]$ and $2x-2y=z\wedge z\geq0$ are equivalent statements.

share|cite|improve this answer

This is true: $$ (x\ge y)\land(z=2(x-y))\Longrightarrow\exists i(i\ge 0\land(z-2i=0)\land (y+i=x)). $$ (namely, $i=x-y$)

But this is false: $$ (\frac{z}{2}\geq 0)\land(x-y\geq 0)\Longrightarrow\exists i(i\ge 0\land(z-2i=0)\land (y+i=x)). $$ (when $z\ne 2(x-y)$)

share|cite|improve this answer

You can remove this quantifier using (what Dijkstra-Scholten and Gries-Schneider call) the one-point rule.

In general, this rule is $$ \langle \odot x : x = E : P(x) \rangle \;=\; P(E) $$ provided $\;E\;$ does not contain $\;x\;$, where $\;\odot\;$ is any symmetric and associative operator.

In this case, the operator is $\;\lor\;$, which in a quantification we customarily write as $\;\exists\;$.

So we can calculate: \begin{align} & \langle \exists i :: i \geq 0 \;\land\; z-2i = 0 \;\land\; y+i=x \rangle \\ = & \qquad \text{"arithmetic -- to introduce $\;i = \ldots\;$"} \\ & \langle \exists i :: i \geq 0 \;\land\; i=z/2 \;\land\; y+i=x \rangle \\ = & \qquad \text{"rewrite to match the form of the rule given above"} \\ & \langle \exists i : i=z/2 : i \geq 0 \;\land\; y+i=x \rangle \\ = & \qquad \text{"one-point rule: substitute $\;z/2\;$ for $\;i\;$"} \\ & z/2 \geq 0 \;\land\; y+z/2=x \\ \end{align} Or alternatively: \begin{align} & \langle \exists i :: i \geq 0 \;\land\; z-2i = 0 \;\land\; y+i=x \rangle \\ = & \qquad \text{"arithmetic -- to introduce $\;i = \ldots\;$"} \\ & \langle \exists i :: i \geq 0 \;\land\; z-2i = 0 \;\land\; i=x-y \rangle \\ = & \qquad \text{"rewrite to match the form of the rule given above"} \\ & \langle \exists i : i=x-y : i \geq 0 \;\land\; z-2i = 0 \rangle \\ = & \qquad \text{"one-point rule: substitute $\;x-y\;$ for $\;i\;$"} \\ & x-y \geq 0 \;\land\; z-2(x-y) = 0 \\ \end{align}

share|cite|improve this answer
See several other answers of mine for applications of this rule. – Marnix Klooster Jan 30 '14 at 19:53

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.