Any solution to prove (∀x)(∃y)(Fx & Gy) ⊢ (∃y)(∀x)(Fx & Gy) with natural deduction?

Question

(∀x)(∃y)(Fx & Gy) ⊢ (∃y)(∀x)(Fx & Gy)
I cannot figure out a way to prove this. I am not even certain that it is provable.

Answer 1

At first let's look at what cases first formula is true. Since conjunction requires both operands to be true, we know (through simplification):

(∀x)(Fx)

This means

Fx ⇔ 1

Now, since Fx is always true, we get

(Fx & Gy) ⇔ (1 & Gy) ⇔ (Gy)

and

(∀x)(∃y)(Fx & Gy) ⇔ (∃y)(Gy)

as well as

(∃y)(∀x)(Fx & Gy) ⇔ (∃y)(Gy)

Therefore

(∀x)(∃y)(Fx & Gy) ⇔ (∃y)(∀x)(Fx & Gy)

Deducibility follows from equivalence (but not necessarily the opposite):

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

Answer 2

This is an illustration of the fact that, if all the predicates take only one argument (i.e. F(x), G(y) ) this can be reduced to a problem in sentential logic.

If you want to do it step-by-step, you only need the "irrelevance" rules -- the scope of a quantifier doesn't need to include any conjuncts that don't use the variable.

(∀x)(∃y)(Fx & Gy) ⊢ Irrelevant quantifier

(∀x)(Fx & (∃y) Gy) ⊢ Irrelevant quantifier

(∀x) Fx & (∃y) Gy ⊢ Irrelevant quantifier (notice this is really a sentential expression)

(∃y)((∀x) Fx & Gy) ⊢ Irrelevant quantifier

(∃y)(∀x)(Fx & Gy)

Answer 3

Here is one way to prove the result:

I attempt an indirect proof (IP) by negating what I want to show in line 2. In line 23 I finally reach a contradiction (⊥). In the process of getting there I use the conversion of quantifiers rule (CQ), De Morgan rule (DeM) and disjunctive syllogism (DS) along with introduction and elimination rules.

For more information on these rules associated with the proof checker I used see forall x: Calgary Remix.

---

Reference

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/

Answer 4

You may use Introduction and Elimination rules to prove 'quantifier irrelevance' in non-empty universes.

|_ Ɐx Ǝy (Fx & Gy)
|  |_ [a]
|  |  Ǝy (Fa & Gy)
|  |  |_ [b] Fa & Gb
|  |  |  Fa
|  |  Fa
|  Ɐx Fx
|  |_ [a]
|  |  Ǝy (Fa & Gy)
|  |  |_ [b] Fa & Gb
|  |  |  Gb
|  |  |  |_ [c]
|  |  |  |  Fc
|  |  |  |  Fc & Gb
|  |  |  Ɐx (Fx & Gb)
|  |  Ǝy Ɐx (Fx & Gy)
|  Ǝy Ɐx (Fx & Gy)

And similarly for the converse.