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 v a) = a
Theorem	anidm 103	Idempotent law.
(a ^ a) = a
Theorem	orordi 104	Distribution of disjunction over disjunction.
(a v (b v c)) = ((a v b) v (a v c))
Theorem	orordir 105	Distribution of disjunction over disjunction.
((a v b) v c) = ((a v c) v (b v 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 v (a ^ b)) = a
Theorem	a5c 113	Absorption law.
(a ^ (a v 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 v c) = b   =>   (a ^ b) = a
Theorem	leao 116	Relation between two methods of expressing "less than or equal to".
(c ^ b) = a   =>   (a v b) = b
Theorem	mi 117	Mittelstaedt implication.
((a v b) == b) = (b v (a_|_ ^ b_|_))
Theorem	di 118	Dishkant implication.
((a ^ b) == a) = (a_|_ v (a ^ b))
Theorem	omlem1 119	Lemma in proof of Th. 1 of Pavicic 1987.
((a v (a_|_ ^ (a v b))) v (a v b)) = (a v b)
Theorem	omlem2 120	Lemma in proof of Th. 1 of Pavicic 1987.
((a v b)_|_ v (a v (a_|_ ^ (a v b)))) = 1
Definition	df-le 121	Define 'less than or equal to' analogue.
(a =<2 b) = ((a v b) == b)
Definition	df-le1 122	Define 'less than or equal to'. See df-le2 123 for the other direction.
(a v 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 v b) = b
Definition	df-c1 124	Define 'commutes'. See df-c2 125 for the other direction.
a = ((a ^ b) v (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) v (a ^ b_|_))
Definition	df-cmtr 126	Define 'commutator'.
C (a, b) = (((a ^ b) v (a ^ b_|_)) v ((a_|_ ^ b) v (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 v c)
Theorem	lerr 142	Add disjunct to right of l.e.
a =< b   =>   a =< (c v 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 v c) =< (b v 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 v b)
Theorem	leor 151	L.e. absorption.
a =< (b v 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 v c)
Theorem	leao2 155	L.e. absorption.
(b ^ a) =< (a v c)
Theorem	leao3 156	L.e. absorption.
(a ^ b) =< (c v a)
Theorem	leao4 157	L.e. absorption.
(b ^ a) =< (c v a)
Theorem	lelor 158	Add disjunct to left of both sides
a =< b   =>   (c v a) =< (c v 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 v c) =< (b v 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 v 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 v 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) v (a ^ c)) =< (a ^ (b v c))
Theorem	ledir 167	Half of distributive law.
((b ^ a) v (c ^ a)) =< ((b v c) ^ a)
Theorem	ledio 168	Half of distributive law.
(a v (b ^ c)) =< ((a v b) ^ (a v c))
Theorem	ledior 169	Half of distributive law.
((b ^ c) v a) =< ((b v a) ^ (c v 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 v 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 v c)) =< b   =>   (a ^ (b v c)) = ((a ^ b) v (a ^ c))
Theorem	str 181	Strengthening rule.
a =< (b v c)   &   (a ^ (b v 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 v b) == (b v a)) = 1
Theorem	wa3 185	Weak A3.
(((a v b) v c) == (a v (b v c))) = 1
Theorem	wa4 186	Weak A4.
((a v (b v b_|_)) == (b v b_|_)) = 1
Theorem	wa5 187	Weak A5.
((a v (a_|_ v b_|_)_|_) == a) = 1
Theorem	wa6 188	Weak A6.
((a == b) == ((a_|_ v b_|_)_|_ v (a v 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 v (a ^ b)) == a) = 1
Theorem	wa5c 193	Absorption law.
((a ^ (a v 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