# Predicate logic, proof of validity of sequent.

The goal is to prove that $\forall x (P(x) \land Q(x)) \vdash \forall x (P(x) \to Q(x))$ in natural deduction.

Would like to find out if I did this natural deduction correctly and if not where did I go wrong?

Any advice would be appreciated. Thank you!

• Correct; but why you have repeated step 5 in step 6 ? – Mauro ALLEGRANZA Aug 31 '18 at 12:02
• To display perhaps the moving from P(x) ∧ Q(x)) to P(x) → Q(x) or am I wrong in doing this? – Kazy Kamakaze Aug 31 '18 at 12:06
• I think this way is also to step out of the sub proof as to display P(x) → Q(x) so I could use it in the next line to add ∀x . – Kazy Kamakaze Aug 31 '18 at 12:07
• But there are no sub-proofs: no assumptions are needed and thus no assumption need to be discharged. – Mauro ALLEGRANZA Aug 31 '18 at 12:09
• Sorry let me clarify ,as to jump out of the box otherwise you have to reference the entire box or might I have it wrong? – Kazy Kamakaze Aug 31 '18 at 12:11

The first assumption should be arbitrary. $P(x_0)$ is an assumption, not derived from the premise. Conditional Introduction discharges the second assumption, and Universal Introduction immediately finishes the proof.
$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline #2\end{array}}\fitch{~~1.~~\forall x~(P(x)\land Q(x))\hspace{10ex}\textsf{Premise}}{\fitch{~~2.~~[x_0]\hspace{20.5ex}\textsf{Assumption (Arbitrary Witness)}}{\fitch{~~3.~~P(x_0)\hspace{15ex}\textsf{Assumption}}{~~4.~~P(x_0)\land Q(x_0)\hspace{6.5ex}\textsf{Universal Elimination (1,2)}\\~~5.~~Q(x_0)\hspace{14.75ex}\textsf{Conjunction Elimination (4)}}\\~~6.~~P(x_0)\to Q(x_0)\hspace{9ex}\textsf{Conditional Introduction (3-5)}}\\~~7.~~\forall x~(P(x)\to Q(x))\hspace{9.25ex}\textsf{Universal Introduction (2-6)}}$$
$$\fitch{~~1.~~\forall x~(P(x)\land Q(x)\hspace{10ex}\textsf{Premise}}{\fitch{~~2.~~[x_0]~P(x_0)\hspace{13ex}\textsf{Assumption (Restricted Arbitrary Witness)}}{~~3.~~P(x_0)\land Q(x_0)\hspace{8.75ex}\textsf{Universal Elimination (1,2)}\\~~4.~~Q(x_0)\hspace{17ex}\textsf{Conjunction Elimination (3)}}\\~~5.~~\forall x~(P(x)\to Q(x))\hspace{8.25ex}\textsf{Universal Introduction (2-4)}}$$