Quantum Logic Explorer - mmtheorems2

Jump to page: 1 1-100 2 101-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-1024

Statement List for Quantum Logic Explorer - 101-200 - Page 2 of 11

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