$Pa\rightarrow \exists y Qy \vdash \exists y (Pa\rightarrow Qy)$
My friend asked me to prove this using natural deduction. He knows I studied logic but I know little about natural deduction since I studied logic only by hilbert style.
Using inference rules he presented I thought a lot, but couldn't find any proof easier than these two. First, introduce $Pa\rightarrow \exists y Qy$ as a premise.
1-1. Assume $\neg\exists y(Pa\rightarrow Qy)$ and derive $\forall y\neg(Pa\rightarrow Qy)$
1-2. Derive $\neg(Pa\rightarrow Qb)$ and find subproof of $(Pa\wedge \neg Qb)$
1-3. Derive $\forall y\neg Qy$ from $\neg Qb$ and $\exists y Qy$ from $Pa$
1-4. Derive $\neg\exists yQy$ from $\forall y \neg Qy$ and conclude there's a contradiction
Here's another.
2-1. Drive $\neg Pa \vee\exists yQy$
2-2. Derive $Pa\rightarrow Qb$ each from $\neg Pa$ and $\exists y Qy$ and conclude $\exists y(Pa\rightarrow Qy)$
Since I haven't tried this in a full content, I don't know how long proof will be but I guess it will be.. I think there should be easier proof than these but I don't know how to find it.
Best Answer
The first proof works, also if you need a lot of sub-proof to "play with" the propositional and quantifiers equivalences.
A more straightforward proof will be :
1) $Pa → ∃yQy$ --- premise
2) $\lnot Pa \lor Pa$ --- Excluded Middle
3) $\lnot Pa$ --- first sub-proof from 2) by $\lor$-elim
4) $Pa$ --- assumed [a]
5) $\bot$
6) $Qb$ --- from 5)
7) $Pa \to Qb$ --- by $→$-intro, discharging [a]
9) $Pa$ --- second sub-proof from 2) by $\lor$-elim
10) $∃yQy$ --- from 1) and 9) by $→$-elim
11) $Qb$ --- assumed from 10) for $∃$-elim
12) $Pa$ --- reiteration of 9)
13) $Pa \to Qb$ --- by $→$-intro, discharging 12)