fitch proof chapter 13 (ex. 13.29) [closed]

Question

how to proof exercise 13.29 without using taut con

Answer 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

Answer 2

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: