Quantum Logic Explorer - mmtheorems3

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 - 201-300 - Page 3 of 11

Type	Label	Description
Statement
Theorem	wcon3 201	Weak contraposition.
(a_|_ == b) = 1   =>   (a == b_|_) = 1
Theorem	wlem3.1 202	Weak analogue to lemma used in proof of Th. 3.1 of Pavicic 1993.
(a v b) = b   &   (b_|_ v a) = 1   =>   (a == b) = 1
Theorem	woml 203	Theorem structurally similar to orthomodular law but does not require R3.
((a v (a_|_ ^ (a v b))) == (a v b)) = 1
Theorem	wwoml2 204	Weak orthomodular law.
a =< b   =>   ((a v (a_|_ ^ b)) == b) = 1
Theorem	wwoml3 205	Weak orthomodular law.
a =< b   &   (b ^ a_|_) = 0   =>   (a == b) = 1
Theorem	wwcomd 206	Commutation dual (weak). Kalmbach 83 p. 23.
a_|_ C b   =>   a = ((a v b) ^ (a v b_|_))
Theorem	wwcom3ii 207	Lemma 3(ii) (weak) of Kalmbach 83 p. 23.
b_|_ C a   =>   (a ^ (a_|_ v b)) = (a ^ b)
Theorem	wwfh1 208	Foulis-Holland Theorem (weak).
b C a   &   c C a   =>   ((a ^ (b v c)) == ((a ^ b) v (a ^ c))) = 1
Theorem	wwfh2 209	Foulis-Holland Theorem (weak).
a C b   &   c_|_ C a   =>   ((b ^ (a v c)) == ((b ^ a) v (b ^ c))) = 1
Theorem	wwfh3 210	Foulis-Holland Theorem (weak).
b_|_ C a   &   c_|_ C a   =>   ((a v (b ^ c)) == ((a v b) ^ (a v c))) = 1
Theorem	wwfh4 211	Foulis-Holland Theorem (weak).
a_|_ C b   &   c C a   =>   ((b v (a ^ c)) == ((b v a) ^ (b v c))) = 1
Theorem	womao 212	Weak OM-like absorption law for ortholattices.
(a_|_ ^ (a v (a_|_ ^ (a v b)))) = (a_|_ ^ (a v b))
Theorem	womaon 213	Weak OM-like absorption law for ortholattices.
(a ^ (a_|_ v (a ^ (a_|_ v b)))) = (a ^ (a_|_ v b))
Theorem	womaa 214	Weak OM-like absorption law for ortholattices.
(a_|_ v (a ^ (a_|_ v (a ^ b)))) = (a_|_ v (a ^ b))
Theorem	womaan 215	Weak OM-like absorption law for ortholattices.
(a v (a_|_ ^ (a v (a_|_ ^ b)))) = (a v (a_|_ ^ b))
Theorem	anorabs2 216	Absorption law for ortholattices.
(a ^ (b v (a ^ (b v c)))) = (a ^ (b v c))
Theorem	anorabs 217	Absorption law for ortholattices.
(a_|_ ^ (b v (a_|_ ^ (a v b)))) = (a_|_ ^ (a v b))
Theorem	ska2a 218	Axiom KA2a in Pavicic and Megill, 1998
(((a v c) == (b v c)) == ((c v a) == (c v b))) = 1
Theorem	ska2b 219	Axiom KA2b in Pavicic and Megill, 1998
(((a v c) == (b v c)) == ((a_|_ ^ c_|_)_|_ == (b_|_ ^ c_|_)_|_)) = 1
Theorem	ka4lemo 220	Lemma for KA4 soundness (OR version) - uses OL only.
((a v b) v ((a v c) == (b v c))) = 1
Theorem	ka4lem 221	Lemma for KA4 soundness (AND version) - uses OL only.
((a ^ b)_|_ v ((a ^ c) == (b ^ c))) = 1
Theorem	sklem 222	Soundness lemma.
a =< b   =>   (a_|_ v b) = 1
Theorem	ska1 223	Soundness theorem for Kalmbach's quantum propositional logic axiom KA1.
(a == a) = 1
Theorem	ska3 224	Soundness theorem for Kalmbach's quantum propositional logic axiom KA3.
((a == b)_|_ v (a_|_ == b_|_)) = 1
Theorem	ska5 225	Soundness theorem for Kalmbach's quantum propositional logic axiom KA5.
((a ^ b) == (b ^ a)) = 1
Theorem	ska6 226	Soundness theorem for Kalmbach's quantum propositional logic axiom KA6.
((a ^ (b ^ c)) == ((a ^ b) ^ c)) = 1
Theorem	ska7 227	Soundness theorem for Kalmbach's quantum propositional logic axiom KA7.
((a ^ (a v b)) == a) = 1
Theorem	ska8 228	Soundness theorem for Kalmbach's quantum propositional logic axiom KA8.
((a_|_ ^ a) == ((a_|_ ^ a) ^ b)) = 1
Theorem	ska9 229	Soundness theorem for Kalmbach's quantum propositional logic axiom KA9.
(a == a_|__|_) = 1
Theorem	ska10 230	Soundness theorem for Kalmbach's quantum propositional logic axiom KA10.
((a v b)_|_ == (a_|_ ^ b_|_)) = 1
Theorem	ska11 231	Soundness theorem for Kalmbach's quantum propositional logic axiom KA11.
((a v (a_|_ ^ (a v b))) == (a v b)) = 1
Theorem	ska12 232	Soundness theorem for Kalmbach's quantum propositional logic axiom KA12.
((a == b) == (b == a)) = 1
Theorem	ska13 233	Soundness theorem for Kalmbach's quantum propositional logic axiom KA13.
((a == b)_|_ v (a_|_ v b)) = 1
Theorem	skr0 234	Soundness theorem for Kalmbach's quantum propositional logic axiom KR0.
a = 1   &   (a_|_ v b) = 1   =>   b = 1
Theorem	wlem1 235	Lemma for 2-variable WOML proof.
((a == b)_|_ v ((a ->1 b) ^ (b ->1 a))) = 1
Theorem	ska15 236	Soundness theorem for Kalmbach's quantum propositional logic axiom KA15.
((a ->3 b)_|_ v (a_|_ v b)) = 1
Theorem	skmp3 237	Soundness proof for KMP3.
a = 1   &   (a ->3 b) = 1   =>   b = 1
Theorem	lei3 238	L.e. to Kalmbach implication.
a =< b   =>   (a ->3 b) = 1
Theorem	mccune2 239	E2 - OL theorem proved by EQP
(a v ((a_|_ ^ ((a v b_|_) ^ (a v b))) v (a_|_ ^ ((a_|_ ^ b) v (a_|_ ^ b_|_))))) = 1
Theorem	mccune3 240	E3 - OL theorem proved by EQP
((((a_|_ ^ b) v (a_|_ ^ b_|_)) v (a ^ (a_|_ v b)))_|_ v (a_|_ v b)) = 1
Theorem	i3n1 241	Equivalence for Kalmbach implication.
(a_|_ ->3 b_|_) = (((a ^ b_|_) v (a ^ b)) v (a_|_ ^ (a v b_|_)))
Theorem	ni31 242	Equivalence for Kalmbach implication.
(a ->3 b)_|_ = (((a v b_|_) ^ (a v b)) ^ (a_|_ v (a ^ b_|_)))
Theorem	i3id 243	Identity for Kalmbach implication.
(a ->3 a) = 1
Theorem	li3 244	Introduce Kalmbach implication to the left.
a = b   =>   (c ->3 a) = (c ->3 b)
Theorem	ri3 245	Introduce Kalmbach implication to the right.
a = b   =>   (a ->3 c) = (b ->3 c)
Theorem	2i3 246	Join both sides with Kalmbach implication.
a = b   &   c = d   =>   (a ->3 c) = (b ->3 d)
Theorem	ud1lem0a 247	Introduce ->1 to the left.
a = b   =>   (c ->1 a) = (c ->1 b)
Theorem	ud1lem0b 248	Introduce ->1 to the right.
a = b   =>   (a ->1 c) = (b ->1 c)
Theorem	ud1lem0ab 249	Join both sides of hypotheses with ->1.
a = b   &   c = d   =>   (a ->1 c) = (b ->1 d)
Theorem	ud2lem0a 250	Introduce ->2 to the left.
a = b   =>   (c ->2 a) = (c ->2 b)
Theorem	ud2lem0b 251	Introduce ->2 to the right.
a = b   =>   (a ->2 c) = (b ->2 c)
Theorem	ud3lem0a 252	Introduce Kalmbach implication to the left.
a = b   =>   (c ->3 a) = (c ->3 b)
Theorem	ud3lem0b 253	Introduce Kalmbach implication to the right.
a = b   =>   (a ->3 c) = (b ->3 c)
Theorem	ud4lem0a 254	Introduce ->4 to the left.
a = b   =>   (c ->4 a) = (c ->4 b)
Theorem	ud4lem0b 255	Introduce ->4 to the right.
a = b   =>   (a ->4 c) = (b ->4 c)
Theorem	ud5lem0a 256	Introduce ->5 to the left.
a = b   =>   (c ->5 a) = (c ->5 b)
Theorem	ud5lem0b 257	Introduce ->5 to the right.
a = b   =>   (a ->5 c) = (b ->5 c)
Theorem	i1i2 258	Correspondence between Sasaki and Dishkant conditionals.
(a ->1 b) = (b_|_ ->2 a_|_)
Theorem	i2i1 259	Correspondence between Sasaki and Dishkant conditionals.
(a ->2 b) = (b_|_ ->1 a_|_)
Theorem	i1i2con1 260	Correspondence between Sasaki and Dishkant conditionals.
(a ->1 b_|_) = (b ->2 a_|_)
Theorem	i1i2con2 261	Correspondence between Sasaki and Dishkant conditionals.
(a_|_ ->1 b) = (b_|_ ->2 a)
Theorem	i3i4 262	Correspondence between Kalmbach and non-tollens conditionals.
(a ->3 b) = (b_|_ ->4 a_|_)
Theorem	i4i3 263	Correspondence between Kalmbach and non-tollens conditionals.
(a ->4 b) = (b_|_ ->3 a_|_)
Theorem	i5con 264	Converse of ->5.
(a ->5 b) = (b_|_ ->5 a_|_)
Theorem	0i1 265	Antecedent of 0 on Sasaki conditional.
(0 ->1 a) = 1
Theorem	1i1 266	Antecedent of 1 on Sasaki conditional.
(1 ->1 a) = a
Theorem	i1id 267	Identity law for Sasaki conditional.
(a ->1 a) = 1
Theorem	i2id 268	Identity law for Dishkant conditional.
(a ->2 a) = 1
Theorem	ud1lem0c 269	Lemma for unified disjunction.
(a ->1 b)_|_ = (a ^ (a_|_ v b_|_))
Theorem	ud2lem0c 270	Lemma for unified disjunction.
(a ->2 b)_|_ = (b_|_ ^ (a v b))
Theorem	ud3lem0c 271	Lemma for unified disjunction.
(a ->3 b)_|_ = (((a v b_|_) ^ (a v b)) ^ (a_|_ v (a ^ b_|_)))
Theorem	ud4lem0c 272	Lemma for unified disjunction.
(a ->4 b)_|_ = (((a_|_ v b_|_) ^ (a v b_|_)) ^ ((a ^ b_|_) v b))
Theorem	ud5lem0c 273	Lemma for unified disjunction.
(a ->5 b)_|_ = (((a_|_ v b_|_) ^ (a v b_|_)) ^ (a v b))
Theorem	bina1 274	Pavicic binary logic ax-a1 analog.
(a ->3 a_|__|_) = 1
Theorem	bina2 275	Pavicic binary logic ax-a2 analog.
(a_|__|_ ->3 a) = 1
Theorem	bina3 276	Pavicic binary logic ax-a3 analog.
(a ->3 (a v b)) = 1
Theorem	bina4 277	Pavicic binary logic ax-a4 analog.
(b ->3 (a v b)) = 1
Theorem	bina5 278	Pavicic binary logic ax-a5 analog.
(b ->3 (a v a_|_)) = 1
Theorem	wql1lem 279	Classical implication inferred from Sakaki implication.
(a ->1 b) = 1   =>   (a_|_ v b) = 1
Theorem	wql2lem 280	Classical implication inferred from Dishkant implication.
(a ->2 b) = 1   =>   (a_|_ v b) = 1
Theorem	wql2lem2 281	Lemma for ->2 WQL axiom.
((a v c) ->2 (b v c)) = 1   =>   ((a v (b v c))_|_ v (b v c)) = 1
Theorem	wql2lem3 282	Lemma for ->2 WQL axiom.
(a ->2 b) = 1   =>   ((a ^ b_|_) ->2 a_|_) = 1
Theorem	wql2lem4 283	Lemma for ->2 WQL axiom.
(((a ^ b_|_) v (a ^ b)) ->2 (a_|_ v (a ^ b))) = 1   &   ((a ->1 b) v (a ^ b_|_)) = 1   =>   (a ->1 b) = 1
Theorem	wql2lem5 284	Lemma for ->2 WQL axiom.
(a ->2 b)