$Pa\rightarrow \exists y Qy \vdash \exists y (Pa\rightarrow Qy)$ using natural deduction

Question

$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.

Answer 1

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]

8) $∃y(Pa \to Qy)$ --- by $∃$-intro, closing 1st sub-proof

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)

14) $∃y(Pa \to Qy)$ --- by $∃$-intro, closing the $∃$-elim sub-proof and closing 2nd sub-proof

15) $∃y(Pa → Qy)$ --- from 3)-8) and 9)-14) and 2) by $\lor$-elim.

Answer 2

$\def\fitch#1#2{~~~~~\begin{array}{|l}#1\\\hline #2\end{array}}$

It might be worth noting that any proof will necessarily involve something like excluded middle or double negation elimination - the statement is not valid in intuitionistic first-order logic.

Here's Mauro ALLEGRANZA's LEM proof, reformatted.

$$\fitch{~~1.~~Pa\to\exists y~Qy\hspace{21ex}\textsf{Premise}}{~~2.~~Pa\lor\lnot Pa\hspace{23ex}\textsf{Tautology (Law of Excluded Middle)}\\\fitch{~~3.~~\lnot Pa\hspace{25ex}\textsf{Assumption}}{\fitch{~~4.~~Pa\hspace{23ex}\textsf{Assumption}}{~~5.~~\bot\hspace{24ex}\textsf{Negation Elimination 5, 4}\\~~6.~~Qa\hspace{23ex}\textsf{Explosion 5}}\\~~7.~~Pa\to Qa\hspace{20ex}\textsf{Conditional Introduction 4-6}\\~~8.~~\exists y~(Pa\to Qy)\hspace{15ex}\textsf{Existential Introduction 7}}\\\fitch{~~9.~~Pa\hspace{27ex}\textsf{Assumption}}{10.~~\exists y~Qy\hspace{24ex}\textsf{Conditional Elimination 1, 9}\\\fitch{\boxed b 11.~~Qb\hspace{21ex}\textsf{Assumption}}{\fitch{12.~~Pa\hspace{19ex}\textsf{Assumption}}{13.~~Qb\hspace{19ex}\textsf{Reiteration 11}}\\14.~~Pa\to Qb\hspace{16ex}\textsf{Conditional Introduction 12-13}\\15.~~\exists y~(Pa\to Qy)\hspace{11ex}\textsf{Existential Introduction 15}}\\16.~~\exists y~(Pa\to Qy)\hspace{15ex}\textsf{Existential Elimination 10, 11-15}}\\20.~~\exists y~(Pa\to Qy)\hspace{19ex}\textsf{Disjunction Elimination 2, 11-19, 4-10}}$$

Here's the DNE version.

$$\fitch{~~1.~~Pa\to\exists y~Qy\hspace{21ex}\textsf{Premise}}{\fitch{~~2.~~\lnot\exists y~(Pa\to Qy)\hspace{13.5ex}\textsf{Assumption}}{\fitch{~~3.~~Pa\hspace{22.5ex}\textsf{Assumption}}{~~4.~~\exists y~Qy\hspace{19.5ex}\textsf{Conditional Elimination 1, 3}\\\fitch{\boxed b~~5.~~Qb\hspace{16.5ex}\textsf{Assumption}}{\fitch{~~6.~~Pa\hspace{15ex}\textsf{Assumption}}{~~7.~~Qb\hspace{15ex}\textsf{Reiteration 5}}\\~~8.~~Pa\to Qb\hspace{12ex}\textsf{Conditional Introduction 6-7}\\~~9.~~\exists y~(Pa\to Qy)\hspace{7ex}\textsf{Existential Introduction 8}\\10.~~\bot\hspace{20ex}\textsf{Negation Elimination 9, 2}\\11.~~Qa\hspace{19ex}\textsf{Explosion 10}}\\12.~~Qa\hspace{23ex}\textsf{Existential Elimination 5-11}}\\13.~~Pa\to Qa\hspace{20ex}\textsf{Conditional Introduction 3-12}\\14.~~\exists y~(Pa\to Qy)\hspace{15.5ex}\textsf{Existential Introduction 13}\\15.~~\bot\hspace{28ex}\textsf{Negation Elimination 14, 2}}\\16.~~\lnot\lnot\exists y~(Pa\to Qy)\hspace{16ex}\textsf{Negation Introduction 2-15}\\17.~~\exists y~(Pa\to Qy)\hspace{19ex}\textsf{Double Negation Elimination 16}}$$