3

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!

  • 1
    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. – Mauro ALLEGRANZA Oct 30 '14 at 9:00
1

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! – cookie monster Oct 30 '14 at 14:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.