Get rid of an existential quantifier

Question

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?

Answer 1

$\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.

Answer 2

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$.

Answer 3

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)$)

Answer 4

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}