Wednesday, October 5, 2011 CC-BY-NC
Existential rules and more example proofs

Maintainer: admin

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

Sequent Justification/rule
(1) $(Bx \land Gx) \to Fx, \, Bx \land Gx \vdash Bx \land Fx$ Tautology
(2) $(Bx \land Gx) \to Fx,\,Bx \land Gx \vdash \exists x(Bx \land Fx)$ $\exists$-introduction from (1)
(3) $\forall x((Bx \land Gx) \to Fx) \vdash (Bx \land Gx) \to Fx)$ $\forall$-elimination
(4) $\forall x((Bx \land Gx) \to Fx),\, Bx \land Gx \vdash (Bx \land Gx) \to Fx$ Monotonicity from (3)
(5) $\forall x ((Bx \land Gx) \to Fx),\, Bx \land Gx,\,(Bx \land Gx) \to Fx \vdash \exists x(Bx \land Fx)$ Monotonicity from (2)
(6) $\forall x ((Bx \land Gx) \to Fx), \, Bx \land Gx \vdash \exists x (Bx \land Fx)$ Transitivity from (4), (5)
(7) $\forall x((Bx \land Gx) \to Fx) ,\,\exists x (Bx \land Gx) \vdash \exists x (Bx \land Fx)$ $\exists$-elimination

An alternative proof1:

Sequent Justification/rule
(1) $\forall x((Bx \land Gx) \to Fx) \vdash (Bx \land Gx) \to Fx$ $\forall$-elimination
(2) $(Bx \land Gx) \to Fx,\, Bx \land Gx \vdash Bx \land Fx$ Tautology
(3) $\forall x ((Bx \land Gx) \to Fx),\, Bx \land Gx \vdash (Bx \land Gx) \to Fx$ Monotonicity from (1)
(4) $\forall x ((Bx \land Gx) \to Fx),\, (Bx \land Gx) \to Fx,\,Bx \land Gx \vdash Bx \land Fx$ Monotonicity from (2)
(5) $\forall x ((Bx \land Gx) \to Fx),\, Bx \land Gx \vdash Bx \land Fx$ Transitivity using (3), (4)
(6) $\forall x ((Bx \land Gx) \to Fx),\,Bx \land Gx \vdash \exists x (Bx \land Fx)$ $\exists$-introduction from (5)
(7) $\forall x ((Bx \land Gx) \to Fx), \, \exists x (Bx \land Gx) \vdash \exists x(Bx \land Fx)$ $\exists$-elimination from (6)

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

Sequent Justification/rule
(6') $\forall x ((Bx \land Gx) \to Fx),\,\exists x (Bx \land Gx) \vdash Bx \land Fx$ $\exists$-elimination from (5)
(7') $\forall x((Bx \land Gx) \to Fx),\,\exists x (Bx \land Gx) \vdash \exists x (Bx \land Fx)$ $\exists$-introduction from (6')

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:

Sequent Justification/rule
(1) $Bx,\, Gx \vdash Bx \land Gx$ Tautology (valid)
(2) $Bx, \, Gx \vdash \exists x (Bx \land Gx)$ $\exists$-introduction from (1) (valid)
(3) $\exists x Bx,\, Gx \vdash \exists x (Bx \land Gx)$ $\exists$-elimination from (2) (invalid - clash of variables)
(4) $\exists x Bx,\, \exists x Gx \vdash \exists x (Bx \land Gx)$ $\exists$-elimination from (3) (invalid conclusion due to (3))

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

Sequent Justification/rule
(1) $By, \, Gx \vdash By \land Gx$ Tautology
(2) $By,\,Gx \vdash \exists x (By \land Gx)$ $\exists$-introduction from (1)
(3) $By,\,Gx \vdash \exists y \exists x (By \land Gx)$ $\exists$-introduction from (2)
(4) $\exists y By,\, Gx \vdash \exists y \exists x (By \land Gx)$ $\exists$-elimination from (3)
(5) $\exists y By,\,\exists x Gx \vdash \exists y \exists x(By \land Gx)$ $\exists$-elimination from (4)
(6) $Bx \vdash Bx$ Tautology lol
(7) $Bx \vdash \exists x Bx$ $\exists$-introduction from (6)
(8) $\exists x Bx \vdash \exists y By$ $\exists$-elimination from (7)
... (skipped some steps I guess)
(12) $\exists x Bx,\,\exists x Gx \vdash \exists y \exists x (By \land Gx)$ idk

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

  1. Main difference: the $\forall$ was put back in before the $\exists$. Equally valid though. 

  2. A formula $\Phi$ such that $\vdash \Phi$ can show up in some correct proof. Note: tautologies are logical theorems.