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, 2017 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, 2017 at 4:25
  • $\begingroup$ Why do you think you'd need to do it on the same line? $\endgroup$ Oct 2, 2017 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, 2017 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, 2017 at 4:43

3 Answers 3


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


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .