Is this a valid proof for the following problem?


$$\models (\exists x : A(x) \to \forall x : B(x)) \to \forall x : (A(x) \to B(x))$$

Proof by contradiction:

  1. Assume $(\exists x: A(x) \to \forall x : B(x)) \land \lnot (\forall x(A(x) \to B(x))$

  2. $ (\lnot \exists x : A(x) \lor \forall x : B(x)) \land \lnot\forall x : (A(x) \to B(x))$ logical equivalence

  3. $\forall x : \lnot A(x) \lor \forall x : B(x)) \land \lnot(\forall x : (A(x) \to B(x))$ logical equivalence

  4. $\lnot A(a) \lor B(a) \land \lnot((A(a) \to B(a))$ instantiation

  5. $((A(a) \to B(a)) \land \lnot((A(a) \to B(a))$ a contradiction

$\therefore (\exists x: A(x) \to \forall x : B(x)) \to \forall x(A(x) \to B(x))$

Edit: corrected a typo on step 2

Update: Professor's Solution:

  1. Assume $(\exists x: A(x) \to \forall x : B(x)) \land \lnot (\forall x(A(x) \to B(x))$

  2. $ (\lnot \exists x : A(x) \lor \forall x : B(x)) \land \lnot\forall x : (A(x) \to B(x))$ logical equivalence

  3. $ (\lnot \exists x : A(x) \lor \forall x : B(x)) \land \lnot\forall x : (\lnot A(x) \lor B(x))$ logical equivalence

  4. $ ( \forall x : \lnot A(x) \lor \forall x : B(x)) \land \lnot\forall x : (\lnot A(x) \lor B(x))$ logical equivalence

  5. $ ( \forall x : \lnot A(x) \lor \forall x : B(x)) \land \exists x : \lnot(\lnot A(x) \lor B(x))$ logical equivalence

  6. $ ( \forall x : \lnot A(x) \lor \forall x : B(x)) \land \exists x : ( A(x) \land \lnot B(x))$ distribute negation
  7. $ ( \lnot A(a) \lor B(a)) \land ( A(a) \land \lnot B(a))$ instantiation
  8. $ ( \lnot A(a) \lor B(a)) \land ( \lnot A(a) \lor B(a))$ logical equivalence, resulting in a contradiction

$\therefore (\exists x: A(x) \to \forall x : B(x)) \to \forall x(A(x) \to B(x))$

What I learned: it is typically safe to instantiate when there is one existential quantifier, which is not negated.

  • 3
    $\begingroup$ Why on Earth is this downvoted? Sure, the user didn't use $\LaTeX$, but come on! They're new! $\endgroup$
    – Shaun
    Nov 18, 2018 at 1:43
  • $\begingroup$ Please use MathJax is future, @OldGreg. $\endgroup$
    – Shaun
    Nov 18, 2018 at 1:44
  • $\begingroup$ @Shaun: It's not my downvote, but there's a loose group of users who don't like pure proof-verification questions and think they don't add value to the site. $\endgroup$ Nov 18, 2018 at 1:49
  • $\begingroup$ I am of the view that it is better to edit new contributor's work into mathjax rather then downvoting them for that. $\endgroup$ Nov 18, 2018 at 1:49
  • $\begingroup$ Same. I've started the hard parts of editing the mathjax into the post, but I'm a bit strapped on time. Finishing up the mathjax edits would be good editing practice if someone else is interested. $\endgroup$
    – Larry B.
    Nov 18, 2018 at 1:50

3 Answers 3


In step 2 you make use of the equivalence

$\neg(\exists x . A(x) \lor \forall x.B(x)) \iff \forall x . \neg A(x) ∨ \forall x . B(x) $

This is not a real equivalence compare it to demorgans law.

$\neg(\exists x . A(x) \lor \forall x.B(x)) \iff \neg(\exists x . A(x)) \land \neg(\forall x.B(x))$


If you want a syntactic proof for a conditional statement, I suggest that you should use a Conditional Proof format.

So assume $\exists x~A(x)\to\forall x~B(x)$ and do something to derive $\forall x~(A(x)\to B(x))$.

Then discharge the assumption with conditional introduction.

$\def\fitch#1#2{\quad\begin{array}{|l} #1\\\hline #2\end{array}} \fitch{}{\fitch{1.~\exists x~A(x)~\to~\forall x~B(x)}{\fitch{~\ldots}{~\ddots}\\8.~\forall x~(A(x)\to B(x))}\\9.~(\exists x~A(x)\to\forall x~B(x))\to\forall x~(A(x)\to B(x))}$


Step 4 is wrong!

It looks like you instantiated all universals with an $a$, but you cannot do that when the universals are part of a larger sentence.

Consider: Suppose you have

$$\neg \forall x \ P(x) \land \neg \forall x \ \neg P(x)$$

Now, if we are allowed to just instantiate each of these universals with an $a$, we would get $\neg P(a) \land \neg \neg P(a)$, which is a contradiction. But, the orginal statement is not a contradiction at all; if we interpret $P(x)$ as '$x$ is even', and the domain is all numbers, then the original statement is obviously true.

Even more fundamentally, if you have $\neg \forall x \ P(x)$, you cannot fill in anything you want. Using the same interpretation as before, it is clear that $\neg \forall x \ P(x)$ is true, but $\neg P(0)$ is not. So, you cannot instantiate a universal with anything you wany if it is being negated, but this is what you did when in step 4 you went from $\neg \forall x (A(x) \rightarrow B(x))$ to $\neg (A(a) \rightarrow B(x))$

Step 2 is also wrong. The result of rewriting the conditional as an implication should be:

$(\neg \exists x \ A(x) \lor \forall x \ B(x)) \land \neg \forall x (A(x) \rightarrow B(x))$

Interestingly, given your step 2, step 3 is also wrong, as pointed out by @QthePlatypus, but with this corrected step 2, your step 3 actually would follow ... so maybe this was just a typo on your part?

  • $\begingroup$ Thank you for the detailed example. I am a beginner, and I am still struggling with understanding when instantiation is allowed, I don't yet have a good strategy. It looks like a strategy might be to translate the line into informal English, in order to see whether or not instantiating will lead to a contradiction. Would a translation of your example be something like: "No number x is both even and not even."? If you know of any good resources, I would love more practice with quantifiers and instantiation, the more examples the better. $\endgroup$
    – OldGreg
    Nov 19, 2018 at 3:43
  • $\begingroup$ thanks again, I made the correction to step 2. $\endgroup$
    – OldGreg
    Nov 19, 2018 at 3:54
  • $\begingroup$ @oldgreg The official rule of instantiation is such that you can only use it when the whole statement is a universal. Any universal that is part of a larger statement cannit be instantiated. $\endgroup$
    – Bram28
    Nov 19, 2018 at 3:59

You must log in to answer this question.

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