1
$\begingroup$

Given the premises in lines 1 and 2, I need to prove that $(\forall x)(\exists y)(Cx \rightarrow Axy)$.

  1. $(\exists x)(\forall y)Ayx \lor (\forall x)(\forall y)Bxy$
  2. $(\exists x)(\forall y)(Cy \rightarrow \neg Byx)\\ \qquad \qquad \qquad \therefore (\forall x)(\exists y)(Cx \rightarrow Axy)$
  3. $(\forall y)(Cy \rightarrow \neg Bya) \qquad$ (2, existential instance)
  4. $\neg (\forall x)(\exists y)(Cx \rightarrow Axy) \qquad$ (reductio ad absurdum)
  5. $\qquad (\exists x)\neg(\exists y)(Cx \rightarrow Axy) \qquad$ (4, quantifier negation)
  6. $\qquad (\exists x)(\forall y)\neg(Cx \rightarrow Axy) \qquad$ (5, quantifier negation)
  7. $\qquad (\forall y)\neg(Cb \rightarrow Aby) \qquad$ (6, existential instantiation)
  8. $\qquad \neg(Cb \rightarrow Aba) \qquad$ (7, universal instantiation)
  9. $\qquad \neg(\neg Cb \lor Aba) \qquad$ (8, material implication)
  10. $\qquad Cb \land \neg Aba \qquad$ (9, DeMorgan)
  11. $\qquad Cb \qquad$ (10, simplification)
  12. $\qquad \neg Aba \qquad$ (10, simplification)

If this is correct so far, then I need a contradiction. I can sort of "see" the contradiction in the first premise (which I haven't used yet). If I could instance the $Bxy$ on the RHS of line 1, I'd be done. But I can't instance that while the quantifier is not thee major operator. So, am I on the right track? If so, how do I separate line 1 so I can instance it?

Thanks.

$\endgroup$
7
  • 3
    $\begingroup$ Don't you think it might be of at least marginal relevance to tell us what you're trying to prove? (By the way, I think it should be $10$ instead of $11$ in line $12$?) $\endgroup$
    – joriki
    Jul 29, 2012 at 18:19
  • $\begingroup$ @joriki The three dot triangular symbol often means "therefore". So, he almost surely wants to prove the formula in the second part of line 2. Though now I'm guessing you just mean to say that he could have stated what he wanted to prove more clearly elsewhere, and I do agree with that. $\endgroup$
    – Doug Spoonwood
    Jul 29, 2012 at 18:29
  • $\begingroup$ I updated in consideration both your comments. $\endgroup$
    – Jeff
    Jul 29, 2012 at 18:54
  • $\begingroup$ Why did the variables go missing behind the quantifiers in lines $5$ and $6$? $\endgroup$
    – joriki
    Jul 29, 2012 at 19:25
  • $\begingroup$ @joriki Because of bad editing/typing. :D Fixed. $\endgroup$
    – Jeff
    Jul 29, 2012 at 23:07

1 Answer 1

Reset to default
1
$\begingroup$

Well, we managed to figure out the proof. But it was pretty damn hard (for us). I don't really understand what the proof "says", and it's kind of all over the place (it's easier to understand if you color code the lines, which I can't do on here), but we think this is right.

  1. $(\exists x)(\forall y)Ayx \lor (\forall x)(\forall y)Bxy$
  2. $(\exists x)(\forall y)(Cy \rightarrow \neg Byx)\\ \qquad \qquad \qquad \therefore (\forall x)(\exists y)(Cx \rightarrow Axy)$
  3. $(\forall y)(Cy \rightarrow \neg Bya) \qquad$ (2, existential instance)
  4. $\qquad \neg (\forall x)(\exists y)(Cx \rightarrow Axy) \qquad$ (reductio ad absurdum)
  5. $\qquad (\exists x)\neg(\exists y)(Cx \rightarrow Axy) \qquad$ (4, quantifier negation)
  6. $\qquad (\exists x)(\forall y)\neg(Cx \rightarrow Axy) \qquad$ (5, quantifier negation)
  7. $\qquad (\forall y)\neg(Cb \rightarrow Aby) \qquad$ (6, existential instantiation)
  8. $\qquad \neg(Cb \rightarrow Aba) \qquad$ (7, universal instantiation)
  9. $\qquad \neg(\neg Cb \lor Aba) \qquad$ (8, material implication)
  10. $\qquad Cb \land \neg Aba \qquad$ (9, DeMorgan)
  11. $\qquad Cb \qquad$ (10, simplification)
  12. $\qquad \neg Aba \qquad$ (10, simplification)
  13. $\qquad (\exists y)\neg Aya \qquad$ (12, existential generalization)
  14. $\qquad (\forall x)(\exists y)\neg Aya \qquad$ (13, universal generalization)
  15. $\qquad (\forall x)\neg(\forall y) Aya \qquad$ (14, quantifier negation)
  16. $\qquad \neg(\exists x)(\forall y) Aya \qquad$ (15, quantifier negation)
  17. $\qquad (Cb \rightarrow \neg Bba) \qquad$ (3, universal instantiation)
  18. $\qquad \neg Bba \qquad$ (11,17,modus ponens)
  19. $\qquad (\forall x)(\forall y)Bxy \qquad$ (1,16 disjunctive syllogism)
  20. $\qquad (\forall y)Bby \qquad$ (19, universal instantiation)
  21. $\qquad Bba \qquad$ (20, universal instantiation)
  22. $\qquad Bba \land \neg Bba \qquad$ (18,21, conjunction)
  23. $(\forall x)(\exists y)(Cx \rightarrow Axy) \qquad$ (4-22, reductio ad absurdum)
$\endgroup$

You must log in to answer this question.

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