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 '18 at 1:43
  • $\begingroup$ Please use MathJax is future, @OldGreg. $\endgroup$ – Shaun Nov 18 '18 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$ – Henning Makholm Nov 18 '18 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$ – Q the Platypus Nov 18 '18 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 '18 at 1:50

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 '18 at 3:43
  • $\begingroup$ thanks again, I made the correction to step 2. $\endgroup$ – OldGreg Nov 19 '18 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 '18 at 3:59

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.