Prove: $(\forall x Fx \vee \forall x Gx)\to \forall x(Fx\vee Gx)$

My attempt:

\begin{align} 1.\space & \neg\forall x(Fx\vee Gx) & \text{(Conditional Proof)}\\ 2.\space & \exists x\neg(Fx\vee Gx) & \text{Quantifier Negation on line 1}\\ 3.\space & \exists x(\neg Fx\wedge \neg Gx) & \text{De Morgan's on line 2}\\ & \qquad 4.\space \neg Fx\wedge \neg Gx & \text{Existential Instantiation on line 3}\\ & \qquad 5.\space \neg Fx & \text{Simplification on line 4}\\ & \qquad 6.\space \neg Gx & \text{Simplification on line 4}\\ & \qquad 7.\space \exists x \neg Fx & \text{Existential Generalization on line 5}\\ & \qquad 8.\space \neg\forall x Fx & \text{Quantifier Negation on line 7}\\ & \qquad 9.\space \exists x \neg Gx & \text{Existential Generalization on line 6}\\ & \qquad 10.\space \neg\forall x Gx & \text{Quantifier Negation on line 9}\\ & \qquad 11.\space \neg\forall x Fx \wedge\neg\forall x Gx & \text{Conjunction from lines 8, 10}\\ 12.\space & \neg\forall x Fx \wedge\neg\forall x Gx & \text{Existential Instantiation lines 3, 4-11}\\ 13.\space & \neg(\forall xFx \vee \forall x Gx) & \text{De Morgan's on line 12}\\ 14.\space & \neg\forall x(Fx\vee Gx)\rightarrow \neg(\forall Fx \vee \forall Gx) & \text{Conditional Proof on lines 1-13}\\ 15.\space &\boxed{(\forall x Fx \vee \forall x Gx) \rightarrow \forall x(Fx\vee Gx)} & \text{Transposition on line 14} \end{align}

I am mostly concerned about the Existential Instantiation subproof from 4-11. Also, it is the first time I have done this kind of proof. So, let me know of ways to improve it!

  • $\begingroup$ Is there some reason why you proved the contrapositive instead of just directly proving the statement? $\endgroup$ Oct 2 '17 at 4:19
  • $\begingroup$ I wasn't sure about Universally Instantiating $\forall x Fx$ and $\forall x Gx$ on the same line. Can I? $\endgroup$
    – G_D
    Oct 2 '17 at 4:25
  • $\begingroup$ Why do you think you'd need to do it on the same line? $\endgroup$ Oct 2 '17 at 4:31
  • $\begingroup$ IIRC, Universal Instantiation needs to affect the entire line. And I would be instantiating to $x$ twice (if that makes sense). $\endgroup$
    – G_D
    Oct 2 '17 at 4:36
  • 1
    $\begingroup$ If you start the direct proof, you'll find that when you need to instantiate $\forall x.Fx$ or $\forall x.Gx$, the other won't be there, but even in cases where you are instantiating a universal quantifier, only things in the scope of the quantifier are going to be affected. You pick a quantified formula and instantiate it. You don't just instantiate every quantifier on the line. That said, I think you mean to worry about Universal Generalization as that's the rule with side conditions. $\endgroup$ Oct 2 '17 at 4:43

Your use of "existential generalization" and "existential instantiation" seems backward. Existential instantiation is:

$$\begin{align} \exists x \phi(x) \\ \hline \phi(c) \end{align}$$

For some constant $c$. And existential generalization is when you go the other way.

Also note that after existential instatiation the symbol $c$ is a constant and you should not use that one in a quantifier then. You should probably used another name than $x$ for the constant introduced by existential instantiation.

Also note that it's normally the conditional proof that would require indentation to indicate that these statements are only a consequence of an assumption. For the existential instantiation this is not as required as we only require that we can simply get rid of a constant not appearing in our formula any longer.


Here is a proof using a Fitch-style proof checker to make sure I am applying the rules correctly:

enter image description here

Note that I consider both cases of the disjunction in line 1 and arrive at the same result on lines 4 and 7. Then I use disjunction elimination on line 8 and finally universal introduction on line 9.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/


$\vdash (\forall x~Fx~\vee~\forall x~Gx)~\to~~\forall x~(Fx\vee Gx)$

...may be proven directly via disjunctive syllogism (aka disjunctive elimination):

$(\forall x~Fx~\vee~\forall x~Gx), (\forall x~Fx)~\to~\forall x~(Fx\vee Gx), (\forall x~Gx)~\to~\forall x~(Fx\vee Gx)\vdash\forall x~(Fx\vee Gx)$

Since $\vdash (\forall x~Fx)\to \forall x~(Fx\vee Gx)$ is provable by assumption, universal elimination, disjunctive introduction, conditional introduction, and universal reintroduction.   Quite similarly we have $\vdash (\forall x~Gx)\to \forall x~(Fx\vee Gx)$.

$$\begin{array}{l|l:ll} \hdashline 1 & \quad \forall x~Fx~\vee~\forall x~Gx&& \text{Assume} \\\hdashline 2 & \qquad \forall x ~Fx &1& \text{Assume }\vee\mathsf L\\\hdashline 3 & \quad\qquad Fc &2& \forall-\\ 4 & \quad\qquad Fc\vee Gc &3& \vee+ \\\hline 5 & \qquad \forall x~(Fx\vee Gx) &4& \forall + \\ \hline 6 & \quad(\forall x~Fx)\to(\forall x~(Fx\vee Gx)) &2,5& \to+ \\ \hdashline 7 & \qquad\forall x~Gx &1&\text{Assume }\vee\mathsf R \\ \hdashline 8 & \quad\qquad Gc &7& \forall -\\ 9 & \quad\qquad Fc\vee Gc &8& \vee+ \\ \hline 10& \qquad \forall x~(Fx\vee Gx) &9& \forall + \\ \hline 11& \quad(\forall x~Gx)\to \forall x~(Fx\vee Gx) &7,10& \to+\\ \hline 12& (\forall ~Fx~\vee~\forall x~Gx)\to \forall x~(Fx\vee Gx) &1,6,11& \vee-\end{array}$$


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.