THEOREM
*******
De Morgan's Law: A | B <=> ~[~A & ~B]
The proof uses only the following rules of inference that give the essential properties of the OR-operator ('|'):
1. Or Not: A | ~A (Law of the Excluded Middle) (line 20)
2. Arb Or: A ---> A | B or B | A (lines 22, 30)
3. Cases: P1 | P2 | P3 | ... Pn and P1 => Q, P2 => Q, P3 => Q, ... Pn => Q ---> Q (lines 17, 33)
This machine-verified formal proof was written with the aid of the author's DC Proof 2.0 software downloadable at http://www.dcproof.com
Dan Christensen
2022-06-03
PROOF
*****
'=>'
Prove: A | B => ~[~A & ~B]
Suppose (two cases to consider)...
1 A | B
Premise
Case 1
Prove: A => ~[~A & ~B]
Suppose...
2 A
Premise
Prove: ~[~A & ~B]
Suppose to the contrary...
3 ~A & ~B
Premise
4 ~A
Split, 3
5 ~B
Split, 3
6 A & ~A
Join, 2, 4
As Required:
7 ~[~A & ~B]
4 Conclusion, 3
Case 1
As Required:
8 A => ~[~A & ~B]
4 Conclusion, 2
Case 2
Prove: B => ~[~A & ~B]
Suppose...
9 B
Premise
Prove: ~[~A & ~B]
Suppose to the contrary...
10 ~A & ~B
Premise
11 ~A
Split, 10
12 ~B
Split, 10
13 B & ~B
Join, 9, 12
As Required:
14 ~[~A & ~B]
4 Conclusion, 10
Case 2
As Required:
15 B => ~[~A & ~B]
4 Conclusion, 9
16 [A => ~[~A & ~B]] & [B => ~[~A & ~B]]
Join, 8, 15
17 ~[~A & ~B]
Cases, 1, 16
'=>'
As Required:
18 A | B => ~[~A & ~B]
4 Conclusion, 1
'<='
Prove: ~[~A & ~B] => A | B
Suppose...
19 ~[~A & ~B]
Premise
Two cases to consider:
20 A | ~A
Or Not
Case 1
Prove: A => A | B
Suppose...
21 A
Premise
22 A | B
Arb Or, 21
Case 1
As Required:
23 A => A | B
4 Conclusion, 21
Case 2
Prove: ~A => A | B
Suppose...
24 ~A
Premise
Prove: ~~B
Suppose to the contrary...
25 ~B
Premise
26 ~A & ~B
Join, 24, 25
Obtain contradiction...
27 ~A & ~B & ~[~A & ~B]
Join, 26, 19
As Required:
28 ~~B
4 Conclusion, 25
29 B
Rem DNeg, 28
30 A | B
Arb Or, 29
Case 2
As Required:
31 ~A => A | B
4 Conclusion, 24
32 [A => A | B] & [~A => A | B]
Join, 23, 31
33 A | B
Cases, 20, 32
'<='
As Required:
34 ~[~A & ~B] => A | B
4 Conclusion, 19
Joing results...
35 [A | B => ~[~A & ~B]] & [~[~A & ~B] => A | B]
Join, 18, 34
As Required:
36 A | B <=> ~[~A & ~B]
Iff-And, 35