How to prove $∀x ∀y (P(x) → Q(y)) ↔ (∃x P(x) → ∀y Q(y))$ using Fitch Intro and Elim rules $∀x ∀y (P(x) → Q(y)) ↔ (∃x P(x) → ∀y Q(y))$ 
We are only permitted to use Intro and Elim rules, and I am stuck on how to even begin this proof. Any help would be appreciated. Thanks!
 A: Tips for Constructing Fitch Proofs:


*

*You'll want to look at the overall form of the premises and the conclusions as hints for figuring out what the frame of the proof should look like.

*If your conclusion has the form $\varphi \rightarrow \psi$, often you'll want to create a new subproof with $\varphi$ as the assumption, and $\psi$ as the conclusion in the subproof. Then use $\rightarrow$-Intro to introduce $\varphi \rightarrow \psi$ outside the subproof.

*If your premise has the form $\exists x \varphi(x)$, often you'll want to create a new subproof with $\fbox{$c$} \ \ \varphi(c)$ for some $c$ that hasn't yet occurred in the proof. Then once you've deduced your conclusion $\psi$ from $\varphi(c)$, so long as $c$ doesn't occur in $\psi$, you can infer $\psi$ outside this subproof using $\exists$-Elim.

*If your premise has the form $\forall x \varphi(x)$, often you'll want to instantiate it with $\varphi(c)$ for some $c$ using $\forall$-Elim. Which $c$ is helpful to pick will depend on the particular proof.

*If your conclusion has the form $\exists x \varphi(x)$, often you'll use $\exists$-Intro citing a line of the form $\varphi(c)$ for some $c$.

*If your conclusion has the form $\forall x \varphi(x)$, often you'll use $\forall$-Intro to get it; this will be introduced right outside a subproof whose assumption is just $\fbox{$c$}$, and whose conclusion is $\varphi(c)$.

*If your conclusion has the form of a biconditional, you'll need to prove two conditionals, and then use whatever it is you use to get the biconditional (you probably have some $\leftrightarrow$-Intro rule you'll have to use, but sometimes people use TautCon, or just cheat).


Using tips like these, you should try to construct your proof from the outside (top and bottom) and work your way inward. Often by using this strategy, you'll reduce the proof to much simpler steps which can be filled in, as opposed to just working from top to bottom.

Example: Proving $\forall x \forall y (P(x) \rightarrow Q(y)) \rightarrow (\exists x P(x) \rightarrow \forall y Q(y))$.
At each stage, I show where you should be in your construction of the Fitch proof, so the proofs below are just the same as the proofs above it, except with more details filled in. First, using tip 2, I create a subproof as follows:


*

*(Nothing)

*
*

*$\forall x \forall y (P(x) \rightarrow Q(y))$


*
*

*... (stuff) ...


*
*

*$\exists x P(x) \rightarrow \forall y Q(y)$


*$\forall x \forall y (P(x) \rightarrow Q(y)) \rightarrow \exists x P(x) \rightarrow \forall y Q(y)$  ($\rightarrow$-Intro)


Next, using tip 2 again, I fill in some more:


*

*(Nothing)

*
*

*$\forall x \forall y (P(x) \rightarrow Q(y))$


*
*

*
*

*$\exists x P(x)$



*
*

*
*

*... (stuff) ...



*
*

*
*

*$\forall y Q(y)$



*
*

*$\exists x P(x) \rightarrow \forall y Q(y)$ ($\rightarrow$-Intro)


*$\forall x \forall y (P(x) \rightarrow Q(y)) \rightarrow \exists x P(x) \rightarrow \forall y Q(y)$  ($\rightarrow$-Intro)


Now, using tip 3:


*

*(Nothing)

*
*

*$\forall x \forall y (P(x) \rightarrow Q(y))$


*
*

*
*

*$\exists x P(x)$



*
*

*
*

*
*

*$\fbox{$a$} \ \ P(a)$




*
*

*
*

*
*

*... (stuff) ...




*
*

*
*

*
*

*$\forall y Q(y)$




*
*

*
*

*$\forall y Q(y)$ ($\exists$-Elim)



*
*

*$\exists x P(x) \rightarrow \forall y Q(y)$ ($\rightarrow$-Intro)


*$\forall x \forall y (P(x) \rightarrow Q(y)) \rightarrow \exists x P(x) \rightarrow \forall y Q(y)$  ($\rightarrow$-Intro)


Using tip 4:


*

*(Nothing)

*
*

*$\forall x \forall y (P(x) \rightarrow Q(y))$


*
*

*
*

*$\exists x P(x)$



*
*

*
*

*
*

*$\fbox{$a$} \ \ P(a)$




*
*

*
*

*
*

*
*

*$\fbox{$b$}$





*
*

*
*

*
*

*
*

*... (stuff) ...





*
*

*
*

*
*

*
*

*$Q(b)$





*
*

*
*

*
*

*$\forall y Q(y)$ ($\forall$-Intro)




*
*

*
*

*$\forall y Q(y)$ ($\exists$-Elim)



*
*

*$\exists x P(x) \rightarrow \forall y Q(y)$ ($\rightarrow$-Intro)


*$\forall x \forall y (P(x) \rightarrow Q(y)) \rightarrow \exists x P(x) \rightarrow \forall y Q(y)$  ($\rightarrow$-Intro)


Finally, you should use tip 4 on your very first assumption to get $Q(b)$. This should be relatively straightforward. And that's how it should be! Often (not always), by following these tips, you can construct Fitch-style proofs from the outside-in in such a way that when you get to the middle where none of these tips apply, it's much easier to see how to close the gap. You should try the other direction, viz. "$(\exists x P(x) \rightarrow \forall y Q(y)) \rightarrow \forall x \forall y (P(x) \rightarrow Q(y))$" on your own using this method. You should also check that the various constraints that might be placed on the Intro and Elim rules are all satisfied at each stage.
