0
$\begingroup$

I was asked to apply universal elimination on $\forall x A(x) \rightarrow B,$ but the $\forall$ here is not the main operator, what should I do? here's the question and what I have for now enter image description here

$\endgroup$
2
  • $\begingroup$ You cannot..... $\endgroup$ – Mauro ALLEGRANZA Mar 1 at 7:32
  • $\begingroup$ I am trying to prove $\forall x A(x) \rightarrow B \vdash \exists x (A(x) \rightarrow B)$, I will edit the question and post what I have for now $\endgroup$ – n.y Mar 1 at 7:40
1
$\begingroup$

Universal elimination when $∀$ is not the main operator.

You cannot apply UE when the quantifier is not the main operator.

You have to derive $\forall x A(x)$ in order to use it to "detach" $B$ using ($\to$-E):

  1. $\forall x A(x) \to B$ --- premise

  2. $\lnot \exists x (A(x) \to B)$ --- assumed [a]

  3. $\lnot A(y)$ --- assumed [b]

  4. $A(y)$ --- assumed [c]

  5. $\bot$

  6. $B$ --- from 5)

  7. $A(y) \to B$ --- from 4) and 6) by ($\to$-I), discharging [c]

  8. $\exists x (A(x) \to B)$ --- from 7) by ($\exists$-I)

  9. $\bot$

  10. $\lnot \lnot A(y)$ --- from 3) and 9) by ($\to$-I), discharging [b]

  11. $A(y)$ --- from 10) by ($\lnot \lnot$-E)

  12. $\forall x A(x)$ --- from 11) by ($\forall$-I)

  13. $B$ --- from 1) and 12) by ($\to$-E)

  14. $A(y) \to B$ --- from 13) by ($\to$-I)

  15. $\exists x (A(x) \to B)$ --- from 14) by ($\exists$-I)

  16. $\bot$

  1. $\exists x (A(x) \to B)$ --- from 2) and 16) by ($\to$-I), discharging [a], followed by ($\lnot \lnot$-E)
$\endgroup$
5
  • $\begingroup$ line 14 won't work because $\rightarrow I$ rule needs to start with an assumption, I'll update what I have $\endgroup$ – n.y Mar 1 at 21:20
  • $\begingroup$ @n.yc - it works. It is enough to reiterate the assumption... $\endgroup$ – Mauro ALLEGRANZA Mar 2 at 6:51
  • $\begingroup$ Well it doesn't work as I posted...Did I do something wrong? $\endgroup$ – n.y Mar 3 at 5:06
  • $\begingroup$ @n.y - 10 is not an assumption. After 12 assume $A(a)$ and then re-iterate $B$. $\endgroup$ – Mauro ALLEGRANZA Mar 3 at 6:55
  • $\begingroup$ But in this case the $A(a)\rightarrow B$ will be the second layer, but the final conclusion will need to be at the out most layer? $\endgroup$ – n.y Mar 3 at 21:52

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.