# Show that $\forall{x}\exists{y}{(P(x) \to Q(y))} \vdash \exists{y}\forall{x}{(P(x) \to Q(y))}$

I need to show that

$$\forall{x}\exists{y}{(P(x) \to Q(y))} \vdash \exists{y}\forall{x}{(P(x) \to Q(y))}$$

using the natural deduction rules outlined in Logic in Computer Science: Modelling and Reasoning about Systems by Michael Huth and Mark Ryan.

There is a proof outlined in this answer. However, it seems to violate the scope requirements for $$\forall{}$$ introduction, as outlined in the book.

• Are you sure the formula is correct? – Rodrigo de Azevedo Jun 9 at 16:07
• Should they not be equivalent? $\vdash \psi \rightarrow \phi$ is equivalent to $\psi \vdash \phi$ and because of soundness, $\psi \vDash \phi$ no? – TheConfuZzledDude Jun 9 at 16:14
• I did realise that I miswrote P(y) when I meant Q(y) in the original question, I've corrected that now – TheConfuZzledDude Jun 9 at 16:16
• When you speak of natural deduction rules, you probably rather want to show $\forall{x}\exists{y}{(P(x) \to Q(y))} \vdash \exists{y}\forall{x}{(P(x) \to Q(y))}$? – Hagen von Eitzen Jun 9 at 16:24

Yeah, that one is nasty! Using the Prenex Laws their equivalence is easily demonstrated, but proving those Prenex laws can be a pain. You'll need to use a proof by contradiction. Here is a proof that is quite similar ... and using very similar rules as well.

OK, here's the actual proof:

• Thanks, this is great, but this proves it for $P(x) v Q(y)$ instead of $P(x) \rightarrow Q(y)$, but I suppose it's somewhat equivalent / the proof will be similar. Out of interest, what did you use to generate this proof? – TheConfuZzledDude Jun 11 at 21:57
• @TheConfuZzledDude Yes, I actually did the proof for what you want yesterday, and it is very similar. The program I use here is called Fitch ... it is not free, unfortunately; it comes iwht the textbook Language, Proof, and Logic – Bram28 Jun 11 at 22:24
• Thanks, I adapted your proof to the question, and used FitchJS to check it – TheConfuZzledDude Jun 11 at 23:12
• On line 19, b is used outside of its declaration scope. – Graham Kemp Aug 9 at 0:41
• @GrahamKemp In this particular proof system you can introduce variable-free terms for $\forall \ Elim$ as well as $\bot \ Elim$ without having to declare a specific scope for them. So yes, I used a $b$ as an arbitrary individual in lines $3$ through $10$, but I specifically introduced it since this was used for a $\forall \ Elim$. But on line $19$ it was obtained from a $\bot \ Elim$, and in this proof system that's ok. – Bram28 Aug 9 at 11:04

• @Bram28 Line 25 looks suspect to me. Term c is used outside of its Flag scope. – Graham Kemp Aug 9 at 0:25
• @GrahamKemp Same here ... the $Qc$ on line $25$ comes from a $\bot \ Elim$, which this system allows: any statement follows from a contradiction ... and it does not effect the validity of the subproof on ines $3$ through $12$, since line $25$ comes only after that subproof. But I can understand that in some proof systems the use of temporary terms used in a $\forall \ Intro$ proof is restricted to that very subproof, just to avoid any possible confusion. – Bram28 Aug 9 at 11:08