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

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

• 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. Dec 9, 2018 at 0:28

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.

• I also thought about this before. what I was worried about is second assumption [b] exists after assuming [a]. So I thought that [b] should handled first and then [a]. I couldn't find such a way so I give up this method before
– fbg
Dec 8, 2018 at 17:21

$$\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}}$$