Given ∃y.∀x.p(x,y), use the Fitch system to prove ∀x.∃y.p(x,y).

Question

I have a problem to solve this question. I thought I should eliminate the existential first but it seems not work..Not sure how to use the existential condition to prove the later one.

Here's the rule for existential elimination,
1: Ev.p(v) // use E for ∃
2: Av.(p(v) => q) //use A for ∀
EE 1,2: q

And the Fitch system provides new method also, it calls equalization introduction and equalization elimination..But I don't know how to use it..Since the lecture doesn't have any information about that..If someone know, could you tell me??

Thanks for your help!!

Answer 1

Ugh, I hate how they defined that Existential Elimination rule!

Anyway, here is how you do that one:

1. $\exists y \forall x \: p(x,y)$ Premise

2. $\quad \forall x \: p(x,y)$ Assumption

3. $\quad p(x,y)$ $\forall $ Elim 2

4. $\quad \exists y \: p(x,y)$ $\exists$ Intro 3

5. $\forall x \: p(x,y) \rightarrow \exists y \: p(x,y)$ $\rightarrow$ Intro 2-4

6. $\forall y (\forall x \: p(x,y) \rightarrow \exists y \: p(x,y))$ $\forall$ Intro 5

7. $\exists y \: p(x,y)$ $\exists$ Elim 1,6

8. $\forall x \exists y \: p(x,y)$ $\forall $ Intro 7