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

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??

• Let $y_0$ be the value of $y$ such that $\forall x. p(x,y)$, whose existence is guaranteed by the assumption. Then, $\forall x. p(x,y_0)$, so $\forall x. \exists y. p(x,y)$. – DHMO Apr 13 '17 at 0:14
• @DHMO Unfortunately that isn't natural deduction. Most formal proof systems don't have the concept of "constant" in them (notable exception being peano arithmetic). – DanielV Apr 13 '17 at 17:32
• @DanielV Looks like I need to really study logic... – DHMO Apr 13 '17 at 17:37
• If you know proof by cases, it might help understand existential elimination. $$\frac {C_1 \lor C_2,~ C_1 \Rightarrow Q,~ C_2 \Rightarrow Q}{Q}$$ generalizes to $$\frac {C_1 \lor \dots \lor C_N,~ C_1 \Rightarrow Q,~\dots,~C_N \Rightarrow Q}{Q}$$ which then generalizes to $$\frac {\exists k~ C_k,~ C_k \Rightarrow Q}{Q}$$ – DanielV Apr 13 '17 at 17:44
• @DHMO To be able to reason and to be able to convey your reasoning in a formal language are 2 different things. You don't really need to learn "logic" (putting reasoning into a formal language) unless you have some reason to want to convey that reasoning in painstaking formality (such as software design, or investigations of what is and isn't possible to deduce). – DanielV Apr 13 '17 at 17:46

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

• WOW, I guess I need to study harder and harder...I am kind of relying on this website. and thanks a lot~!!! You are impressive!!! – tang aqua Apr 13 '17 at 3:02
• @tangaqua Well, don't feel bad about this one .. That Existential elimination rule is real tricky! – Bram28 Apr 13 '17 at 3:04
• I'm pretty sure that $$\frac {\exists x ~P(x), P(x) \Rightarrow Q}{Q}$$ is the standard rule? What do you prefer? – DanielV Apr 13 '17 at 4:14
• @DanielV I prefer either $\exists x P(x) \vdash P(a)$ (with $a$ a new constant) or $\exists x P(x), P(a) \vdash Q \vdash Q$ (again with $a$ a new constant) or $\exists P(x) \vdash P(x)$ (with appropriate constraints as well); in all cases I can just drop the quantifier. But with this rule, I am required to first generate a Universal Conditional, which I find very unintutive. For example, to infer $\exists x (P(x) \land Q(x))$ from $\exists x(Q(x) \land P(x))$ I would first need to prove something like $\forall x ((Q(x) \land P(x)) \rightarrow (P(x) \land Q(x)))$ which seems overly complicated. – Bram28 Apr 13 '17 at 12:12
• @Bram28 I see, thank you. It tentatively seems to me that the "required subproof" of the no-constants-version is equivalent to the parts of the constants-version which assume that y0 is a constant. That is, if you explicitly annotated that y0 is a constant wherever it appears, the annotated parts are equivalent to the $P(x) \Rightarrow Q$ subproof. – DanielV Apr 13 '17 at 15:16