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

Question

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

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.

Answer 1

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

Answer 2

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

Answer 3

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?