Given ∀x.(p(x) ⇒ q(x)), use the Fitch System to prove ∀x.p(x) ⇒ ∀x.q(x) I'm having trouble solving this exercise: Given ∀x.(p(x) ⇒ q(x)), use the Fitch System to prove ∀x.p(x) ⇒ ∀x.q(x)
My idea was to use Universal Introduction on steps 4 and 5, and once I get AX:p(X) and AX:q(X), use Implication Introduction to reach the goal. However, I'm clicking on "Universal Introduction " in step 5, try to add X as a variable and nothing happens.
Am I completely wrong here? Any help? I'm using Stanford's Platform. Thanks in advance.
1.  AX:(p(X) => q(X)).      Premise
2.  p(X) => q(X).           Universal Elimination: 1
3.  p(X)                    Assumption
4.  q(X)                    Implication Elimination: 2, 3
5.  p(X)                    Reiteration: 3

 A: The sentence you are trying to prove has $\to$ as its main logical operator. So, in order to prove it, you would need to use Implication Introduction rule.
$
\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}
\def\Ae#1{\qquad\text{Universal Elimination:} #1 \\}
\def\Ai#1{\qquad\text{Universal Introduction:} #1 \\}
\def\Ee#1{\qquad\mathbf{\exists\,Elim: } #1 \\}
\def\Ei#1{\qquad\mathbf{\exists I} \: #1 \\}
\def\R#1{\qquad\mathbf{R} \: #1 \\}
\def\ci#1{\qquad\mathbf{\land\,Intro} #1 \\}
\def\ce#1{\qquad\mathbf{\land\,Elim: } #1 \\}
\def\ii#1{\qquad\text{Implication Introduction} \: #1 \\}
\def\ie#1{\qquad\text{Implication Elimination} \: #1 \\}
\def\be#1{\qquad\mathbf{\leftrightarrow E} \: #1 \\}
\def\bi#1{\qquad\mathbf{\leftrightarrow I} \: #1 \\}
\def\qi#1{\qquad\mathbf{=I}\\}
\def\qe#1{\qquad\mathbf{=E} \: #1 \\}
\def\ne#1{\qquad\mathbf{\neg E} \: #1 \\}
\def\ni#1{\qquad\mathbf{\neg I} \: #1 \\}
\def\IP#1{\qquad\mathbf{IP} \: #1 \\}
\def\x#1{\qquad\mathbf{X} \: #1 \\}
\def\DNE#1{\qquad\mathbf{DNE} \: #1 \\}
$
$
\fitch{1.\, \forall x(P(x) \to Q(x))}{
 \fitch{\forall xP(x)}{
 \vdots\\
    \forall xQ(x)
}\\
\forall xP(x) \to \forall xQ(x)
}
$
Then, using Universal Elimination with the premise and assumption...

 $ \fitch{1.\, \forall x(P(x) \to Q(x))}{  \fitch{2.\, \forall xP(x)}{  3.\,P(a) \to Q(a) \Ae{1}  4.\,P(a) \Ae{2}  5.\,Q(a) \ie{3,4}  6.\,\forall xQ(x) \Ai{5} }\\ 7.\,\forall xP(x) \to \forall xQ(x) \ii{2-6} } $

