Return to Answer

whith Excluded Middle : A ∨ ¬A, that is provable from Double Negation (or Rule of Indirect Proof) : (¬¬E).

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

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

11. C --- from 10) and 1) by →E

12. ⊥ --- from 4) and 11) by →E

13. ¬ (A & B) --- from 5) and 12) by →I, discharging [a]

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

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

Thus, by Excluded Middle : C ∨ ¬C, we can conclude with :

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.

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

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

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

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 --- from 7) and 9) by ↔I

11. C --- from 10) and 1) by →E

12. ⊥ --- from 4) and 11) by →E

13. ¬ (A & B) --- from 5) and 12) by →I, discharging [a]

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

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

11. C --- from 10) and 1) by →E

12. ⊥ --- from 4) and 11) by →E

13. ¬ (A & B) --- from 5) and 12) by →I, discharging [a]

We can prove :

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

whith Excluded Middle : A ∨ ¬A, that is provable from Double Negation (or Rule of Indirect Proof) : (¬¬E).

(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 --- from 7) and 9) by ↔I

11. C --- from 10) and 1) by →E

12. ⊥ --- from 4) and 11) by →E

13. ¬ (A & B) --- from 5) and 12) by →I, discharging [a]

14. ¬ (A & B) ∨ C --- from 13) 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)-14)

Thus, by Excluded Middle : 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)=t and thus V((A ↔ B) → C)=V(t → f)=f.

But with the above valuation, V(A & B)=f and thus V(¬ (A & B) ∨ C)=V(t ∨ f)=t.

Thus :

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

and so :

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

We can prove :

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

whith Excluded Middle : A ∨ ¬A, that is provable from Double Negation (or Rule of Indirect Proof) : (¬¬E).

(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 --- from 7) and 9) by ↔I

11. C --- from 10) and 1) by →E

12. ⊥ --- from 4) and 11) by →E

13. ¬ (A & B) --- from 5) and 12) by →I, discharging [a]

14. ¬ (A & B) ∨ C --- from 13) 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)-14)

Thus, by Excluded Middle : 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 .