Help with a proof for the following arguments

Question

I want to proof the following argument from both sides using the following rules ^I, ^E, vI, vE, →I, →E, ↔I, ↔E, --E, -I

Argument

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

Please let me know if my steps are correct, if not please correct me.

1) [(A ↔ B ) → C]       A
2) A → B                A
3) B → A                A
4) (A → B) ^ ( B → A )  2,3 ^I
5) A ↔ B                4 ↔I
6) C                    1,5 →E
7) -(A ^ B ) V C        6 VI  

Now the other side

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

Here are my steps

1) - ( A ^ B) V C ]     A
2) A → B                A
3) B → A                A
4) (A → B) ^ ( B → A )  2,3 ^I
5) A ↔ B                4 ↔I

I am stuck at this point, I know I want to get C but I don't know what the next move should be. I hope someone can help me out here. Thanks!

Answer 1

We can prove :

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

whith the Law of Excluded Middle : ⊢ φ ∨ ¬φ, that is provable from Double Negation (or Rule of Indirect Proof or Proof by Contradiction) : ¬¬φ ⊢ φ,(¬¬E).

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) C --- assumed

3) ¬ (A & B) ∨ C --- from 2) by ∨I

4) ¬ C --- assumed

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

6) A --- from 5) by &E

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

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

9) A → B --- from 8) by →I

10) (A → B) & (B → A) --- from 7) and 9) by &I

11) A ↔ B --- from 10) by ↔I

12) C --- from 11) and 1) by →E

13) ⊥ --- from 4) and 12) by ¬E : φ, ¬φ ⊢ ⊥

14) ¬ (A & B) --- from 5) and 13) by ¬I : if φ ⊢ ⊥, then ⊢ ¬φ, discharging [a]

15) ¬ (A & B) ∨ C --- from 14) by ∨I

Now we have :

(A ↔ B) → C, C ⊢ ¬ (A & B) ∨ C --- from 2)-3)

and :

(A ↔ B) → C, ¬ C ⊢ ¬ (A & B) ∨ C --- from 4)-15)

Thus, by LEM : C ∨ ¬C, we can conclude with :

(A ↔ B) → C ⊢ ¬ (A & B) ∨ C by ∨E.

---

---

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

we cannot prove it, because it is not valid.

Assume a valuation V such that V(A)=V(B)=V(C)=f.

We have that : V(A & B)=f and thus V(¬ (A & B) ∨ C)=V(t ∨ f)=t.

But with the above valuation : V(A ↔ B)=t and thus V((A ↔ B) → C)=V(t → f)=f.

Thus :

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

and so :

¬ (A & B) ∨ C ⊬ (A ↔ B) → C .