Theorem List for Quantum Logic Explorer - 101-200   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremdff 101 Alternate definition of "false". (Contributed by NM, 29-Aug-1997.)
0 = (aa )

Theoremor0 102 Disjunction with 0. (Contributed by NM, 10-Aug-1997.)
(a ∪ 0) = a

Theoremor0r 103 Disjunction with 0. (Contributed by NM, 26-Nov-1997.)
(0 ∪ a) = a

Theoremor1 104 Disjunction with 1. (Contributed by NM, 10-Aug-1997.)
(a ∪ 1) = 1

Theoremor1r 105 Disjunction with 1. (Contributed by NM, 26-Nov-1997.)
(1 ∪ a) = 1

Theoreman1 106 Conjunction with 1. (Contributed by NM, 10-Aug-1997.)
(a ∩ 1) = a

Theoreman1r 107 Conjunction with 1. (Contributed by NM, 26-Nov-1997.)
(1 ∩ a) = a

Theoreman0 108 Conjunction with 0. (Contributed by NM, 10-Aug-1997.)
(a ∩ 0) = 0

Theoreman0r 109 Conjunction with 0. (Contributed by NM, 26-Nov-1997.)
(0 ∩ a) = 0

Theoremoridm 110 Idempotent law. (Contributed by NM, 10-Aug-1997.)
(aa) = a

Theoremanidm 111 Idempotent law. (Contributed by NM, 10-Aug-1997.)
(aa) = a

Theoremorordi 112 Distribution of disjunction over disjunction. (Contributed by NM, 27-Aug-1997.)
(a ∪ (bc)) = ((ab) ∪ (ac))

Theoremorordir 113 Distribution of disjunction over disjunction. (Contributed by NM, 27-Aug-1997.)
((ab) ∪ c) = ((ac) ∪ (bc))

Theoremanandi 114 Distribution of conjunction over conjunction. (Contributed by NM, 27-Aug-1997.)
(a ∩ (bc)) = ((ab) ∩ (ac))

Theoremanandir 115 Distribution of conjunction over conjunction. (Contributed by NM, 27-Aug-1997.)
((ab) ∩ c) = ((ac) ∩ (bc))

Theorembiid 116 Identity law. (Contributed by NM, 10-Aug-1997.)
(aa) = 1

Theorem1b 117 Identity law. (Contributed by NM, 10-Aug-1997.)
(1 ≡ a) = a

Theorembi1 118 Identity inference. (Contributed by NM, 30-Aug-1997.)
a = b       (ab) = 1

Theorem1bi 119 Identity inference. (Contributed by NM, 30-Aug-1997.)
a = b       1 = (ab)

Theoremorabs 120 Absorption law. (Contributed by NM, 11-Aug-1997.)
(a ∪ (ab)) = a

Theoremanabs 121 Absorption law. (Contributed by NM, 11-Aug-1997.)
(a ∩ (ab)) = a

Theoremconb 122 Contraposition law. (Contributed by NM, 10-Aug-1997.)
(ab) = (ab )

Theoremleoa 123 Relation between two methods of expressing "less than or equal to". (Contributed by NM, 11-Aug-1997.)
(ac) = b       (ab) = a

Theoremleao 124 Relation between two methods of expressing "less than or equal to". (Contributed by NM, 11-Aug-1997.)
(cb) = a       (ab) = b

Theoremmi 125 Mittelstaedt implication. (Contributed by NM, 12-Aug-1997.)
((ab) ≡ b) = (b ∪ (ab ))

Theoremdi 126 Dishkant implication. (Contributed by NM, 12-Aug-1997.)
((ab) ≡ a) = (a ∪ (ab))

Theoremomlem1 127 Lemma in proof of Thm. 1 of Pavicic 1987. (Contributed by NM, 12-Aug-1997.)
((a ∪ (a ∩ (ab))) ∪ (ab)) = (ab)

Theoremomlem2 128 Lemma in proof of Thm. 1 of Pavicic 1987. (Contributed by NM, 12-Aug-1997.)
((ab) ∪ (a ∪ (a ∩ (ab)))) = 1

0.1.3  Relationship analogues (ordering; commutation)

Definitiondf-le 129 Define "less than or equal to" analogue. (Contributed by NM, 27-Aug-1997.)
(a2 b) = ((ab) ≡ b)

Definitiondf-le1 130 Define "less than or equal to". See df-le2 131 for the other direction. (Contributed by NM, 27-Aug-1997.)
(ab) = b       ab

Definitiondf-le2 131 Define "less than or equal to". See df-le1 130 for the other direction. (Contributed by NM, 27-Aug-1997.)
ab       (ab) = b

Definitiondf-c1 132 Define "commutes". See df-c2 133 for the other direction. (Contributed by NM, 27-Aug-1997.)
a = ((ab) ∪ (ab ))       a C b

Definitiondf-c2 133 Define "commutes". See df-c1 132 for the other direction. (Contributed by NM, 27-Aug-1997.)
a C b       a = ((ab) ∪ (ab ))

