P. 2 of Theorem List - Quantum Logic Explorer

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

Type	Label	Description
Statement
Theorem	dff 101	Alternate defintion of "false".
0 = (a ∩ a⊥ )
Theorem	or0 102	Disjunction with 0.
(a ∪ 0) = a
Theorem	or0r 103	Disjunction with 0.
(0 ∪ a) = a
Theorem	or1 104	Disjunction with 1.
(a ∪ 1) = 1
Theorem	or1r 105	Disjunction with 1.
(1 ∪ a) = 1
Theorem	an1 106	Conjunction with 1.
(a ∩ 1) = a
Theorem	an1r 107	Conjunction with 1.
(1 ∩ a) = a
Theorem	an0 108	Conjunction with 0.
(a ∩ 0) = 0
Theorem	an0r 109	Conjunction with 0.
(0 ∩ a) = 0
Theorem	oridm 110	Idempotent law.
(a ∪ a) = a
Theorem	anidm 111	Idempotent law.
(a ∩ a) = a
Theorem	orordi 112	Distribution of disjunction over disjunction.
(a ∪ (b ∪ c)) = ((a ∪ b) ∪ (a ∪ c))
Theorem	orordir 113	Distribution of disjunction over disjunction.
((a ∪ b) ∪ c) = ((a ∪ c) ∪ (b ∪ c))
Theorem	anandi 114	Distribution of conjunction over conjunction.
(a ∩ (b ∩ c)) = ((a ∩ b) ∩ (a ∩ c))
Theorem	anandir 115	Distribution of conjunction over conjunction.
((a ∩ b) ∩ c) = ((a ∩ c) ∩ (b ∩ c))
Theorem	biid 116	Identity law.
(a ≡ a) = 1
Theorem	1b 117	Identity law.
(1 ≡ a) = a
Theorem	bi1 118	Identity inference.
a = b    ⇒   (a ≡ b) = 1
Theorem	1bi 119	Identity inference.
a = b    ⇒   1 = (a ≡ b)
Theorem	orabs 120	Absorption law.
(a ∪ (a ∩ b)) = a
Theorem	anabs 121	Absorption law.
(a ∩ (a ∪ b)) = a
Theorem	conb 122	Contraposition law.
(a ≡ b) = (a⊥ ≡ b⊥ )
Theorem	leoa 123	Relation between two methods of expressing "less than or equal to".
(a ∪ c) = b    ⇒   (a ∩ b) = a
Theorem	leao 124	Relation between two methods of expressing "less than or equal to".
(c ∩ b) = a    ⇒   (a ∪ b) = b
Theorem	mi 125	Mittelstaedt implication.
((a ∪ b) ≡ b) = (b ∪ (a⊥ ∩ b⊥ ))
Theorem	di 126	Dishkant implication.
((a ∩ b) ≡ a) = (a⊥ ∪ (a ∩ b))
Theorem	omlem1 127	Lemma in proof of Th. 1 of Pavicic 1987.
((a ∪ (a⊥ ∩ (a ∪ b))) ∪ (a ∪ b)) = (a ∪ b)
Theorem	omlem2 128	Lemma in proof of Th. 1 of Pavicic 1987.
((a ∪ b)⊥ ∪ (a ∪ (a⊥ ∩ (a ∪ b)))) = 1
0.1.3  Relationship analogues (ordering; commutation)
Definition	df-le 129	Define 'less than or equal to' analogue.
(a ≤2 b) = ((a ∪ b) ≡ b)
Definition	df-le1 130	Define 'less than or equal to'. See df-le2 131 for the other direction.
(a ∪ b) = b    ⇒   a ≤ b
Definition	df-le2 131	Define 'less than or equal to'. See df-le1 130 for the other direction.
a ≤ b    ⇒   (a ∪ b) = b
Definition	df-c1 132	Define 'commutes'. See df-c2 133 for the other direction.
a = ((a ∩ b) ∪ (a ∩ b⊥ ))    ⇒   a C b
Definition	df-c2 133	Define 'commutes'. See df-c1 132 for the other direction.
a C b    ⇒   a = ((a ∩ b) ∪ (a ∩ b⊥ ))
Definition	df-cmtr 134	Define 'commutator'.
C (a, b) = (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
Theorem	df2le1 135	Alternate definition of 'less than or equal to'.
(a ∩ b) = a    ⇒   a ≤ b
Theorem	df2le2 136	Alternate definition of 'less than or equal to'.
a ≤ b    ⇒   (a ∩ b) = a
Theorem	letr 137	Transitive law for l.e.
a ≤ b    &   b ≤ c    ⇒   a ≤ c
Theorem	bltr 138	Transitive inference.
a = b    &   b ≤ c    ⇒   a ≤ c
Theorem	lbtr 139	Transitive inference.
a ≤ b    &   b = c    ⇒   a ≤ c
Theorem	le3tr1 140	Transitive inference useful for introducing definitions.
a ≤ b    &   c = a    &   d = b    ⇒   c ≤ d
Theorem	le3tr2 141	Transitive inference useful for eliminating definitions.
a ≤ b    &   a = c    &   b = d    ⇒   c ≤ d
Theorem	bile 142	Biconditional to l.e.
a = b    ⇒   a ≤ b
Theorem	qlhoml1a 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).
a ≤ a⊥ ⊥
Theorem	qlhoml1b 144	An ortholattice inequality, corresponding to a theorem provable in Hilbert space.
a⊥ ⊥ ≤ a
Theorem	lebi 145	L.e. to biconditional.
a ≤ b    &   b ≤ a    ⇒   a = b
Theorem	le1 146	Anything is l.e. 1.
a ≤ 1
Theorem	le0 147	0 is l.e. anything.
0 ≤ a
Theorem	leid 148	Identity law for less-than-or-equal.
a ≤ a
Theorem	ler 149	Add disjunct to right of l.e.
a ≤ b    ⇒   a ≤ (b ∪ c)
Theorem	lerr 150	Add disjunct to right of l.e.
a ≤ b    ⇒   a ≤ (c ∪ b)
Theorem	lel 151	Add conjunct to left of l.e.
a ≤ b    ⇒   (a ∩ c) ≤ b
Theorem	leror 152	Add disjunct to right of both sides.
a ≤ b    ⇒   (a ∪ c) ≤ (b ∪ c)
Theorem	leran 153	Add conjunct to right of both sides.
a ≤ b    ⇒   (a ∩ c) ≤ (b ∩ c)
Theorem	lecon 154	Contrapositive for l.e.
a ≤ b    ⇒   b⊥ ≤ a⊥
Theorem	lecon1 155	Contrapositive for l.e.
a⊥ ≤ b⊥    ⇒   b ≤ a
Theorem	lecon2 156	Contrapositive for l.e.
a⊥ ≤ b    ⇒   b⊥ ≤ a
Theorem	lecon3 157	Contrapositive for l.e.
a ≤ b⊥    ⇒   b ≤ a⊥
Theorem	leo 158	L.e. absorption.
a ≤ (a ∪ b)
Theorem	leor 159	L.e. absorption.
a ≤ (b ∪ a)
Theorem	lea 160	L.e. absorption.
(a ∩ b) ≤ a
Theorem	lear 161	L.e. absorption.
(a ∩ b) ≤ b
Theorem	leao1 162	L.e. absorption.
(a ∩ b) ≤ (a ∪ c)
Theorem	leao2 163	L.e. absorption.
(b ∩ a) ≤ (a ∪ c)
Theorem	leao3 164	L.e. absorption.
(a ∩ b) ≤ (c ∪ a)
Theorem	leao4 165	L.e. absorption.
(b ∩ a) ≤ (c ∪ a)
Theorem	lelor 166	Add disjunct to left of both sides.
a ≤ b    ⇒   (c ∪ a) ≤ (c ∪ b)
Theorem	lelan 167	Add conjunct to left of both sides.
a ≤ b    ⇒   (c ∩ a) ≤ (c ∩ b)
Theorem	le2or 168	Disjunction of 2 l.e.'s.
a ≤ b    &   c ≤ d    ⇒   (a ∪ c) ≤ (b ∪ d)
Theorem	le2an 169	Conjunction of 2 l.e.'s.
a ≤ b    &   c ≤ d    ⇒   (a ∩ c) ≤ (b ∩ d)
Theorem	lel2or 170	Disjunction of 2 l.e.'s.
a ≤ b    &   c ≤ b    ⇒   (a ∪ c) ≤ b
Theorem	lel2an 171	Conjunction of 2 l.e.'s.
a ≤ b    &   c ≤ b    ⇒   (a ∩ c) ≤ b
Theorem	ler2or 172	Disjunction of 2 l.e.'s.
a ≤ b    &   a ≤ c    ⇒   a ≤ (b ∪ c)
Theorem	ler2an 173	Conjunction of 2 l.e.'s.
a ≤ b    &   a ≤ c    ⇒   a ≤ (b ∩ c)
Theorem	ledi 174	Half of distributive law.
((a ∩ b) ∪ (a ∩ c)) ≤ (a ∩ (b ∪ c))
Theorem	ledir 175	Half of distributive law.
((b ∩ a) ∪ (c ∩ a)) ≤ ((b ∪ c) ∩ a)
Theorem	ledio 176	Half of distributive law.
(a ∪ (b ∩ c)) ≤ ((a ∪ b) ∩ (a ∪ c))
Theorem	ledior 177	Half of distributive law.
((b ∩ c) ∪ a) ≤ ((b ∪ a) ∩ (c ∪ a))
Theorem	comm0 178	Commutation with 0. Kalmbach 83 p. 20.
a C 0
Theorem	comm1 179	Commutation with 1. Kalmbach 83 p. 20.
1 C a
Theorem	lecom 180	Comparable elements commute. Beran 84 2.3(iii) p. 40.
a ≤ b    ⇒   a C b
Theorem	bctr 181	Transitive inference.
a = b    &   b C c    ⇒   a C c
Theorem	cbtr 182	Transitive inference.
a C b    &   b = c    ⇒   a C c
Theorem	comcom2 183	Commutation equivalence. Kalmbach 83 p. 23. Does not use OML.
a C b    ⇒   a C b⊥
Theorem	comorr 184	Commutation law. Does not use OML.
a C (a ∪ b)
Theorem	coman1 185	Commutation law. Does not use OML.
(a ∩ b) C a
Theorem	coman2 186	Commutation law. Does not use OML.
(a ∩ b) C b
Theorem	comid 187	Identity law for commutation. Does not use OML.
a C a
Theorem	distlem 188	Distributive law inference (uses OL only).
(a ∩ (b ∪ c)) ≤ b    ⇒   (a ∩ (b ∪ c)) = ((a ∩ b) ∪ (a ∩ c))
Theorem	str 189	Strengthening rule.
a ≤ (b ∪ c)    &   (a ∩ (b ∪ c)) ≤ b    ⇒   a ≤ b
0.1.4  Commutator (ortholattice theorems)
Theorem	cmtrcom 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.
Theorem	wa1 191	Weak A1.
(a ≡ a⊥ ⊥ ) = 1
Theorem	wa2 192	Weak A2.
((a ∪ b) ≡ (b ∪ a)) = 1
Theorem	wa3 193	Weak A3.
(((a ∪ b) ∪ c) ≡ (a ∪ (b ∪ c))) = 1
Theorem	wa4 194	Weak A4.
((a ∪ (b ∪ b⊥ )) ≡ (b ∪ b⊥ )) = 1
Theorem	wa5 195	Weak A5.
((a ∪ (a⊥ ∪ b⊥ )⊥ ) ≡ a) = 1
Theorem	wa6 196	Weak A6.
((a ≡ b) ≡ ((a⊥ ∪ b⊥ )⊥ ∪ (a ∪ b)⊥ )) = 1
Theorem	wr1 197	Weak R1.
(a ≡ b) = 1    ⇒   (b ≡ a) = 1
Theorem	wr3 198	Weak R3.
(1 ≡ a) = 1    ⇒   a = 1
Theorem	wr4 199	Weak R4.
(a ≡ b) = 1    ⇒   (a⊥ ≡ b⊥ ) = 1
Theorem	wa5b 200	Absorption law.
((a ∪ (a ∩ b)) ≡ a) = 1