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

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