Given ∀x.(p(x) ⇒ q(x)), use the Fitch System to prove ∀x.p(x) ⇒ ∀x.q(x)

Question

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

Answer 1

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} } $