# Does this prove the validity of this First Order Logic formula?

Is this a valid proof for the following problem?

Prove:

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

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.

• Why on Earth is this downvoted? Sure, the user didn't use $\LaTeX$, but come on! They're new! Commented Nov 18, 2018 at 1:43
• Please use MathJax is future, @OldGreg. Commented Nov 18, 2018 at 1:44
• @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. Commented Nov 18, 2018 at 1:49
• I am of the view that it is better to edit new contributor's work into mathjax rather then downvoting them for that. Commented Nov 18, 2018 at 1:49
• 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. Commented Nov 18, 2018 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?

• 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. Commented Nov 19, 2018 at 3:43
• thanks again, I made the correction to step 2. Commented Nov 19, 2018 at 3:54
• @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. Commented Nov 19, 2018 at 3:59