Universal quantifier introduction seemingly follows all rules, yet, it doesn't

Question

I am asked to prove $(\forall x):[P(x)\rightarrow Q(x)]$ from the two premises $(\forall x):[P(x) \rightarrow (Q(x) \vee R(x))]$ and $\neg[(\exists x):[P(x) \wedge R(x)]]$.

I replicated my paper attempt on Fitch, a Logic proof checker. Fitch tells me my last step of universal introduction is not a logical step. I am struggling to see why this is the case, especially since I've used this step in seemingly the same manner countless times before, and, my step follows the universal introduction rule, namely:

$$\dfrac{\boxed{x_0 \\.\\.\\.\\\phi[x_0/x]}}{\forall x \phi} \forall x \text{ i}$$

My attempt at the proof and the Fitch error is shown below. The prompt advises me that the step in question "is of the wrong form". May anyone advise on what I did wrong?

Answer 1

You must begin the subproof for a universal introduction with an arbitrary assumption.   That is just a declaration of the local variable without any further assumptions about it.

Line 3 is not an arbitrary assumption. It has an added assumption of $P(a)\to(Q(a)\lor R(a))$. Do not do that.

You will want to derive $P(a)\to(Q(a)\lor R(a))$ separately from the declaration of the variable, using universal elimination of line 1.

$${\begin{array}{|l}~~3~.~\boxed a\\\hline~~4'.~ P(a)\to(Q(a)\lor R(a))\quad\forall\mathsf E~1\\~~\vdots\\16'.~P(a)\to Q(a)\end{array}\\17'.\forall x~(P(x)\to Q(x))\qquad\quad~~\forall\mathsf I~3{-}16'}$$

Answer 2

Note that $\neg\exists x(P(x) \wedge R(x)) \iff (\forall x):[\neg P(x) \vee \neg R(x)].$

Using Universal Instantiation, we get that $\neg P(a) \vee \neg R(a)$ for some arbitrary $a.$

Also, using the same rule, you conclude that $P(a) \to (Q(a) \vee R(a)).$

Using the material implication, you get $\neg P(a) \vee Q(a) \vee R(a).$

Adjuntcion rule yields $[\neg P(a) \vee \neg R(a)] \wedge [\neg P(a) \vee Q(a) \vee R(a)].$

From the distributive rule follows $\neg P(a) \vee [\neg R(a) \wedge (Q(a) \vee R(a))].$

Modus Tollendo Ponens tells you that $\neg P(a) \vee Q(a).$

Finally, using the Material Implication again, you get $P(a) \to Q(a).$

Since $a$ is an arbitrary element, you use Universal Generalization to conclude that $(\forall x):[P(x) \to Q(x)].$