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

Theoremdff 101 Alternate defintion of "false".
0 = (aa )

Theoremor0 102 Disjunction with 0.
(a ∪ 0) = a

Theoremor0r 103 Disjunction with 0.
(0 ∪ a) = a

Theoremor1 104 Disjunction with 1.
(a ∪ 1) = 1

Theoremor1r 105 Disjunction with 1.
(1 ∪ a) = 1

Theoreman1 106 Conjunction with 1.
(a ∩ 1) = a

Theoreman1r 107 Conjunction with 1.
(1 ∩ a) = a

Theoreman0 108 Conjunction with 0.
(a ∩ 0) = 0

Theoreman0r 109 Conjunction with 0.
(0 ∩ a) = 0

Theoremoridm 110 Idempotent law.
(aa) = a

Theoremanidm 111 Idempotent law.
(aa) = a

Theoremorordi 112 Distribution of disjunction over disjunction.
(a ∪ (bc)) = ((ab) ∪ (ac))

Theoremorordir 113 Distribution of disjunction over disjunction.
((ab) ∪ c) = ((ac) ∪ (bc))

Theoremanandi 114 Distribution of conjunction over conjunction.
(a ∩ (bc)) = ((ab) ∩ (ac))

Theoremanandir 115 Distribution of conjunction over conjunction.
((ab) ∩ c) = ((ac) ∩ (bc))

Theorembiid 116 Identity law.
(aa) = 1

Theorem1b 117 Identity law.
(1 ≡ a) = a

Theorembi1 118 Identity inference.
a = b       (ab) = 1

Theorem1bi 119 Identity inference.
a = b       1 = (ab)

Theoremorabs 120 Absorption law.
(a ∪ (ab)) = a

Theoremanabs 121 Absorption law.
(a ∩ (ab)) = a

Theoremconb 122 Contraposition law.
(ab) = (ab )

Theoremleoa 123 Relation between two methods of expressing "less than or equal to".
(ac) = b       (ab) = a

Theoremleao 124 Relation between two methods of expressing "less than or equal to".
(cb) = a       (ab) = b

Theoremmi 125 Mittelstaedt implication.
((ab) ≡ b) = (b ∪ (ab ))

Theoremdi 126 Dishkant implication.
((ab) ≡ a) = (a ∪ (ab))

Theoremomlem1 127 Lemma in proof of Th. 1 of Pavicic 1987.
((a ∪ (a ∩ (ab))) ∪ (ab)) = (ab)

Theoremomlem2 128 Lemma in proof of Th. 1 of Pavicic 1987.
((ab) ∪ (a ∪ (a ∩ (ab)))) = 1

0.1.3  Relationship analogues (ordering; commutation)

Definitiondf-le 129 Define 'less than or equal to' analogue.
(a2 b) = ((ab) ≡ b)

Definitiondf-le1 130 Define 'less than or equal to'. See df-le2 131 for the other direction.
(ab) = b       ab

Definitiondf-le2 131 Define 'less than or equal to'. See df-le1 130 for the other direction.
ab       (ab) = b

Definitiondf-c1 132 Define 'commutes'. See df-c2 133 for the other direction.
a = ((ab) ∪ (ab ))       a C b

Definitiondf-c2 133 Define 'commutes'. See df-c1 132 for the other direction.
a C b       a = ((ab) ∪ (ab ))

Definitiondf-cmtr 134 Define 'commutator'.
C (a, b) = (((ab) ∪ (ab )) ∪ ((ab) ∪ (ab )))

Theoremdf2le1 135 Alternate definition of 'less than or equal to'.
(ab) = a       ab

Theoremdf2le2 136 Alternate definition of 'less than or equal to'.
ab       (ab) = a

Theoremletr 137 Transitive law for l.e.
ab    &   bc       ac

Theorembltr 138 Transitive inference.
a = b    &   bc       ac

Theoremlbtr 139 Transitive inference.
ab    &   b = c       ac

Theoremle3tr1 140 Transitive inference useful for introducing definitions.
ab    &   c = a    &   d = b       cd

Theoremle3tr2 141 Transitive inference useful for eliminating definitions.
ab    &   a = c    &   b = d       cd

Theorembile 142 Biconditional to l.e.
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).
aa

Theoremqlhoml1b 144 An ortholattice inequality, corresponding to a theorem provable in Hilbert space.
a a

Theoremlebi 145 L.e. to biconditional.
ab    &   ba       a = b

Theoremle1 146 Anything is l.e. 1.
a ≤ 1

Theoremle0 147 0 is l.e. anything.
0 ≤ a

Theoremleid 148 Identity law for less-than-or-equal.
aa

Theoremler 149 Add disjunct to right of l.e.
ab       a ≤ (bc)

Theoremlerr 150 Add disjunct to right of l.e.
ab       a ≤ (cb)

