Why universal instantiation cannot be used here?

Question

I have a following sentence:

$$\forall x~(Fx \to \forall y~(Fy \to Gy)) ~\vdash~ \forall x~(Fx \to Gx) $$

Why I cannot use UI twice and get:

$$Fa \rightarrow (Fa \rightarrow Ga) $$

This is my proof:

1) $\forall x~(Fx \to \forall y~(Fy \to Gy))$

$\quad$2) $Fa \to (Fa \to Ga)$

$\qquad$3) $Fa$ (Assumption)

$\qquad$4) $Ga$ (From 2,3)

$\quad$5) $Fa \to Ga$

6) $\forall x~(Fx \to Gx) $

And the second line was marked as the wrong one by somehow.

Thanks in advance.

Answer 1

UI allows us to deduce $\phi$ from $(\forall x)(\phi)$ and nothing more.

In your case, it seems like you have tried to deduce $Fa\to \phi$ from $Fa\to (\forall y)(\phi)$ with a single application of UI. This is an invalid use of UI.

Answer 2

Universal instantiation says $$ \forall_x\phi(x)\Rightarrow\phi(a) $$ So, in your case you can get $$ Fa\Rightarrow\forall_y(Fy\Rightarrow Gy) $$ But, you have by UI that $\forall_y(Fy\Rightarrow Gy)\Rightarrow(Fa\Rightarrow Ga)$ so, by transitivity, $Fa\Rightarrow(Fa\Rightarrow Ga)$

Answer 3

You can use Universal Instantiation(Elimination) twice.   You just cannot do it immediately.   You must instantiate the universal $x$, raise the assumption of $Fa$, modus ponens, and then instantiate the universal $y$ (to the same arbitrary $a$).   After that your proof continues as you wanted.

$$\def\fitch#1#2{\begin{array}{|l}#1\\\hline #2\end{array}}\fitch{1.\quad \forall x~(Fx\to \forall y~(Fy\to Gy))\quad\text{Premise} }{\fitch{[a]}{2.\quad Fa \to(\forall y~(Fy\to Gy))\quad~~1,\forall\text{Elim}\\\fitch{3.\quad Fa\qquad\qquad\qquad\qquad\quad~~\text{Assume}}{4.\quad \forall y~(Fy\to Gy)\qquad\qquad~~~2,3,\to\text{Elim (modus ponens)}\\ 5.\quad Fa\to Ga\qquad\qquad\qquad~~~ 4,\forall\text{Elim}\\6.\quad Ga\qquad\qquad\qquad\qquad\quad~~ 3,5,\to\text{Elim}}\\7.\quad Fa\to Ga\qquad\qquad\qquad\quad~3,6\to\text{Intro}}\\8.\quad \forall x~(Fx\to Gx)\qquad\qquad\quad~~ 7,\forall\text{Intro}}$$