# How to discharge an assumption?

I am proving the follow argument

`[(A ↔ B ) → C] ⊢ [ - ( A ^ B) V C ]`

Using the following set of rules

`I, ^E, vI, vE, →I, →E, ↔I, ↔E, --E, -I`

Here are my steps but I got to the point where I couldn't discharge an assumption. I need to know know if my steps are correct, if not, I hope someone can correct me here. I'm kind of confident that my steps are right except for not discharging `-C` assumption on line 2.

Here are my steps

``````1) [(A ↔ B ) → C]       A
2) -C                   A
3) A ^ B                A    for (-I)
4) A                    3    ^E
5) B                    3    ^E
6) A → B                4,5  →I
7) B → A                4,5  →I
8) (A → B) ^ (B → A)    6,7  ^I
9) A ↔ B                8    ↔I
10)C                    1,9  →E
11)C^-C                 2,10 ^I
12)-(A^B)               3,11 -I //discharged line 3 (A^B)
13)-(A^B) V C           12    vI
``````

Are my steps valid ? How do I discharge line 2? Please show me, thanks!

• The steps in your derivation are Ok, but the assumption 2) ¬ C is not discharged; thus, what you have proved is : (A ↔ B ) → C, ¬ C ⊢ ¬(A^B) V C. Oct 30, 2014 at 9:00

You can avoid step 2), i.e. the assumption ¬ C, with a longer derivation.

I'll use the natural deduction rules of :

(A ↔ B) → C ⊢ ¬ (A & B) ∨ C

Proof :

1) (A ↔ B) → C --- premise

2) A & B --- assumed [a]

3) A --- from 2) by &E

4) B → A --- from 3) by →I

5) B --- from 2) by &E

6) A → B --- from 5) by →I

7) (A → B) & (B → A) --- from 4) and 6) by &I

8) A ↔ B --- from 7) by ↔I

9) C --- from 8) and 1) by →E

10) ¬ (A & B) ∨ C --- from 9) by ∨I

11) ¬ [¬ (A & B) ∨ C] --- assumed [b]

12) ¬ (A & B) --- from 2)-10) and 11) by ¬I : if φ ⊢ ⊥, then ⊢ ¬φ, discharging [a]

13) ¬ (A & B) ∨ C --- from 12) by ∨I

14) ¬ ¬ [¬ (A & B) ∨ C] --- from 11) and 13) by ¬I, discharging [b]

15) ¬ (A & B) ∨ C --- from 14) by ¬¬E : ¬¬φ ⊢ φ

• This one was clear to follow, thanks for your help! Oct 30, 2014 at 14:53