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!

Improve this question
1
  • 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
    Commented Oct 29, 2014 at 4:49

1 Answer 1

Reset to default
5

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(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 .

Improve this answer
7
  • 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
    Commented Oct 29, 2014 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
    Commented Oct 29, 2014 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
    Commented Oct 29, 2014 at 16:28
  • please can you go over your answer again and correct the rest!
    – cookie monster
    Commented Oct 29, 2014 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
    Commented Oct 29, 2014 at 16:35

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .