**Maintainer:**admin

*1*Existential quantifier rules¶

Continued from last class.

*1.1*Exists introduction¶

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

*1.2*Exists 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?

*2*An 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 proof^{1}:

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.

*3*An 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)) |

*4*A 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 theorem^{2}. Not that relevant, just a sidenote.