0
$\begingroup$

I know it's true but I have no idea how to write the deduction as there is no ∃ elimination rule that I know of. Am I supposed to use some kind of substitution?

$\endgroup$
6
  • 1
    $\begingroup$ Like you say, you need rules ... are you working with a specific proof system? $\endgroup$
    – Bram28
    May 13 at 19:42
  • 2
    $\begingroup$ @Bram28 I don't think so. The rules are in pages 137-138 of this book: mileti.math.grinnell.edu/MathematicalLogic.pdf $\endgroup$
    – Íñigo
    May 13 at 19:53
  • 2
    $\begingroup$ Oh! So the rules are right there: two Existential rules and two Universal rules… you’ll probably need all 4 $\endgroup$
    – Bram28
    May 13 at 20:24
  • $\begingroup$ How am I supposed to remove the ∃x though? $\endgroup$
    – Íñigo
    May 13 at 21:46
  • $\begingroup$ Follow the rule of $\exists\mathsf P$.$$\dfrac{\mathcal S, \varphi^c_x\vdash \psi}{\mathcal S, \exists x~\varphi\vdash \psi}{\small\text{ where $c$ is not free in $\mathcal S, \exists x~\varphi, \psi$ and is a valid substituent for $x$ in $\varphi$}}$$ So $\small\dfrac{\dfrac{\ddots}{\forall y~Rcy\vdash \forall y~\exists x~Rxy}}{\exists x~\forall y~Rxy\vdash \forall y~\exists x~Rxy}{(\exists\mathsf P)}$ $\endgroup$ May 14 at 3:32

1 Answer 1

0
$\begingroup$

Your book implements 'existental elimination' as 'existential premise'

$$\dfrac{\mathcal S, \varphi^c_x\vdash \psi}{\mathcal S, \exists x~\varphi\vdash \psi}{(\exists P)}{\small\text{ where $c$ is not free in $\mathcal S, \exists x~\varphi, \psi$ and is a valid substituent for $x$ in $\varphi$}}$$

Which says: When in a certain context, you can derive a conclusion under the assumption of a witness for an existential, you may infer in that context that you can derive that conclusion under the assumption of the existential statement. (As long as the above caveat is followed.)

You can see it being applied in the examples on page 141.

Thus your proof should end with:

$$\dfrac{\dfrac{\vdots}{~~~~~~\forall y~Rcy\vdash \forall y~\exists x~Rxy}}{\exists x~\forall y~Rxy\vdash \forall y~\exists x~Rxy}{(\exists\mathsf P)}$$

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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