∀x∃y(Fx→Gy) ⊢ ∃y∀x(Fx→Gy)

I tried to use reductio ad absurdum by assuming ¬∃y∀x(Fx→Gy) and then using quantifier negation to simplify it further, but it got very messy when I had to use ∃-elimination and ∀-elimination. I can't seem to get a contradiction that would allow me to prove ∃y∀x(Fx→Gy).

How would I prove this?


Well, first understand what it's saying and why it would intuitively be true. ∀x∃y(Fx→Gy) means that:

  • If Fx is true, then there must exist a y such that Gy is true. It could be a different y for each x, or it could be the same y for each x; it doesn't matter. If Fx is true, there just has to be at least one y such that Gy is true.
  • If Fx is false, it doesn't matter whether Gy is true or not, because Fx→Gy will be true either way.

So either Fx is false for every x, in which case it doesn't matter if Gy is true for any y because the implication holds for every x - or Fx is true for some x, in which case there is some y for which Gy is true.

Based on this, you can see why ∃y∀x(Fx→Gy) must be true; if Fx is false for every x, we can choose any y and the implication will hold for all x, and if Fx is true for some x, we can choose a y for which Gy holds and the implication will hold for all x.

It's always easier to write a proof if you first understand what the idea is.

Anyway, there may be a shorter way, but you can just use that idea directly: break it into two cases, the case in which there is an x satisfying Fx, and the case in which there is no such x.

First assume ∀x~Fx, and show this implies ∃y∀x(Fx→Gy). (Simple because from ~Fx you obtain Fx→Gy immediately).

Then assume ~∀x~Fx (which is the same as ∃x Fx), and show this also implies ∃y∀x(Fx→Gy). Use the premise ∀x∃y(Fx→Gy). First you obtain Fc, then you obtain ∃y(Fc→Gy), then you obtain Fc→Gd, and using that with Fc gives you Gd. Now that you have Gd (i.e. you've identified a y for which Gy holds), you can get Fx→Gd, then ∀x Fx→Gd, then ∃y∀x Fx→Gy.

So, having solved both cases, now you have (∀x~Fx) → (∃y∀x Fx→Gy), and you have (~∀x~Fx) → (∃y∀x Fx→Gy), from which we can conclude ∃y∀x Fx→Gy by constructive dilemma.


You can translate the following proof into natural deduction. here is the proof

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