THEOREM
*******
[A => B] <=> ~[A & ~B]
PROOF
*****
'=>'
Suppose...
1 A => B
Premise
Suppose to the
contrary...
2 A & ~B
Premise
3 A
Split, 2
4 ~B
Split, 2
Apply Detachment
Rule
5 B
Detach, 1, 3
Obtain the
contradiction...
6 B & ~B
Join, 5, 4
Apply Conclusion Rule
(By Contradiction)
7 ~[A & ~B]
4 Conclusion, 2
'=>'
Apply Conclusion Rule (Direct Proof)
8 A => B => ~[A
& ~B]
4 Conclusion, 1
'<='
Suppose...
9 ~[A & ~B]
Premise
Suppose...
10 A
Premise
Suppose to the
contrary...
11 ~B
Premise
12 A & ~B
Join, 10, 11
Obtain the
contradiction...
13 A & ~B &
~[A & ~B]
Join, 12, 9
Apply Conclusion
Rule (By Contradiction)
14 ~~B
4 Conclusion, 11
15 B
Rem DNeg,
14
Apply Conclusion Rule
(Direct Proof)
16 A => B
4 Conclusion, 10
'<='
Apply Conclusion Rule (Direct Proof)
17 ~[A & ~B]
=> [A => B]
4 Conclusion, 9
18 [A => B => ~[A
& ~B]] & [~[A & ~B] => [A => B]]
Join, 8, 17
As Required:
19 A => B <=> ~[A
& ~B]
Iff-And, 18