# Universal elimination when $\forall$ is not the main operator

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

• You cannot..... – Mauro ALLEGRANZA Mar 1 at 7:32
• 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 – n.y Mar 1 at 7:40

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)
• line 14 won't work because $\rightarrow I$ rule needs to start with an assumption, I'll update what I have – n.y Mar 1 at 21:20
• @n.yc - it works. It is enough to reiterate the assumption... – Mauro ALLEGRANZA Mar 2 at 6:51
• Well it doesn't work as I posted...Did I do something wrong? – n.y Mar 3 at 5:06
• @n.y - 10 is not an assumption. After 12 assume $A(a)$ and then re-iterate $B$. – Mauro ALLEGRANZA Mar 3 at 6:55
• 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? – n.y Mar 3 at 21:52