0

how to proof exercise 13.29 without using taut conenter image description here

  • Assume ¬∃xCube(x) and ¬Cube(a) and proceed from there. – F. Zer Jun 9 at 23:18
1

Any proof by LEM+disjunction elimination may be rewritten as a proof by Reduction to Absurdity. Take the following structure:

 |   P v ~P     TautCon (LEM)
 |  |_ P        Assume
 |  |  :        
 |  |  Q        derived somehow
 |  +
 |  |_ ~P       Assume
 |  |  :
 |  |  Q        derived somehow
 |  Q           Disjunction Elimination

When Q may be derived from both P and ~P, we may rewrite this to give the required contradiction.

 |  |_ ~Q       Assume
 |  |  |_ P     Assume
 |  |  |  :
 |  |  |  Q     derived
 |  |  |  #     Negation Elimination
 |  |  ~P       Negation Introduction
 |  |  :
 |  |  Q        derived
 |  |  #        Negation Elimination
 |  ~~Q         Negation Introduction
 |  Q           Double Negation Elimination
| improve this answer | |
0

You can of course first prove Cube(a) v ~Cube(a) using a Proof by contradiction .. the book should have the schema for that

But a little more efficient is to use the following set-up:

enter image description here

| improve this answer | |
  • Thank you so much! got it – user47078 Jun 10 at 16:25
  • @user47078 You're welcome! – Bram28 Jun 11 at 18:13

Not the answer you're looking for? Browse other questions tagged or ask your own question.