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.

  • 2
    $\begingroup$ Are you sure the formula is correct? $\endgroup$ – Rodrigo de Azevedo Jun 9 at 16:07
  • $\begingroup$ Should they not be equivalent? $\vdash \psi \rightarrow \phi$ is equivalent to $\psi \vdash \phi$ and because of soundness, $\psi \vDash \phi$ no? $\endgroup$ – TheConfuZzledDude Jun 9 at 16:14
  • $\begingroup$ I did realise that I miswrote P(y) when I meant Q(y) in the original question, I've corrected that now $\endgroup$ – TheConfuZzledDude Jun 9 at 16:16
  • 1
    $\begingroup$ 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))}$? $\endgroup$ – 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.

enter image description here

OK, here's the actual proof:

enter image description here

  • $\begingroup$ 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? $\endgroup$ – TheConfuZzledDude Jun 11 at 21:57
  • $\begingroup$ @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 $\endgroup$ – Bram28 Jun 11 at 22:24
  • $\begingroup$ Thanks, I adapted your proof to the question, and used FitchJS to check it $\endgroup$ – TheConfuZzledDude Jun 11 at 23:12
  • $\begingroup$ On line 19, b is used outside of its declaration scope. $\endgroup$ – Graham Kemp Aug 9 at 0:41
  • $\begingroup$ @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. $\endgroup$ – Bram28 Aug 9 at 11:04

A proof of the problem given, adapted from @Bram28's answer


  • $\begingroup$ Good work! I did the second part a little more quickly. I'l add my proof to my Answer $\endgroup$ – Bram28 Jun 11 at 23:46
  • $\begingroup$ @Bram28 Line 25 looks suspect to me. Term c is used outside of its Flag scope. $\endgroup$ – Graham Kemp Aug 9 at 0:25
  • $\begingroup$ @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. $\endgroup$ – Bram28 Aug 9 at 11:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.