Definitiondf-cmtr 134 Define "commutator". (Contributed by NM, 24-Jan-1999.)
C (a, b) = (((ab) ∪ (ab )) ∪ ((ab) ∪ (ab )))

Theoremdf2le1 135 Alternate definition of "less than or equal to". (Contributed by NM, 27-Aug-1997.)
(ab) = a       ab

Theoremdf2le2 136 Alternate definition of "less than or equal to". (Contributed by NM, 27-Aug-1997.)
ab       (ab) = a

Theoremletr 137 Transitive law for "less than or equal to". (Contributed by NM, 27-Aug-1997.)
ab    &   bc       ac

Theorembltr 138 Transitive inference. (Contributed by NM, 28-Aug-1997.)
a = b    &   bc       ac

Theoremlbtr 139 Transitive inference. (Contributed by NM, 28-Aug-1997.)
ab    &   b = c       ac

Theoremle3tr1 140 Transitive inference useful for introducing definitions. (Contributed by NM, 27-Aug-1997.)
ab    &   c = a    &   d = b       cd

Theoremle3tr2 141 Transitive inference useful for eliminating definitions. (Contributed by NM, 27-Aug-1997.)
ab    &   a = c    &   b = d       cd

Theorembile 142 Biconditional to "less than or equal to". (Contributed by NM, 27-Aug-1997.)
a = b       ab

Theoremqlhoml1a 143 An ortholattice inequality, corresponding to a theorem provable in Hilbert space. Part of Definition 2.1 p. 2092, in M. Pavicic and N. Megill, "Quantum and Classical Implicational Algebras with Primitive Implication", Int. J. of Theor. Phys. 37, 2091-2098 (1998). (Contributed by NM, 3-Feb-2002.)
aa

Theoremqlhoml1b 144 An ortholattice inequality, corresponding to a theorem provable in Hilbert space. (Contributed by NM, 3-Feb-2002.)
a a

Theoremlebi 145 "Less than or equal to" to biconditional. (Contributed by NM, 27-Aug-1997.)
ab    &   ba       a = b

Theoremle1 146 Anything is less than or equal to 1. (Contributed by NM, 30-Aug-1997.)
a ≤ 1

Theoremle0 147 0 is less than or equal to anything. (Contributed by NM, 30-Aug-1997.)
0 ≤ a

Theoremleid 148 Identity law for "less than or equal to". (Contributed by NM, 24-Dec-1998.)
aa

Theoremler 149 Add disjunct to right of l.e. (Contributed by NM, 27-Aug-1997.)
ab       a ≤ (bc)

Theoremlerr 150 Add disjunct to right of l.e. (Contributed by NM, 11-Nov-1997.)
ab       a ≤ (cb)

Theoremlel 151 Add conjunct to left of l.e. (Contributed by NM, 27-Aug-1997.)
ab       (ac) ≤ b

Theoremleror 152 Add disjunct to right of both sides. (Contributed by NM, 27-Aug-1997.)
ab       (ac) ≤ (bc)

Theoremleran 153 Add conjunct to right of both sides. (Contributed by NM, 27-Aug-1997.)
ab       (ac) ≤ (bc)

Theoremlecon 154 Contrapositive for l.e. (Contributed by NM, 27-Aug-1997.)
ab       ba

Theoremlecon1 155 Contrapositive for l.e. (Contributed by NM, 7-Nov-1997.)
ab       ba

Theoremlecon2 156 Contrapositive for l.e. (Contributed by NM, 19-Dec-1998.)
ab       ba

Theoremlecon3 157 Contrapositive for l.e. (Contributed by NM, 19-Dec-1998.)
ab       ba

Theoremleo 158 L.e. absorption. (Contributed by NM, 27-Aug-1997.)
a ≤ (ab)

Theoremleor 159 L.e. absorption. (Contributed by NM, 11-Nov-1997.)
a ≤ (ba)

Theoremlea 160 L.e. absorption. (Contributed by NM, 27-Aug-1997.)
(ab) ≤ a

Theoremlear 161 L.e. absorption. (Contributed by NM, 11-Nov-1997.)
(ab) ≤ b

Theoremleao1 162 L.e. absorption. (Contributed by NM, 8-Jul-2000.)
(ab) ≤ (ac)

Theoremleao2 163 L.e. absorption. (Contributed by NM, 8-Jul-2000.)
(ba) ≤ (ac)

Theoremleao3 164 L.e. absorption. (Contributed by NM, 8-Jul-2000.)
(ab) ≤ (ca)

Theoremleao4 165 L.e. absorption. (Contributed by NM, 8-Jul-2000.)
(ba) ≤ (ca)

Theoremlelor 166 Add disjunct to left of both sides. (Contributed by NM, 25-Oct-1997.)
ab       (ca) ≤ (cb)

Theoremlelan 167 Add conjunct to left of both sides. (Contributed by NM, 25-Oct-1997.)
ab       (ca) ≤ (cb)

Theoremle2or 168 Disjunction of 2 l.e.'s. (Contributed by NM, 25-Oct-1997.)
ab    &   cd       (ac) ≤ (bd)

