3

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!

  • 1
    If you're assuming (2) and (3) in the first proof, then you're not proving [(A ↔ B ) → C] ⊢ [ - ( A ^ B) V C ]. Rather, you are proving [(A ↔ B ) → C] & (A → B) & (B → A) ⊢ [ - ( A ^ B) V C ]. Which one of those sequents are you trying to prove? – Hunan Rostomyan Oct 29 '14 at 4:49
4

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 :


(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(tf)=t.

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

Thus :

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

and so :

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

  • 1
    Isn't step 6 from ^ E on line 5? Also step 7 doesn't seem correct.You don't even have B yet? In addition on step 8, shouldn't that be ^ E on line 5? – cookie monster Oct 29 '14 at 16:10
  • Also you can't really get step 10 unless you have (A → B) ^ (B → A). I don't understand what you mean by step 12. Step 13 is not clear as well. I'm not sure if I can understand this well, it seems like you are using the symbols in a different way. – cookie monster Oct 29 '14 at 16:28
  • @cookiemonster - right, tanks ! coorected the typo into steps 6 and 8. For step 7, it is correct : A ⊢ B → A, for every A, because A → (B → A) is valid (it is a tautology). – Mauro ALLEGRANZA Oct 29 '14 at 16:28
  • please can you go over your answer again and correct the rest! – cookie monster Oct 29 '14 at 16:34
  • @cookiemonster - in 12 the symbol ⊥ stay for a contradiction : step 4) ¬ C and step 11) C ; thus, having derived a contradiction, we negate the assumption 5) A & B, getting 13) ¬ (A & B). This can be done with the abbreviation ¬ P := P → ⊥; in this way, deriving a contradiction from ¬ C, C is nothing else than apply →E to C → ⊥, C in order to derive ⊥. Then, having (A & B) ⊢ ⊥, we derive (A & B) → ⊥, i.e. ¬ (A & B) by →I. – Mauro ALLEGRANZA Oct 29 '14 at 16:35

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.