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.

  • 0
    Maybe. I thought you insert the line after it. Fixing it now.2012-07-29

1 Answers 1

1

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)