mmtheorems2 - Quantum Logic Explorer

Jump to page: Contents + 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-1100 12 1101-1118

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

Type	Label	Description
Statement
Theorem	dff 101	Alternate defintion of "false".
0 = (a ^ a')
Theorem	or0 102	Disjunction with 0.
(a v 0) = a
Theorem	or0r 103	Disjunction with 0.
(0 v a) = a
Theorem	or1 104	Disjunction with 1.
(a v 1) = 1
Theorem	or1r 105	Disjunction with 1.
(1 v 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 v a) = a
Theorem	anidm 111	Idempotent law.
(a ^ a) = a
Theorem	orordi 112	Distribution of disjunction over disjunction.
(a v (b v c)) = ((a v b) v (a v c))
Theorem	orordir 113	Distribution of disjunction over disjunction.
((a v b) v c) = ((a v c) v (b v 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	a5b 120	Absorption law.
(a v (a ^ b)) = a
Theorem	a5c 121	Absorption law.
(a ^ (a v 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 v c) = b   =>   (a ^ b) = a
Theorem	leao 124	Relation between two methods of expressing "less than or equal to".
(c ^ b) = a   =>   (a v b) = b
Theorem	mi 125	Mittelstaedt implication.
((a v b) == b) = (b v (a' ^ b'))
Theorem	di 126	Dishkant implication.
((a ^ b) == a) = (a' v (a ^ b))
Theorem	omlem1 127	Lemma in proof of Th. 1 of Pavicic 1987.
((a v (a' ^ (a v b))) v (a v b)) = (a v b)
Theorem	omlem2 128	Lemma in proof of Th. 1 of Pavicic 1987.
((a v b)' v (a v (a' ^ (a v b)))) = 1
Relationship analogues (ordering; commutation)
Definition	df-le 129	Define 'less than or equal to' analogue.
(a =<2 b) = ((a v b) == b)
Definition	df-le1 130	Define 'less than or equal to'. See df-le2 131 for the other direction.
(a v 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 v b) = b
Definition	df-c1 132	Define 'commutes'. See df-c2 133 for the other direction.
a = ((a ^ b) v (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) v (a ^ b'))
Definition	df-cmtr 134	Define 'commutator'.
C (a, b) = (((a ^ b) v (a ^ b')) v ((a' ^ b) v (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 v c)
Theorem	lerr 150	Add disjunct to right of l.e.
a =< b   =>   a =< (c v 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 v c) =< (b v 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 v b)
Theorem	leor 159	L.e. absorption.
a =< (b v 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 v c)
Theorem	leao2 163	L.e. absorption.
(b ^ a) =< (a v c)
Theorem	leao3 164	L.e. absorption.
(a ^ b) =< (c v a)
Theorem	leao4 165	L.e. absorption.
(b ^ a) =< (c v a)
Theorem	lelor 166	Add disjunct to left of both sides
a =< b   =>   (c v a) =< (c v 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 v c) =< (b v 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 v 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 v 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) v (a ^ c)) =< (a ^ (b v c))
Theorem	ledir 175	Half of distributive law.
((b ^ a) v (c ^ a)) =< ((b v c) ^ a)
Theorem	ledio 176	Half of distributive law.
(a v (b ^ c)) =< ((a v b) ^ (a v c))
Theorem	ledior 177	Half of distributive law.
((b ^ c) v a) =< ((b v a) ^ (c v 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 v 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 v c)) =< b   =>   (a ^ (b v c)) = ((a ^ b) v (a ^ c))
Theorem	str 189	Strengthening rule.
a =< (b v c)   &   (a ^ (b v c)) =< b   =>   a =< b
Commutator (ortholattice theorems)
Theorem	cmtrcom 190	Commutative law for commutator.
C (a, b) = C (b, a)
Weak "orthomodular law" in ortholattices.
Theorem	wa1 191	Weak A1.
(a == a'') = 1
Theorem	wa2 192	Weak A2.
((a v b) == (b v a)) = 1
Theorem	wa3 193	Weak A3.
(((a v b) v c) == (a v (b v c))) = 1
Theorem	wa4 194	Weak A4.
((a v (b v b')) == (b v b')) = 1
Theorem	wa5 195	Weak A5.
((a v (a' v b')') == a) = 1
Theorem	wa6 196	Weak A6.
((a == b) == ((a' v b')' v (a v 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 v (a ^ b)) == a) = 1