Theoremle2an 169 Conjunction of 2 l.e.'s. (Contributed by NM, 25-Oct-1997.)
ab    &   cd       (ac) ≤ (bd)

Theoremlel2or 170 Disjunction of 2 l.e.'s. (Contributed by NM, 11-Nov-1997.)
ab    &   cb       (ac) ≤ b

Theoremlel2an 171 Conjunction of 2 l.e.'s. (Contributed by NM, 11-Nov-1997.)
ab    &   cb       (ac) ≤ b

Theoremler2or 172 Disjunction of 2 l.e.'s. (Contributed by NM, 11-Nov-1997.)
ab    &   ac       a ≤ (bc)

Theoremler2an 173 Conjunction of 2 l.e.'s. (Contributed by NM, 11-Nov-1997.)
ab    &   ac       a ≤ (bc)

Theoremledi 174 Half of distributive law. (Contributed by NM, 28-Aug-1997.)
((ab) ∪ (ac)) ≤ (a ∩ (bc))

Theoremledir 175 Half of distributive law. (Contributed by NM, 30-Nov-1998.)
((ba) ∪ (ca)) ≤ ((bc) ∩ a)

Theoremledio 176 Half of distributive law. (Contributed by NM, 28-Aug-1997.)
(a ∪ (bc)) ≤ ((ab) ∩ (ac))

Theoremledior 177 Half of distributive law. (Contributed by NM, 30-Nov-1998.)
((bc) ∪ a) ≤ ((ba) ∩ (ca))

Theoremcomm0 178 Commutation with 0. Kalmbach 83 p. 20. (Contributed by NM, 27-Aug-1997.)
a C 0

Theoremcomm1 179 Commutation with 1. Kalmbach 83 p. 20. (Contributed by NM, 27-Aug-1997.)
1 C a

Theoremlecom 180 Comparable elements commute. Beran 84 2.3(iii) p. 40. (Contributed by NM, 30-Aug-1997.)
ab       a C b

Theorembctr 181 Transitive inference. (Contributed by NM, 30-Aug-1997.)
a = b    &   b C c       a C c

Theoremcbtr 182 Transitive inference. (Contributed by NM, 30-Aug-1997.)
a C b    &   b = c       a C c

Theoremcomcom2 183 Commutation equivalence. Kalmbach 83 p. 23. Does not use OML. (Contributed by NM, 27-Aug-1997.)
a C b       a C b

Theoremcomorr 184 Commutation law. Does not use OML. (Contributed by NM, 30-Aug-1997.)
a C (ab)

Theoremcoman1 185 Commutation law. Does not use OML. (Contributed by NM, 30-Aug-1997.)
(ab) C a

Theoremcoman2 186 Commutation law. Does not use OML. (Contributed by NM, 9-Nov-1997.)
(ab) C b

Theoremcomid 187 Identity law for commutation. Does not use OML. (Contributed by NM, 9-Nov-1997.)
a C a

Theoremdistlem 188 Distributive law inference (uses OL only). (Contributed by NM, 17-Nov-1998.)
(a ∩ (bc)) ≤ b       (a ∩ (bc)) = ((ab) ∪ (ac))

Theoremstr 189 Strengthening rule. (Contributed by NM, 18-Nov-1998.)
a ≤ (bc)    &   (a ∩ (bc)) ≤ b       ab

0.1.4  Commutator (ortholattice theorems)

Theoremcmtrcom 190 Commutative law for commutator. (Contributed by NM, 24-Jan-1999.)
C (a, b) = C (b, a)

0.1.5  Weak "orthomodular law" in ortholattices.

All theorems here do not require R3 and are true in all ortholattices.

Theoremwa1 191 Weak A1. (Contributed by NM, 27-Sep-1997.)
(aa ) = 1

Theoremwa2 192 Weak A2. (Contributed by NM, 27-Sep-1997.)
((ab) ≡ (ba)) = 1

Theoremwa3 193 Weak A3. (Contributed by NM, 27-Sep-1997.)
(((ab) ∪ c) ≡ (a ∪ (bc))) = 1

Theoremwa4 194 Weak A4. (Contributed by NM, 27-Sep-1997.)
((a ∪ (bb )) ≡ (bb )) = 1

Theoremwa5 195 Weak A5. (Contributed by NM, 27-Sep-1997.)
((a ∪ (ab ) ) ≡ a) = 1

Theoremwa6 196 Weak A6. (Contributed by NM, 12-Jul-1998.)
((ab) ≡ ((ab ) ∪ (ab) )) = 1

Theoremwr1 197 Weak R1. (Contributed by NM, 2-Sep-1997.)
(ab) = 1       (ba) = 1

Theoremwr3 198 Weak R3. (Contributed by NM, 2-Sep-1997.)
(1 ≡ a) = 1       a = 1

Theoremwr4 199 Weak R4. (Contributed by NM, 2-Sep-1997.)
(ab) = 1       (ab ) = 1

Theoremwa5b 200 Absorption law. (Contributed by NM, 27-Sep-1997.)
((a ∪ (ab)) ≡ a) = 1

Page List
Jump to page: Contents  1 1-100101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1217
 Copyright terms: Public domain < Previous  Next >