Originally Posted by

**emakarov** What you have listed as disjunction elimination is in fact

disjunctive syllogism, or modus tollendo ponens. A more standard

disjunction elimination rule has the form

(taken from the book "Proofs and Types" by Girard, Lafont, Taylor, p. 72). This rule can be simulated in your system as follows.

Numbers in parentheses indicate where corresponding assumptions have been closed. Now you can proceed using reasoning by cases.

I'm not too sure I understand what you said, but I think I may have derived a proof as follows:

1. Given

2. Assume

3. Assume

4.

-Introduction

5.

from lines 2 and 4

6.

by RAA

7. Assume

8.

by

-Elimination

9.

from lines 6 and 8

10.

by RAA

11.

by

-Elimination on lines 1 and 10

12.

by

-Elimination

13.

by

-Introduction

14.

from lines 2 and 13

15. by RAA

How does this seem to you?

Thanks