prove de morgan's rule
Proloy Mishra
1 year, 9 months ago
15 | 15 | axiom (#and-comp) and(A, not(A)) = 0 |
16 | 16 | |
17 | 17 | We'll now establish some basic lemmas based on these axioms. |
18 | These in turn could, in another setting, provide support for | |
19 | a proof of De Morgan's Laws. In this purely equational setting though, | |
20 | for reasons I'll explain below, we won't actually be able to give | |
21 | a proof De Morgan's Laws using them. Still, the lemmas | |
18 | These in turn would provide support for | |
19 | a proof of De Morgan's Laws. Also, the lemmas | |
22 | 20 | are instructive, could be useful for other proofs, and serve |
23 | 21 | the point of exercising the Eqthy language and its proof-checkers. |
24 | 22 | |
85 | 83 | and(X, 0) = 0 |
86 | 84 | qed |
87 | 85 | |
88 | theorem | |
86 | theorem (#and-rel) | |
89 | 87 | and(and(A, B), or(not(A), not(B))) = 0 |
90 | 88 | proof |
91 | 89 | 0 = 0 |
102 | 100 | and(and(A, B), or(not(A), not(B))) = 0 |
103 | 101 | qed |
104 | 102 | |
105 | theorem | |
103 | theorem (#or-rel) | |
106 | 104 | or(and(A, B), or(not(A), not(B))) = 1 |
107 | 105 | proof |
108 | 106 | 1 = 1 |
134 | 132 | > infer |
135 | 133 | > not(and(A, B)) = or(not(A), not(B)) |
136 | 134 | |
137 | is not expressible in equational logic, so can't be written in Eqthy. | |
138 | This is why I said above that we would not be able to follow this | |
139 | path of lemmas all the way to a proof of De Morgan's Laws. | |
140 | ||
141 | (There _is_ a purely equational proof of De Morgan's Laws; I know this | |
142 | because I asked the E prover to find one, and it did so. I would | |
143 | need to translate it into Eqthy to include it here, and I haven't | |
144 | done so yet. I also don't know yet how much similarity it bears to | |
145 | Huntington's approach.) | |
146 | ||
147 | In the meantime however, we can state a couple of other potentially | |
135 | is not expressible in equational logic, so can't directly be written in Eqthy. At least, not the general version of it: | |
136 | > From | |
137 | > and(X, Y) = 0 | |
138 | > and | |
139 | > or(X, Y) = 1 | |
140 | > infer | |
141 | > not(X) = Y | |
142 | ||
143 | ||
144 | But, we can still express the specific instance of it: | |
145 | ||
146 | theorem | |
147 | not(and(A, B)) = or(not(A), not(B)) | |
148 | proof | |
149 | not(and(A, B)) = not(and(A, B)) [by reflexivity] | |
150 | not(and(A, B)) = and(not(and(A, B)), 1) [by #and-ident] | |
151 | not(and(A, B)) = and(not(and(A, B)), or(and(A, B), or(not(A), not(B)))) [by #or-rel] | |
152 | not(and(A, B)) = or(and(not(and(A, B)), and(A, B)), and(not(and(A, B)), or(not(A), not(B)))) [by #and-dist] | |
153 | not(and(A, B)) = or(and(and(A, B), not(and(A, B))), and(not(and(A, B)), or(not(A), not(B)))) [by #and-comm] | |
154 | not(and(A, B)) = or(0, and(not(and(A, B)), or(not(A), not(B)))) [by #and-comp] | |
155 | not(and(A, B)) = or(and(and(A, B), or(not(A), not(B))), and(not(and(A, B)), or(not(A), not(B)))) [by #and-rel] | |
156 | not(and(A, B)) = or(and(or(not(A), not(B)), and(A, B)), and(not(and(A, B)), or(not(A), not(B)))) [by #and-comm] | |
157 | not(and(A, B)) = or(and(or(not(A), not(B)), and(A, B)), and(or(not(A), not(B)), not(and(A, B)))) [by #and-comm] | |
158 | not(and(A, B)) = and(or(not(A), not(B)), or(and(A, B), not(and(A, B)))) [by #and-dist] | |
159 | not(and(A, B)) = and(or(not(A), not(B)), 1) [by #or-comp] | |
160 | not(and(A, B)) = or(not(A), not(B)) [by #and-ident] | |
161 | qed | |
162 | ||
163 | To finish this off, we can state a couple of other potentially | |
148 | 164 | useful lemmas involving `not`. |
149 | 165 | |
150 | 166 | theorem |