Vrftjkry

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 lnotforall 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 lnotforall x : (A(x) to B(x))$ logical equivalence




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




4. $ ( forall x : lnot A(x) lor forall x : B(x)) land lnotforall 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.

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)toforall x~B(x)$ and do something to derive $forall x~(A(x)to B(x))$.

Then discharge the assumption with conditional introduction.

$deffitch#1#2{quadbegin{array}{|l} #1\hline #2end{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)toforall x~B(x))toforall 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?