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

how to proof exercise 13.29 without using taut con

• Assume ¬∃xCube(x) and ¬Cube(a) and proceed from there. Jun 9, 2020 at 23:18

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
``````

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:

• Thank you so much! got it Jun 10, 2020 at 16:25
• @user47078 You're welcome! Jun 11, 2020 at 18:13