How to discharge an assumption?

Question

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!

Answer 1

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

I'll use the natural deduction rules of :

• Michael Huth & Mark Ryan, LOGIC IN COMPUTER SCIENCE : Modelling and Reasoning about Systems (2nd ed 2004), page 27.

---

(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 : ¬¬φ ⊢ φ