Wednesday, October 5, 2011

Existential rules and more example proofs

1Existential quantifier rules¶

Continued from last class.

1.1Exists introduction¶

If you can do $\forall$-elimination, then you can do $\exists$-introduction, and vice versa.

1.2Exists elimination¶

$$\frac{\Gamma, \Phi(x) \vdash \Psi}{\Gamma, \exists x \Phi(x) \vdash \Psi}$$

provided $x$ is not free in $\Gamma$ or $\Phi$.

For example, if $x$ is rational, then there exist $a, b$ such that $a / b = x$.

Or, if $x$ is even, then $x^2$ is divisible by 4; let $x = 2y$, $x^2 = (2y)^2 = 4y^2$ so $4 \mid x^2$ where $y \in \mathbb{N}$. So $\exists y(x = 2y) \vdash 4 \mid x^2$. What?

2An example proof¶

"Every good boy deserves fudge. There exists a good boy. Therefore, there exists a boy that deserves fudge."

$$\forall x ((Bx \land Gx) \to Fx),\, \exists x (Bx \land Gx) \vdash \exists x (Bx \land Fx)$$

An alternative proof¹:

Note that if we replaced the last two lines by the following (switched order of $\exists$-elimination and introduction):

then this would not be valid, as there would be a free $x$ in (6') and so $\exists$-elimination could not be done. It would have to be done in the original order (from the alternative proof), to respect the free/bound limitations.

3An impossible proof¶

"There are boys. There are girls. Therefore there is someone who is both a boy and a girl."

$$\exists x Bx,\,\exists x Gx \vdash \exists x (Bx \land Gx)$$

We should not be able to prove this, and fortunately, we can't using the rules of formal logic. However, if one were to misuse the $\exists$-elimination rule (by not respecting the clash of variables thing) then this "proof" might result:

4A possible proof¶

"There are boys. There are girls. Therefore there is someone who is a boy and someone who is a girl."

$$\exists x Bx, \,\exists x Gx \vdash \exists y \exists x (By \land Gx)$$

Note: $\exists x Bx \vdash \exists y By$ may be logically provable, but it's not a tautology because it's not a logical theorem². Not that relevant, just a sidenote.