Theoremlel 151 Add conjunct to left of l.e.
ab       (ac) ≤ b

Theoremleror 152 Add disjunct to right of both sides.
ab       (ac) ≤ (bc)

Theoremleran 153 Add conjunct to right of both sides.
ab       (ac) ≤ (bc)

Theoremlecon 154 Contrapositive for l.e.
ab       ba

Theoremlecon1 155 Contrapositive for l.e.
ab       ba

Theoremlecon2 156 Contrapositive for l.e.
ab       ba

Theoremlecon3 157 Contrapositive for l.e.
ab       ba

Theoremleo 158 L.e. absorption.
a ≤ (ab)

Theoremleor 159 L.e. absorption.
a ≤ (ba)

Theoremlea 160 L.e. absorption.
(ab) ≤ a

Theoremlear 161 L.e. absorption.
(ab) ≤ b

Theoremleao1 162 L.e. absorption.
(ab) ≤ (ac)

Theoremleao2 163 L.e. absorption.
(ba) ≤ (ac)

Theoremleao3 164 L.e. absorption.
(ab) ≤ (ca)

Theoremleao4 165 L.e. absorption.
(ba) ≤ (ca)

Theoremlelor 166 Add disjunct to left of both sides.
ab       (ca) ≤ (cb)

Theoremlelan 167 Add conjunct to left of both sides.
ab       (ca) ≤ (cb)

Theoremle2or 168 Disjunction of 2 l.e.'s.
ab    &   cd       (ac) ≤ (bd)

Theoremle2an 169 Conjunction of 2 l.e.'s.
ab    &   cd       (ac) ≤ (bd)

Theoremlel2or 170 Disjunction of 2 l.e.'s.
ab    &   cb       (ac) ≤ b

Theoremlel2an 171 Conjunction of 2 l.e.'s.
ab    &   cb       (ac) ≤ b

Theoremler2or 172 Disjunction of 2 l.e.'s.
ab    &   ac       a ≤ (bc)

Theoremler2an 173 Conjunction of 2 l.e.'s.
ab    &   ac       a ≤ (bc)

Theoremledi 174 Half of distributive law.
((ab) ∪ (ac)) ≤ (a ∩ (bc))

Theoremledir 175 Half of distributive law.
((ba) ∪ (ca)) ≤ ((bc) ∩ a)

Theoremledio 176 Half of distributive law.
(a ∪ (bc)) ≤ ((ab) ∩ (ac))

Theoremledior 177 Half of distributive law.
((bc) ∪ a) ≤ ((ba) ∩ (ca))

Theoremcomm0 178 Commutation with 0. Kalmbach 83 p. 20.
a C 0

Theoremcomm1 179 Commutation with 1. Kalmbach 83 p. 20.
1 C a

Theoremlecom 180 Comparable elements commute. Beran 84 2.3(iii) p. 40.
ab       a C b

Theorembctr 181 Transitive inference.
a = b    &   b C c       a C c

Theoremcbtr 182 Transitive inference.
a C b    &   b = c       a C c

Theoremcomcom2 183 Commutation equivalence. Kalmbach 83 p. 23. Does not use OML.
a C b       a C b

Theoremcomorr 184 Commutation law. Does not use OML.
a C (ab)

Theoremcoman1 185 Commutation law. Does not use OML.
(ab) C a

Theoremcoman2 186 Commutation law. Does not use OML.
(ab) C b

Theoremcomid 187 Identity law for commutation. Does not use OML.
a C a

Theoremdistlem 188 Distributive law inference (uses OL only).
(a ∩ (bc)) ≤ b       (a ∩ (bc)) = ((ab) ∪ (ac))

Theoremstr 189 Strengthening rule.
a ≤ (bc)    &   (a ∩ (bc)) ≤ b       ab

0.1.4  Commutator (ortholattice theorems)

Theoremcmtrcom 190 Commutative law for commutator.
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.
(aa ) = 1

Theoremwa2 192 Weak A2.
((ab) ≡ (ba)) = 1

Theoremwa3 193 Weak A3.
(((ab) ∪ c) ≡ (a ∪ (bc))) = 1

Theoremwa4 194 Weak A4.
((a ∪ (bb )) ≡ (bb )) = 1

Theoremwa5 195 Weak A5.
((a ∪ (ab ) ) ≡ a) = 1

Theoremwa6 196 Weak A6.
((ab) ≡ ((ab ) ∪ (ab) )) = 1

Theoremwr1 197 Weak R1.
(ab) = 1       (ba) = 1

Theoremwr3 198 Weak R3.
(1 ≡ a) = 1       a = 1

Theoremwr4 199 Weak R4.
(ab) = 1       (ab ) = 1

Theoremwa5b 200 Absorption law.
((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-1215
 Copyright terms: Public domain < Previous  Next >