P. 3 of Theorem List - Quantum Logic Explorer

Theorem List for Quantum Logic Explorer - 201-300   *Has distinct variable group(s)

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